Finite-dimensional real ell_p geometry for the frozen O3 probe

The exponent is a genuine real number and the dimension is an arbitrary natural number. We use the literal finite-sum formula from the TeX source rather than the ambient Euclidean norm on Fin d → ℝ.

@[reducible, inline]

abbrev O3.Point (d : ℕ) : Type

A point of the arbitrary finite-dimensional ambient space ℝ^d.

Equations

• O3.Point d = (Fin d → ℝ)

def O3.pairing {d : ℕ} (x y : Point d) : ℝ

The coordinate pairing used between ell_p and ell_q.

Equations

• O3.pairing x y = ∑ i : Fin d, x i * y i

noncomputable def O3.conjugateExponent (p : ℝ) : ℝ

The real conjugate exponent q = p / (p - 1).

Equations

• O3.conjugateExponent p = p.conjExponent

theorem O3.conjugateExponent_eq (p : ℝ) : conjugateExponent p = p / (p - 1)

theorem O3.holderConjugate_conjugateExponent {p : ℝ} (hp : 1 < p) : p.HolderConjugate (conjugateExponent p)

theorem O3.one_lt_conjugateExponent {p : ℝ} (hp : 1 < p) : 1 < conjugateExponent p

noncomputable def O3.lpPower (p : ℝ) {d : ℕ} (x : Point d) : ℝ

The p-th power sum underlying the finite-dimensional ell_p norm.

Equations

• O3.lpPower p x = ∑ i : Fin d, |x i| ^ p

noncomputable def O3.lpNorm (p : ℝ) {d : ℕ} (x : Point d) : ℝ

The literal finite-dimensional ell_p norm for a real exponent.

Equations

• O3.lpNorm p x = O3.lpPower p x ^ (1 / p)

theorem O3.lpPower_nonneg (p : ℝ) {d : ℕ} (x : Point d) : 0 ≤ lpPower p x

theorem O3.lpNorm_nonneg (p : ℝ) {d : ℕ} (x : Point d) : 0 ≤ lpNorm p x

@[simp]

theorem O3.lpPower_zero {p : ℝ} (hp : p ≠ 0) {d : ℕ} : lpPower p 0 = 0

@[simp]

theorem O3.lpNorm_zero {p : ℝ} (hp : 0 < p) {d : ℕ} : lpNorm p 0 = 0

theorem O3.lpPower_pos_of_ne_zero {p : ℝ} {d : ℕ} {x : Point d} (hx : x ≠ 0) : 0 < lpPower p x

theorem O3.lpNorm_pos_of_ne_zero {p : ℝ} {d : ℕ} {x : Point d} (hx : x ≠ 0) : 0 < lpNorm p x

theorem O3.lpNorm_eq_zero_iff {p : ℝ} (hp : 0 < p) {d : ℕ} {x : Point d} : lpNorm p x = 0 ↔ x = 0

@[simp]

theorem O3.lpPower_neg (p : ℝ) {d : ℕ} (x : Point d) : lpPower p (-x) = lpPower p x

@[simp]

theorem O3.lpNorm_neg (p : ℝ) {d : ℕ} (x : Point d) : lpNorm p (-x) = lpNorm p x

theorem O3.pairing_comm {d : ℕ} (x y : Point d) : pairing x y = pairing y x

@[simp]

theorem O3.pairing_neg_left {d : ℕ} (x y : Point d) : pairing (-x) y = -pairing x y

@[simp]

theorem O3.pairing_neg_right {d : ℕ} (x y : Point d) : pairing x (-y) = -pairing x y

theorem O3.pairing_le_lpNorm_mul {p q : ℝ} (hpq : p.HolderConjugate q) {d : ℕ} (x y : Point d) : pairing x y ≤ lpNorm p x * lpNorm q y

Finite-dimensional Hölder inequality in the exact explicit norms used by O3.

theorem O3.abs_pairing_le_lpNorm_mul {p q : ℝ} (hpq : p.HolderConjugate q) {d : ℕ} (x y : Point d) : |pairing x y| ≤ lpNorm p x * lpNorm q y

Absolute-value form of finite-dimensional Hölder.

noncomputable def O3.powerDualityMap (p : ℝ) {d : ℕ} (u : Point d) : Point d

The power-duality map J_p(u)_i = |u_i|^(p-2) u_i from the TeX source.

Equations

• O3.powerDualityMap p u i = |u i| ^ (p - 2) * u i

noncomputable def O3.uniformRegularizer (p : ℝ) {d : ℕ} (c x : Point d) : ℝ

h_c(x) = (1/p) ||x-c||_p^p, written using its literal power sum.

Equations

• O3.uniformRegularizer p c x = 1 / p * O3.lpPower p (x - c)

noncomputable def O3.dualityMap (p : ℝ) {d : ℕ} (u : Point d) : Point d

The normalized ell_p duality map used in the 1 < p ≤ 2 chain.

Equations

• O3.dualityMap p u = if O3.lpNorm p u = 0 then 0 else fun (i : Fin d) => O3.lpNorm p u ^ (2 - p) * (|u i| ^ (p - 2) * u i)

noncomputable def O3.quadraticRegularizer (p : ℝ) {d : ℕ} (c x : Point d) : ℝ

ψ_c(x) = (1/2) ||x-c||_p^2.

Equations

• O3.quadraticRegularizer p c x = 1 / 2 * O3.lpNorm p (x - c) ^ 2

noncomputable def O3.PUniformConvexityStatement : Prop

Exact unproved target of TeX Lemma lem:puniform. Keeping this as a transparent proposition records the residual obligation without presenting it as a proved theorem.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def O3.BelowGeometryStatement : Prop

Exact unproved target of TeX Lemma lem:belowgeometry. This proposition preserves real p and arbitrary d; it is not a theorem or certificate.

Equations

• One or more equations did not get rendered due to their size.