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

Equations

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

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

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

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

theorem section14_le_zero_on_dom_of_mem_recessionCone_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ProperERealFunction f) {yStar : Module.Dual ℝ E} (hy : yStar ∈ recessionConeEReal (fenchelConjugateBilin LinearMap.applyₗ f)) (hxStar0 : ∃ (xStar0 : Module.Dual ℝ E), fenchelConjugateBilin LinearMap.applyₗ f xStar0 < ⊤) (x : E) : x ∈ erealDom f → yStar x ≤ 0

If y★ is in the recession cone of f* and f* is finite somewhere, then y★ is nonpositive on erealDom f.

theorem polar_coneGenerated_dom_eq_recessionCone_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hdom : ∃ (xStar0 : Module.Dual ℝ E), fenchelConjugateBilin LinearMap.applyₗ f xStar0 < ⊤) : polarCone ↑(ConvexCone.hull ℝ (erealDom f)) = recessionConeEReal (fenchelConjugateBilin LinearMap.applyₗ f)

Theorem 14.2. Let f be a proper convex function. The polar of the convex cone generated by dom f is the recession cone of the Fenchel conjugate f*. Dually, if f is closed, the polar of the recession cone of f is the closure of the convex cone generated by dom f*.

def section14_polarConeConvexCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] (K : Set E) : ConvexCone ℝ (Module.Dual ℝ E)

The polar cone of a set, packaged as a ConvexCone, so that we can use ConvexCone.hull minimality arguments.

Equations

• section14_polarConeConvexCone K = { carrier := polarCone K, smul_mem' := ⋯, add_mem' := ⋯ }

theorem section14_mem_polar_recessionCone_of_mem_dom_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ProperERealFunction f) {xStar : Module.Dual ℝ E} (hxStar : xStar ∈ erealDom (fenchelConjugateBilin LinearMap.applyₗ f)) : xStar ∈ polarCone (recessionConeEReal f)

If x★ is in the effective domain of f*, then x★ lies in the polar cone of the recession cone of f.

theorem section14_closure_coneHull_dom_fenchelConjugate_subset_polar_recessionCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {f : E → EReal} (hf : ProperConvexERealFunction f) : closure ↑(ConvexCone.hull ℝ (erealDom (fenchelConjugateBilin LinearMap.applyₗ f))) ⊆ polarCone (recessionConeEReal f)

The closed conic hull of dom f* is contained in the polar of the recession cone of f.

theorem section14_exists_eval_of_continuousLinearMap_dualWeak {E : Type u_1} [AddCommGroup E] [Module ℝ E] (ℓ : Module.Dual ℝ E →L[ℝ] ℝ) : ∃ (y : E), ∀ (xStar : Module.Dual ℝ E), ℓ xStar = xStar y

Any continuous linear functional on Module.Dual ℝ E equipped with the weak topology induced by evaluation is itself an evaluation at some y : E.

theorem section14_exists_eval_sep_of_not_mem_closure_coneHull_dom_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {xStar : Module.Dual ℝ E} (hDom : (erealDom (fenchelConjugateBilin LinearMap.applyₗ f)).Nonempty) (hxStar : xStar ∉ closure ↑(ConvexCone.hull ℝ (erealDom (fenchelConjugateBilin LinearMap.applyₗ f)))) : ∃ (y : E), (∀ z ∈ closure ↑(ConvexCone.hull ℝ (erealDom (fenchelConjugateBilin LinearMap.applyₗ f))), z y ≤ 0) ∧ 0 < xStar y

If x★ is not in the (weak) closure of the conic hull of dom f*, then one can separate it from that cone by evaluation at some y : E.

theorem section14_exists_affine_minorant_strict_of_lt {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) {x0 : E} {μ0 : ℝ} (hμ0 : ↑μ0 < f x0) : ∃ (xStar : Module.Dual ℝ E) (β : ℝ), (∀ (x : E), ↑(xStar x - β) ≤ f x) ∧ μ0 < xStar x0 - β ∧ fenchelConjugateBilin LinearMap.applyₗ f xStar < ⊤

A Hahn–Banach separation gadget for a proper convex lower semicontinuous function: given a point (x0, μ0) strictly below the epigraph of f, produce a continuous affine minorant x ↦ x★ x - β that lies below f everywhere and is strictly above μ0 at x0. In particular, the Fenchel conjugate is finite at x★.

theorem section14_exists_mem_dom_fenchelConjugate_of_properConvex_lsc {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) : (erealDom (fenchelConjugateBilin LinearMap.applyₗ f)).Nonempty

For a proper convex lower semicontinuous function, the Fenchel conjugate is finite somewhere.

theorem section14_mem_recessionConeEReal_of_forall_mem_dom_fenchelConjugate_le_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) {y : E} (hy : ∀ xStar ∈ erealDom (fenchelConjugateBilin LinearMap.applyₗ f), xStar y ≤ 0) : y ∈ recessionConeEReal f

If y is nonpositive on dom f* and f is proper convex and closed, then y is a recession direction of f.

theorem section14_polar_recessionCone_subset_closure_coneHull_dom_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) : polarCone (recessionConeEReal f) ⊆ closure ↑(ConvexCone.hull ℝ (erealDom (fenchelConjugateBilin LinearMap.applyₗ f)))

If x★ is in polarCone (recessionConeEReal f), then x★ lies in the weak closure of the conic hull of dom f* (dual part of Theorem 14.2).

theorem polar_recessionCone_eq_closure_coneGenerated_dom_fenchelConjugate {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {f : E → EReal} (hf : ProperConvexERealFunction f) (hf_closed : LowerSemicontinuous f) : polarCone (recessionConeEReal f) = closure ↑(ConvexCone.hull ℝ (erealDom (fenchelConjugateBilin LinearMap.applyₗ f)))

Theorem 14.2 (dual statement). If f is closed, then the polar of the recession cone of f is the closure of the convex cone generated by dom f*.

theorem section14_mem_dual_flip_eval_iff_forall_le_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] (S : Set (Module.Dual ℝ E)) (x : E) : x ∈ ↑(PointedCone.dual (-LinearMap.applyₗ).flip S) ↔ ∀ φ ∈ S, φ x ≤ 0

Membership in a dual cone with respect to the flipped evaluation pairing is exactly a pointwise nonpositivity condition.

theorem section14_recessionCone_subset_polar_barrierCone {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hCne : C.Nonempty) : C.recessionCone ⊆ ↑(PointedCone.dual (-LinearMap.applyₗ).flip C.barrierCone)

Recession directions lie in the polar (with respect to flipped evaluation) of the barrier cone.