Pairing-preserving ℓp symmetries preserve every coordinate-power norm.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_lpPower {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (x : Point d) : O3.lpPower p (Q x) = O3.lpPower p x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.hasDerivAt_lpPower_line {d : ℕ} {p : ℝ} (hp : 2 < p) (x h : Point d) (t : ℝ) : HasDerivAt (fun (s : ℝ) => O3.lpPower p (x + s • h)) (p * O3.Stage2RouteA.linePowerPair p x h t) t

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_linePowerPair {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (x h : Point d) : O3.Stage2RouteA.linePowerPair p (Q x) (Q h) = O3.Stage2RouteA.linePowerPair p x h

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_columns_disjoint {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) {i j : Fin d} (hij : i ≠ j) (k : Fin d) : Q (coordinateUnit i) k = 0 ∨ Q (coordinateUnit j) k = 0

Distinct columns of a frozen signed ell_p symmetry have disjoint coordinate support. The proof differentiates the preserved p-power twice at a coordinate vector; this avoids importing a packaged Lamperti theorem.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpPower_coordinateUnit {d : ℕ} (p : ℝ) (hp : p ≠ 0) (i : Fin d) : O3.lpPower p (coordinateUnit i) = 1

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpNorm_coordinateUnit {d : ℕ} {p : ℝ} (hp : 0 < p) (i : Fin d) : O3.lpNorm p (coordinateUnit i) = 1

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_column_ne_zero {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (i : Fin d) : Q (coordinateUnit i) ≠ 0

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.signedLpColumnIndex {d : ℕ} {p : ℝ} (hp : 2 < p) (Q Qdual : Point d → Point d) (hsym : SignedLpSymmetry p Q Qdual) (i : Fin d) : Fin d

A nonzero coordinate in the image of a coordinate unit under an ℓp symmetry.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.signedLpColumnIndex hp Q Qdual hsym i = Classical.choose ⋯

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpColumnIndex_spec {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (i : Fin d) : Q (coordinateUnit i) (signedLpColumnIndex hp Q Qdual hsym i) ≠ 0

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpColumnIndex_injective {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) : Function.Injective (signedLpColumnIndex hp Q Qdual hsym)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpColumnIndex_surjective {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) : Function.Surjective (signedLpColumnIndex hp Q Qdual hsym)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_column_off_index {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) {i k : Fin d} (hk : k ≠ signedLpColumnIndex hp Q Qdual hsym i) : Q (coordinateUnit i) k = 0

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_column_abs_at_index {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (i : Fin d) : |Q (coordinateUnit i) (signedLpColumnIndex hp Q Qdual hsym i)| = 1

def V7.Stage5AboveTwoLowerS5A2Envelope.signedLpLinearMap {d : ℕ} {p : ℝ} (Q Qdual : Point d → Point d) (hsym : SignedLpSymmetry p Q Qdual) : Point d →ₗ[ℝ] Point d

The primal symmetry bundled as a real linear map.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.signedLpLinearMap Q Qdual hsym = { toFun := Q, map_add' := ⋯, map_smul' := ⋯ }

theorem V7.Stage5AboveTwoLowerS5A2Envelope.point_eq_sum_coordinateUnit {d : ℕ} (x : Point d) : x = ∑ i : Fin d, x i • coordinateUnit i

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_lpPower_all {d : ℕ} {p r : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (x : Point d) : O3.lpPower r (Q x) = O3.lpPower r x

Every frozen signed ell_p symmetry preserves every coordinate r-power, not only the physical p-power.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_lpNorm_all {d : ℕ} {p r : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (x : Point d) : O3.lpNorm r (Q x) = O3.lpNorm r x