Subgradient calculus

How ∂ interacts with sums and with linear maps. Both rules have the same shape: one inclusion is unconditional — a subgradient of each piece assembles into a subgradient of the whole — and the reverse inclusion, the useful one, needs exactly the constraint qualification that makes the corresponding conjugacy rule exact. Both are therefore stated against the IsExactSum and IsExactImage interfaces; the classical ri versions of the two rules are these composed with the of_relint constructors.

Main results

• IsExactSum.subgradient_add, IsExactFinsetSum.subgradient_finsetSum — ∂(∑ fᵢ) = ∑ ∂fᵢ, for two summands and for m of them (Theorem 23.8 in [^1]).
• IsExactImage.subgradient_compLin — ∂(g A) x = A' (∂g (A x)) (Theorem 23.9 in [^1]).
• subgradient_coe_mul, subgradient_coe_affineMap — ∂(cf) = c ∂f for c > 0, and for arbitrary c when f is affine.
• IsExactSum.normalCone_inter — the normal cone to an intersection, as a sum of normal cones.
• subgradient_add_normalCone_dom_subset, normalCone_dom_eq_zero_of_subgradient_eq_singleton — the normal cone to dom f, and what a unique subgradient does to it.

Implementation notes

Everything reduces to the conjugate characterisation y ∈ ∂f x ↔ f x + f* y ≤ ⟨x, y⟩, written so that no ∞ - ∞ can arise; no epigraph, directional derivative or separating hyperplane appears in any proof here. The sum rule additionally needs the EReal fact that two slack inequalities whose sum is tight must each be tight, and that is where the properness carried by IsExactSum is spent. Its m-ary form is proved for the whole family in one pass, because the binary rule does not iterate: EReal has no subtraction to peel a summand off with.

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §23.

Sums

theorem Tdaf.ConvexAnalysis.subgradient_add_subset {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f g : E → EReal) (x : E) : subgradient B f x + subgradient B g x ⊆ subgradient B (f + g) x

The unconditional inclusion: a subgradient of f plus a subgradient of g is a subgradient of f + g. The two subgradient inequalities simply add.

theorem Tdaf.ConvexAnalysis.IsExactSum.subgradient_add {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} (h : IsExactSum B f g) (x : E) : subgradient B (f + g) x = subgradient B f x + subgradient B g x

∂(f + g) x = ∂f x + ∂g x whenever the sum is exact. Exactness splits y = y₁ + y₂ with f* y₁ + g* y₂ ≤ (f+g)* y, and tightness of Fenchel's inequality for f + g then leaves the two inequalities for f at y₁ and g at y₂ no room to be strict.

Sums of m functions

theorem Tdaf.ConvexAnalysis.subgradient_finsetSum_subset {ι : Type u_1} {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (s : Finset ι) (f : ι → E → EReal) (x : E) : ∑ i ∈ s, subgradient B (f i) x ⊆ subgradient B (∑ i ∈ s, f i) x

The unconditional inclusion for m summands: ∂f₁ x + ⋯ + ∂fₘ x ⊆ ∂(f₁ + ⋯ + fₘ) x. Over the empty Finset the left side is {0} and the right side is ∂(0) x, which contains 0.

theorem Tdaf.ConvexAnalysis.IsExactFinsetSum.subgradient_finsetSum {ι : Type u_1} {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Finset ι} {f : ι → E → EReal} (h : IsExactFinsetSum B s f) (x : E) : subgradient B (∑ i ∈ s, f i) x = ∑ i ∈ s, subgradient B (f i) x

∂(f₁ + ⋯ + fₘ) x = ∂f₁ x + ⋯ + ∂fₘ x whenever the family adds exactly. Exactness hands back a splitting y = y₁ + ⋯ + yₘ whose conjugate values already sum to (∑ fᵢ)* y, and y ∈ ∂(∑ fᵢ) x makes the sum of the m Fenchel inequalities tight, hence each of them. This is not the binary rule iterated.

Linear maps

theorem Tdaf.ConvexAnalysis.image_subgradient_subset {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [AddCommGroup H] [Module ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} (hA : IsAdjointPair B B' A A') (g : G → EReal) (x : E) : ⇑A' '' subgradient B' g (A x) ⊆ subgradient B (compLin g A) x

The unconditional inclusion: the transpose carries subgradients of g at A x to subgradients of g A at x. Only the adjointness datum is used; g is arbitrary.

theorem Tdaf.ConvexAnalysis.IsExactImage.subgradient_compLin {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [AddCommGroup H] [Module ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} {g : G → EReal} {hA : IsAdjointPair B B' A A'} (h : IsExactImage B B' A A' hA g) (x : E) : subgradient B (compLin g A) x = ⇑A' '' subgradient B' g (A x)

∂(g A) x = A' (∂g (A x)) whenever the pullback is exact. Unlike the sum rule this needs no splitting: exactness hands back a single z in the fibre with g* z ≤ (g A)* (A' z), which slots straight into Fenchel's inequality once a subgradient at x is seen to force (g A)* y finite.

Scalar multiples

theorem Tdaf.ConvexAnalysis.subgradient_coe_mul {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {c : ℝ} (hc : 0 < c) (f : E → EReal) (x : E) : subgradient B (fun (y : E) => ↑c * f y) x = c • subgradient B f x

∂(cf) x = c ∂f x for c > 0, with no hypothesis on f: multiplying the subgradient inequality through by c > 0 is reversible even on EReal.

Positivity is essential in both directions. At c = 0 the left side is {y | ∀ w, B w y = 0}, which has nothing to do with ∂f x; for c < 0 the scaled inequality reverses and cf is concave where f is convex. The negative case survives only when f is affine.

theorem Tdaf.ConvexAnalysis.subgradient_zero_mul {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (hB : Function.Injective ⇑B.flip) (f : E → EReal) (x : E) : subgradient B (fun (y : E) => ↑0 * f y) x = {0}

∂(0 · f) x = {0}: the zero function has the origin as its only subgradient.

This is what the parenthesis "(Omit terms with λᵢ = 0.)" in the Kuhn–Tucker conditions means, and why it is not cosmetic: ∂fᵢ x may be empty at a boundary point of dom fᵢ, so the term 0 · ∂fᵢ x that the parenthesis drops would be ∅ rather than {0}, emptying the whole sum.

theorem Tdaf.ConvexAnalysis.subgradient_coe_affineMap {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (hB : Function.Injective ⇑B.flip) (a : E →ᵃ[ℝ] ℝ) {b : F} (hb : ∀ (w : E), (B w) b = a.linear w) (x : E) : subgradient B (fun (y : E) => ↑(a y)) x = {b}

The subdifferential of an affine function is one point, namely the vector b representing its linear part through the pairing. No differentiation is needed: b is handed in, together with the identity ⟨w, b⟩ = a.linear w naming it, and nothing in the statement mentions a topology.

theorem Tdaf.ConvexAnalysis.subgradient_coe_mul_affineMap {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (hB : Function.Injective ⇑B.flip) (c : ℝ) (a : E →ᵃ[ℝ] ℝ) {b : F} (hb : ∀ (w : E), (B w) b = a.linear w) (x : E) : subgradient B (fun (y : E) => ↑c * ↑(a y)) x = c • subgradient B (fun (y : E) => ↑(a y)) x

∂(ca) x = c ∂a x for an arbitrary real c, when a is affine. An affine function satisfies the subgradient inequality with equality, so scaling by a negative c reverses nothing; this is what covers equality-constraint multipliers, which may be negative.

Normal cones to an intersection

theorem Tdaf.ConvexAnalysis.normalCone_add_subset {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (C D : Set E) (x : E) : normalCone B C x + normalCone B D x ⊆ normalCone B (C ∩ D) x

The unconditional inclusion. Proved directly rather than through indicators, so that it needs neither x ∈ C nor x ∈ D.

theorem Tdaf.ConvexAnalysis.IsExactSum.normalCone_inter {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {C D : Set E} {x : E} (h : IsExactSum B (indicatorFn C) (indicatorFn D)) (hC : x ∈ C) (hD : x ∈ D) : normalCone B (C ∩ D) x = normalCone B C x + normalCone B D x

The normal cone to an intersection is the sum of the normal cones, under the exact-sum hypothesis for the two indicators.

The normal cone to the effective domain

theorem Tdaf.ConvexAnalysis.subgradient_add_normalCone_dom_subset {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 f x + normalCone B (dom f) x ⊆ subgradient B f x

A normal to the effective domain may be added to a subgradient — the elementary inclusion behind ∂f x + N_{dom f}(x) = ∂f x. Neither convexity nor a topology is needed.

theorem Tdaf.ConvexAnalysis.normalCone_dom_eq_zero_of_subgradient_eq_singleton {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {y₀ : F} (h : subgradient B f x = {y₀}) : normalCone B (dom f) x = {0}

A lone subgradient leaves no room for a normal direction: if ∂f x = {y₀} then y₀ + n is again a subgradient for every n normal to dom f at x, so n = 0. With mem_interior_of_normalCone_eq_zero this turns uniqueness into an interiority statement.