The Legendre–Fenchel conjugate on a real dual pair

Let E and F be real vector spaces paired by a bilinear form B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ, written ⟪x, y⟫ = B x y. The Legendre–Fenchel conjugate of an extended-real function f : E → EReal is the function

f⋆ y = ⨆ x, (⟪x, y⟫ - f x)

on F. It is the basic operation of convex analysis: it turns a function into the supremum of the affine functions y ↦ ⟪x, y⟫ - f x indexed by the points of E, so whatever f is, it is convex, and it is lower semicontinuous for any topology on F making every functional B x continuous. When the pairing is separating and E carries a locally convex topology compatible with it (for instance the weak topology σ(E, F)), the Fenchel–Moreau theorem describes the biconjugate f⋆⋆. If f lies above some affine function x ↦ ⟪x, y⟫ + c (so in particular f never takes the value ⊥), then f⋆⋆ is the largest lower-semicontinuous convex minorant of f; in particular f⋆⋆ = f when f is proper, convex and lower semicontinuous. If f has no such affine minorant, for instance when f x = ⊥ at some point (TauCeti.fenchelConjugate_eq_top_of_eq_bot), then f⋆ ≡ ⊤ and f⋆⋆ ≡ ⊥, even though the lower-semicontinuous convex minorants of f need not all be ⊥. The equality f⋆⋆ = f needs a separation theorem and is proved in TauCeti.Analysis.Convex.FenchelMoreau, for a pairing that represents every continuous linear functional. For a bare bilinear pairing only the inequality f⋆⋆ ≤ f holds (for the zero pairing, f⋆⋆ is the constant ⨅ x, f x). This file contains the algebraic part of the theory, valid on a bare dual pair: the conjugate itself, the Fenchel–Young inequality, the antitone Galois connection between the functions on E and on F that the conjugate and its transpose B.flip form, the biconjugate inequality f⋆⋆ ≤ f and the bound of f⋆⋆ from below by every affine minorant of f, the triple-conjugate identity f⋆⋆⋆ = f⋆, the normalisation rule for an additive constant, the convexity of every conjugate, and its lower semicontinuity for any topology on F making every functional B x continuous.

The codomain is EReal throughout: the supremum defining f⋆ can be +∞ even for a finite f, and it is -∞ exactly when f ≡ +∞. The only subtraction that occurs is ⟪x, y⟫ - f x, a real number minus an extended real, which is always defined and never of the form ∞ - ∞; the value f x = -∞ gives the term +∞, and f x = +∞ gives the term -∞, which contributes nothing to the supremum. Consequently every statement that adds f x to f⋆ y carries the hypotheses that keep ⊥ + ⊤ from arising, and those hypotheses are recorded exactly rather than replaced by a blanket properness assumption.

For a self-paired real seminormed inner product space, B is innerₗ E, whose transpose is itself. The two Galois-connection maps therefore coincide, and every conjugate is lower semicontinuous for the seminorm topology, since the inner product is continuous in each variable.

Main definitions

• TauCeti.fenchelConjugate B f — the Legendre–Fenchel conjugate y ↦ ⨆ x, (B x y - f x).

Main statements

• TauCeti.sub_le_fenchelConjugate and TauCeti.le_add_fenchelConjugate — the Fenchel–Young inequality ⟪x, y⟫ ≤ f x + f⋆ y, in the subtraction form that needs no hypothesis and in the additive form that needs neither summand to be -∞;
• TauCeti.fenchelConjugate_le_iff_fenchelConjugate_flip_le and TauCeti.fenchelConjugate_galoisConnection — f⋆ ≤ g and g⋆ ≤ f both say that the pair (f, g) satisfies the Fenchel–Young inequality; the conjugate for B and the conjugate for the transposed pairing B.flip form an antitone Galois connection;
• TauCeti.fenchelConjugate_flip_fenchelConjugate_le — the biconjugate inequality f⋆⋆ ≤ f, TauCeti.coe_add_le_fenchelConjugate_flip_fenchelConjugate — every affine minorant x ↦ ⟪x, y⟫ + c of f lies below f⋆⋆, and TauCeti.fenchelConjugate_fenchelConjugate_flip_fenchelConjugate — f⋆⋆⋆ = f⋆;
• TauCeti.fenchelConjugate_eq_bot_iff — f⋆ y = -∞ exactly when f ≡ +∞, and TauCeti.fenchelConjugate_eq_top_of_eq_bot — f⋆ ≡ +∞ as soon as f takes the value -∞;
• TauCeti.fenchelConjugate_add_const — adding a real constant to f subtracts it from f⋆;
• TauCeti.convex_epigraph_fenchelConjugate — the real epigraph of a conjugate is convex, and TauCeti.lowerSemicontinuous_fenchelConjugate — a conjugate is lower semicontinuous for any topology on F making every functional B x continuous, such as the weak topology of the pairing, and TauCeti.lowerSemicontinuous_fenchelConjugate_innerₗ — for the inner product pairing of a real seminormed inner product space, every conjugate is lower semicontinuous.

Implementation notes

The conjugate is a supremum, so f x = +∞ is harmless and f x = -∞ is the degenerate value, whereas for the infimal c-transform of optimal transport the roles of the two infinities are exchanged. Up to the sign change c (x, y) = -B x y and the negation of both potentials the two transforms agree, but the sup-based normal form is the one used throughout convex analysis and by the differentiability theory of convex functions, so it is developed on its own terms here. The bridge between the two is a statement about the quadratic transport cost ‖x - y‖ ^ 2 / 2, whose c-concave potentials are exactly ‖x‖ ^ 2 / 2 - u x for u a conjugate (TauCeti.MeasureTheory.OptimalTransport.CTransform.Quadratic).

Convexity of a conjugate is stated as convexity of the real epigraph {p : F × ℝ | f⋆ p.1 ≤ p.2} rather than through ConvexOn, whose scalar action would have to be defined on EReal.

References

• R. T. Rockafellar, Convex Analysis, Princeton Mathematical Series 28, 1970, §12.
• I. Ekeland and R. Témam, Convex Analysis and Variational Problems, Classics in Applied Mathematics 28, SIAM 1999, Chapter I, §4.
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §2.1, for the Legendre transform in the setting of optimal transport.

noncomputable def TauCeti.fenchelConjugate {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (y : F) : EReal

The Legendre–Fenchel conjugate of f : E → EReal with respect to the pairing B, the function y ↦ ⨆ x, (B x y - f x) on F. The subtraction is of an extended real from a real, so it is always defined; the supremum is ⊥ exactly when f ≡ ⊤, and it is ⊤ as soon as f takes the value ⊥.

Equations

• TauCeti.fenchelConjugate B f y = ⨆ (x : E), ↑((B x) y) - f x

theorem TauCeti.fenchelConjugate_apply {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (y : F) : fenchelConjugate B f y = ⨆ (x : E), ↑((B x) y) - f x

The defining formula for the Legendre–Fenchel conjugate.

The Fenchel–Young inequality

theorem TauCeti.sub_le_fenchelConjugate {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (x : E) (y : F) : ↑((B x) y) - f x ≤ fenchelConjugate B f y

The Fenchel–Young inequality, in the form that holds with no hypothesis: every point of E bounds the conjugate from below.

theorem TauCeti.fenchelConjugate_le_iff {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {y : F} {a : EReal} : fenchelConjugate B f y ≤ a ↔ ∀ (x : E), ↑((B x) y) - f x ≤ a

An upper bound for the conjugate at a point is an upper bound for every term of the supremum.

theorem TauCeti.fenchelConjugate_le {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {y : F} {a : EReal} (h : ∀ (x : E), ↑((B x) y) - f x ≤ a) : fenchelConjugate B f y ≤ a

A bound valid for every term of the supremum bounds the conjugate.

theorem TauCeti.fenchelConjugate_eq_top_of_eq_bot {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} (hx : f x = ⊥) (y : F) : fenchelConjugate B f y = ⊤

The conjugate is ⊤ everywhere as soon as f takes the value ⊥ somewhere.

@[simp]

theorem TauCeti.fenchelConjugate_eq_bot_iff {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {y : F} : fenchelConjugate B f y = ⊥ ↔ ∀ (x : E), f x = ⊤

The conjugate takes the value ⊥ exactly when f is identically ⊤.

theorem TauCeti.fenchelConjugate_ne_bot {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} (hx : f x ≠ ⊤) (y : F) : fenchelConjugate B f y ≠ ⊥

The conjugate is not ⊥ as soon as f is finite or ⊥ somewhere.

theorem TauCeti.le_add_fenchelConjugate {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {x : E} {y : F} (hx : f x ≠ ⊥) (hy : fenchelConjugate B f y ≠ ⊥) : ↑((B x) y) ≤ f x + fenchelConjugate B f y

The Fenchel–Young inequality in additive form, ⟪x, y⟫ ≤ f x + f⋆ y, valid whenever neither summand is ⊥; the second summand is ⊥ only when f ≡ ⊤.

@[simp]

theorem TauCeti.fenchelConjugate_top {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (y : F) : fenchelConjugate B ⊤ y = ⊥

The conjugate of the constant ⊤ is the constant ⊥.

@[simp]

theorem TauCeti.fenchelConjugate_bot {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (y : F) : fenchelConjugate B ⊥ y = ⊤

The conjugate of the constant ⊥ is the constant ⊤.

The Galois connection and the biconjugate

theorem TauCeti.fenchelConjugate_le_iff_fenchelConjugate_flip_le {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {g : F → EReal} : fenchelConjugate B f ≤ g ↔ fenchelConjugate B.flip g ≤ f

f⋆ ≤ g and g⋆ ≤ f, the latter for the transposed pairing, both express the Fenchel–Young inequality for the pair (f, g), so they are equivalent, with no finiteness hypothesis.

theorem TauCeti.fenchelConjugate_galoisConnection {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : GaloisConnection (fun (g : (F → EReal)ᵒᵈ) => fenchelConjugate B.flip (OrderDual.ofDual g)) fun (f : E → EReal) => OrderDual.toDual (fenchelConjugate B f)

The conjugate for B and the conjugate for the transposed pairing B.flip form an antitone Galois connection between the functions on E and the functions on F. Order reversal, the biconjugate inequality and the triple-conjugate identity are its standard consequences.

theorem TauCeti.fenchelConjugate_antitone {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : Antitone (fenchelConjugate B)

The conjugate reverses the pointwise order.

theorem TauCeti.fenchelConjugate_flip_fenchelConjugate_le {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : fenchelConjugate B.flip (fenchelConjugate B f) ≤ f

The biconjugate inequality: f⋆⋆ ≤ f, where the second conjugate is taken for the transposed pairing.

theorem TauCeti.fenchelConjugate_fenchelConjugate_flip_fenchelConjugate {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : fenchelConjugate B (fenchelConjugate B.flip (fenchelConjugate B f)) = fenchelConjugate B f

The triple conjugate is the conjugate: f⋆⋆⋆ = f⋆.

theorem TauCeti.coe_add_le_fenchelConjugate_flip_fenchelConjugate {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {f : E → EReal} {y : F} {c : ℝ} (h : ∀ (x : E), ↑((B x) y + c) ≤ f x) (x : E) : ↑((B x) y + c) ≤ fenchelConjugate B.flip (fenchelConjugate B f) x

Every affine minorant x ↦ B x y + c of f lies below the biconjugate f⋆⋆: the minorant bounds f⋆ y by -c.

@[simp]

theorem TauCeti.fenchelConjugate_add_const {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (r : ℝ) (y : F) : fenchelConjugate B (fun (x : E) => f x + ↑r) y = fenchelConjugate B f y - ↑r

Adding a real constant to a function subtracts it from the conjugate.

Convexity and lower semicontinuity

theorem TauCeti.convex_epigraph_fenchelConjugate {E : Type u_1} {F : Type u_2} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : Convex ℝ {p : F × ℝ | fenchelConjugate B f p.1 ≤ ↑p.2}

The real epigraph {(y, r) | f⋆ y ≤ r} of a conjugate is convex: it is the intersection over x of the half-spaces {(y, r) | B x y - r ≤ f x}, each of which is the whole space when f x = ⊤ and empty when f x = ⊥.

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

A conjugate is lower semicontinuous for every topology on F in which each functional B x is continuous, since it is a supremum of continuous or constant extended-real functions.

The inner product pairing

theorem TauCeti.lowerSemicontinuous_fenchelConjugate_innerₗ {G : Type u_3} [SeminormedAddCommGroup G] [InnerProductSpace ℝ G] (f : G → EReal) : LowerSemicontinuous (fenchelConjugate (innerₗ G) f)

The Legendre–Fenchel conjugate for the pairing of a real seminormed inner product space is lower semicontinuous, the inner product being continuous in each variable.