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

Equations

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

theorem section14_sublevelZero_fenchelBiconjugate_posHomHull_subset_closure_coneHull_sublevelZero {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) : have p := LinearMap.applyₗ; have k := section14_posHomHull f; have kcl := fenchelConjugateBilin p.flip (fenchelConjugateBilin p k); {y : E | kcl y ≤ 0} ⊆ closure ↑(ConvexCone.hull ℝ {x : E | f x ≤ 0})

(Theorem 14.3, auxiliary) Analytic core: a point in the 0-sublevel set of the Fenchel biconjugate of k = posHomHull f lies in the closed conic hull of {x | f x ≤ 0}.

theorem section14_recessionConeEReal_fenchelBiconjugate_subset_closure {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) : have p := LinearMap.applyₗ; have k := section14_posHomHull f; have kcl := fenchelConjugateBilin p.flip (fenchelConjugateBilin p k); recessionConeEReal kcl ⊆ closure (recessionConeEReal k)

(Theorem 14.3, auxiliary) Recession directions of the Fenchel biconjugate (k*)* lie in the closure of the recession directions of k.

This is the missing structural bridge in the conic-separation proof of Theorem 14.3.

theorem section14_dual_flip_closure_coneHull_sublevelZero_fenchelConjugate_subset_closure_coneHull_sublevelZero {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) : ↑(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, auxiliary) Geometric conversion step for the separation proof.

This is the missing implication in the contradiction argument: if a point x : E is nonpositive under every functional in the closed cone generated by {φ | f* φ ≤ 0}, then x lies in the closed cone generated by {x | f x ≤ 0}.

The textbook proof routes this through the positively-homogeneous hull k of f, the conjugacy (cl k)* = ι_{ {φ | f* φ ≤ 0} }, and the polar/recession correspondence (Theorem 14.2).

theorem section14_polarCone_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 {x : E | f x ≤ 0} ⊆ closure ↑(ConvexCone.hull ℝ {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0})