noncomputable def section14_instTopologicalSpace_dualWeak_part9 {E : Type u_1} [AddCommGroup E] [Module ℝ E] : TopologicalSpace (Module.Dual ℝ E)

noncomputable def section14_triplePairing {E : Type u_1} [AddCommGroup E] [Module ℝ E] (p : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : ℝ × E × ℝ →ₗ[ℝ] ℝ × E × ℝ →ₗ[ℝ] ℝ

A canonical bilinear pairing on triples (λ, x, μ) induced by a bilinear pairing p on E: ⟪(λ, x, μ), (λ★, x★, μ★)⟫ = λ * λ★ + p x x★ + μ * μ★.

@[simp]

theorem section14_triplePairing_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] (p : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (z w : ℝ × E × ℝ) : ((section14_triplePairing p) z) w = z.1 * w.1 + (p z.2.1) w.2.1 + z.2.2 * w.2.2

@[simp]

theorem section14_triplePairing_one_x_mu_negMuStar_xStar_negOne {E : Type u_1} [AddCommGroup E] [Module ℝ E] (p : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (x xStar : E) (μ μStar : ℝ) : ((section14_triplePairing p) (1, x, μ)) (-μStar, xStar, -1) = -μStar + (p x) xStar - μ

theorem section14_fenchelConjugate_le_iff_forall {E : Type u_1} [AddCommGroup E] [Module ℝ E] {F : Type u_2} [AddCommGroup F] [Module ℝ F] (p : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (xStar : F) (μStar : EReal) : fenchelConjugateBilin p f xStar ≤ μStar ↔ ∀ (x : E), ↑((p x) xStar) - f x ≤ μStar

A pointwise reformulation of fenchelConjugateBilin p f x★ ≤ μ★.

theorem section14_isClosed_pointedCone_dual {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module ℝ M] [Module ℝ N] [TopologicalSpace N] [IsTopologicalAddGroup N] [ContinuousSMul ℝ N] [T2Space N] [FiniteDimensional ℝ N] (p : M →ₗ[ℝ] N →ₗ[ℝ] ℝ) (s : Set M) : IsClosed ↑(PointedCone.dual p s)

In finite dimensions, PointedCone.dual p s is a closed set.

theorem section14_mem_dual_liftedEpigraphCone_slice_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {f : E → EReal} (hf : ProperConvexERealFunction f) (p : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (xStar : E) (μStar : ℝ) : have q := section14_triplePairing p; have K := ↑(ConvexCone.hull ℝ {z : ℝ × E × ℝ | ∃ (x : E) (μ : ℝ), z = (1, x, μ) ∧ f x ≤ ↑μ}); (-μStar, xStar, -1) ∈ ↑(PointedCone.dual (-q) K) ↔ fenchelConjugateBilin p f xStar ≤ ↑μStar

Slice characterization for the lifted-epigraph cone (core of Theorem 14.4).

theorem section14_polarCone_closure_coneHull_sublevelZero_subset_closure_coneHull_sublevelZero_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) (hf0 : 0 < f 0) (hf0_ltTop : f 0 < ⊤) (hInf : sInf (Set.range f) < 0) : polarCone (closure ↑(ConvexCone.hull ℝ {x : E | f x ≤ 0})) ⊆ closure ↑(ConvexCone.hull ℝ {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0})

Key inclusion for Theorem 14.3: any functional nonpositive on the closed cone generated by the 0-sublevel set {x | f x ≤ 0} lies in the closed cone generated by the 0-sublevel set of the Fenchel conjugate {φ | f* φ ≤ 0}.

theorem polar_closure_coneHull_sublevelZero_eq_closure_coneHull_sublevelZero_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) (hf0 : 0 < f 0) (hf0_ltTop : f 0 < ⊤) (hInf : sInf (Set.range f) < 0) : polarCone (closure ↑(ConvexCone.hull ℝ {x : E | f x ≤ 0})) = closure ↑(ConvexCone.hull ℝ {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0}) ∧ ↑(PointedCone.dual (-LinearMap.applyₗ).flip (closure ↑(ConvexCone.hull ℝ {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0}))) = closure ↑(ConvexCone.hull ℝ {x : E | f x ≤ 0})

Theorem 14.3. Let f be a closed proper convex function such that f 0 > 0 > inf f. Then the closed convex cones generated by the sublevel sets {x | f x ≤ 0} and {x★ | f* x★ ≤ 0} are polar to each other, where f* denotes the Fenchel–Legendre conjugate of f with respect to the evaluation pairing.

def section14_swapNegₗ (E : Type u_2) [AddCommGroup E] [Module ℝ E] : ℝ × E × ℝ →ₗ[ℝ] ℝ × E × ℝ

Coordinate involution used in Theorem 14.4: swapNeg (λ, x, μ) = (-μ, x, -λ).

@[simp]

theorem section14_swapNegₗ_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] (z : ℝ × E × ℝ) : (section14_swapNegₗ E) z = (-z.2.2, z.2.1, -z.1)

def section14_swapNeg (E : Type u_2) [AddCommGroup E] [Module ℝ E] : (ℝ × E × ℝ) ≃ₗ[ℝ] ℝ × E × ℝ

The linear equivalence associated to section14_swapNegₗ.

@[simp]

theorem section14_swapNeg_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] (z : ℝ × E × ℝ) : (section14_swapNeg E) z = (-z.2.2, z.2.1, -z.1)

@[simp]

theorem section14_swapNeg_swapNeg {E : Type u_1} [AddCommGroup E] [Module ℝ E] (z : ℝ × E × ℝ) : (section14_swapNeg E) ((section14_swapNeg E) z) = z

theorem section14_dual_liftedEpigraphCone_last_nonpos {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {f : E → EReal} (hf : ProperConvexERealFunction f) (p : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : have q := section14_triplePairing p; have K := ↑(ConvexCone.hull ℝ {z : ℝ × E × ℝ | ∃ (x : E) (μ : ℝ), z = (1, x, μ) ∧ f x ≤ ↑μ}); ∀ w ∈ ↑(PointedCone.dual (-q) K), w.2.2 ≤ 0

Elements of the dual of the lifted-epigraph cone have nonpositive last coordinate.

theorem section14_swapNeg_preimage_dual_subset_closure_Kstar {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (p : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (hdom : ∃ (x0 : E) (μ0 : ℝ), fenchelConjugateBilin p f x0 ≤ ↑μ0) : have q := section14_triplePairing p; have K := ↑(ConvexCone.hull ℝ {z : ℝ × E × ℝ | ∃ (x : E) (μ : ℝ), z = (1, x, μ) ∧ f x ≤ ↑μ}); have Kstar := ↑(ConvexCone.hull ℝ {z : ℝ × E × ℝ | ∃ (x : E) (μ : ℝ), z = (1, x, μ) ∧ fenchelConjugateBilin p f x ≤ ↑μ}); {z : ℝ × E × ℝ | (section14_swapNeg E) z ∈ ↑(PointedCone.dual (-q) K)} ⊆ closure Kstar

Cone-slicing reconstruction for the lifted-epigraph polar (reverse inclusion in Theorem 14.4).

If swapNeg z lies in the polar of the lifted-epigraph cone, then z lies in the closure of the cone generated by the epigraph of the Fenchel conjugate.

theorem closure_coneHull_liftedEpigraph_fenchelConjugate_eq_setOf_swapNeg_mem_dual {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (_hf_closed : LowerSemicontinuous f) (p : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (q : ℝ × E × ℝ →ₗ[ℝ] ℝ × E × ℝ →ₗ[ℝ] ℝ) (hq : q = section14_triplePairing p) : (∃ (x0 : E) (μ0 : ℝ), fenchelConjugateBilin p f x0 ≤ ↑μ0) → have K := ↑(ConvexCone.hull ℝ {z : ℝ × E × ℝ | ∃ (x : E) (μ : ℝ), z = (1, x, μ) ∧ f x ≤ ↑μ}); have Kstar := ↑(ConvexCone.hull ℝ {z : ℝ × E × ℝ | ∃ (x : E) (μ : ℝ), z = (1, x, μ) ∧ fenchelConjugateBilin p f x ≤ ↑μ}); closure Kstar = {z : ℝ × E × ℝ | (-z.2.2, z.2.1, -z.1) ∈ ↑(PointedCone.dual (-q) K)}

Theorem 14.4. Let f be a closed proper convex function on ℝⁿ. Let K be the convex cone generated by points (1, x, μ) ∈ ℝ × ℝⁿ × ℝ such that μ ≥ f x, and let K★ be the convex cone generated by points (1, x★, μ★) such that μ★ ≥ f★ x★, where f★ is the Fenchel–Legendre conjugate of f. Then

cl K★ = { (λ★, x★, μ★) | (-μ★, x★, -λ★) ∈ Kᵒ }.

In this formalization, f★ is fenchelConjugateBilin p f for a chosen bilinear pairing p on E, and Kᵒ is modeled as PointedCone.dual (-q) K for a chosen bilinear pairing q on ℝ × E × ℝ.

theorem section14_sanity_gauge_counterexample : (fun (x : ℝ) => ↑(gauge {0} x)) ≠ have p := LinearMap.applyₗ; fenchelConjugateBilin p.flip (erealIndicator (polar {0}))

Sanity check for Theorem 14.5: mathlib's gauge is real-valued, so it cannot match a support function that can take the value ⊤ (e.g. for C = {0}).