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

Equations

• section14_instTopologicalSpace_dualWeak_part10 = WeakBilin.instTopologicalSpace LinearMap.applyₗ.flip

theorem section14_polar_eq_iInter_halfspaces {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : polar C = ⋂ x ∈ C, {φ : Module.Dual ℝ E | φ x ≤ 1}

Polar sets are intersections of half-spaces {φ | φ x ≤ 1}.

theorem section14_isClosed_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : IsClosed (polar C)

Under the weak topology on the algebraic dual induced by evaluation, polar sets are closed.

theorem section14_convex_and_zeroMem_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) : Convex ℝ (polar C) ∧ 0 ∈ polar C

Convexity and 0-membership of a polar set (topology-free).

theorem section14_bipolar_eq_of_closed_convex {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {C : Set E} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : {x : E | ∀ φ ∈ polar C, φ x ≤ 1} = C

The bipolar identity for closed convex sets containing the origin.

noncomputable def section14_egauge {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) (x : E) : EReal

An EReal-valued gauge: sInf {r | 0 < r ∧ x ∈ r • C} (with ⊤ for points not in any positive scaling of C). This is the textbook gauge, unlike mathlib's real-valued gauge.

Equations

• section14_egauge C x = sInf ((fun (r : ℝ) => ↑r) '' {r : ℝ | 0 < r ∧ x ∈ r • C})

theorem section14_mem_smul_set_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) {r : ℝ} (hr : r ≠ 0) {x : E} : x ∈ r • C ↔ (1 / r) • x ∈ C

For r ≠ 0, membership in r • C is equivalent to membership of (1 / r) • x in C.

theorem section14_mem_smul_set_iff_forall_polar_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hCpolar : {x : E | ∀ φ ∈ polar C, φ x ≤ 1} = C) {r : ℝ} (hr : 0 < r) {x : E} : x ∈ r • C ↔ ∀ φ ∈ polar C, φ x ≤ r

If C satisfies the bipolar identity, then x ∈ r • C is equivalent to φ x ≤ r for all φ ∈ polar C (for r > 0).

theorem section14_fenchelConjugate_flip_erealIndicator_polar_eq_sSup {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) (x : E) : have p := LinearMap.applyₗ; fenchelConjugateBilin p.flip (erealIndicator (polar C)) x = sSup ((fun (φ : Module.Dual ℝ E) => ↑(φ x)) '' polar C)

fenchelConjugateBilin of an erealIndicator is a support function: for the flipped evaluation pairing, it is sSup {φ x | φ ∈ polar C}.

theorem section14_fenchelConjugate_erealIndicator_eq_sSup {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) (φ : Module.Dual ℝ E) : have p := LinearMap.applyₗ; fenchelConjugateBilin p (erealIndicator C) φ = sSup ((fun (x : E) => ↑(φ x)) '' C)

fenchelConjugateBilin of an erealIndicator is a support function: for the evaluation pairing, it is sSup {φ x | x ∈ C}.

theorem section14_egauge_eq_fenchelConjugate_indicator_polar {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {C : Set E} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : have p := LinearMap.applyₗ; (fun (x : E) => section14_egauge C x) = fenchelConjugateBilin p.flip (erealIndicator (polar C))

The EReal-valued gauge of a closed convex set containing 0 agrees with the support function of its polar set.

theorem section14_mem_smul_polar_iff_forall_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) {r : ℝ} (hr : 0 < r) {φ : Module.Dual ℝ E} : φ ∈ r • polar C ↔ ∀ x ∈ C, φ x ≤ r

Membership in r • polar C is equivalent to a uniform bound φ x ≤ r on C (for r > 0).

theorem section14_egauge_polar_eq_fenchelConjugate_indicator {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hC0 : 0 ∈ C) : have p := LinearMap.applyₗ; (fun (φ : Module.Dual ℝ E) => section14_egauge (polar C) φ) = fenchelConjugateBilin p (erealIndicator C)

The EReal-valued gauge of the polar set agrees with the support function of C.

theorem polar_closed_convex_bipolar_eq_and_gauge_eq_support {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {C : Set E} : IsClosed C → Convex ℝ C → 0 ∈ C → (IsClosed (polar C) ∧ Convex ℝ (polar C) ∧ 0 ∈ polar C) ∧ {x : E | ∀ φ ∈ polar C, φ x ≤ 1} = C ∧ have p := LinearMap.applyₗ; (fun (x : E) => section14_egauge C x) = fenchelConjugateBilin p.flip (erealIndicator (polar C)) ∧ (fun (φ : Module.Dual ℝ E) => section14_egauge (polar C) φ) = fenchelConjugateBilin p (erealIndicator C)

Theorem 14.5: Let C be a closed convex set containing the origin. Then the polar C^∘ is another closed convex set containing the origin, and the bipolar identity C^{∘∘} = C holds. The gauge function of C is the support function of C^∘. Dually, the gauge function of C^∘ is the support function of C.

theorem section14_zero_mem_interior_iff_forall_exists_pos_smul_mem {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [FiniteDimensional ℝ E] [T2Space E] {C : Set E} (hCconv : Convex ℝ C) : 0 ∈ interior C ↔ ∀ (y : E), ∃ (ε : ℝ), 0 < ε ∧ ε • y ∈ C

In a finite-dimensional Hausdorff real topological vector space, a convex set contains the origin in its interior iff every vector can be scaled into it.

theorem polar_bounded_iff_zero_mem_interior_and_dual {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [FiniteDimensional ℝ E] [T2Space E] {C : Set E} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC0 : 0 ∈ C) : (Bornology.IsBounded (polar C) ↔ 0 ∈ interior C) ∧ (Bornology.IsBounded C ↔ 0 ∈ interior (polar C))

Corollary 14.5.1. Let C be a closed convex set containing the origin. Then the polar C^∘ is bounded if and only if 0 ∈ int C. Dually, C is bounded if and only if 0 ∈ int C^∘.

theorem section14_recessionCone_eq_forall_polar_le_zero_of_bipolar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {Cpolar : Set (Module.Dual ℝ E)} (hbipolar : {x : E | ∀ φ ∈ Cpolar, φ x ≤ 1} = C) (hC0 : 0 ∈ C) : C.recessionCone = {y : E | ∀ φ ∈ Cpolar, φ y ≤ 0}

If C is given as {x | ∀ φ ∈ Cpolar, φ x ≤ 1}, then its recession cone is exactly the set of directions on which every φ ∈ Cpolar is nonpositive.

theorem section14_neg_rec_inter_rec_eq_forall_polar_eq_zero_of_bipolar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {Cpolar : Set (Module.Dual ℝ E)} (hbipolar : {x : E | ∀ φ ∈ Cpolar, φ x ≤ 1} = C) (hC0 : 0 ∈ C) : -C.recessionCone ∩ C.recessionCone = {y : E | ∀ φ ∈ Cpolar, φ y = 0}

Under the same bipolar hypothesis, the set of "two-sided" recession directions is exactly the set of vectors annihilated by all φ ∈ Cpolar.

theorem section14_dualCoannihilator_span_polar_eq_span_negRec_inter_rec_of_bipolar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {Cpolar : Set (Module.Dual ℝ E)} (hbipolar : {x : E | ∀ φ ∈ Cpolar, φ x ≤ 1} = C) (hC0 : 0 ∈ C) : (Submodule.span ℝ Cpolar).dualCoannihilator = Submodule.span ℝ (-C.recessionCone ∩ C.recessionCone)

Under the bipolar hypothesis, the lineality subspace of C (spanned by (-rec C) ∩ rec C) is the dual coannihilator of the span of Cpolar.

theorem section14_recessionCone_Cpolar_eq_forall_primal_le_zero_of_hpolar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {Cpolar : Set (Module.Dual ℝ E)} (hpolar : Cpolar = polar C) (hCpolar0 : 0 ∈ Cpolar) : Cpolar.recessionCone = {ψ : Module.Dual ℝ E | ∀ x ∈ C, ψ x ≤ 0}

If Cpolar = polar C and 0 ∈ Cpolar, then recession directions in Cpolar are exactly the functionals nonpositive on C.

theorem section14_lineality_Cpolar_eq_forall_primal_eq_zero_of_hpolar {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} {Cpolar : Set (Module.Dual ℝ E)} (hpolar : Cpolar = polar C) (hCpolar0 : 0 ∈ Cpolar) : -Cpolar.recessionCone ∩ Cpolar.recessionCone = {ψ : Module.Dual ℝ E | ∀ x ∈ C, ψ x = 0}

If Cpolar = polar C and 0 ∈ Cpolar, then the two-sided recession directions in Cpolar are exactly the functionals vanishing on C.