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

The unit sublevel of a closed gauge is polar to the unit sublevel of its polar gauge.

theorem k_eq_closedGauge_from_cor1531 {n : ℕ} {p q : ℝ} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) {f k0 : (Fin n → ℝ) → EReal} (hk0 : IsClosedGauge k0) (hfk0 : f = fun (x : Fin n → ℝ) => ↑(1 / p) * phiPow p (k0 x)) (hfc : ∀ (xStar : Fin n → ℝ), fenchelConjugate n f xStar = ↑(1 / q) * phiPow q (polarGauge k0 xStar)) : (fun (x : Fin n → ℝ) => phiPow (1 / p) (↑p * f x)) = k0 ∧ (fun (xStar : Fin n → ℝ) => phiPow (1 / q) (↑q * fenchelConjugate n f xStar)) = polarGauge k0

Recover (p f)^{1/p} and (q f^*)^{1/q} from the power representation.