Monotonicity of the subdifferential

The subdifferential of a proper convex function is not merely monotone — ⟨x₁ - x₂, y₁ - y₂⟩ ≥ 0 whenever yᵢ ∈ ∂f xᵢ — but cyclically monotone: every finite cycle (x₀, y₀), …, (x_m, y_m) in its graph satisfies

⟨x₁ - x₀, y₀⟩ + ⟨x₂ - x₁, y₁⟩ + ⋯ + ⟨x₀ - x_m, y_m⟩ ≤ 0.

That is the whole story: a multivalued mapping is cyclically monotone exactly when it is contained in the subdifferential of a closed proper convex function, and that function can be written down as the supremum of the telescoping sums above, read as affine functions of a free endpoint. Since a closed proper convex function is determined by its subdifferential up to an additive constant, the maximal cyclically monotone mappings are precisely the subdifferentials — a different condition from maximal monotonicity, neither implying the other.

Main definitions

• IsMonotoneRel, IsMaximalMonotoneRel, IsCyclicallyMonotone, IsMaximalCyclicallyMonotone.
• cyclicPotential B ρ s — the convex function reconstructed from a cyclically monotone ρ.

Main results

• isCyclicallyMonotone_iff_exists_convexFn — cyclic monotonicity is containment in some ∂f.
• isClosed_subgradientRel — the graph of ∂f is closed.
• eq_add_coe_of_subgradientRel_subset — rigidity: ∂f ⊆ ∂g forces g = f + α, by subdivision.
• isMaximalCyclicallyMonotone_iff_exists_closedProperConvexFn — the maximal cyclically monotone mappings are exactly the subdifferentials.

Implementation notes

A cycle is a List (E × F) with the starting pair carried separately, so that every proof is a list induction. chainVal B s l x keeps the free endpoint last, which makes cyclicPotential a supremum of affine functions of x and the cycle condition read chainVal B s l s.1 ≤ 0. Closedness of the graph asks for joint continuity of the pairing, Continuous fun p : E × F => B p.1 p.2: continuity of ⟨·, y⟩ for each fixed y is not enough to pass to the limit in ⟨z - xᵢ, yᵢ⟩ when both arguments move. In ℝⁿ the hypothesis is automatic.

Maximal monotonicity of ∂f for a closed proper convex f is not here: it is isMaximalMonotoneRel_subgradientRel in Optimization/Prox.lean, because its proof is Moreau's theorem and that file is downstream of this one.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §24.
• R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (1966) 497–510.

Chains and cyclic monotonicity

def Tdaf.ConvexAnalysis.chainVal {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : E × F → List (E × F) → E → ℝ

The telescoping sum along a finite chain in the graph of a multivalued mapping. The chain starts at the pair s = (x₀, y₀), runs through l = [(x₁, y₁), …, (x_m, y_m)] and ends at the free point x:

chainVal B s l x = ⟨x₁ - x₀, y₀⟩ + ⟨x₂ - x₁, y₁⟩ + ⋯ + ⟨x - x_m, y_m⟩.

Taking x = x₀ closes the chain into a cycle.

Equations

• Tdaf.ConvexAnalysis.chainVal B x✝¹ [] x✝ = (B (x✝ - x✝¹.1)) x✝¹.2
• Tdaf.ConvexAnalysis.chainVal B x✝¹ (q :: l) x✝ = (B (q.1 - x✝¹.1)) x✝¹.2 + Tdaf.ConvexAnalysis.chainVal B q l x✝

@[simp]

theorem Tdaf.ConvexAnalysis.chainVal_nil {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (s : E × F) (x : E) : chainVal B s [] x = (B (x - s.1)) s.2

@[simp]

theorem Tdaf.ConvexAnalysis.chainVal_cons {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (s q : E × F) (l : List (E × F)) (x : E) : chainVal B s (q :: l) x = (B (q.1 - s.1)) s.2 + chainVal B q l x

theorem Tdaf.ConvexAnalysis.chainVal_append_singleton {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (s q : E × F) (l : List (E × F)) (z : E) : chainVal B s (l ++ [q]) z = chainVal B s l q.1 + (B (z - q.1)) q.2

Appending one more edge to a chain: the value along l ++ [q] ending at z is the value along l ending at q.1, plus the last edge. This is the step that makes a chain into a longer chain in the reconstruction below.

theorem Tdaf.ConvexAnalysis.exists_chainVal_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (l : List (E × F)) (s : E × F) : ∃ (y : F) (c : ℝ), ∀ (x : E), chainVal B s l x = (B x) y - c

A chain is affine in its free endpoint: chainVal B s l x = ⟨x, y⟩ - c for a (y, c) that depends only on the chain. This is why cyclicPotential is a supremum of affine functions.

Monotone and cyclically monotone multivalued mappings

def Tdaf.ConvexAnalysis.IsMonotoneRel {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ρ : SetRel E F) : Prop

A multivalued mapping is monotone when ⟨x₁ - x₂, y₁ - y₂⟩ ≥ 0 for all pairs in its graph.

Equations

• Tdaf.ConvexAnalysis.IsMonotoneRel B ρ = ∀ p ∈ ρ, ∀ q ∈ ρ, 0 ≤ (B (p.1 - q.1)) (p.2 - q.2)

def Tdaf.ConvexAnalysis.IsCyclicallyMonotone {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ρ : SetRel E F) : Prop

A multivalued mapping is cyclically monotone when every finite cycle in its graph has non-positive telescoping sum. The cycle is written as a starting pair s followed by a list l; chainVal B s l s.1 is the sum around it.

Equations

• Tdaf.ConvexAnalysis.IsCyclicallyMonotone B ρ = ∀ s ∈ ρ, ∀ (l : List (E × F)), (∀ q ∈ l, q ∈ ρ) → Tdaf.ConvexAnalysis.chainVal B s l s.1 ≤ 0

def Tdaf.ConvexAnalysis.IsMaximalMonotoneRel {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ρ : SetRel E F) : Prop

A monotone mapping is maximal when no strictly larger monotone mapping contains it.

Equations

• Tdaf.ConvexAnalysis.IsMaximalMonotoneRel B ρ = (Tdaf.ConvexAnalysis.IsMonotoneRel B ρ ∧ ∀ (σ : SetRel E F), Tdaf.ConvexAnalysis.IsMonotoneRel B σ → ρ ⊆ σ → σ ⊆ ρ)

def Tdaf.ConvexAnalysis.IsMaximalCyclicallyMonotone {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ρ : SetRel E F) : Prop

A cyclically monotone mapping is maximal when no strictly larger cyclically monotone mapping contains it. These turn out to be exactly the subdifferentials.

Equations

• Tdaf.ConvexAnalysis.IsMaximalCyclicallyMonotone B ρ = (Tdaf.ConvexAnalysis.IsCyclicallyMonotone B ρ ∧ ∀ (σ : SetRel E F), Tdaf.ConvexAnalysis.IsCyclicallyMonotone B σ → ρ ⊆ σ → σ ⊆ ρ)

theorem Tdaf.ConvexAnalysis.IsMonotoneRel.mono {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ σ : SetRel E F} (h : IsMonotoneRel B σ) (hsub : ρ ⊆ σ) : IsMonotoneRel B ρ

Monotonicity passes to sub-mappings.

theorem Tdaf.ConvexAnalysis.IsCyclicallyMonotone.mono {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ σ : SetRel E F} (h : IsCyclicallyMonotone B σ) (hsub : ρ ⊆ σ) : IsCyclicallyMonotone B ρ

Cyclic monotonicity passes to sub-mappings.

theorem Tdaf.ConvexAnalysis.IsCyclicallyMonotone.isMonotoneRel {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} (h : IsCyclicallyMonotone B ρ) : IsMonotoneRel B ρ

Cyclic monotonicity implies monotonicity: a two-element cycle is exactly the monotonicity inequality.

theorem Tdaf.ConvexAnalysis.isCyclicallyMonotone_singleton {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (p : E × F) : IsCyclicallyMonotone B {p}

A one-element mapping is cyclically monotone: every cycle in it has all its edges equal to zero. Used only to see that a maximal cyclically monotone mapping is nonempty.

theorem Tdaf.ConvexAnalysis.IsMaximalCyclicallyMonotone.nonempty {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} (h : IsMaximalCyclicallyMonotone B ρ) : Set.Nonempty ρ

A maximal cyclically monotone mapping is nonempty: the empty mapping is strictly contained in the cyclically monotone {(0, 0)}.

Necessity: ∂f is cyclically monotone

theorem Tdaf.ConvexAnalysis.le_of_chain_mem_subgradientRel {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (l : List (E × F)) (s : E × F) : s ∈ subgradientRel B f → (∀ q ∈ l, q ∈ subgradientRel B f) → ∀ (x : E), f s.1 + ↑(chainVal B s l x) ≤ f x

The telescoping estimate: walking a chain of subgradients from s to x cannot gain more than the increase of f. The chain of inequalities ⟨x_{i+1} - x_i, y_i⟩ ≤ f x_{i+1} - f x_i, summed.

theorem Tdaf.ConvexAnalysis.isCyclicallyMonotone_subgradientRel {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hp : Proper f) : IsCyclicallyMonotone B (subgradientRel B f)

The graph of ∂f is cyclically monotone. Convexity of f is not used; properness is, and only to know that f is finite at the base point of the cycle.

theorem Tdaf.ConvexAnalysis.isMonotoneRel_subgradientRel {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hp : Proper f) : IsMonotoneRel B (subgradientRel B f)

The subdifferential is monotone, the classical inequality ⟨x₁ - x₂, y₁ - y₂⟩ ≥ 0.

Sufficiency: the potential

noncomputable def Tdaf.ConvexAnalysis.cyclicPotential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ρ : SetRel E F) (s : E × F) (x : E) : EReal

The potential of a multivalued mapping ρ: the supremum of the telescoping sums of all finite chains in ρ that start at s and end at x. Being a supremum of affine functions of x it is a closed convex function, and cyclic monotonicity of ρ is exactly what keeps it from being +∞ at s.1.

Equations

• Tdaf.ConvexAnalysis.cyclicPotential B ρ s x = ⨆ l ∈ {l : List (E × F) | ∀ q ∈ l, q ∈ ρ}, ↑(Tdaf.ConvexAnalysis.chainVal B s l x)

theorem Tdaf.ConvexAnalysis.le_cyclicPotential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} {l : List (E × F)} (hl : ∀ q ∈ l, q ∈ ρ) (s : E × F) (x : E) : ↑(chainVal B s l x) ≤ cyclicPotential B ρ s x

theorem Tdaf.ConvexAnalysis.cyclicPotential_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} {s : E × F} {c : EReal} {x : E} (h : ∀ (l : List (E × F)), (∀ q ∈ l, q ∈ ρ) → ↑(chainVal B s l x) ≤ c) : cyclicPotential B ρ s x ≤ c

theorem Tdaf.ConvexAnalysis.convexFn_cyclicPotential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ρ : SetRel E F) (s : E × F) : ConvexFn (cyclicPotential B ρ s)

The potential is convex: it is a supremum of affine functions.

theorem Tdaf.ConvexAnalysis.cyclicPotential_ne_bot {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ρ : SetRel E F) (s : E × F) (x : E) : cyclicPotential B ρ s x ≠ ⊥

The potential never takes the value -∞: the empty chain already gives it a real lower bound.

theorem Tdaf.ConvexAnalysis.cyclicPotential_eq_zero {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} {s : E × F} (hρ : IsCyclicallyMonotone B ρ) (hs : s ∈ ρ) : cyclicPotential B ρ s s.1 = 0

Cyclic monotonicity is exactly what makes the potential finite at its base point, where it vanishes.

theorem Tdaf.ConvexAnalysis.proper_cyclicPotential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} {s : E × F} (hρ : IsCyclicallyMonotone B ρ) (hs : s ∈ ρ) : Proper (cyclicPotential B ρ s)

The potential is proper.

theorem Tdaf.ConvexAnalysis.mem_subgradient_cyclicPotential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} {s p : E × F} (hp : p ∈ ρ) : p.2 ∈ subgradient B (cyclicPotential B ρ s) p.1

Every pair of ρ is a subgradient of the potential. A chain ending at x followed by the edge (x, y) is again a chain, so the supremum defining f z dominates chainVal … x + ⟨z - x, y⟩ for every chain, hence f x + ⟨z - x, y⟩ ≤ f z.

Cyclically monotone mappings and subdifferentials

theorem Tdaf.ConvexAnalysis.exists_convexFn_subgradientRel_of_isCyclicallyMonotone {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} [IsContinuousPairing B] (hρ : IsCyclicallyMonotone B ρ) (hne : Set.Nonempty ρ) : ∃ (f : E → EReal), ConvexFn f ∧ ClosedFn f ∧ Proper f ∧ ρ ⊆ subgradientRel B f

A nonempty cyclically monotone multivalued mapping is contained in the subdifferential of a closed proper convex function.

theorem Tdaf.ConvexAnalysis.isCyclicallyMonotone_iff_exists_convexFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} [IsContinuousPairing B] (hne : Set.Nonempty ρ) : IsCyclicallyMonotone B ρ ↔ ∃ (f : E → EReal), ConvexFn f ∧ ClosedFn f ∧ Proper f ∧ ρ ⊆ subgradientRel B f

For a nonempty multivalued mapping, being contained in a subdifferential and being cyclically monotone are the same thing.

theorem Tdaf.ConvexAnalysis.exists_eq_subgradientRel_of_isMaximalCyclicallyMonotone {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {ρ : SetRel E F} [IsContinuousPairing B] (h : IsMaximalCyclicallyMonotone B ρ) : ∃ (f : E → EReal), ConvexFn f ∧ ClosedFn f ∧ Proper f ∧ ρ = subgradientRel B f

The half the reconstruction gives at once: a maximal cyclically monotone multivalued mapping is the subdifferential of a closed proper convex function.

The graph of ∂f is closed

theorem Tdaf.ConvexAnalysis.isClosed_subgradientRel {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [IsTopologicalAddGroup E] (hB : Continuous fun (p : E × F) => (B p.1) p.2) (hp : Proper f) (hlsc : LowerSemicontinuous f) : IsClosed (subgradientRel B f)

The graph of ∂f is closed in E × F; equivalently xᵢ* ∈ ∂f xᵢ, xᵢ → x and xᵢ* → x* force x* ∈ ∂f x. Convexity of f is not used. Lower semicontinuity is, and so is joint continuity of the pairing: the subgradient inequality at xᵢ involves ⟨z - xᵢ, xᵢ*⟩, where both arguments move.

Increments along a chain of subgradients

theorem Tdaf.ConvexAnalysis.pairing_le_sub_of_mem_subgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {p q : E} {a b : ℝ} {u : F} (hp : f p = ↑a) (hq : f q = ↑b) (hu : u ∈ subgradient B f p) : (B (q - p)) u ≤ b - a

One half of the subgradient inequality, read as a bound on an increment of f: a subgradient at the left endpoint underestimates the increment.

theorem Tdaf.ConvexAnalysis.sub_le_pairing_of_mem_subgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {p q : E} {a b : ℝ} {v : F} (hp : f p = ↑a) (hq : f q = ↑b) (hv : v ∈ subgradient B f q) : b - a ≤ (B (q - p)) v

The other half: a subgradient at the right endpoint overestimates the increment.

theorem Tdaf.ConvexAnalysis.abs_sub_increment_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} (hsub : subgradientRel B f ⊆ subgradientRel B g) {x : ℕ → E} {v : ℕ → F} {a b : ℕ → ℝ} {d : E} {N : ℕ} (hx : ∀ i < N, x (i + 1) = x i + d) (hv : ∀ i ≤ N, v i ∈ subgradient B f (x i)) (ha : ∀ i ≤ N, f (x i) = ↑(a i)) (hb : ∀ i ≤ N, g (x i) = ↑(b i)) : |a N - a 0 - (b N - b 0)| ≤ (B d) (v N - v 0)

The subdivision estimate. Along a chain of equally spaced points x 0, …, x N with common step d, with v i ∈ ∂f (x i) and ∂f ⊆ ∂g, the increments of f and of g across the chain differ by at most ⟨d, v N - v 0⟩: both are trapped between the same two telescoping sums, since the subgradients of f serve g as well. Halving the step halves the bound while leaving the ends of the chain alone, which is what forces the two increments to agree.

Raising a function by a constant

theorem Tdaf.ConvexAnalysis.conj_add_coe {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (α : ℝ) : (conj B fun (x : E) => f x + ↑α) = fun (y : F) => conj B f y + ↑(-α)

Raising a function by a real constant lowers its conjugate by that constant. This is the one piece of conjugacy the rigidity argument needs beyond Fenchel–Moreau: ∂f ⊆ ∂g pins g to f + α only after the same relation on the conjugate side has been turned back into an inequality on E.

∂f determines f up to an additive constant

theorem Tdaf.ConvexAnalysis.exists_coe_of_subgradient_nonempty {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : E → EReal} (hpg : Proper g) {x : E} (h : (subgradient B g x).Nonempty) : ∃ (c : ℝ), g x = ↑c

A point at which a proper function is subdifferentiable is a point where it is finite.

theorem Tdaf.ConvexAnalysis.increment_eq_of_subgradientRel_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} [IsCompatiblePairing B] (hf : ConvexFn f) (hpf : Proper f) (hpg : Proper g) (hsub : subgradientRel B f ⊆ subgradientRel B g) {x₁ x₂ : E} {a₁ a₂ b₁ b₂ : ℝ} (h₁ : x₁ ∈ intrinsicInterior ℝ (dom f)) (h₂ : x₂ ∈ intrinsicInterior ℝ (dom f)) (hfa₁ : f x₁ = ↑a₁) (hfa₂ : f x₂ = ↑a₂) (hgb₁ : g x₁ = ↑b₁) (hgb₂ : g x₂ = ↑b₂) : a₂ - a₁ = b₂ - b₁

The analytic core: if ∂f ⊆ ∂g then f and g have the same increments between relative interior points of dom f. The classical proof integrates the common one-sided derivative along the segment, through the one-dimensional theory; the argument here needs none of it. Subdivide [x₁, x₂] into N equal steps and pick v i ∈ ∂f (x i) at each node; each step traps both increments in [⟨d, v i⟩, ⟨d, v (i+1)⟩], so the two differ by at most the telescoping total N⁻¹ ⟨x₂ - x₁, v N - v 0⟩, which tends to 0.

theorem Tdaf.ConvexAnalysis.exists_forall_le_add_coe_of_subgradientRel_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} [IsCompatiblePairing B] (hf : ConvexFn f) (hpf : Proper f) (hcf : ClosedFn f) (hg : ConvexFn g) (hpg : Proper g) (hlg : LowerSemicontinuous g) (hsub : subgradientRel B f ⊆ subgradientRel B g) : ∃ (α : ℝ), (∀ (y : E), g y ≤ f y + ↑α) ∧ ∀ y ∈ closure (dom f), g y = f y + ↑α

The geometric half: if ∂f ⊆ ∂g then g ≤ f + α for a real constant α, with equality on cl (dom f). Agreement of the increments on ri (dom f) fixes α, and a closed convex function is the limit of its values along a segment running into a boundary point, which carries the identity out to cl (dom f). Off cl (dom f) the right-hand side is ⊤.

Maximality of the subdifferential

@[simp]

theorem Tdaf.ConvexAnalysis.subgradient_add_coe {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (α : ℝ) (x : E) : subgradient B (fun (x : E) => f x + ↑α) x = subgradient B f x

Raising a function by a real constant does not change its subdifferential.

theorem Tdaf.ConvexAnalysis.subgradientRel_add_coe {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (α : ℝ) : (subgradientRel B fun (x : E) => f x + ↑α) = subgradientRel B f

The graph form of subgradient_add_coe.

theorem Tdaf.ConvexAnalysis.eq_add_coe_of_subgradientRel_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hf : ClosedProperConvexFn f) (hg : ClosedProperConvexFn g) (hsub : subgradientRel B f ⊆ subgradientRel B g) : ∃ (α : ℝ), ∀ (x : E), g x = f x + ↑α

A closed proper convex function is determined by its subdifferential up to an additive constant, and already by the inclusion ∂f ⊆ ∂g.

The geometric half gives g ≤ f + α with equality on cl (dom f); inverting the subdifferential turns ∂f ⊆ ∂g into ∂f* ⊆ ∂g* and repeats it on the conjugate side, giving g* ≤ f* + β. Equality in Fenchel's inequality at a pair of the graph of ∂f, where both hold, forces β = -α, and conjugating g* ≤ (f + α)* back gives g ≥ f + α.

theorem Tdaf.ConvexAnalysis.isMaximalCyclicallyMonotone_subgradientRel {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hf : ClosedProperConvexFn f) : IsMaximalCyclicallyMonotone B (subgradientRel B f)

The subdifferential of a closed proper convex function is a maximal cyclically monotone mapping. If ∂f ⊆ σ with σ cyclically monotone then the reconstruction puts σ ⊆ ∂g for some closed proper convex g; uniqueness makes g = f + α, and a constant does not change a subdifferential.

theorem Tdaf.ConvexAnalysis.isMaximalCyclicallyMonotone_iff_exists_closedProperConvexFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {ρ : SetRel E F} : IsMaximalCyclicallyMonotone B ρ ↔ ∃ (f : E → EReal), ClosedProperConvexFn f ∧ ρ = subgradientRel B f

In full: on a finite-dimensional space the maximal cyclically monotone mappings are exactly the subdifferentials of the closed proper convex functions.