theorem infimumRepresentation_posHomogeneousHull {n : ℕ} {h : (Fin n → ℝ) → EReal} (hh : ConvexFunctionOn Set.univ h) (hfinite : ∃ (x : Fin n → ℝ), h x ≠ ⊤) : have f := positivelyHomogeneousConvexFunctionGenerated h; (∀ (x : Fin n → ℝ), f x = sInf {z : EReal | ∃ (lam : ℝ), 0 ≤ lam ∧ z = rightScalarMultiple h lam x}) ∧ ∀ (x : Fin n → ℝ), x ≠ 0 ∨ h 0 < ⊤ → f x = sInf {z : EReal | ∃ (lam : ℝ), 0 < lam ∧ z = rightScalarMultiple h lam x}

Text 5.4.9 (Infimum representation of the positively homogeneous hull): Assume h is not identically +∞ and let f be the positively homogeneous convex function generated by h. Then f x = inf { (h λ)(x) | λ ≥ 0 } for all x. Moreover, λ = 0 may be omitted from the infimum if x ≠ 0 or if h(0) < +∞.

theorem convexFunctionOn_perspective_h {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) : ConvexFunctionOn Set.univ fun (y : Fin (n + 1) → ℝ) => if y 0 = 1 then f fun (i : Fin n) => y i.succ else ⊤

The perspective kernel is convex when f is convex.

theorem first_coord_inv_smul_eq_one {n : ℕ} {lam : ℝ} (hlam : 0 < lam) (y : Fin (n + 1) → ℝ) : (lam⁻¹ • y) 0 = 1 ↔ y 0 = lam

For positive lam, the first coordinate of lam⁻¹ • y equals 1 iff y 0 = lam.

theorem rightScalarMultiple_perspective_h_pos {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) {lam : ℝ} (hlam : 0 < lam) (y : Fin (n + 1) → ℝ) : rightScalarMultiple (fun (y : Fin (n + 1) → ℝ) => if y 0 = 1 then f fun (i : Fin n) => y i.succ else ⊤) lam y = if y 0 = lam then ↑lam * f (lam⁻¹ • fun (i : Fin n) => y i.succ) else ⊤

Positive right scalar multiples of the perspective kernel simplify.

theorem ereal_mul_ne_bot_of_pos' {t : ℝ} (ht : 0 < t) {x : EReal} (hx : x ≠ ⊥) : ↑t * x ≠ ⊥

A positive scalar multiple of a non-⊥ EReal is non-⊥.

theorem nonempty_epigraph_perspective_h {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : (epigraph Set.univ fun (y : Fin (n + 1) → ℝ) => if y 0 = 1 then f fun (i : Fin n) => y i.succ else ⊤).Nonempty

The perspective kernel has a nonempty epigraph when f is proper.

theorem perspective_posHomogeneous_convex {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : have g := fun (y : Fin (n + 1) → ℝ) => if 0 ≤ y 0 then rightScalarMultiple f (y 0) fun (i : Fin n) => y i.succ else ⊤; have h := fun (y : Fin (n + 1) → ℝ) => if y 0 = 1 then f fun (i : Fin n) => y i.succ else ⊤; ProperConvexFunctionOn Set.univ g ∧ PositivelyHomogeneous g ∧ g = positivelyHomogeneousConvexFunctionGenerated h

Text 5.4.9.1: Perspective as a positively homogeneous convex function. Let f be a proper convex function on ℝ^n. Define g(λ,x) = (f λ)(x) for λ ≥ 0 (with the closed perspective convention at λ = 0) and g(λ,x) = +∞ for λ < 0. Then g is proper, convex, and positively homogeneous on ℝ^{n+1}; moreover, g coincides with the positively homogeneous convex function generated by h(λ,x) = f(x) when λ = 1 and +∞ otherwise.

theorem properConvexFunctionOn_perspective_param {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) (x : Fin n → ℝ) : x ∈ effectiveDomain Set.univ f → ProperConvexFunctionOn {t : Fin 1 → ℝ | 0 ≤ t 0} fun (t : Fin 1 → ℝ) => rightScalarMultiple f (t 0) x

Text 5.4.9.1: For each fixed x ∈ dom f, the map λ ↦ (f λ)(x) is a proper convex function of λ on [0, ∞).

noncomputable def gaugeOfConvexSet {n : ℕ} (C : Set (Fin n → ℝ)) : (Fin n → ℝ) → ℝ

Text 5.4.10 (Gauge of a convex set): Let C ⊆ ℝ^n be a nonempty convex set. The gauge of C is the function gamma(·|C) : ℝ^n → [0,+∞] defined by gamma(x|C) = inf { lambda ≥ 0 | x ∈ lambda C }.

Equations

• gaugeOfConvexSet C x = sInf {r : ℝ | 0 ≤ r ∧ x ∈ (fun (y : Fin n → ℝ) => r • y) '' C}

theorem gaugeOfConvexSet_eq_gauge {n : ℕ} (C : Set (Fin n → ℝ)) : gaugeOfConvexSet C = gauge C

Text 5.4.10: The gauge of a convex set agrees with mathlib's gauge.

theorem properConvexFunctionOn_const {n : ℕ} (c : ℝ) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑c

A finite constant function is proper convex on Set.univ.

theorem convexFunctionOn_indicator_add_const {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (c : ℝ) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => indicatorFunction C x + ↑c

The indicator function plus a real constant is convex on Set.univ.

theorem indicatorFunction_image_smul_eq {n : ℕ} {C : Set (Fin n → ℝ)} {lam : ℝ} (hlam : lam ≠ 0) (x : Fin n → ℝ) : indicatorFunction ((fun (y : Fin n → ℝ) => lam • y) '' C) x = indicatorFunction C (lam⁻¹ • x)

The indicator of a scaled image is rewritten by inverse scaling when lam ≠ 0.

theorem rightScalarMultiple_indicator_add_one_pos {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCconv : Convex ℝ C) {lam : ℝ} (hlam : 0 < lam) (x : Fin n → ℝ) : rightScalarMultiple (fun (y : Fin n → ℝ) => indicatorFunction C y + 1) lam x = indicatorFunction ((fun (y : Fin n → ℝ) => lam • y) '' C) x + ↑lam

For positive lam, the right scalar multiple of indicatorFunction C + 1 is explicit.

theorem rightScalarMultiple_indicator_add_one_zero {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCconv : Convex ℝ C) (x : Fin n → ℝ) : rightScalarMultiple (fun (y : Fin n → ℝ) => indicatorFunction C y + 1) 0 x = indicatorFunction ((fun (y : Fin n → ℝ) => 0 • y) '' C) x + 0

For lam = 0, the right scalar multiple of indicatorFunction C + 1 is an indicator.

theorem rightScalarMultiple_indicator_add_one_nonneg {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCconv : Convex ℝ C) {lam : ℝ} (hlam : 0 ≤ lam) (x : Fin n → ℝ) : rightScalarMultiple (fun (y : Fin n → ℝ) => indicatorFunction C y + 1) lam x = indicatorFunction ((fun (y : Fin n → ℝ) => lam • y) '' C) x + ↑lam

Nonnegative scalars give the explicit indicator formula.