theorem supremumInnerSub_eq_fenchelConjugate_fExt {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → ℝ} : have fExt := fun (x : Fin n → ℝ) => ↑(f x) + indicatorFunction S x; ∀ (z : Fin n → ℝ), supremumInnerSub S (fun (x : ↑S) => ↑(f ↑x)) z = fenchelConjugate n fExt z

The restricted supremum supremumInnerSub matches the Fenchel conjugate of the +∞ extension.

theorem supremumInnerSub_ne_top_and_ne_bot_of_continuousOn_closed_bounded {n : ℕ} {S : Set (Fin n → ℝ)} (hS_ne : S.Nonempty) (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) (z : Fin n → ℝ) : supremumInnerSub S (fun (x : ↑S) => ↑(f ↑x)) z ≠ ⊤ ∧ supremumInnerSub S (fun (x : ↑S) => ↑(f ↑x)) z ≠ ⊥

Under the compactness hypotheses, supremumInnerSub is finite everywhere.

theorem clConv_mono {n : ℕ} {f₁ f₂ : (Fin n → ℝ) → EReal} (h : f₁ ≤ f₂) : clConv n f₁ ≤ clConv n f₂

clConv is monotone with respect to pointwise order.

theorem clConv_fExt_eq_convexHullFunction_fExt_of_closedConvexHull {n : ℕ} {S : Set (Fin n → ℝ)} (hS_ne : S.Nonempty) (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : have fExt := fun (x : Fin n → ℝ) => ↑(f x) + indicatorFunction S x; clConv n fExt = convexHullFunction fExt

For compact S and continuous f, the biconjugate envelope coincides with the convex hull function of the +∞ extension.

theorem supremumInnerSub_finite_and_fenchelConjugate_eq_convexHullFunction_of_continuousOn_closed_bounded {n : ℕ} {S : Set (Fin n → ℝ)} (hS_ne : S.Nonempty) (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → ℝ) → ℝ} (hf : ContinuousOn f S) : have fExt := fun (x : Fin n → ℝ) => ↑(f x) + indicatorFunction S x; have h := fun (z : Fin n → ℝ) => supremumInnerSub S (fun (x : ↑S) => ↑(f ↑x)) z; (∀ (z : Fin n → ℝ), h z ≠ ⊤ ∧ h z ≠ ⊥) ∧ fenchelConjugate n h = convexHullFunction fExt

Proposition 17.2.3 (Finiteness of h and identification of its conjugate), LaTeX label prop:h_conj.

Assume the hypotheses of Corollary 17.2.1: S is a nonempty closed bounded subset of ℝⁿ, f is continuous on S, and we extend f by f(x) = +∞ outside S.

Then the function h from Definition 17.2.2 is finite everywhere (hence continuous everywhere). Moreover, using Theorem 12.2, the conjugate h^* equals conv f (here: convexHullFunction applied to the extension).

structure HalfspaceRep (n : ℕ) : Type

Definition 17.2.4 (Half-space representation), LaTeX label def:halfspace.

A closed half-space H ⊆ ℝⁿ can be represented by a pair (x^*, μ^*) ∈ ℝ^{n+1} with x^* ≠ 0, as

H = {x ∈ ℝⁿ | ⟪x, x^*⟫ ≤ μ^*}.

In Fin n → ℝ, the inner product ⟪x, x^*⟫ is x ⬝ᵥ x^*.

• xStar : Fin n → ℝ
• muStar : ℝ
• hxStar : self.xStar ≠ 0

def HalfspaceRep.set {n : ℕ} (r : HalfspaceRep n) : Set (Fin n → ℝ)

The closed half-space represented by r.

Equations

• r.set = {x : Fin n → ℝ | x ⬝ᵥ r.xStar ≤ r.muStar}

def intersectionOfHalfspaces {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) : Set (Fin n → ℝ)

Definition 17.2.5 (Intersection of half-spaces), LaTeX label def:C.

Let S* ⊆ ℝ^{n+1} be nonempty. Define the closed convex set

C = {x ∈ ℝⁿ | ∀ (x*, μ*) ∈ S*, ⟪x, x*⟫ ≤ μ*}.

In this formalization, we model ℝⁿ as Fin n → ℝ and ℝ^{n+1} as (Fin n → ℝ) × ℝ. The inner product ⟪x, x*⟫ is x ⬝ᵥ x*.

Equations

• intersectionOfHalfspaces Sstar = {x : Fin n → ℝ | ∀ p ∈ Sstar, x ⬝ᵥ p.1 ≤ p.2}

theorem convex_intersectionOfHalfspaces {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) : Convex ℝ (intersectionOfHalfspaces Sstar)

Definition 17.2.5 (Intersection of half-spaces), LaTeX label def:C: the set intersectionOfHalfspaces S* is convex.

theorem isClosed_intersectionOfHalfspaces {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) : IsClosed (intersectionOfHalfspaces Sstar)

Definition 17.2.5 (Intersection of half-spaces), LaTeX label def:C: the set intersectionOfHalfspaces S* is closed.

theorem halfspaceRep_set_superset_iff_forall_dot_le {n : ℕ} (C : Set (Fin n → ℝ)) (r : HalfspaceRep n) : r.set ⊇ C ↔ ∀ x ∈ C, x ⬝ᵥ r.xStar ≤ r.muStar

Containment in a half-space is equivalent to a pointwise dot-product bound.

theorem dotProduct_comm_bridge_for_supportFunction {n : ℕ} (xStar x : Fin n → ℝ) : xStar ⬝ᵥ x = x ⬝ᵥ xStar

Swap the dot-product order to match the ⬝ᵥ notation.

theorem supportFunction_le_iff_forall_dot_le {n : ℕ} (C : Set (Fin n → ℝ)) (r : HalfspaceRep n) (hC : C.Nonempty) (hbd : BddAbove {t : ℝ | ∃ y ∈ C, t = r.xStar ⬝ᵥ y}) : supportFunction C r.xStar ≤ r.muStar ↔ ∀ x ∈ C, r.xStar ⬝ᵥ x ≤ r.muStar

A support-function bound is equivalent to a pointwise dot-product bound.

theorem halfspaceRep_set_superset_iff_supportFunction_le {n : ℕ} (C : Set (Fin n → ℝ)) (r : HalfspaceRep n) (hC : C.Nonempty) (hbd : BddAbove {t : ℝ | ∃ y ∈ C, t = r.xStar ⬝ᵥ y}) : r.set ⊇ C ↔ supportFunction C r.xStar ≤ r.muStar

Lemma 17.2.6 (Containment characterized by the support function), LaTeX label lem:containment_support.

Let C ⊆ ℝⁿ and let (x^*, μ^*) ∈ ℝ^{n+1} with x^* ≠ 0. Set H = {x ∈ ℝⁿ | ⟪x, x^*⟫ ≤ μ^*}. Then H ⊇ C if and only if μ^* ≥ sup_{x ∈ C} ⟪x, x^*⟫ =: supp(x^*, C).

In this formalization, H is r.set for r : HalfspaceRep n, and the support function is supportFunction C r.xStar (up to symmetry of the dot product).

def verticalVector (n : ℕ) : (Fin n → ℝ) × ℝ

Definition 17.2.7 (The cone K and the function f generated by S*), LaTeX label def:Kf.

Let S* ⊆ ℝ^{n+1} be nonempty and consider the “vertical” vector (0, 1) ∈ ℝ^{n+1}. Set D := S* ∪ {(0, 1)} and let K ⊆ ℝ^{n+1} be the convex cone generated by D. Define f : ℝⁿ → ℝ ∪ {+∞} by

f(x*) = inf { μ* ∈ ℝ | (x*, μ*) ∈ K }.

In this formalization, we model ℝⁿ as Fin n → ℝ and ℝ^{n+1} as (Fin n → ℝ) × ℝ, and we take the codomain ℝ ∪ {+∞} to be WithTop ℝ.

Equations

• verticalVector n = (0, 1)

def adjoinVertical {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) : Set ((Fin n → ℝ) × ℝ)

The set D := S* ∪ {(0, 1)} obtained by adjoining the vertical vector to S*.

Equations

• adjoinVertical Sstar = Sstar ∪ {verticalVector n}

def coneK {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) : Set ((Fin n → ℝ) × ℝ)

The convex cone K generated by D = S* ∪ {(0, 1)} (as a subset of ℝ^{n+1}).

Equations

• coneK Sstar = Set.insert 0 ↑(ConvexCone.hull ℝ (adjoinVertical Sstar))

noncomputable def infMuInCone {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (xStar : Fin n → ℝ) : WithTop ℝ

The function f(x*) = inf {μ* | (x*, μ*) ∈ K} with values in ℝ ∪ {+∞}.

Equations

• infMuInCone Sstar xStar = sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (xStar, μ) ∈ coneK Sstar})

theorem infMuInCone_embed_ne_bot {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (xStar : Fin n → ℝ) : (match infMuInCone Sstar xStar with | some μ => ↑μ | none => ⊤) ≠ ⊥

The infMuInCone-based embedding into EReal never hits ⊥.

theorem epigraph_convexFunctionClosure_eq_closure_epigraph_of_infMuInCone {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) : have f := fun (xStar : Fin n → ℝ) => match infMuInCone Sstar xStar with | some μ => ↑μ | none => ⊤; epigraph Set.univ (convexFunctionClosure f) = closure (epigraph Set.univ f)

The epigraph of the closure of infMuInCone equals the closure of its epigraph.

theorem coneK_subset_epigraph_supportFunctionEReal {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) : have C := intersectionOfHalfspaces Sstar; coneK Sstar ⊆ epigraph Set.univ (supportFunctionEReal C)

The cone coneK is contained in the epigraph of the support function of C.

theorem exists_mu_mem_coneK_lt_of_infMuInCone_lt {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) {xStar : Fin n → ℝ} {a : ℝ} (h : infMuInCone Sstar xStar < ↑a) : ∃ μ < a, (xStar, μ) ∈ coneK Sstar

Approximate the infimum in infMuInCone by a point in coneK.

theorem mem_coneK_add_vertical {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) {xStar : Fin n → ℝ} {μ t : ℝ} (hp : (xStar, μ) ∈ coneK Sstar) (ht : 0 ≤ t) : (xStar, μ + t) ∈ coneK Sstar

Adding a nonnegative multiple of the vertical vector keeps points in coneK.

theorem smul_mem_coneK {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) {t : ℝ} (ht : 0 < t) {p : (Fin n → ℝ) × ℝ} (hp : p ∈ coneK Sstar) : t • p ∈ coneK Sstar

Positive scaling preserves membership in coneK.

theorem convex_coneK {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) : Convex ℝ (coneK Sstar)

The cone coneK is convex.

theorem mem_epigraph_infMuInCone_imp_mem_closure_coneK {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) : have f := fun (xStar : Fin n → ℝ) => match infMuInCone Sstar xStar with | some μ => ↑μ | none => ⊤; epigraph Set.univ f ⊆ closure (coneK Sstar)

Points in the epigraph of the infMuInCone embedding lie in the closure of coneK.

theorem coneK_subset_epigraph_infMuInCone {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) : have f := fun (xStar : Fin n → ℝ) => match infMuInCone Sstar xStar with | some μ => ↑μ | none => ⊤; coneK Sstar ⊆ epigraph Set.univ f

Points of coneK lie in the epigraph of the infMuInCone embedding.

theorem closure_coneK_subset_epigraph_supportFunctionEReal {n : ℕ} (Sstar : Set ((Fin n → ℝ) × ℝ)) (hC_ne : intersectionOfHalfspaces Sstar ≠ ∅) : have C := intersectionOfHalfspaces Sstar; closure (coneK Sstar) ⊆ epigraph Set.univ (supportFunctionEReal C)

The closure of coneK lies in the epigraph of the support function of C.