Scalar and vector uniform convexity for the power mirror geometry.

noncomputable def O3.Experimental.scalarJ (p u : ℝ) : ℝ

The scalar power-duality map u ↦ |u|^(p - 2) u.

Equations

• O3.Experimental.scalarJ p u = |u| ^ (p - 2) * u

theorem O3.Experimental.scalarJ_nonneg {p u : ℝ} (hp : 2 < p) (hu : 0 ≤ u) : scalarJ p u = u ^ (p - 1)

theorem O3.Experimental.scalarJ_nonpos {p u : ℝ} (hp : 2 < p) (hu : u ≤ 0) : scalarJ p u = -(-u) ^ (p - 1)

theorem O3.Experimental.scalarJ_strongMonotone_ordered {p u v : ℝ} (hp : 2 < p) (huv : v ≤ u) : 2 ^ (2 - p) * |u - v| ^ p ≤ (scalarJ p u - scalarJ p v) * (u - v)

theorem O3.Experimental.scalarJ_strongMonotone {p u v : ℝ} (hp : 2 < p) : 2 ^ (2 - p) * |u - v| ^ p ≤ (scalarJ p u - scalarJ p v) * (u - v)

theorem O3.Experimental.powerDualityMap_strongMonotone {p : ℝ} (hp : 2 < p) {d : ℕ} (u v : Point d) : 2 ^ (2 - p) * lpPower p (u - v) ≤ pairing (powerDualityMap p u - powerDualityMap p v) (u - v)

noncomputable def O3.Experimental.scalarEnergy (p x : ℝ) : ℝ

The scalar power energy whose derivative is the power-duality map.

Equations

• O3.Experimental.scalarEnergy p x = |x| ^ p / p

theorem O3.Experimental.hasDerivAt_scalarEnergy {p : ℝ} (hp : 2 < p) (x : ℝ) : HasDerivAt (scalarEnergy p) (scalarJ p x) x

theorem O3.Experimental.continuous_scalarJ {p : ℝ} (hp : 2 < p) : Continuous (scalarJ p)

theorem O3.Experimental.scalarUniformConvexity_of_le {p x y : ℝ} (hp : 2 < p) (hxy : x ≤ y) : scalarEnergy p y ≥ scalarEnergy p x + scalarJ p x * (y - x) + 2 ^ (2 - p) / p * |y - x| ^ p

theorem O3.Experimental.scalarJ_neg (p x : ℝ) : scalarJ p (-x) = -scalarJ p x

theorem O3.Experimental.scalarEnergy_neg (p x : ℝ) : scalarEnergy p (-x) = scalarEnergy p x

theorem O3.Experimental.scalarUniformConvexity {p x y : ℝ} (hp : 2 < p) : scalarEnergy p y ≥ scalarEnergy p x + scalarJ p x * (y - x) + 2 ^ (2 - p) / p * |y - x| ^ p

theorem O3.Experimental.lpNorm_rpow_eq_lpPower {p : ℝ} (hp : p ≠ 0) {d : ℕ} (z : Point d) : lpNorm p z ^ p = lpPower p z

theorem O3.Experimental.pUniformConvexity {p : ℝ} (hp : 2 < p) {d : ℕ} (x y c : Point d) : uniformRegularizer p c y ≥ uniformRegularizer p c x + pairing (powerDualityMap p (x - c)) (y - x) + 2 ^ (2 - p) / p * lpNorm p (y - x) ^ p

theorem O3.pUniformConvexity : PUniformConvexityStatement

Frozen TeX Lemma lem:puniform, proved for every real p > 2 and every finite dimension with the source-exact constant.