The subdifferential and conjugate-subgradient reciprocity

Let E and F be real vector spaces paired by B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ, written ⟪x, y⟫ = B x y, and let f : E → EReal. A point y : F is a subgradient of f at x when f x is finite and the affine function x' ↦ f x + ⟪x' - x, y⟫ lies below f everywhere; the set of subgradients is the subdifferential ∂f(x). It is empty wherever f is infinite.

The subdifferential is characterised by equality in the Fenchel–Young inequality: y ∈ ∂f(x) exactly when f x + f⋆ y = ⟪x, y⟫, where f⋆ is the Legendre–Fenchel conjugate of TauCeti.Analysis.Convex.Conjugate. Equivalently, x maximises x' ↦ ⟪x', y⟫ - f x'. Since the equality is symmetric in (f, x) and (f⋆, y) up to the biconjugate, it gives the conjugate-subgradient reciprocity: y ∈ ∂f(x) implies x ∈ ∂f⋆(y) (for the transposed pairing), and the converse holds at every point where f⋆⋆ x = f x, which is in particular the case whenever ∂f(x) is nonempty. Nothing here needs f convex: the subdifferential of an arbitrary extended-real function is defined by the same inequality, and it is a closed convex subset of F for any topology in which the functionals B x are continuous.

Main definitions

• TauCeti.subdifferential B f x — the set of y : F with f x finite and f x + B (x' - x) y ≤ f x' for every x'.

Main statements

• TauCeti.mem_subdifferential_iff_forall_sub_le — a subgradient at x is a y for which x maximises x' ↦ B x' y - f x', and TauCeti.mem_subdifferential_iff_add_fenchelConjugate_eq — the Fenchel–Young equality characterisation y ∈ ∂f(x) ↔ f x + f⋆ y = B x y;
• TauCeti.mem_subdifferential_coe_iff — for a real-valued f the finiteness condition is automatic and membership is the subgradient inequality;
• TauCeti.convex_subdifferential and TauCeti.isClosed_subdifferential — the subdifferential is convex, and closed for a topology making every B x continuous;
• TauCeti.mem_subdifferential_fenchelConjugate_of_mem_subdifferential — conjugate-subgradient reciprocity: y ∈ ∂f(x) implies x ∈ ∂f⋆(y);
• TauCeti.fenchelConjugate_flip_fenchelConjugate_eq_of_mem_subdifferential — f⋆⋆ x = f x wherever f has a subgradient;
• TauCeti.mem_subdifferential_fenchelConjugate_iff — where f⋆⋆ x = f x, the two subgradient relations are equivalent.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, §23, in particular Theorem 23.5 and Corollary 23.5.1.
• I. Ekeland and R. Témam, Convex Analysis and Variational Problems, Classics in Applied Mathematics 28, SIAM 1999, Chapter I, §5.

def TauCeti.subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (x : E) : Set F

The subdifferential of f : E → EReal at x with respect to the pairing B: the set of y : F such that f x is finite and f x + B (x' - x) y ≤ f x' for every x'. It is empty wherever f takes an infinite value.

Equations

• TauCeti.subdifferential B f x = {y : F | f x ≠ ⊥ ∧ f x ≠ ⊤ ∧ ∀ (x' : E), f x + ↑((B (x' - x)) y) ≤ f x'}

@[simp]

theorem TauCeti.mem_subdifferential_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} : y ∈ subdifferential B f x ↔ f x ≠ ⊥ ∧ f x ≠ ⊤ ∧ ∀ (x' : E), f x + ↑((B (x' - x)) y) ≤ f x'

The defining condition for a subgradient.

theorem TauCeti.ne_bot_of_mem_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} (h : y ∈ subdifferential B f x) : f x ≠ ⊥

A function has a subgradient at x only if it does not take the value ⊥ there.

theorem TauCeti.ne_top_of_mem_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} (h : y ∈ subdifferential B f x) : f x ≠ ⊤

A function has a subgradient at x only if it does not take the value ⊤ there.

theorem TauCeti.add_le_of_mem_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} (h : y ∈ subdifferential B f x) (x' : E) : f x + ↑((B (x' - x)) y) ≤ f x'

The subgradient inequality.

theorem TauCeti.apply_ne_bot_of_mem_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} (h : y ∈ subdifferential B f x) (x' : E) : f x' ≠ ⊥

A function with a subgradient somewhere never takes the value ⊥: the affine minorant through the subgradient is real everywhere.

theorem TauCeti.subdifferential_eq_empty_of_eq_bot {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} (h : f x = ⊥) : subdifferential B f x = ∅

The subdifferential is empty where the function takes the value ⊥.

theorem TauCeti.subdifferential_eq_empty_of_eq_top {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} (h : f x = ⊤) : subdifferential B f x = ∅

The subdifferential is empty where the function takes the value ⊤.

theorem TauCeti.mem_subdifferential_coe_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {x : E} {y : F} (f : E → ℝ) : y ∈ subdifferential B (fun (x : E) => ↑(f x)) x ↔ ∀ (x' : E), f x + (B (x' - x)) y ≤ f x'

For a real-valued function, a subgradient is a y satisfying the subgradient inequality.

Subgradients and the conjugate

theorem TauCeti.mem_subdifferential_iff_forall_sub_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} {r : ℝ} (hr : f x = ↑r) : y ∈ subdifferential B f x ↔ ∀ (x' : E), ↑((B x') y) - f x' ≤ ↑((B x) y - r)

When f x = r is real, y is a subgradient at x exactly when x maximises x' ↦ B x' y - f x', whose value at x is B x y - r.

theorem TauCeti.fenchelConjugate_eq_of_mem_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} (h : y ∈ subdifferential B f x) : fenchelConjugate B f y = ↑((B x) y) - f x

At a subgradient, the conjugate is given by the Fenchel–Young equality f⋆ y = B x y - f x.

theorem TauCeti.mem_subdifferential_iff_add_fenchelConjugate_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} : y ∈ subdifferential B f x ↔ f x + fenchelConjugate B f y = ↑((B x) y)

The Fenchel–Young equality characterisation of subgradients: y ∈ ∂f(x) exactly when f x + f⋆ y = B x y. The equality forces both f x and f⋆ y to be finite.

Convexity and closedness

theorem TauCeti.subdifferential_eq_iInter {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {r : ℝ} (hr : f x = ↑r) : subdifferential B f x = ⋂ (x' : E), {y : F | ↑(r + (B (x' - x)) y) ≤ f x'}

Where f x = r is real, the subdifferential is the intersection over x' of the affine constraints r + B (x' - x) y ≤ f x'.

theorem TauCeti.convex_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (x : E) : Convex ℝ (subdifferential B f x)

The subdifferential is a convex set: it is an intersection of half-spaces, or empty.

theorem TauCeti.isClosed_subdifferential {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [TopologicalSpace F] (hB : ∀ (x : E), Continuous ⇑(B x)) (f : E → EReal) (x : E) : IsClosed (subdifferential B f x)

The subdifferential is closed for every topology on F in which each functional B x is continuous: it is an intersection of closed half-spaces, or empty.

Conjugate-subgradient reciprocity

theorem TauCeti.mem_subdifferential_fenchelConjugate_of_mem_subdifferential {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 : y ∈ subdifferential B f x) : x ∈ subdifferential B.flip (fenchelConjugate B f) y

Conjugate-subgradient reciprocity. If y is a subgradient of f at x, then x is a subgradient of the conjugate f⋆ at y, for the transposed pairing.

theorem TauCeti.fenchelConjugate_flip_fenchelConjugate_eq_of_mem_subdifferential {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 : y ∈ subdifferential B f x) : fenchelConjugate B.flip (fenchelConjugate B f) x = f x

Wherever f has a subgradient, f agrees with its biconjugate.

theorem TauCeti.mem_subdifferential_fenchelConjugate_iff {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} (hx : fenchelConjugate B.flip (fenchelConjugate B f) x = f x) : x ∈ subdifferential B.flip (fenchelConjugate B f) y ↔ y ∈ subdifferential B f x

Conjugate-subgradient reciprocity, both ways: at a point where f agrees with its biconjugate, x is a subgradient of f⋆ at y exactly when y is a subgradient of f at x.