noncomputable def lpNormEReal {n : ℕ} (p : ℝ) (x : Fin n → ℝ) : EReal

The ℓᵖ gauge as an EReal-valued function.

Equations

• lpNormEReal p x = ↑((∑ i : Fin n, |x i|.rpow p).rpow (1 / p))

theorem lpNormEReal_eq_phiPow_sum_abs_rpow {n : ℕ} (p : ℝ) (x : Fin n → ℝ) : lpNormEReal p x = phiPow (1 / p) ↑(∑ i : Fin n, |x i|.rpow p)

lpNormEReal is the phiPow of the ℓ^p sum.

theorem lpNormEReal_symm {n : ℕ} (p : ℝ) (x : Fin n → ℝ) : lpNormEReal p (-x) = lpNormEReal p x

lpNormEReal is even.

theorem lpNormEReal_pos_of_ne_zero {n : ℕ} {p : ℝ} (x : Fin n → ℝ) (hx : x ≠ 0) : 0 < lpNormEReal p x

lpNormEReal is strictly positive away from the origin.

theorem closedGauge_rpow_mul_and_polar_eq_of_closedProperConvex_posHomogeneous {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) (hf_hom : PositivelyHomogeneousOfDegree p f) : have k := fun (x : Fin n → ℝ) => phiPow (1 / p) (↑p * f x); have kStar := fun (xStar : Fin n → ℝ) => phiPow (1 / q) (↑q * fenchelConjugate n f xStar); IsClosedGauge k ∧ polarGauge k = kStar

Closed gauge and polar gauge for power profiles of closed proper convex functions.

theorem lpNormEReal_isClosedGauge_and_polarGauge_eq {n : ℕ} {p q : ℝ} (hp : 1 < p) (hpq : 1 / p + 1 / q = 1) : IsClosedGauge (lpNormEReal p) ∧ polarGauge (lpNormEReal p) = lpNormEReal q

The ℓᵖ gauge is closed and its polar gauge is the ℓᵠ gauge.

theorem lpNormEReal_isNormGauge_of_isGauge {n : ℕ} {p : ℝ} (hg : IsGauge (lpNormEReal p)) : IsNormGauge (lpNormEReal p)

A gauge instance for lpNormEReal upgrades to a norm gauge.

theorem lpNormEReal_polarGauge_eq_self_of_closedGauge {n : ℕ} {k kPolar : (Fin n → ℝ) → EReal} (hk : IsClosedGauge k) (hpol : polarGauge k = kPolar) : polarGauge kPolar = k

A closed gauge is fixed by the polar gauge involution.