Hyperoctahedral symmetry of the cutoff covariance

This file transports the cutoff's B₄ symmetry through Euclidean convolution and lattice periodization. These structural facts supply the symmetry half of the primitive-kernel estimates independently of their analytic bounds.

Measure-preserving Euclidean coordinate actions

def Anderson4D.permuteR4 (σ : Equiv.Perm (Fin dim)) (x : R4) : R4

Permute Euclidean coordinates.

Equations

• Anderson4D.permuteR4 σ x = x ∘ ⇑σ

def Anderson4D.permuteR4MeasurableEquiv (σ : Equiv.Perm (Fin dim)) : R4 ≃ᵐ R4

Coordinate permutation as a measurable equivalence.

Equations

• Anderson4D.permuteR4MeasurableEquiv σ = MeasurableEquiv.piCongrLeft (fun (x : Fin Anderson4D.dim) => ℝ) (Equiv.symm σ)

@[simp]

theorem Anderson4D.permuteR4MeasurableEquiv_apply (σ : Equiv.Perm (Fin dim)) (x : R4) : (permuteR4MeasurableEquiv σ) x = permuteR4 σ x

theorem Anderson4D.measurePreserving_permuteR4 (σ : Equiv.Perm (Fin dim)) : MeasureTheory.MeasurePreserving (⇑(permuteR4MeasurableEquiv σ)) MeasureTheory.volume MeasureTheory.volume

Coordinate permutation preserves Lebesgue measure on ℝ⁴.

def Anderson4D.coordinateFlipR4 (i : Fin dim) (x : R4) : R4

Flip one Euclidean coordinate.

Equations

• Anderson4D.coordinateFlipR4 i x = Function.update x i (-x i)

def Anderson4D.coordinateFlipR4MeasurableEquiv (i : Fin dim) : R4 ≃ᵐ R4

A Euclidean coordinate flip as a measurable involution.

Equations

• Anderson4D.coordinateFlipR4MeasurableEquiv i = { toEquiv := Function.Involutive.toPerm (Anderson4D.coordinateFlipR4 i) ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem Anderson4D.coordinateFlipR4MeasurableEquiv_apply (i : Fin dim) (x : R4) : (coordinateFlipR4MeasurableEquiv i) x = coordinateFlipR4 i x

theorem Anderson4D.measurePreserving_coordinateFlipR4 (i : Fin dim) : MeasureTheory.MeasurePreserving (⇑(coordinateFlipR4MeasurableEquiv i)) MeasureTheory.volume MeasureTheory.volume

A single-coordinate sign flip preserves Lebesgue measure on ℝ⁴.

Euclidean covariance symmetry

theorem Anderson4D.SmoothCutoff.eta_perm_invariant (ρ : SmoothCutoff) (σ : Equiv.Perm (Fin dim)) (x : R4) : ρ.eta (x ∘ ⇑σ) = ρ.eta x

Euclidean covariance is invariant under coordinate permutations.

theorem Anderson4D.SmoothCutoff.eta_even_coord (ρ : SmoothCutoff) (i : Fin dim) (x : R4) : ρ.eta (Function.update x i (-x i)) = ρ.eta x

Euclidean covariance is invariant under a sign flip in one slot.

theorem Anderson4D.SmoothCutoff.eta_memE (ρ : SmoothCutoff) : MemEClassR4 ρ.eta

The Euclidean covariance belongs to the same B₄ symmetry class as the cutoff.

Permutation symmetry after lattice periodization

def Anderson4D.SmoothCutoff.permuteZ4Equiv (σ : Equiv.Perm (Fin dim)) : Z4 ≃ Z4

Coordinate permutation of the integer period lattice.

Equations

• Anderson4D.SmoothCutoff.permuteZ4Equiv σ = Equiv.piCongrLeft (fun (x : Fin Anderson4D.dim) => ℤ) (Equiv.symm σ)

@[simp]

theorem Anderson4D.SmoothCutoff.permuteZ4Equiv_apply (σ : Equiv.Perm (Fin dim)) (k : Z4) : (permuteZ4Equiv σ) k = k ∘ ⇑σ

theorem Anderson4D.SmoothCutoff.etaPeriodTerm_perm (ρ : SmoothCutoff) (ε : ℝ) (σ : Equiv.Perm (Fin dim)) (z : T4) (k : Z4) : ρ.etaPeriodTerm ε (z ∘ ⇑σ) ((permuteZ4Equiv σ) k) = ρ.etaPeriodTerm ε z k

Simultaneously permuting a torus displacement and its period vector leaves one covariance-periodization term unchanged.

theorem Anderson4D.SmoothCutoff.etaEpsT4_perm_invariant (ρ : SmoothCutoff) (ε : ℝ) (σ : Equiv.Perm (Fin dim)) (z : T4) : ρ.etaEpsT4 ε (z ∘ ⇑σ) = ρ.etaEpsT4 ε z

The periodized torus covariance is invariant under coordinate permutations.

Representative independence and coordinate-flip symmetry

noncomputable def Anderson4D.SmoothCutoff.covariancePeriodVector (a : Z4) : R4

Euclidean period vector attached to an integer lattice point.

Equations

• Anderson4D.SmoothCutoff.covariancePeriodVector a j = 2 * Real.pi * ↑(a j)

noncomputable def Anderson4D.SmoothCutoff.etaPeriodTermR4 (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (k : Z4) : ℝ

A periodization term based at an arbitrary Euclidean representative.

Equations

• ρ.etaPeriodTermR4 ε x k = ε⁻¹ ^ Anderson4D.dim * ρ.eta fun (j : Fin Anderson4D.dim) => ε⁻¹ * (x j + Anderson4D.SmoothCutoff.covariancePeriodVector k j)

noncomputable def Anderson4D.SmoothCutoff.etaPeriodizationR4 (ρ : SmoothCutoff) (ε : ℝ) (x : R4) : ℝ

Periodization at an arbitrary Euclidean representative.

Equations

• ρ.etaPeriodizationR4 ε x = ∑' (k : Anderson4D.Z4), ρ.etaPeriodTermR4 ε x k

theorem Anderson4D.SmoothCutoff.etaEpsT4_eq_etaPeriodizationR4 (ρ : SmoothCutoff) (ε : ℝ) (z : T4) : ρ.etaEpsT4 ε z = ρ.etaPeriodizationR4 ε (torusLift z)

theorem Anderson4D.SmoothCutoff.etaPeriodTermR4_add_period (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (a k : Z4) : ρ.etaPeriodTermR4 ε (x + covariancePeriodVector a) k = ρ.etaPeriodTermR4 ε x (k + a)

Translating the representative and the period index in opposite descriptions gives the same summand.

theorem Anderson4D.SmoothCutoff.etaPeriodizationR4_add_period (ρ : SmoothCutoff) (ε : ℝ) (x : R4) (a : Z4) : ρ.etaPeriodizationR4 ε (x + covariancePeriodVector a) = ρ.etaPeriodizationR4 ε x

Lattice periodization is independent of the Euclidean representative.

def Anderson4D.SmoothCutoff.coordinateFlipZ4 (i : Fin dim) (k : Z4) : Z4

Flip one coordinate of the integer lattice.

Equations

• Anderson4D.SmoothCutoff.coordinateFlipZ4 i k = Function.update k i (-k i)

def Anderson4D.SmoothCutoff.coordinateFlipZ4Equiv (i : Fin dim) : Z4 ≃ Z4

The lattice coordinate flip as an involutive equivalence.

Equations

• Anderson4D.SmoothCutoff.coordinateFlipZ4Equiv i = Function.Involutive.toPerm (Anderson4D.SmoothCutoff.coordinateFlipZ4 i) ⋯

@[simp]

theorem Anderson4D.SmoothCutoff.coordinateFlipZ4Equiv_apply (i : Fin dim) (k : Z4) : (coordinateFlipZ4Equiv i) k = coordinateFlipZ4 i k

theorem Anderson4D.SmoothCutoff.etaPeriodTermR4_coordinateFlip (ρ : SmoothCutoff) (ε : ℝ) (i : Fin dim) (x : R4) (k : Z4) : ρ.etaPeriodTermR4 ε (coordinateFlipR4 i x) ((coordinateFlipZ4Equiv i) k) = ρ.etaPeriodTermR4 ε x k

Flipping a representative and the matching lattice coordinate leaves one periodization term unchanged.

theorem Anderson4D.SmoothCutoff.etaPeriodizationR4_coordinateFlip (ρ : SmoothCutoff) (ε : ℝ) (i : Fin dim) (x : R4) : ρ.etaPeriodizationR4 ε (coordinateFlipR4 i x) = ρ.etaPeriodizationR4 ε x

Arbitrary-representative periodization is even in every coordinate.

theorem Anderson4D.SmoothCutoff.exists_periodVector_torusLift_coordinateFlip (i : Fin dim) (z : T4) : ∃ (a : Z4), torusLift (Function.update z i (-z i)) = coordinateFlipR4 i (torusLift z) + covariancePeriodVector a

The canonical lift of a flipped torus coordinate differs from the flipped canonical lift by an integer period vector.

theorem Anderson4D.SmoothCutoff.etaEpsT4_even_coord (ρ : SmoothCutoff) (ε : ℝ) (i : Fin dim) (z : T4) : ρ.etaEpsT4 ε (Function.update z i (-z i)) = ρ.etaEpsT4 ε z

The torus covariance is invariant under a sign flip in one coordinate.

theorem Anderson4D.SmoothCutoff.etaEpsT4_memE (ρ : SmoothCutoff) (ε : ℝ) : MemEClassT4 (ρ.etaEpsT4 ε)

The periodized covariance belongs to the torus symmetry class.