theorem fenchelConjugate_eq_monotoneConjugate_polarGauge_of_comp {n : ℕ} {f k : (Fin n → ℝ) → EReal} {g : EReal → EReal} (hk : IsClosedGauge k) (hfg : f = fun (x : Fin n → ℝ) => g (k x)) (hg_mono : Monotone g) (hg_top : g ⊤ = ⊤) (hζ : ∃ (ζ : ℝ), 0 < ζ ∧ g ↑ζ ≠ ⊤ ∧ g ↑ζ ≠ ⊥) : IsGaugeLike (fenchelConjugate n f) ∧ ∀ (xStar : Fin n → ℝ), fenchelConjugate n f xStar = monotoneConjugateERealNonneg g (polarGauge k xStar)

Theorem 15.3 (conjugate formula): If f(x) = g (k x) with k a closed gauge and g as above, then f* is gauge-like and satisfies f*(x⋆) = g⁺ (kᵒ x⋆), where g⁺ is monotoneConjugateERealNonneg g and kᵒ is the polar gauge polarGauge k.

def PositivelyHomogeneousOfDegree {n : ℕ} (p : ℝ) (f : (Fin n → ℝ) → EReal) : Prop

Text 15.0.21: Let p > 0. A function f : ℝⁿ → (-∞, +∞] is positively homogeneous of degree p if f (λ x) = λ^p f x for all x and all λ > 0.

In this development, ℝⁿ is Fin n → ℝ, (-∞, +∞] is EReal, and λ^p is Real.rpow λ p.

Equations

• PositivelyHomogeneousOfDegree p f = ∀ (x : Fin n → ℝ) (t : ℝ), 0 < t → f (t • x) = ↑(t.rpow p) * f x

theorem sublevel_eq_smul_sublevel_of_posHomogeneous {n : ℕ} {p : ℝ} {f : (Fin n → ℝ) → EReal} (hp : 0 < p) (hf_hom : PositivelyHomogeneousOfDegree p f) {αr βr : ℝ} (hα : 0 < αr) (hβ : 0 < βr) : have t := (αr / βr).rpow (1 / p); {x : Fin n → ℝ | f x ≤ ↑αr} = t • {x : Fin n → ℝ | f x ≤ ↑βr}

Sublevel sets scale under positive homogeneity.

noncomputable def phiPow (r : ℝ) : EReal → EReal

Power profile used in the rpow representation.

Equations

• phiPow r z = if z = ⊥ then 0 else if z = ⊤ then ⊤ else ↑((max z.toReal 0).rpow r)

theorem ereal_coe_mul_top_of_pos {t : ℝ} (ht : 0 < t) : ↑t * ⊤ = ⊤

Multiplying ⊤ by a positive real yields ⊤ in EReal.

theorem phiPow_mul_of_nonneg {r : ℝ} {z : EReal} {t : ℝ} (hz : 0 ≤ z) (ht : 0 < t) : phiPow r (↑t * z) = ↑(t.rpow r) * phiPow r z

The power profile scales on nonnegative inputs.

theorem phiPow_mono {r : ℝ} (hr : 0 ≤ r) : Monotone (phiPow r)

The power profile is monotone for nonnegative exponents.

theorem gPow_basic {p : ℝ} (hp : 1 < p) : (Monotone fun (z : EReal) => ↑(1 / p) * phiPow p z) ∧ (fun (z : EReal) => ↑(1 / p) * phiPow p z) ⊤ = ⊤ ∧ ∃ (ζ : ℝ), 0 < ζ ∧ (fun (z : EReal) => ↑(1 / p) * phiPow p z) ↑ζ ≠ ⊤ ∧ (fun (z : EReal) => ↑(1 / p) * phiPow p z) ↑ζ ≠ ⊥

Basic properties of gPow z = (1/p) * phiPow p z.

theorem monotoneConjugateERealNonneg_gPow_eq_one_div_q_phiPow {p q : ℝ} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) {s : EReal} (hs : 0 ≤ s) : monotoneConjugateERealNonneg (fun (z : EReal) => ↑(1 / p) * phiPow p z) s = ↑(1 / q) * phiPow q s

The monotone conjugate of the power profile (1/p) * phiPow p on nonnegative inputs.

theorem sublevel_closedGauge_eq_sublevel_f_pow {n : ℕ} {p : ℝ} {f k : (Fin n → ℝ) → EReal} (hp : 0 < p) (hf_hom : PositivelyHomogeneousOfDegree p f) (hk : IsGauge k) (hunit : {x : Fin n → ℝ | k x ≤ 1} = {x : Fin n → ℝ | f x ≤ ↑(1 / p)}) {r : ℝ} : 0 < r → {x : Fin n → ℝ | k x ≤ ↑r} = {x : Fin n → ℝ | f x ≤ ↑(1 / p * r.rpow p)}

Sublevel sets of a closed gauge match sublevels of a positive-homogeneous function.

theorem f0_ne_top_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 ≠ ⊤

A closed proper convex positively homogeneous function is finite at the origin.

theorem isGaugeLike_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) : IsGaugeLike f

A closed proper convex positively homogeneous function is gauge-like.