theorem section14_sublevel_posHomHull_le_zero_subset_closure_strictSublevel {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) : {x : E | section14_posHomHull f x ≤ 0} ⊆ closure {x : E | section14_posHomHull f x < 0}

(Theorem 14.3, auxiliary) If inf f < 0, then the 0-sublevel set of the positively homogeneous hull is contained in the closure of its strict 0-sublevel set.

theorem section14_recessionCone_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) : recessionConeEReal (section14_posHomHull f) ⊆ closure ↑(ConvexCone.hull ℝ {x : E | f x ≤ 0})

(Theorem 14.3, auxiliary) Recession directions of posHomHull f lie in the closed conic hull of the 0-sublevel set {x | f x ≤ 0}.

theorem section14_mem_polarCone_of_mem_polarCone_closure_of_subset {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] {A B : Set E} {φ : Module.Dual ℝ E} (hA : A ⊆ closure B) (hφ : φ ∈ polarCone B) : φ ∈ polarCone A

(Theorem 14.3, auxiliary) If A ⊆ closure B and φ is nonpositive on B, then φ is nonpositive on A.

This is the form needed to transfer a polar condition along an inclusion into a closure.

theorem section14_mem_recessionConeEReal_iff_map_mem_recessionConeEReal_of_linearEquiv {E₁ : Type u_2} {F₁ : Type u_3} [AddCommGroup E₁] [Module ℝ E₁] [AddCommGroup F₁] [Module ℝ F₁] (e : E₁ ≃ₗ[ℝ] F₁) (g : E₁ → EReal) (y : E₁) : y ∈ recessionConeEReal g ↔ e y ∈ recessionConeEReal fun (z : F₁) => g (e.symm z)

Transport membership in recessionConeEReal along a linear equivalence.

theorem section14_recessionConeEReal_image_linearEquiv {E₁ : Type u_2} {F₁ : Type u_3} [AddCommGroup E₁] [Module ℝ E₁] [AddCommGroup F₁] [Module ℝ F₁] (e : E₁ ≃ₗ[ℝ] F₁) (g : E₁ → EReal) : ⇑e '' recessionConeEReal g = recessionConeEReal fun (z : F₁) => g (e.symm z)

recessionConeEReal commutes with linear equivalences, as a set.

theorem section14_recessionConeEReal_eq_sublevel_of_subadd_zero {F : Type u_2} [AddCommGroup F] (g : F → EReal) (hg0 : g 0 = 0) (hg_subadd : ∀ (x y : F), g (x + y) ≤ g x + g y) : recessionConeEReal g = {y : F | g y ≤ 0}

Recession directions of a subadditive function with g 0 = 0 are exactly its 0-sublevel set.

theorem section14_le_at_zero_of_mem_recessionConeEReal {F : Type u_2} [AddCommGroup F] (g : F → EReal) {y : F} (hy : y ∈ recessionConeEReal g) (h0dom : 0 ∈ erealDom g) : g y ≤ g 0

Recession directions give a pointwise inequality at the origin: if y ∈ recessionConeEReal g and 0 ∈ dom g, then g y ≤ g 0.

theorem section14_kcl_zero_dom_and_le_zero {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 < ⊤) : have p := LinearMap.applyₗ; have k := section14_posHomHull f; have kcl := fenchelConjugateBilin p.flip (fenchelConjugateBilin p k); 0 ∈ erealDom kcl ∧ kcl 0 ≤ 0

For kcl = (k*)* coming from the positively homogeneous hull k of f, we have 0 ∈ dom kcl and kcl 0 ≤ 0.

theorem section14_not_mem_closure_epigraph_of_not_mem_closure_strictSublevel {F : Type u_2} [TopologicalSpace F] {k : F → EReal} {y : F} {ε : ℝ} (hε : 0 < ε) (hy : y ∉ closure {z : F | k z < ↑ε}) : have r0 := ε / 2; have epi := {p : F × ℝ | k p.1 ≤ ↑p.2}; (y, r0) ∉ closure epi

(Theorem 14.3, auxiliary) If y is not in the closure of the strict ε-sublevel set of k, then (y, ε/2) is not in the closure of the (real) epigraph of k.

theorem section14_fenchelConjugate_le_neg_const_of_add_const_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {k : E → EReal} {ψ : Module.Dual ℝ E} {c : ℝ} (hk_ne_bot : ∀ (x : E), k x ≠ ⊥) (hψ : ∀ (x : E), ↑(ψ x) + ↑c ≤ k x) : have p := LinearMap.applyₗ; fenchelConjugateBilin p k ψ ≤ -↑c

(Theorem 14.3, auxiliary) From an affine bound ψ + c ≤ k, one gets k* ψ ≤ -c.

theorem section14_fenchelBiconjugate_pos_of_dual_certificate {E : Type u_1} [AddCommGroup E] [Module ℝ E] {k : E → EReal} {y : E} {ψ : Module.Dual ℝ E} {c r0 : ℝ} (hr0 : ↑r0 < ↑(ψ y) + ↑c) (hconj : fenchelConjugateBilin LinearMap.applyₗ k ψ ≤ -↑c) : have p := LinearMap.applyₗ; have kcl := fenchelConjugateBilin p.flip (fenchelConjugateBilin p k); ↑r0 < kcl y

(Theorem 14.3, auxiliary) A dual certificate forces strict positivity of the biconjugate.

theorem section14_closure_epigraph_upwardClosed {F : Type u_2} [TopologicalSpace F] {k : F → EReal} {x : F} {r r' : ℝ} (hr : (x, r) ∈ closure {p : F × ℝ | k p.1 ≤ ↑p.2}) (hrr' : r ≤ r') : (x, r') ∈ closure {p : F × ℝ | k p.1 ≤ ↑p.2}

(Theorem 14.3, auxiliary) The closure of a real epigraph is upward closed in the ℝ-coordinate.

This is the basic monotonicity property inherited from the definition k x ≤ r.

theorem section14_linearPerturb_bound_on_closure_epigraph {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] {k : E → EReal} {ψ₁ : Module.Dual ℝ E} {c₁ : ℝ} (hminor : ∀ (x : E), ↑(ψ₁ x) + ↑c₁ ≤ k x) : have epi := {p : E × ℝ | k p.1 ≤ ↑p.2}; have g := (LinearMap.toContinuousLinearMap ψ₁).comp (ContinuousLinearMap.fst ℝ E ℝ) - ContinuousLinearMap.snd ℝ E ℝ; ∀ p ∈ closure epi, g p ≤ -c₁

(Theorem 14.3, auxiliary) If ψ₁ + c₁ ≤ k, then g(x,r) = ψ₁ x - r is bounded above on closure (epi k).

theorem section14_sep_dual_certificate_of_not_mem_closure_epigraph {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] [LocallyConvexSpace ℝ E] {k : E → EReal} (hk : ProperConvexERealFunction k) (hk0 : k 0 = 0) (hminor : ∃ (ψ₁ : Module.Dual ℝ E) (c₁ : ℝ), ∀ (x : E), ↑(ψ₁ x) + ↑c₁ ≤ k x) {y : E} {r0 : ℝ} : have epi := {p : E × ℝ | k p.1 ≤ ↑p.2}; (y, r0) ∉ closure epi → ∃ (ψ : Module.Dual ℝ E) (c : ℝ), ↑r0 < ↑(ψ y) + ↑c ∧ ∀ (x : E), ↑(ψ x) + ↑c ≤ k x

(Theorem 14.3, auxiliary) Separation of a point from closure (epi k) yields a dual certificate ψ + c ≤ k that is strictly above the point in the epigraph direction.

theorem section14_fenchelBiconjugate_sublevelZero_approx_by_posHomHull {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 < ⊤) : have p := LinearMap.applyₗ; have k := section14_posHomHull f; have kcl := fenchelConjugateBilin p.flip (fenchelConjugateBilin p k); ∀ {y : E}, kcl y ≤ 0 → ∀ {ε : ℝ}, 0 < ε → y ∈ closure {z : E | k z < ↑ε}

(Theorem 14.3, auxiliary) Approximation of kcl-sublevel points by strict sublevels of k.

This is the analytic heart of Theorem 14.3: from kcl y ≤ 0 one should be able to find points arbitrarily close to y where the (possibly non-closed) positively homogeneous hull k takes an arbitrarily small (strict) value.

theorem section14_strictSublevel_mem_of_smallValue_add_smul_negDir {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 < ⊤) {x0 z : E} {ε t : ℝ} (ht : 0 < t) (hz : section14_posHomHull f z < ↑ε) (hx0 : ↑t * f x0 < -↑ε) : section14_posHomHull f (z + t • x0) < 0

(Theorem 14.3, auxiliary) If k z is small and moving in a fixed direction makes k very negative, then the translated point lies in the strict 0-sublevel set.

theorem section14_sublevelZero_fenchelBiconjugate_posHomHull_subset_closure_strictSublevel_posHomHull {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 {z : E | k z < 0}

(Theorem 14.3, auxiliary) From kcl y ≤ 0 we can reach the strict 0-sublevel of k by arbitrarily small perturbations, hence y lies in the closure of {k < 0}.