theorem obverseConvex_le_zero_iff_recessionFunction_le_one {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) (x : Fin n → ℝ) : obverseConvex f x ≤ 0 ↔ recessionFunction f x ≤ 1

The obverse at 0 equals the recession function sublevel.

theorem epigraph_obverseConvex_eq_sublevel_one {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 ⊤; epigraph Set.univ g = {p : (Fin n → ℝ) × ℝ | h p.2 p.1 ≤ 1}

Text 15.0.33: Let f : ℝⁿ → [0, +∞] and let g be the function defined by the obverse formula g x = inf {λ > 0 | f_λ x ≤ 1}, where f_λ x := λ * f (x / λ) for λ > 0. Then the epigraph of g admits the geometric representation

epi g = {(x, λ) | h (λ, x) ≤ 1},

where

h (λ, x) = f_λ x if λ > 0, h (0, x) = (f₀⁺) x (the recession function), and h (λ, x) = +∞ if λ < 0.

theorem h_at_one_simp {n : ℕ} (f : (Fin n → ℝ) → EReal) : have h := fun (t : ℝ) (x : Fin n → ℝ) => if 0 < t then ↑t * f (t⁻¹ • x) else if t = 0 then recessionFunction f x else ⊤; ∀ (x : Fin n → ℝ), h 1 x = f x

At λ = 1, the auxiliary function h agrees with f.

theorem image_P_slice_lambda_one_eq_epigraph_f {n : ℕ} (f : (Fin n → ℝ) → EReal) : 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}; (fun (q : (ℝ × (Fin n → ℝ)) × ℝ) => (q.1.2, q.2)) '' (P ∩ {q : (ℝ × (Fin n → ℝ)) × ℝ | q.1.1 = 1}) = epigraph Set.univ f

The λ = 1 slice of P = epi h projects to epi f.

theorem image_P_slice_mu_one_eq_sublevel_h {n : ℕ} (f : (Fin n → ℝ) → EReal) : 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}; (fun (q : (ℝ × (Fin n → ℝ)) × ℝ) => (q.1.2, q.1.1)) '' (P ∩ {q : (ℝ × (Fin n → ℝ)) × ℝ | q.2 = 1}) = {p : (Fin n → ℝ) × ℝ | h p.2 p.1 ≤ 1}

The μ = 1 slice of P = epi h projects to the h ≤ 1 sublevel set.

theorem sublevel_h_one_eq_epigraph_obverseConvex {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 ⊤; {p : (Fin n → ℝ) × ℝ | h p.2 p.1 ≤ 1} = epigraph Set.univ g

The sublevel set h ≤ 1 is the epigraph of obverseConvex f.

theorem epigraph_h_slice_hyperplanes_correspond {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}; (fun (q : (ℝ × (Fin n → ℝ)) × ℝ) => (q.1.2, q.2)) '' (P ∩ {q : (ℝ × (Fin n → ℝ)) × ℝ | q.1.1 = 1}) = epigraph Set.univ f ∧ (fun (q : (ℝ × (Fin n → ℝ)) × ℝ) => (q.1.2, q.1.1)) '' (P ∩ {q : (ℝ × (Fin n → ℝ)) × ℝ | q.2 = 1}) = epigraph Set.univ g

Text 15.0.34: Let P = epi h ⊆ ℝ^{n+2} be the (closed convex) cone given as the epigraph of the function h (λ, x) from Text 15.0.33; it is the smallest closed convex cone containing the points (1, x, μ) with μ ≥ f x.

Then the slice of P by the hyperplane λ = 1 corresponds to the epigraph epi f, and the slice by the hyperplane μ = 1 corresponds to the epigraph epi g of the obverse g.

theorem recessionFunction_nonneg_of_nonneg_zero {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf0 : f 0 = 0) (y : Fin n → ℝ) : 0 ≤ recessionFunction f y

The recession function is nonnegative when f ≥ 0 and f 0 = 0.

theorem recessionFunction_posHom_of_nonneg_closedConvex_zero {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) : PositivelyHomogeneous (recessionFunction f)

The recession function is positively homogeneous under closedness and nonnegativity.

theorem h_div_mu_le_one_of_h_le_mu {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 ⊤; ∀ {lam μ : ℝ} {x : Fin n → ℝ}, 0 < μ → h lam x ≤ ↑μ → h (lam / μ) (μ⁻¹ • x) ≤ 1

Normalizing the h-inequality at positive μ.

theorem mem_P_imp_lam_nonneg {n : ℕ} {f : (Fin n → ℝ) → EReal} : 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}; ∀ {q : (ℝ × (Fin n → ℝ)) × ℝ}, q ∈ P → 0 ≤ q.1.1

Points in P have nonnegative λ.

theorem h_nonneg_of_lam_nonneg {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (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 ⊤; ∀ {lam : ℝ} {x : Fin n → ℝ}, 0 ≤ lam → 0 ≤ h lam x

The auxiliary function h is nonnegative when λ ≥ 0.

theorem dotProduct_le_mu_add_lam_mul_fStar_toReal_of_mem_P {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_nonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) (hf_closed : ClosedConvexFunction f) (hf0 : f 0 = 0) : have fStar := fenchelConjugate n f; have C := effectiveDomain Set.univ fStar; 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}; ∀ {q : (ℝ × (Fin n → ℝ)) × ℝ}, q ∈ P → ∀ y ∈ C, q.1.2 ⬝ᵥ y ≤ q.2 + q.1.1 * (fStar y).toReal

Dot-product bound for points in the epigraph set P.

theorem isClosed_P {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}; IsClosed P

The epigraph set P is closed.