Dual pairs

Convex duality — conjugacy, support functions, polarity, the dual operations, normal cones — is a theory about a pairing B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ between two real vector spaces, not about ℝⁿ and not about a space and its topological dual. This file collects the vocabulary the rest of the development is stated against. The topology on E relates to the pairing in two graded ways: IsContinuousPairing B says every ⟨·, y⟩ is a continuous functional on E, and IsCompatiblePairing B says moreover that every continuous functional on E is one. Half of the theory — the conjugate is closed, the polar is closed, f* does not see cl f — needs only the first, and the decisive example is a Banach space paired with its dual in the dual's norm topology: that pairing is continuous on both sides, but compatible only if E is reflexive.

Main definitions

• affineFn B y c — the affine function x ↦ ⟨x, y⟩ - c. Conjugacy is bookkeeping for the affine functions below a convex function, and these are they.
• IsContinuousPairing B, IsCompatiblePairing B — the two classes above, with unbundled fields continuous_pairing and exists_pairing_eq, and evalCLM B : F →ₗ[ℝ] StrongDual ℝ E.
• IsAdjointPair B B' A A' — A : E →ₗ[ℝ] G and A' : H →ₗ[ℝ] F are adjoint for the pairings B and B'.
• prodPairing Bu Bx, negFst B — the pairing of U × X with V × Y, and the sign flip on the first factor that the adjoint of a convex bifunction is stated against.

Main results

• convexFn_affineFn, closedFn_affineFn, affineFn_le_iff — the affine functions of the pairing are closed proper convex, and affineFn B y c ≤ f is the inequality the conjugate measures.
• isAdjointPair_adjoint, isAdjointPair_topDualPairing — the two sources of an adjoint datum: a real inner-product space paired with itself, and a space paired with its topological dual.
• instIsCompatiblePairingTopDual — a topological vector space is compatibly paired with its own continuous dual in its own topology. This is how Fenchel–Moreau is applied in practice.
• instIsContinuousPairingProd, instIsCompatiblePairingProd, isContinuousPairing_prodPairing_flip — a product of continuous (resp. compatible) pairings is continuous (resp. compatible), on either side.
• exists_unique_dual_prod — a continuous linear functional on E × ℝ is (x, μ) ↦ y x + c μ for a unique pair (y, c). Fenchel–Moreau needs this twice, to split a separating functional into a horizontal part and a vertical coefficient before recognising it as an affine minorant.

Implementation notes

There is no transpose: for A : E →ₗ[ℝ] G between arbitrarily paired spaces Aᵀ need not exist, and when it does it is extra data, which is why IsAdjointPair is a four-space predicate on a supplied pair rather than an operation. A separating pairing is Mathlib's LinearMap.Nondegenerate. Where a statement of Rockafellar's needs a hypothesis the book does not write, it is always one of two kinds: a linear map has to be assumed continuous, or a subspace closed. Both are automatic in finite dimensions.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §12.
• H. H. Schaefer, Topological Vector Spaces, Springer, 1966, Chapter IV (dual pairs).

The affine functions of a pairing

noncomputable def Tdaf.ConvexAnalysis.affineFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (y : F) (c : ℝ) : E → EReal

The affine function x ↦ ⟨x, y⟩ - c of the pairing B, as an EReal-valued function. These are the affine minorants conjugacy quantifies over: such a function lies below f exactly when its epigraph contains epi f, and f*(y) is the least c for which that happens.

Equations

• Tdaf.ConvexAnalysis.affineFn B y c x = ↑((B x) y) - ↑c

@[simp]

theorem Tdaf.ConvexAnalysis.affineFn_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (y : F) (c : ℝ) (x : E) : affineFn B y c x = ↑((B x) y) - ↑c

theorem Tdaf.ConvexAnalysis.affineFn_eq_coe {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (y : F) (c : ℝ) (x : E) : affineFn B y c x = ↑((B x) y - c)

theorem Tdaf.ConvexAnalysis.affineFn_ne_bot {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (y : F) (c : ℝ) (x : E) : affineFn B y c x ≠ ⊥

theorem Tdaf.ConvexAnalysis.affineFn_ne_top {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (y : F) (c : ℝ) (x : E) : affineFn B y c x ≠ ⊤

theorem Tdaf.ConvexAnalysis.proper_affineFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (y : F) (c : ℝ) : Proper (affineFn B y c)

theorem Tdaf.ConvexAnalysis.affineFn_smul_add {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (a : ℝ) (y y' : F) (c c' : ℝ) (x : E) : affineFn B (a • y + y') (a * c + c') x = ↑(a * ((B x) y - c) + ((B x) y' - c'))

A multiple of one affine function plus another is again an affine function — the algebraic content of the "vertical half-space" step in the affine-minorant argument.

theorem Tdaf.ConvexAnalysis.convexFn_affineFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} (y : F) (c : ℝ) : ConvexFn (affineFn B y c)

theorem Tdaf.ConvexAnalysis.affineFn_le_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {y : F} {c : ℝ} : affineFn B y c ≤ f ↔ ∀ (x : E), ↑((B x) y) - f x ≤ ↑c

The inequality that the conjugate measures. affineFn B y c ≤ f says exactly that c dominates every value of ⟨x, y⟩ - f x, with no properness hypothesis.

Affine functions and topology

theorem Tdaf.ConvexAnalysis.continuous_affineFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {y : F} {c : ℝ} (h : Continuous fun (x : E) => (B x) y) : Continuous (affineFn B y c)

theorem Tdaf.ConvexAnalysis.lowerSemicontinuous_affineFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {y : F} {c : ℝ} (h : Continuous fun (x : E) => (B x) y) : LowerSemicontinuous (affineFn B y c)

theorem Tdaf.ConvexAnalysis.closedFn_affineFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {y : F} {c : ℝ} [IsTopologicalAddGroup E] (h : Continuous fun (x : E) => (B x) y) : ClosedFn (affineFn B y c)

An affine function of the pairing is a closed convex function as soon as the pairing is continuous. In WeakBilin B — and hence in any finer topology — this holds for every y.

Adjoint pairs

def Tdaf.ConvexAnalysis.IsAdjointPair {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) : Prop

A : E →ₗ[ℝ] G and A' : H →ₗ[ℝ] F are adjoint with respect to the pairings B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ and B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ when ⟨A x, z⟩' = ⟨x, A' z⟩.

The adjoint is data, not a property of A: between arbitrarily paired spaces a transpose need not exist, and when it does it need not be unique unless B is right-separating.

Equations

• Tdaf.ConvexAnalysis.IsAdjointPair B B' A A' = ∀ (x : E) (z : H), (B' (A x)) z = (B x) (A' z)

theorem Tdaf.ConvexAnalysis.isAdjointPair_id {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} : IsAdjointPair B B LinearMap.id LinearMap.id

theorem Tdaf.ConvexAnalysis.IsAdjointPair.flip {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} (h : IsAdjointPair B B' A A') : IsAdjointPair B'.flip B.flip A' A

theorem Tdaf.ConvexAnalysis.IsAdjointPair.comp {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} {K : Type u_5} {L : Type u_6} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [AddCommGroup H] [Module ℝ H] [AddCommGroup K] [Module ℝ K] [AddCommGroup L] [Module ℝ L] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {B'' : K →ₗ[ℝ] L →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} {C : G →ₗ[ℝ] K} {C' : L →ₗ[ℝ] H} (h : IsAdjointPair B B' A A') (h' : IsAdjointPair B' B'' C C') : IsAdjointPair B B'' (C ∘ₗ A) (A' ∘ₗ C')

theorem Tdaf.ConvexAnalysis.IsAdjointPair.add {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 C : E →ₗ[ℝ] G} {A' C' : H →ₗ[ℝ] F} (h : IsAdjointPair B B' A A') (h' : IsAdjointPair B B' C C') : IsAdjointPair B B' (A + C) (A' + C')

theorem Tdaf.ConvexAnalysis.IsAdjointPair.smul {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} (a : ℝ) (h : IsAdjointPair B B' A A') : IsAdjointPair B B' (a • A) (a • A')

theorem Tdaf.ConvexAnalysis.IsAdjointPair.unique {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 →ₗ[ℝ] ℝ} (hB : B.SeparatingRight) {A : E →ₗ[ℝ] G} {A' C' : H →ₗ[ℝ] F} (h : IsAdjointPair B B' A A') (h' : IsAdjointPair B B' A C') : A' = C'

The adjoint is unique when the pairing B is right-separating.

Adjoint pairs from Mathlib's adjoints

theorem Tdaf.ConvexAnalysis.isAdjointPair_clm_adjoint {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [CompleteSpace E] [CompleteSpace G] (A : E →L[ℝ] G) : IsAdjointPair (innerₗ E) (innerₗ G) ↑A ↑(ContinuousLinearMap.adjoint A)

A real Hilbert space paired with itself. ContinuousLinearMap.adjoint supplies the adjoint datum for a continuous linear map between complete real inner-product spaces.

theorem Tdaf.ConvexAnalysis.isAdjointPair_adjoint {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ E] [FiniteDimensional ℝ G] (A : E →ₗ[ℝ] G) : IsAdjointPair (innerₗ E) (innerₗ G) A (LinearMap.adjoint A)

Rockafellar's ℝⁿ. In finite dimension every linear map has an adjoint, and LinearMap.adjoint supplies the datum.

theorem Tdaf.ConvexAnalysis.isAdjointPair_topDualPairing {E : Type u_1} {G : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] (A : E →L[ℝ] G) : IsAdjointPair (topDualPairing ℝ E).flip (topDualPairing ℝ G).flip ↑A ↑(ContinuousLinearMap.precomp ℝ A)

A space paired with its topological dual. For topDualPairing the adjoint datum of a continuous linear map is precomposition; no completeness or finite-dimensionality is needed.

Products of pairings

def Tdaf.ConvexAnalysis.prodPairing {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) : U × X →ₗ[ℝ] V × Y →ₗ[ℝ] ℝ

The pairing of U × X with V × Y determined by pairings of the factors. This is the pairing that a convex bifunction U → X → EReal is conjugated against.

Equations

• Tdaf.ConvexAnalysis.prodPairing Bu Bx = LinearMap.mk₂ ℝ (fun (p : U × X) (q : V × Y) => (Bu p.1) q.1 + (Bx p.2) q.2) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Tdaf.ConvexAnalysis.prodPairing_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (p : U × X) (q : V × Y) : ((prodPairing Bu Bx) p) q = (Bu p.1) q.1 + (Bx p.2) q.2

theorem Tdaf.ConvexAnalysis.prodPairing_flip {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) : (prodPairing Bu Bx).flip = prodPairing Bu.flip Bx.flip

def Tdaf.ConvexAnalysis.negFst {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (B : U × X →ₗ[ℝ] V × Y →ₗ[ℝ] ℝ) : U × X →ₗ[ℝ] V × Y →ₗ[ℝ] ℝ

The sign flip on the first factor: negFst B p q = B (-p.1, p.2) q. This is the pairing the adjoint F* of a convex bifunction is conjugated against; prodPairing alone has the opposite sign on the first factor.

Equations

• Tdaf.ConvexAnalysis.negFst B = B ∘ₗ (-LinearMap.id).prodMap LinearMap.id

@[simp]

theorem Tdaf.ConvexAnalysis.negFst_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (B : U × X →ₗ[ℝ] V × Y →ₗ[ℝ] ℝ) (p : U × X) (q : V × Y) : ((negFst B) p) q = (B (-p.1, p.2)) q

@[simp]

theorem Tdaf.ConvexAnalysis.negFst_prodPairing_apply {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) (p : U × X) (q : V × Y) : ((negFst (prodPairing Bu Bx)) p) q = -(Bu p.1) q.1 + (Bx p.2) q.2

@[simp]

theorem Tdaf.ConvexAnalysis.negFst_negFst {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (B : U × X →ₗ[ℝ] V × Y →ₗ[ℝ] ℝ) : negFst (negFst B) = B

theorem Tdaf.ConvexAnalysis.negFst_prodPairing {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) : negFst (prodPairing Bu Bx) = prodPairing (-Bu) Bx

The sign flip of a product pairing is a product pairing, with the first factor negated.

Stated as an equation of linear maps rather than pointwise (negFst_prodPairing_apply), so that negFst (prodPairing Bu Bx) inherits continuity and compatibility from the factors by instance search.

theorem Tdaf.ConvexAnalysis.negFst_prodPairing_flip {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) : (negFst (prodPairing Bu Bx)).flip = prodPairing (-Bu.flip) Bx.flip

The topological dual of E × ℝ

theorem Tdaf.ConvexAnalysis.dual_prod_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (g : E × ℝ →L[ℝ] ℝ) (x : E) (μ : ℝ) : g (x, μ) = (g ∘SL ContinuousLinearMap.inl ℝ E ℝ) x + g (0, 1) * μ

theorem Tdaf.ConvexAnalysis.exists_unique_dual_prod {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] (g : E × ℝ →L[ℝ] ℝ) : ∃! p : (E →L[ℝ] ℝ) × ℝ, ∀ (x : E) (μ : ℝ), g (x, μ) = p.1 x + p.2 * μ

A continuous linear functional on E × ℝ is (x, μ) ↦ y x + c μ, for a unique (y, c).

The classification of the closed half-spaces of E × ℝ into vertical (c = 0), upper (c < 0) and lower (c > 0) is read off from this decomposition.

Continuous and compatible topologies

The two conditions are two classes, in the order the definitions force: the base class, then the evaluation map evalCLM, then the extension asserting that it is onto. Mathlib's LinearMap.IsContPerfPair is not usable in their place: it asks for joint continuity of (x, y) ↦ B x y (so F would need a topology) and for bijectivity on both sides where surjectivity on one is enough.

class Tdaf.ConvexAnalysis.IsContinuousPairing {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : Prop

The pairing B is continuous in its first variable: every ⟨·, y⟩ is a continuous linear functional on E. This is all that closedness needs — closedFn_conj, conj_clFn, isClosed_polarCone, isClosed_subgradient — and it is strictly weaker than IsCompatiblePairing.

• continuous_left (y : F) : Continuous fun (x : E) => (B x) y

  Every ⟨·, y⟩ is continuous.

theorem Tdaf.ConvexAnalysis.continuous_pairing {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsContinuousPairing B] (y : F) : Continuous fun (x : E) => (B x) y

def Tdaf.ConvexAnalysis.evalCLM {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsContinuousPairing B] : F →ₗ[ℝ] StrongDual ℝ E

The evaluation map of a continuous pairing, y ↦ ⟨·, y⟩, into the continuous dual of E. It turns half-space characterisations that quantify over StrongDual ℝ E into statements about F, and its surjectivity is what IsCompatiblePairing asserts.

Equations

• Tdaf.ConvexAnalysis.evalCLM B = { toFun := fun (y : F) => { toLinearMap := B.flip y, cont := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Tdaf.ConvexAnalysis.evalCLM_apply {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsContinuousPairing B] (y : F) (x : E) : ((evalCLM B) y) x = (B x) y

instance Tdaf.ConvexAnalysis.instIsContinuousPairingFlipFlip {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsContinuousPairing B] : IsContinuousPairing B.flip.flip

B.flip.flip is B definitionally but not syntactically, and instance search does not unfold LinearMap.flip; every result stated for one side and then used at B.flip asks for this instance.

class Tdaf.ConvexAnalysis.IsCompatiblePairing {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) extends Tdaf.ConvexAnalysis.IsContinuousPairing B : Prop

The topology on E is compatible with the pairing B: on top of continuity, evalCLM is onto, so every continuous linear functional on E is ⟨·, y⟩ for some y : F.

This is the hypothesis under which conjugacy is an involution. It says nothing about which compatible topology E carries: σ(E, F) is the coarsest, but a Banach space paired with its own dual satisfies it in the norm topology.

• continuous_left (y : F) : Continuous fun (x : E) => (B x) y
• surjective_eval : Function.Surjective ⇑(evalCLM B)

  Every continuous linear functional on E arises as some ⟨·, y⟩.

theorem Tdaf.ConvexAnalysis.exists_pairing_eq {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsCompatiblePairing B] (g : StrongDual ℝ E) : ∃ (y : F), ∀ (x : E), g x = (B x) y

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingFlipFlip {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsCompatiblePairing B] : IsCompatiblePairing B.flip.flip

Negated pairings

-B is a pairing of the same two spaces, and the minimax theory uses it constantly: the concave argument of a saddle-function pairs against -Bu.

theorem Tdaf.ConvexAnalysis.flip_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) : (-B).flip = -B.flip

instance Tdaf.ConvexAnalysis.isContinuousPairing_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsContinuousPairing B] : IsContinuousPairing (-B)

instance Tdaf.ConvexAnalysis.isCompatiblePairing_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [IsCompatiblePairing B] : IsCompatiblePairing (-B)

instance Tdaf.ConvexAnalysis.isCompatiblePairing_flip_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) [TopologicalSpace F] [IsCompatiblePairing B.flip] : IsCompatiblePairing (-B).flip

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingTopDual {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] : IsCompatiblePairing (topDualPairing ℝ E).flip

A topological vector space is compatibly paired with its own continuous dual, in its own topology. This is the instance that Fenchel–Moreau is applied through in practice.

instance Tdaf.ConvexAnalysis.instIsContinuousPairingTopDualNorm {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] : IsContinuousPairing (topDualPairing ℝ E)

A normed space is continuously paired with its continuous dual in the norm topology of that dual. Compatibility fails here unless E is reflexive, which is why the closedness results are stated over IsContinuousPairing.

theorem Tdaf.ConvexAnalysis.exists_forall_apply_eq {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (Λ : StrongDual ℝ (StrongDual ℝ E)) : ∃ (y : E), ∀ (g : StrongDual ℝ E), Λ g = g y

Every continuous linear functional on the dual of a finite-dimensional normed space is evaluation at a point: reflexivity, in the form the half-space arguments downstream need. Equivalently, topDualPairing ℝ E — as opposed to its flip — is a compatible pairing when E is finite-dimensional.

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingTopDualFinite {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : IsCompatiblePairing (topDualPairing ℝ E)

A finite-dimensional normed space is compatibly paired with its continuous dual from the dual's side as well. With instIsCompatiblePairingTopDual this makes both topDualPairing ℝ E and its flip compatible, which is what lets a conjugate f* be treated as a function in its own right.

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingInner {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : IsCompatiblePairing (innerₗ E)

A real Hilbert space is compatibly paired with itself by the inner product (Fréchet–Riesz).

instance Tdaf.ConvexAnalysis.instIsContinuousPairingProd {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bu] [IsContinuousPairing Bx] : IsContinuousPairing (prodPairing Bu Bx)

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingProd {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] : IsCompatiblePairing (prodPairing Bu Bx)

A product of compatible pairings is compatible: a continuous linear functional on U × X splits as g (u, x) = g (u, 0) + g (0, x).

instance Tdaf.ConvexAnalysis.instIsContinuousPairingNegFstProd {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bu] [IsContinuousPairing Bx] : IsContinuousPairing (negFst (prodPairing Bu Bx))

The pairing an adjoint is conjugated against is continuous whenever the factors are.

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingNegFstProd {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace U] [TopologicalSpace X] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu] [IsCompatiblePairing Bx] : IsCompatiblePairing (negFst (prodPairing Bu Bx))

The pairing an adjoint bifunction is conjugated against is compatible whenever the factors are.

theorem Tdaf.ConvexAnalysis.isContinuousPairing_prodPairing_flip {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace V] [TopologicalSpace Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsContinuousPairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bx.flip] : IsContinuousPairing (prodPairing Bu Bx).flip

The pairing of the two dual factors is continuous whenever each of its halves is. Not an instance, because (prodPairing Bu Bx).flip is not syntactically a prodPairing; prodPairing_flip is what turns it into one.

instance Tdaf.ConvexAnalysis.instIsContinuousPairingNegFstProdFlip {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace V] [TopologicalSpace Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsContinuousPairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsContinuousPairing Bx.flip] : IsContinuousPairing (negFst (prodPairing Bu Bx)).flip

The dual side of the adjoint's pairing. Unlike isContinuousPairing_prodPairing_flip this is an instance, (negFst (prodPairing Bu Bx)).flip being a syntactic match.

instance Tdaf.ConvexAnalysis.instIsCompatiblePairingNegFstProdFlip {U : Type u_1} {V : Type u_2} {X : Type u_3} {Y : Type u_4} [AddCommGroup U] [Module ℝ U] [AddCommGroup V] [Module ℝ V] [AddCommGroup X] [Module ℝ X] [AddCommGroup Y] [Module ℝ Y] [TopologicalSpace V] [TopologicalSpace Y] (Bu : U →ₗ[ℝ] V →ₗ[ℝ] ℝ) [IsCompatiblePairing Bu.flip] (Bx : X →ₗ[ℝ] Y →ₗ[ℝ] ℝ) [IsCompatiblePairing Bx.flip] : IsCompatiblePairing (negFst (prodPairing Bu Bx)).flip

The compatible counterpart of instIsContinuousPairingNegFstProdFlip.