SequenceLaw

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Canonical laws and transformations of shell sequences

The manuscript's probability space is the canonical sequence carrier ℤ → ShellField d. This file provides its coordinate marginal laws and the literal componentwise transformations used by J1 and J3. It introduces no probabilistic assumptions.

Main definitions

• shellMarginalLaw: the law of one specified shell coordinate.
• zeroShellLaw: the law of shell zero.
• translateSequence: simultaneous real translation of every shell.
• negateSequence: simultaneous negation of every shell.
• rotateSequence: simultaneous signed-permutation conjugation of every shell.

Coordinate laws

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_shellCoordinate {d : ℕ} (k : ℤ) : Measurable fun (F : ℤ → ShellField d) => F k

Evaluation of a shell sequence at a fixed integer coordinate is measurable.

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_zeroShellMap {d : ℕ} : Measurable fun (F : ℤ → ShellField d) => F 0

Measurability of the literal zero-coordinate map on shell sequences.

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.shellMarginalLaw {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) (k : ℤ) : MeasureTheory.ProbabilityMeasure (ShellField d)

The exact marginal law of shell coordinate k.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.shellMarginalLaw P k = P.map fun (F : ℤ → Algsuperdiff.Frozen.Assumptions.ShellField d) => F k

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellLaw {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) : MeasureTheory.ProbabilityMeasure (ShellField d)

The literal zero-coordinate shell-field law.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.zeroShellLaw P = P.map fun (F : ℤ → Algsuperdiff.Frozen.Assumptions.ShellField d) => F 0

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.shellMarginalLaw_zero {d : ℕ} (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) : shellMarginalLaw P 0 = zeroShellLaw P

Componentwise whole-sequence transformations

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.translateSequence {d : ℕ} (z : HCPolySupport.Vec d) (F : ℤ → ShellField d) : ℤ → ShellField d

Simultaneously translate every shell by the same real vector.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.translateSequence z F k = Algsuperdiff.Frozen.Assumptions.ShellField.translate z (F k)

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.translateSequence_apply {d : ℕ} (z : HCPolySupport.Vec d) (F : ℤ → ShellField d) (k : ℤ) : translateSequence z F k = translate z (F k)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_translateSequence {d : ℕ} (z : HCPolySupport.Vec d) : Measurable (translateSequence z)

Componentwise real translation is measurable on the whole sequence.

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.negateSequence {d : ℕ} (F : ℤ → ShellField d) : ℤ → ShellField d

Simultaneously negate every shell in the sequence.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.negateSequence F k = (F k).negate

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.negateSequence_apply {d : ℕ} (F : ℤ → ShellField d) (k : ℤ) : negateSequence F k = (F k).negate

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_negateSequence {d : ℕ} : Measurable negateSequence

Componentwise negation is measurable on the whole sequence.

noncomputable def Algsuperdiff.Frozen.Assumptions.ShellField.rotateSequence {d : ℕ} (R : HCPolySupport.Mat d) (hR : HCPolySupport.IsSignedPermutationMatrix R) (F : ℤ → ShellField d) : ℤ → ShellField d

Simultaneously apply one signed-permutation conjugation to every shell.

Equations

• Algsuperdiff.Frozen.Assumptions.ShellField.rotateSequence R hR F k = Algsuperdiff.Frozen.Assumptions.ShellField.rotate R hR (F k)

@[simp]

theorem Algsuperdiff.Frozen.Assumptions.ShellField.rotateSequence_apply {d : ℕ} (R : HCPolySupport.Mat d) (hR : HCPolySupport.IsSignedPermutationMatrix R) (F : ℤ → ShellField d) (k : ℤ) : rotateSequence R hR F k = rotate R hR (F k)

theorem Algsuperdiff.Frozen.Assumptions.ShellField.measurable_rotateSequence {d : ℕ} (R : HCPolySupport.Mat d) (hR : HCPolySupport.IsSignedPermutationMatrix R) : Measurable (rotateSequence R hR)

Componentwise signed-permutation conjugation is measurable on the whole sequence.

Migration cache (mathlib v4.33.1). Under the elementwise matrix norm, blind typeclass search for ContinuousENorm (Matrix m n ℝ) wanders through CStarAlgebra/NormedRing branches and gives up even though the instance exists. The frozen assumption files (Frozen/Assumptions/ShellLawJ*) open Matrix.Norms.Elementwise and integrate matrix-valued observables, so the cache lives here, scoped to that norm, and never inside a manifest-pinned file.

@[instance_reducible]

def Matrix.Norms.Elementwise.instContinuousENormMatrixElementwise {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] : ContinuousENorm (Matrix m n ℝ)

Continuity of the extended norm for the elementwise matrix norm.

Equations

• Matrix.Norms.Elementwise.instContinuousENormMatrixElementwise = id inferInstance