theorem section14_fenchelConjugate_posHomHull_eq_top_of_fenchelConjugate_pos {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (φ : Module.Dual ℝ E) (hpos : 0 < fenchelConjugateBilin LinearMap.applyₗ f φ) : fenchelConjugateBilin LinearMap.applyₗ (section14_posHomHull f) φ = ⊤

(Theorem 14.3, auxiliary) If f* φ is strictly positive, then (posHomHull f)* φ = ⊤.

This is the scaling argument used to identify the effective domain of the conjugate of the positively-homogeneous hull.

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

(Theorem 14.3, auxiliary) The effective domain of the conjugate of the positively homogeneous hull is exactly the 0-sublevel set of the original conjugate.

theorem section14_posHomHull_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf0 : 0 < f 0) (hf0_ltTop : f 0 < ⊤) (hf0_ne_bot : f 0 ≠ ⊥) : section14_posHomHull f 0 = 0

The positively-homogeneous hull takes value 0 at the origin, provided f 0 is finite and strictly positive.

theorem section14_strictSublevel_posHomHull_subset_coneHull_sublevelZero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) : {x : E | section14_posHomHull f x < 0} ⊆ ↑(ConvexCone.hull ℝ {x : E | f x ≤ 0})

Strict negativity for the positively-homogeneous hull forces membership in the conic hull of the 0-sublevel set of f.

theorem section14_posHomHull_ne_bot {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 < ⊤) (x : E) : section14_posHomHull f x ≠ ⊥

(Theorem 14.3, auxiliary) Under the hypotheses ensuring nonemptiness of the dual 0-sublevel set, the positively homogeneous hull never takes the value ⊥.

theorem section14_posHomHull_subadd {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 < ⊤) (x y : E) : section14_posHomHull f (x + y) ≤ section14_posHomHull f x + section14_posHomHull f y

(Theorem 14.3, auxiliary) Subadditivity of the positively homogeneous hull.

theorem section14_properConvex_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 < ⊤) : ProperConvexERealFunction (section14_posHomHull f)

(Theorem 14.3, auxiliary) The positively homogeneous hull is a proper convex function.

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

In the weak topology on the algebraic dual induced by evaluation, every evaluation map φ ↦ φ x is continuous.

Equations

• section14_instTopologicalSpace_dualWeak_part6 = section14_instTopologicalSpace_dualWeak

theorem section14_continuous_dual_apply {E : Type u_1} [AddCommGroup E] [Module ℝ E] (x : E) : Continuous fun (φ : Module.Dual ℝ E) => φ x

theorem section14_lowerSemicontinuous_fenchelConjugate_dual {E : Type u_1} [AddCommGroup E] [Module ℝ E] (f : E → EReal) : LowerSemicontinuous (fenchelConjugateBilin LinearMap.applyₗ f)

The Fenchel conjugate (with respect to the evaluation pairing) is lower semicontinuous in the weak topology on Module.Dual ℝ E.

theorem section14_lowerSemicontinuous_fenchelConjugate_flip {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] (g : Module.Dual ℝ E → EReal) : LowerSemicontinuous (fenchelConjugateBilin LinearMap.applyₗ.flip g)

The Fenchel conjugate with respect to the flipped evaluation pairing is lower semicontinuous as a function of the primal variable (in finite dimensions, where all linear functionals are continuous).

theorem section14_lowerSemicontinuous_posHomHull {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] {f : E → EReal} (_hf_closed : LowerSemicontinuous f) : have p := LinearMap.applyₗ; LowerSemicontinuous (fenchelConjugateBilin p.flip (fenchelConjugateBilin p (section14_posHomHull f)))

(Theorem 14.3, auxiliary) The closed hull cl k of the positively homogeneous hull is modeled as the Fenchel biconjugate (k*)*, and is lower semicontinuous.

theorem section14_fenchelConjugate_ne_bot_of_proper {E₁ : Type u_2} {F₁ : Type u_3} [AddCommGroup E₁] [Module ℝ E₁] [AddCommGroup F₁] [Module ℝ F₁] (p : E₁ →ₗ[ℝ] F₁ →ₗ[ℝ] ℝ) {f : E₁ → EReal} (hf : ProperERealFunction f) (y : F₁) : fenchelConjugateBilin p f y ≠ ⊥

(Theorem 14.3, auxiliary) The Fenchel conjugate of a proper EReal function (with respect to any real bilinear pairing) never takes the value ⊥.

theorem section14_fenchelConjugate_anti {E₁ : Type u_2} {F₁ : Type u_3} [AddCommGroup E₁] [Module ℝ E₁] [AddCommGroup F₁] [Module ℝ F₁] (p : E₁ →ₗ[ℝ] F₁ →ₗ[ℝ] ℝ) {f g : E₁ → EReal} (hfg : ∀ (x : E₁), f x ≤ g x) (y : F₁) : fenchelConjugateBilin p g y ≤ fenchelConjugateBilin p f y

(Theorem 14.3, auxiliary) Antitonicity of the Fenchel conjugate in the primal function.

theorem section14_fenchelBiconjugate_le_of_proper {E₁ : Type u_2} {F₁ : Type u_3} [AddCommGroup E₁] [Module ℝ E₁] [AddCommGroup F₁] [Module ℝ F₁] (p : E₁ →ₗ[ℝ] F₁ →ₗ[ℝ] ℝ) {f : E₁ → EReal} (hf : ProperERealFunction f) (x : E₁) : fenchelConjugateBilin p.flip (fenchelConjugateBilin p f) x ≤ f x

(Theorem 14.3, auxiliary) Fenchel biconjugate inequality: if f is proper, then (f*)* ≤ f.

theorem section14_fenchelConjugate_triconjugate_eq_of_proper {E₁ : Type u_2} {F₁ : Type u_3} [AddCommGroup E₁] [Module ℝ E₁] [AddCommGroup F₁] [Module ℝ F₁] (p : E₁ →ₗ[ℝ] F₁ →ₗ[ℝ] ℝ) {f : E₁ → EReal} (hf : ProperERealFunction f) (hdom : ∃ (y0 : F₁), fenchelConjugateBilin p f y0 < ⊤) : fenchelConjugateBilin p (fenchelConjugateBilin p.flip (fenchelConjugateBilin p f)) = fenchelConjugateBilin p f

(Theorem 14.3, auxiliary) The Fenchel triconjugate with respect to evaluation satisfies ((f*)*)* = f* for a proper function f.

theorem section14_properConvex_fenchelBiconjugate_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; ProperConvexERealFunction (fenchelConjugateBilin p.flip (fenchelConjugateBilin p k))

(Theorem 14.3, auxiliary) The Fenchel biconjugate of the positively homogeneous hull is a proper convex function.