theorem P_eq_closure_P_inter_mu_pos {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) : have h := fun (t : ℝ) (x : Fin n → ℝ) => if 0 < t then ↑t * f (t⁻¹ • x) else if t = 0 then recessionFunction f x else ⊤; have P := {q : (ℝ × (Fin n → ℝ)) × ℝ | h q.1.1 q.1.2 ≤ ↑q.2}; P = closure (P ∩ {q : (ℝ × (Fin n → ℝ)) × ℝ | 0 < q.2})

The cone P is the closure of its μ > 0 slice.

theorem P_subset_any_closed_convexCone_containing_obverse_points {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) : have g := obverseConvex f; have h := fun (t : ℝ) (x : Fin n → ℝ) => if 0 < t then ↑t * f (t⁻¹ • x) else if t = 0 then recessionFunction f x else ⊤; have P := {q : (ℝ × (Fin n → ℝ)) × ℝ | h q.1.1 q.1.2 ≤ ↑q.2}; ∀ (K : ConvexCone ℝ ((ℝ × (Fin n → ℝ)) × ℝ)), IsClosed ↑K → (∀ (lam : ℝ) (x : Fin n → ℝ), g x ≤ ↑lam → ((lam, x), 1) ∈ ↑K) → P ⊆ ↑K

Any closed convex cone containing the obverse points contains P.

theorem epigraph_h_min_closedConvexCone_containing_obverse_points {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) : have g := obverseConvex f; have h := fun (t : ℝ) (x : Fin n → ℝ) => if 0 < t then ↑t * f (t⁻¹ • x) else if t = 0 then recessionFunction f x else ⊤; have P := {q : (ℝ × (Fin n → ℝ)) × ℝ | h q.1.1 q.1.2 ≤ ↑q.2}; P = closure (P ∩ {q : (ℝ × (Fin n → ℝ)) × ℝ | 0 < q.2}) ∧ ∀ (K : ConvexCone ℝ ((ℝ × (Fin n → ℝ)) × ℝ)), IsClosed ↑K → (∀ (lam : ℝ) (x : Fin n → ℝ), g x ≤ ↑lam → ((lam, x), 1) ∈ ↑K) → P ⊆ ↑K

Text 15.0.35: Let P ⊆ ℝ^{n+2} be the closed convex cone P = epi h from Text 15.0.34, where h is built from f as in Text 15.0.33 and g is the obverse of f.

Assuming f ≥ 0, the set P is the closure of its intersection with the open half-space μ > 0. Moreover, P is the smallest closed convex cone containing all points (λ, x, 1) such that λ ≥ g(x). Thus f and g determine the same closed convex cone in ℝ^{n+2}, with the roles of λ and μ reversed when passing between the two descriptions.

theorem polarConvex_nonneg {n : ℕ} (f : (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : 0 ≤ polarConvex f xStar

The polar convex function is nonnegative.

theorem polarConvex_zero {n : ℕ} (f : (Fin n → ℝ) → EReal) : polarConvex f 0 = 0

The polar convex function vanishes at the origin.

def vertReflect {n : ℕ} (p : (Fin n → ℝ) × ℝ) : (Fin n → ℝ) × ℝ

Vertical reflection in the last coordinate.

Equations

• vertReflect p = (p.1, -p.2)

theorem vertReflect_involutive {n : ℕ} : Function.Involutive vertReflect

The vertical reflection is an involution.

def polarSetProd {n : ℕ} (C : Set ((Fin n → ℝ) × ℝ)) : Set ((Fin n → ℝ) × ℝ)

Product-space polar set using the dot-product-plus-scalar pairing.

Equations

• polarSetProd C = {y : (Fin n → ℝ) × ℝ | ∀ x ∈ C, x.1 ⬝ᵥ y.1 + x.2 * y.2 ≤ 1}

theorem polarSetProd_isClosed_and_convex {n : ℕ} (C : Set ((Fin n → ℝ) × ℝ)) : IsClosed (polarSetProd C) ∧ Convex ℝ (polarSetProd C)

polarSetProd is closed and convex as an intersection of closed halfspaces.

theorem polarSetProd_closure_eq {n : ℕ} (C : Set ((Fin n → ℝ) × ℝ)) : polarSetProd (closure C) = polarSetProd C

polarSetProd is unchanged by taking the closure of the set.

theorem polarSetProd_preimage_vertReflect {n : ℕ} (C : Set ((Fin n → ℝ) × ℝ)) : polarSetProd (vertReflect ⁻¹' C) = vertReflect ⁻¹' polarSetProd C

polarSetProd commutes with vertical reflection preimages.

theorem linearMap_eq_dotProduct_add_mul_prod {n : ℕ} (φ : (Fin n → ℝ) × ℝ →ₗ[ℝ] ℝ) (p : (Fin n → ℝ) × ℝ) : φ p = (p.1 ⬝ᵥ fun (i : Fin n) => φ (Pi.single i 1, 0)) + p.2 * φ (0, 1)

A linear functional on the product splits into a dot product and a scalar part.

theorem bipolar_dualSet_eq_polarSetProd_polarSetProd {n : ℕ} (C : Set ((Fin n → ℝ) × ℝ)) : {x : (Fin n → ℝ) × ℝ | ∀ φ ∈ polar C, φ x ≤ 1} = polarSetProd (polarSetProd C)

The dual bipolar set matches the polarSetProd bipolar.