theorem phiPow_one_div_comp_phiPow_of_nonneg {p : ℝ} (hp : 0 < p) {z : EReal} (hz : 0 ≤ z) : phiPow (1 / p) (phiPow p z) = z

phiPow is inverted by the reciprocal exponent on nonnegative inputs.

theorem phiPow_comp_phiPow_one_div_of_nonneg {p : ℝ} (hp : 0 < p) {z : EReal} (hz : 0 ≤ z) : phiPow p (phiPow (1 / p) z) = z

phiPow with exponent p inverts phiPow (1/p) on nonnegative inputs.

theorem sublevel_f_one_div_eq_unitSublevel_k {n : ℕ} {p : ℝ} {f : (Fin n → ℝ) → EReal} (hp : 0 < p) (hnonneg : ∀ (x : Fin n → ℝ), 0 ≤ f x) : {x : Fin n → ℝ | f x ≤ ↑(1 / p)} = {x : Fin n → ℝ | phiPow (1 / p) (↑p * f x) ≤ 1}

The base sublevel of f equals the unit sublevel of k := (p f)^{1/p} under nonnegativity.

theorem unitSublevel_polarGauge_eq_polarSet {n : ℕ} {k : (Fin n → ℝ) → EReal} (hk : IsGauge k) : have C := {x : Fin n → ℝ | k x ≤ 1}; {xStar : Fin n → ℝ | polarGauge k xStar ≤ 1} = {xStar : Fin n → ℝ | ∀ x ∈ C, x ⬝ᵥ xStar ≤ 1}

The unit sublevel of a gauge corresponds to its polar set.