Norm- and pairing-preserving transformations are linear, using the dual image basis.

def V7.Stage5AboveTwoLowerS5A2Envelope.coordinateUnit {d : ℕ} (i : Fin d) : Point d

The vector equal to one at coordinate i and zero elsewhere.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.coordinateUnit i j = if j = i then 1 else 0

theorem V7.Stage5AboveTwoLowerS5A2Envelope.pairing_coordinateUnit {d : ℕ} (x : Point d) (i : Fin d) : O3.pairing (coordinateUnit i) x = x i

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_dual_linearIndependent {d : ℕ} {p : ℝ} {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) : LinearIndependent ℝ fun (i : Fin d) => Qdual (coordinateUnit i)

The dual images of the coordinate vectors are a basis. This is the separation wheel that turns the frozen pairing identity into linearity.

noncomputable def V7.Stage5AboveTwoLowerS5A2Envelope.signedLpDualBasis {d : ℕ} {p : ℝ} (Q Qdual : Point d → Point d) (hsym : SignedLpSymmetry p Q Qdual) : Module.Basis (Fin d) ℝ (Point d)

The basis formed by the dual symmetry images of coordinate unit vectors.

Equations

• V7.Stage5AboveTwoLowerS5A2Envelope.signedLpDualBasis Q Qdual hsym = basisOfPiSpaceOfLinearIndependent ⋯

theorem V7.Stage5AboveTwoLowerS5A2Envelope.eq_zero_of_pairing_dual_images_zero {d : ℕ} {p : ℝ} {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) {z : Point d} (hz : ∀ (i : Fin d), O3.pairing (Qdual (coordinateUnit i)) z = 0) : z = 0

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_Q_add {d : ℕ} {p : ℝ} {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (x y : Point d) : Q (x + y) = Q x + Q y

The frozen pairing identity forces the primal map to be additive.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpSymmetry_Q_smul {d : ℕ} {p : ℝ} {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (a : ℝ) (x : Point d) : Q (a • x) = a • Q x

The frozen pairing identity forces the primal map to be homogeneous.