theorem section14_finrank_dualAnnihilator_eq_sub {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] (W : Submodule ℝ E) : Module.finrank ℝ ↥W.dualAnnihilator = Module.finrank ℝ E - Module.finrank ℝ ↥W

Finite-dimensional formula: dim(Wᵃⁿⁿ) = dim(E) - dim(W) for dual annihilators.

theorem section14_span_polar_eq_dualAnnihilator_span_lineality {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {C : Set E} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : Submodule.span ℝ (polar C) = (Submodule.span ℝ (-C.recessionCone ∩ C.recessionCone)).dualAnnihilator

Orthogonality relation: the span of polar C is the dual annihilator of the lineality subspace of C (spanned by (-rec C) ∩ rec C).

theorem section14_span_lineality_polar_eq_dualAnnihilator_span {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} : Submodule.span ℝ (-(polar C).recessionCone ∩ (polar C).recessionCone) = (Submodule.span ℝ C).dualAnnihilator

Orthogonality relation (dual direction): the span of the lineality subspace of polar C is the dual annihilator of span C.

theorem finrank_span_polar_eq_finrank_sub_finrank_span_lineality_and_dual_and_rank {E : Type u_1} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {C : Set E} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : Module.finrank ℝ ↥(Submodule.span ℝ (polar C)) = Module.finrank ℝ E - Module.finrank ℝ ↥(Submodule.span ℝ (-C.recessionCone ∩ C.recessionCone)) ∧ Module.finrank ℝ ↥(Submodule.span ℝ (-(polar C).recessionCone ∩ (polar C).recessionCone)) = Module.finrank ℝ E - Module.finrank ℝ ↥(Submodule.span ℝ C) ∧ Module.finrank ℝ ↥(Submodule.span ℝ (polar C)) - Module.finrank ℝ ↥(Submodule.span ℝ (-(polar C).recessionCone ∩ (polar C).recessionCone)) = Module.finrank ℝ ↥(Submodule.span ℝ C) - Module.finrank ℝ ↥(Submodule.span ℝ (-C.recessionCone ∩ C.recessionCone))

Corollary 14.6.1. Let C be a closed convex set in ℝ^n containing the origin. Then dimension C^∘ = n - lineality C, lineality C^∘ = n - dimension C, and rank C^∘ = rank C.

In this file, we model C^∘ as polar C : Set (Module.Dual ℝ E). We interpret the book's dimension S as Module.finrank ℝ (Submodule.span ℝ S) and the book's lineality S as Module.finrank ℝ (Submodule.span ℝ ((-Set.recessionCone S) ∩ Set.recessionCone S)), so that rank S = dimension S - lineality S.

theorem section14_fenchelConjugate_nonneg_of_nonneg_and_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf_nonneg : ∀ (x : E), 0 ≤ f x) (hf0 : f 0 = 0) : (∀ (xStar : Module.Dual ℝ E), 0 ≤ fenchelConjugateBilin LinearMap.applyₗ f xStar) ∧ fenchelConjugateBilin LinearMap.applyₗ f 0 = 0

If f is nonnegative and vanishes at 0, then its Fenchel conjugate (for evaluation) is also nonnegative and vanishes at 0.

theorem section14_eval_le_add_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (x : E) (xStar : Module.Dual ℝ E) (hfbot : f x ≠ ⊥) (hftop : f x ≠ ⊤) : ↑(xStar x) ≤ f x + fenchelConjugateBilin LinearMap.applyₗ f xStar

Fenchel–Young inequality for the evaluation pairing: ⟪x★, x⟫ ≤ f x + f★ x★.

theorem section14_inv_smul_sublevel_fenchelConjugate_subset_two_smul_polar_sublevel {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf_nonneg : ∀ (x : E), 0 ≤ f x) {α : ℝ} (hα : 0 < α) : α⁻¹ • {xStar : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f xStar ≤ ↑α} ⊆ 2 • polar {x : E | f x ≤ ↑α}

The α⁻¹-scaled α-sublevel set of the conjugate lies in 2 • polar of the primal α-sublevel set.

theorem section14_polar_sublevel_subset_inv_smul_sublevel_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf_nonneg : ∀ (x : E), 0 ≤ f x) (hf_conv : ConvexERealFunction f) (hf0 : f 0 = 0) {α : ℝ} (hα : 0 < α) : polar {x : E | f x ≤ ↑α} ⊆ α⁻¹ • {xStar : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f xStar ≤ ↑α}

The polar of the primal α-sublevel set is contained in the α⁻¹-scaled α-sublevel set of the conjugate, for a convex function vanishing at 0.

theorem polar_sublevel_eq_inv_smul_sublevel_fenchelConjugate_and_subset_two_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {f : E → EReal} (hf_nonneg : ∀ (x : E), 0 ≤ f x) (hf_conv : ConvexERealFunction f) (hf0 : f 0 = 0) {α : ℝ} (hα : 0 < α) : have p := LinearMap.applyₗ; have fstar := fenchelConjugateBilin p f; (∀ (xStar : Module.Dual ℝ E), 0 ≤ fstar xStar) ∧ fstar 0 = 0 ∧ polar {x : E | f x ≤ ↑α} ⊆ α⁻¹ • {xStar : Module.Dual ℝ E | fstar xStar ≤ ↑α} ∧ α⁻¹ • {xStar : Module.Dual ℝ E | fstar xStar ≤ ↑α} ⊆ 2 • polar {x : E | f x ≤ ↑α}

Theorem 14.7. Let f be a non-negative closed convex function which vanishes at the origin. Then the Fenchel–Legendre conjugate f* (with respect to the evaluation pairing) is also non-negative and vanishes at the origin. Moreover, for 0 < α < ∞ one has

{x | f x ≤ α}^∘ = α⁻¹ • {x★ | f* x★ ≤ α} ⊆ 2 • {x | f x ≤ α}^∘,

where ^∘ denotes the polar of a set (modeled here as polar).