The Fenchel–Moreau theorem

Let E be a real locally convex topological vector space and let f : E → EReal be convex (its real epigraph {(x, r) | f x ≤ r} is convex), lower semicontinuous, and never ⊥. This file proves that such an f is the pointwise supremum of the continuous affine functions below it: for every x₀ and every real t < f x₀ there is a continuous linear functional ℓ and a real c with ℓ + c ≤ f everywhere and ℓ x₀ + c = t. The value f x₀ = ⊤ is allowed, and no point of the effective domain is singled out: this is the extended-valued form of Mathlib's ConvexOn.exists_affine_le_of_lt, which treats real-valued functions on a closed convex set.

For a pairing B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ that represents every continuous linear functional on E, each such affine minorant is x ↦ B x y + c, and each affine minorant lies below the biconjugate f⋆⋆. Together with the algebraic inequality f⋆⋆ ≤ f, this gives the Fenchel–Moreau theorem f⋆⋆ = f. If moreover every functional x ↦ B x y is continuous (that is, the topology of E is compatible with the pairing), the equality characterises the functions it applies to: f⋆⋆ = f holds exactly when f is convex and lower semicontinuous and either never takes the value ⊥ or is identically ⊥. Neither a Hausdorff hypothesis on E nor any topology on F is needed. For a complete real inner product space the inner product represents every continuous linear functional (the Fréchet–Riesz theorem), which gives the self-dual form used in Euclidean optimal transport.

Main statements

• TauCeti.exists_affine_le_of_lt — a convex lower-semicontinuous function f : E → EReal that is never ⊥ has, below every real t < f x₀, a continuous affine minorant taking the value t at x₀;
• TauCeti.fenchelConjugate_flip_fenchelConjugate_eq — the Fenchel–Moreau theorem f⋆⋆ = f for a pairing representing the continuous dual of E, and TauCeti.fenchelConjugate_flip_fenchelConjugate_eq_iff, its converse for a compatible topology;
• TauCeti.fenchelConjugate_innerₗ_fenchelConjugate_innerₗ — the Fenchel–Moreau theorem on a complete real inner product space.

Implementation notes

The affine minorant is obtained by separating the point (x₀, t) from the closed convex real epigraph of f in E × ℝ with geometric_hahn_banach_point_closed. The separating functional has the form (x, r) ↦ ℓ x + a * r. When a > 0 it is non-vertical and yields the minorant at once. This is always the case when f x₀ is finite. When f x₀ = ⊤ the hyperplane may be vertical (a = 0); then f is either identically ⊤, or it has a non-vertical minorant through a point of its effective domain, and adding a large multiple of the vertical separator to that minorant lifts it above t at x₀.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, Theorem 12.1 and Corollary 12.2.1.
• I. Ekeland and R. Témam, Convex Analysis and Variational Problems, Classics in Applied Mathematics 28, SIAM 1999, Chapter I, Proposition 3.1 and Proposition 4.1.
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, CMS Books in Mathematics, Springer 2011, Theorem 13.32.

theorem TauCeti.exists_affine_le_of_lt {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hlsc : LowerSemicontinuous f) (hbot : ∀ (x : E), f x ≠ ⊥) {x₀ : E} {t : ℝ} (ht : ↑t < f x₀) : ∃ (ℓ : E →L[ℝ] ℝ) (c : ℝ), (∀ (x : E), ↑(ℓ x + c) ≤ f x) ∧ ℓ x₀ + c = t

Continuous affine minorants of a convex lower-semicontinuous function. On a real locally convex space, let f : E → EReal have convex real epigraph, be lower semicontinuous and never take the value ⊥. For every point x₀ and every real t < f x₀ (including the case f x₀ = ⊤) there are a continuous linear functional ℓ and a real c such that ℓ + c lies below f everywhere and takes the value t at x₀. Consequently f is the pointwise supremum of its continuous affine minorants.

theorem TauCeti.fenchelConjugate_flip_fenchelConjugate_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} {F : Type u_2} [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (hB : ∀ (ℓ : E →L[ℝ] ℝ), ∃ (y : F), ∀ (x : E), (B x) y = ℓ x) (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hlsc : LowerSemicontinuous f) (hbot : ∀ (x : E), f x ≠ ⊥) : fenchelConjugate B.flip (fenchelConjugate B f) = f

The Fenchel–Moreau theorem. Let the pairing B represent every continuous linear functional on the locally convex space E. If f : E → EReal has convex real epigraph, is lower semicontinuous and never takes the value ⊥, then f equals its biconjugate f⋆⋆, the second conjugate being taken for the transposed pairing.

theorem TauCeti.fenchelConjugate_flip_fenchelConjugate_eq_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} {F : Type u_2} [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (hB : ∀ (ℓ : E →L[ℝ] ℝ), ∃ (y : F), ∀ (x : E), (B x) y = ℓ x) (hBc : ∀ (y : F), Continuous fun (x : E) => (B x) y) : fenchelConjugate B.flip (fenchelConjugate B f) = f ↔ Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2} ∧ LowerSemicontinuous f ∧ ((∀ (x : E), f x ≠ ⊥) ∨ f = ⊥)

The Fenchel–Moreau theorem, with its converse. For a pairing B that represents every continuous linear functional on E and makes every functional x ↦ B x y continuous, a function f : E → EReal equals its biconjugate exactly when it has convex real epigraph, is lower semicontinuous, and either never takes the value ⊥ or is identically ⊥.

theorem TauCeti.fenchelConjugate_innerₗ_fenchelConjugate_innerₗ {G : Type u_2} [NormedAddCommGroup G] [InnerProductSpace ℝ G] [CompleteSpace G] {f : G → EReal} (hf : Convex ℝ {p : G × ℝ | f p.1 ≤ ↑p.2}) (hlsc : LowerSemicontinuous f) (hbot : ∀ (x : G), f x ≠ ⊥) : fenchelConjugate (innerₗ G) (fenchelConjugate (innerₗ G) f) = f

The Fenchel–Moreau theorem on a complete real inner product space. A function f : G → EReal with convex real epigraph that is lower semicontinuous and never takes the value ⊥ is the conjugate of its conjugate for the inner product pairing.