theorem f0_eq_zero_of_closedProperConvex_posHomogeneous {n : ℕ} {p : ℝ} {f : (Fin n → ℝ) → EReal} (hp : 1 < p) (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) (hf_hom : PositivelyHomogeneousOfDegree p f) : f 0 = 0

A closed proper convex positively homogeneous function vanishes at the origin.

theorem nonneg_of_isGaugeLike_f0_eq_zero {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : IsGaugeLike f) (h0 : f 0 = 0) (x : Fin n → ℝ) : 0 ≤ f x

Gauge-like functions with f 0 = 0 are nonnegative.

theorem exists_closedGauge_rpow_representation_of_posHomogeneous {n : ℕ} {p : ℝ} {f : (Fin n → ℝ) → EReal} (hp : 1 < p) (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) (hf_hom : PositivelyHomogeneousOfDegree p f) : ∃ (k : (Fin n → ℝ) → EReal), IsClosedGauge k ∧ f = fun (x : Fin n → ℝ) => ↑(1 / p) * phiPow p (k x)

A positively homogeneous closed proper convex function has a closed-gauge power representation.

theorem posHomogeneous_of_exists_closedGauge_scaled {n : ℕ} {p : ℝ} {f : (Fin n → ℝ) → EReal} {φ : EReal → EReal} (hφ : ∀ {z : EReal} {t : ℝ}, 0 ≤ z → 0 < t → φ (↑t * z) = ↑(t.rpow p) * φ z) : (∃ (k : (Fin n → ℝ) → EReal), IsClosedGauge k ∧ f = fun (x : Fin n → ℝ) => ↑(1 / p) * φ (k x)) → PositivelyHomogeneousOfDegree p f

If a profile φ scales on nonnegative inputs, then (1/p) * φ ∘ k is positively homogeneous of degree p.

theorem fenchelConjugate_rpow_closedGauge_formula_and_posHomogeneous {n : ℕ} {p q : ℝ} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) {f k : (Fin n → ℝ) → EReal} (hk : IsClosedGauge k) (hfk : f = fun (x : Fin n → ℝ) => ↑(1 / p) * phiPow p (k x)) : PositivelyHomogeneousOfDegree q (fenchelConjugate n f) ∧ ∀ (xStar : Fin n → ℝ), fenchelConjugate n f xStar = ↑(1 / q) * phiPow q (polarGauge k xStar)

The conjugate of a closed-gauge power profile is a power profile with conjugate exponent.

theorem section15_abs_combo_le (a b t : ℝ) (ht0 : 0 ≤ t) (ht1 : 0 ≤ 1 - t) : |(1 - t) * a + t * b| ≤ (1 - t) * |a| + t * |b|

Triangle inequality for affine combinations.

theorem section15_abs_rpow_combo_le {p : ℝ} (hp : 1 ≤ p) (a b t : ℝ) (ht0 : 0 ≤ t) (ht1 : 0 ≤ 1 - t) : |(1 - t) * a + t * b|.rpow p ≤ (1 - t) * |a|.rpow p + t * |b|.rpow p

Convexity inequality for |·|^p with p ≥ 1.

theorem section15_convexFunction_sum_abs_rpow_div {n : ℕ} {p : ℝ} (hp : 1 < p) : ConvexFunction fun (x : Fin n → ℝ) => ↑(1 / p) * ↑(∑ i : Fin n, |x i|.rpow p)

Convexity of the (1/p) * ∑ |xᵢ|^p function.

theorem section15_lowerSemicontinuous_sum_abs_rpow_div {n : ℕ} {p : ℝ} (hp : 1 < p) : LowerSemicontinuous fun (x : Fin n → ℝ) => ↑(1 / p) * ↑(∑ i : Fin n, |x i|.rpow p)

Lower semicontinuity of the (1/p) * ∑ |xᵢ|^p function.

theorem section15_posHomogeneous_sum_abs_rpow_div {n : ℕ} {p : ℝ} : PositivelyHomogeneousOfDegree p fun (x : Fin n → ℝ) => ↑(1 / p) * ↑(∑ i : Fin n, |x i|.rpow p)

Positive homogeneity of the (1/p) * ∑ |xᵢ|^p function.

theorem sum_abs_rpow_div_closedProperConvex_posHomogeneous {n : ℕ} {p : ℝ} (hp : 1 < p) : have f := fun (x : Fin n → ℝ) => ↑(1 / p) * ↑(∑ i : Fin n, |x i|.rpow p); ClosedConvexFunction f ∧ ProperConvexFunctionOn Set.univ f ∧ PositivelyHomogeneousOfDegree p f

Text 15.0.22: Let 1 < p < ∞ and define f : ℝⁿ → ℝ by f x = (1/p) * (|ξ₁|^p + ... + |ξₙ|^p) for x = (ξ₁, ..., ξₙ). Then f is a closed proper convex function and is positively homogeneous of degree p.

In this development, ℝⁿ is Fin n → ℝ, f is treated as EReal-valued by coercion, closedness is ClosedConvexFunction, properness is ProperConvexFunctionOn univ, and |ξᵢ|^p is Real.rpow |ξᵢ| p.

theorem section15_holderConjugate_of_hpq {p q : ℝ} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : p.HolderConjugate q

Conjugate-exponent data from 1 / p + 1 / q = 1.

theorem section15_young_term_bound {p q a t : ℝ} (hpq : p.HolderConjugate q) : a * t - 1 / p * |t|.rpow p ≤ 1 / q * |a|.rpow q

Young's inequality in a rearranged single-term form.

theorem section15_dot_sub_sum_abs_rpow_le {n : ℕ} {p q : ℝ} (hpq : p.HolderConjugate q) (xStar x : Fin n → ℝ) : ∑ i : Fin n, x i * xStar i - 1 / p * ∑ i : Fin n, |x i|.rpow p ≤ 1 / q * ∑ i : Fin n, |xStar i|.rpow q

Coordinatewise Young bounds summed over Fin n.

theorem section15_abs_sign_mul_rpow_eq {r a : ℝ} (ha : 0 < a) : |r.sign| * |r|.rpow a = |r|.rpow a

Multiplying by |Real.sign r| does not change |r|^a when a > 0.

theorem section15_eval_at_explicit_maximizer {n : ℕ} {p q : ℝ} (hpq : p.HolderConjugate q) (xStar : Fin n → ℝ) : have x0 := fun (i : Fin n) => (xStar i).sign * |xStar i|.rpow (q - 1); ↑(x0 ⬝ᵥ xStar) - ↑(1 / p) * ↑(∑ i : Fin n, |x0 i|.rpow p) = ↑(1 / q) * ↑(∑ i : Fin n, |xStar i|.rpow q)

Evaluation of the Fenchel expression at the explicit maximizer.

theorem fenchelConjugate_sum_abs_rpow_div_eq_sum_abs_rpow_div {n : ℕ} {p q : ℝ} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : have f := fun (x : Fin n → ℝ) => ↑(1 / p) * ↑(∑ i : Fin n, |x i|.rpow p); fenchelConjugate n f = fun (xStar : Fin n → ℝ) => ↑(1 / q) * ↑(∑ i : Fin n, |xStar i|.rpow q)

Text 15.0.23: Let 1 < p < ∞ and define f : ℝⁿ → ℝ by f x = (1/p) * (|ξ₁|^p + ... + |ξₙ|^p) for x = (ξ₁, ..., ξₙ). Its conjugate is f^*(x^*) = (1/q) * (|ξ₁^*|^q + ... + |ξₙ^*|^q), where 1/p + 1/q = 1.

In this development, ℝⁿ is Fin n → ℝ, |ξᵢ|^p is Real.rpow |ξᵢ| p, and the conjugate is modeled as fenchelConjugate n f.

theorem closedProperConvex_posHomogeneous_degree_iff_exists_closedGauge_rpow {n : ℕ} {p q : ℝ} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) {f : (Fin n → ℝ) → EReal} (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : have φp := fun (z : EReal) => if z = ⊥ then 0 else if z = ⊤ then ⊤ else ↑((max z.toReal 0).rpow p); have φq := fun (z : EReal) => if z = ⊥ then 0 else if z = ⊤ then ⊤ else ↑((max z.toReal 0).rpow q); (PositivelyHomogeneousOfDegree p f ↔ ∃ (k : (Fin n → ℝ) → EReal), IsClosedGauge k ∧ f = fun (x : Fin n → ℝ) => ↑(1 / p) * φp (k x)) ∧ ∀ (k : (Fin n → ℝ) → EReal), IsClosedGauge k → (f = fun (x : Fin n → ℝ) => ↑(1 / p) * φp (k x)) → PositivelyHomogeneousOfDegree q (fenchelConjugate n f) ∧ ∀ (xStar : Fin n → ℝ), fenchelConjugate n f xStar = ↑(1 / q) * φq (polarGauge k xStar)

Corollary 15.3.1: Let 1 < p < ∞ and let q be its conjugate exponent, 1/p + 1/q = 1. For a closed proper convex function f, positive homogeneity of degree p is equivalent to the existence of a closed gauge k such that f(x) = (1/p) * k(x)^p.

In this case, the Fenchel conjugate f^* (modeled as fenchelConjugate n f) is positively homogeneous of degree q and satisfies f^*(x^*) = (1/q) * (k^∘(x^*))^q, where k^∘ is the polar gauge (modeled as polarGauge k).