theorem section14_sublevelZero_nonempty {F : Type u_2} {f : F → EReal} (hInf : sInf (Set.range f) < 0) : {x : F | f x ≤ 0}.Nonempty

If inf f < 0, then the 0-sublevel set of f is nonempty.

theorem section14_exists_lt_zero_of_sInf_lt_zero {F : Type u_2} {f : F → EReal} (hInf : sInf (Set.range f) < 0) : ∃ (x : F), f x < 0

If inf f < 0, then there exists a point with f x < 0.

Auxiliary lemmas for inner-product polar cones

These lemmas are used to connect 0-sublevel sets of support functions (Section 13) with innerDualCone (Mathlib) and to access the bipolar identity in ℝⁿ.

theorem section14_innerDualCone_closure_coneHull_eq {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (s : Set H) : ProperCone.innerDual (closure ↑(ConvexCone.hull ℝ (Set.insert 0 s))) = ProperCone.innerDual s

The inner dual cone is unchanged by replacing a set with the closure of its conic hull.

theorem section14_innerDualCone_innerDualCone_eq_closure_coneHull {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (s : Set H) : ↑(ProperCone.innerDual ↑(ProperCone.innerDual s)) = closure ↑(ConvexCone.hull ℝ (Set.insert 0 s))

Bipolar theorem (inner-product version): the double inner dual cone of a set is the closure of its conic hull.

theorem section14_toDual_mem_polarCone_iff {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (s : Set H) (y : H) : ↑((InnerProductSpace.toDual ℝ H) y) ∈ polarCone s ↔ ∀ x ∈ s, inner ℝ y x ≤ 0

In a real inner product space, the polar cone condition for toDual y is the inequality ⟪y, x⟫ ≤ 0 on the set.

theorem section14_toDual_mem_polarCone_iff_neg_mem_innerDualCone {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (s : Set H) (y : H) : ↑((InnerProductSpace.toDual ℝ H) y) ∈ polarCone s ↔ -y ∈ ↑(ProperCone.innerDual s)

In a real inner product space, the polar cone condition for toDual y is equivalent to membership of -y in the inner dual cone of the set.

theorem section14_le_zero_on_sublevelZero_of_fenchelConjugate_le_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (φ : Module.Dual ℝ E) (hφ : fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0) (x : E) : f x ≤ 0 → φ x ≤ 0

If f* φ ≤ 0, then φ is nonpositive on the 0-sublevel set of f.

theorem section14_fenchelConjugate_le_zero_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (φ : Module.Dual ℝ E) : fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0 ↔ ∀ (x : E), ↑(φ x) ≤ f x

The Fenchel conjugate is nonpositive iff the functional is dominated by the primal function: f* φ ≤ 0 iff φ x ≤ f x for all x.

theorem section14_sublevel_fenchelConjugate_le_zero_subset_polarCone_hull_sublevelZero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} : {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0} ⊆ polarCone ↑(ConvexCone.hull ℝ {x : E | f x ≤ 0})

The 0-sublevel set of f* lies in the polar cone of the convex cone generated by the 0-sublevel set of f.

theorem section14_closure_coneHull_subset_polarCone_of_subset {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace (Module.Dual ℝ E)] {K : Set E} {T : Set (Module.Dual ℝ E)} (hT : T ⊆ polarCone K) (hclosed : IsClosed (polarCone K)) : closure ↑(ConvexCone.hull ℝ T) ⊆ polarCone K

If a set of dual elements is contained in the polar cone of K, then the closed convex cone generated by that set is also contained in the polar cone of K.

theorem section14_polarCone_hull_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] (S : Set E) : polarCone ↑(ConvexCone.hull ℝ S) = polarCone S

The polar cone is unchanged by replacing a set with the convex cone it generates.

theorem section14_polarCone_closure_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] (K : Set E) : polarCone (closure K) = polarCone K

In a finite-dimensional real topological vector space, membership in a polar cone propagates from a set to its closure (and conversely).

theorem section14_mem_polarCone_of_mem_polarCone_closure_coneHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] (S : Set E) [TopologicalSpace E] (φ : Module.Dual ℝ E) (hφ : φ ∈ polarCone (closure ↑(ConvexCone.hull ℝ S))) : φ ∈ polarCone S

Restrict a polar-cone condition from the closed conic hull of a set to the set itself.

theorem section14_sublevel_fenchelConjugate_le_zero_subset_polarCone_sublevelZero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} : {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0} ⊆ polarCone {x : E | f x ≤ 0}

The 0-sublevel set of the Fenchel conjugate lies in the polar cone of the 0-sublevel set of the primal function.

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

The weak topology on the algebraic dual induced by the evaluation pairing.

This is the canonical topology in which closure statements about polar sets and conjugate sublevel sets are meaningful; it ensures that all evaluation maps φ ↦ φ x are continuous.

Equations

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

theorem section14_instContinuousAdd_dualWeak {E : Type u_1} [AddCommGroup E] [Module ℝ E] : ContinuousAdd (Module.Dual ℝ E)

theorem section14_instIsTopologicalAddGroup_dualWeak {E : Type u_1} [AddCommGroup E] [Module ℝ E] : IsTopologicalAddGroup (Module.Dual ℝ E)

theorem section14_instContinuousSMul_dualWeak {E : Type u_1} [AddCommGroup E] [Module ℝ E] : ContinuousSMul ℝ (Module.Dual ℝ E)

theorem section14_instLocallyConvexSpace_dualWeak {E : Type u_1} [AddCommGroup E] [Module ℝ E] : LocallyConvexSpace ℝ (Module.Dual ℝ E)

theorem section14_closure_coneHull_nonempty_of_nonempty {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace (Module.Dual ℝ E)] {T : Set (Module.Dual ℝ E)} (hT : T.Nonempty) : (closure ↑(ConvexCone.hull ℝ T)).Nonempty

If T is nonempty, then the closure of the convex cone generated by T is nonempty.

theorem section14_exists_eval_pos_of_not_mem_closure_coneHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] [LocallyConvexSpace ℝ E] (T : Set (Module.Dual ℝ E)) (hKne : (closure ↑(ConvexCone.hull ℝ T)).Nonempty) (φ : Module.Dual ℝ E) (hφ : φ ∉ closure ↑(ConvexCone.hull ℝ T)) : ∃ (x : E), (∀ ψ ∈ closure ↑(ConvexCone.hull ℝ T), ψ x ≤ 0) ∧ 0 < φ x

If φ is not in the weak-closure of the convex cone generated by T, then there is a point x : E such that all elements of that closed cone are nonpositive on x, but φ x > 0.

This is a separation argument in the weak topology; the separating functional is represented as an evaluation map using reflexivity of finite-dimensional spaces.

Theorem 14.3 (duality backbone)

A functional nonpositive on {x | f x ≤ 0} lies in the closed convex cone generated by {φ | f* φ ≤ 0}.

This is the only missing step in section14_part3: the intended proof uses the Section 13 support-function/positively-homogeneous-hull correspondence (Theorem 13.5) together with the polar recession-cone correspondence (Theorem 14.2) and the 0-sublevel/cone-hull identification (Theorem 7.6). Importing the needed Section 13 files is currently blocked by a global name collision on _root_.fenchelConjugateBilin.

theorem section14_sublevelZero_fenchelConjugate_nonempty {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 < ⊤) : {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0}.Nonempty

(Theorem 14.3, auxiliary) Nonemptiness of the 0-sublevel set of the Fenchel conjugate.

In the textbook proof this is deduced from the Fenchel–Moreau identity at 0: f 0 = - inf (f*), so f 0 > 0 forces inf (f*) < 0 and hence {φ | f* φ ≤ 0} is nonempty.

In this development, the corresponding Section 13/Fenchel–Moreau bridge is not yet imported due to a global name collision on _root_.fenchelConjugateBilin.

noncomputable def section14_posHomHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : E → EReal

Positively homogeneous hull generated by f: k(x) = inf_{t>0} t * f(t⁻¹ • x).

This is the standard conic hull construction used in the proof of Theorem 14.3.

Equations

• section14_posHomHull f x = sInf {r : EReal | ∃ (t : ℝ), 0 < t ∧ r = ↑t * f (t⁻¹ • x)}

noncomputable def section14_mulPosOrderIso (t : ℝ) (ht : 0 < t) : EReal ≃o EReal

Multiplication by a positive real number is an order isomorphism on EReal.

Equations

• section14_mulPosOrderIso t ht = { toFun := fun (x : EReal) => ↑t * x, invFun := fun (x : EReal) => ↑t⁻¹ * x, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem section14_posHomHull_eq_iInf {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) (x : E) : section14_posHomHull f x = ⨅ (t : { t : ℝ // 0 < t }), ↑↑t * f ((↑t)⁻¹ • x)

Rewrite section14_posHomHull as an indexed infimum over positive scalars.

theorem section14_posHomHull_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) {t : ℝ} (ht : 0 < t) (x : E) : section14_posHomHull f (t • x) = ↑t * section14_posHomHull f x

Positive homogeneity of section14_posHomHull for strictly positive scalars.

theorem section14_posHomHull_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) (x : E) : section14_posHomHull f x ≤ f x

The positively-homogeneous hull never exceeds the original function (take t = 1).

theorem section14_le_posHomHull_of_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) (φ : Module.Dual ℝ E) (hφ : ∀ (x : E), ↑(φ x) ≤ f x) (x : E) : ↑(φ x) ≤ section14_posHomHull f x

A linear functional dominated by f is also dominated by the positively-homogeneous hull of f.

theorem section14_le_posHomHull_iff_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) (φ : Module.Dual ℝ E) : (∀ (x : E), ↑(φ x) ≤ section14_posHomHull f x) ↔ ∀ (x : E), ↑(φ x) ≤ f x

Pointwise domination by the positively-homogeneous hull of f is equivalent to domination by f.

theorem section14_sublevelZero_fenchelConjugate_posHomHull_eq {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ (section14_posHomHull f) φ ≤ 0} = {φ : Module.Dual ℝ E | fenchelConjugateBilin LinearMap.applyₗ f φ ≤ 0}

The 0-sublevel set of f* is unchanged if f is replaced by its positively-homogeneous hull.

theorem section14_posHomHull_smul_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) {t : ℝ} (ht : 0 < t) (x : E) : section14_posHomHull f (t • x) ≤ ↑t * f x

A basic scaling estimate for the positively-homogeneous hull: choosing the same scaling parameter in the infimum gives k (t • x) ≤ t * f x for t > 0.