Hyperoctahedral symmetry of primitive kernels at every order

This file proves the symmetry half of Proposition 4.1 without assuming symmetry of the resulting primitive kernel. Coordinate permutations and single-coordinate sign flips are transported simultaneously through every internal integration variable. The product paper measure is preserved, while assembly, chain differences, covariance differences, and the diameter insertion are equivariant.

Coordinate permutations on the torus and product measures

def Anderson4D.permuteT4 (σ : Equiv.Perm (Fin dim)) (x : T4) : T4

Permute the four torus coordinates.

Equations

• Anderson4D.permuteT4 σ x = x ∘ ⇑σ

noncomputable def Anderson4D.permuteT4MeasurableEquiv (σ : Equiv.Perm (Fin dim)) : T4 ≃ᵐ T4

Coordinate permutation as a measurable equivalence of the torus.

Equations

• Anderson4D.permuteT4MeasurableEquiv σ = MeasurableEquiv.piCongrLeft (fun (x : Fin Anderson4D.dim) => AddCircle (2 * Real.pi)) (Equiv.symm σ)

@[simp]

theorem Anderson4D.permuteT4MeasurableEquiv_apply (σ : Equiv.Perm (Fin dim)) (x : T4) : (permuteT4MeasurableEquiv σ) x = permuteT4 σ x

theorem Anderson4D.measurePreserving_permuteT4 (σ : Equiv.Perm (Fin dim)) : MeasureTheory.MeasurePreserving (⇑(permuteT4MeasurableEquiv σ)) paperMeasure paperMeasure

Coordinate permutation preserves the paper-normalized torus measure.

theorem Anderson4D.measurePreserving_permuteT4_fun (σ : Equiv.Perm (Fin dim)) : MeasureTheory.MeasurePreserving (permuteT4 σ) paperMeasure paperMeasure

Function-valued form of coordinate-permutation measure preservation.

def Anderson4D.permuteT4Tuple {ι : Type u_1} (σ : Equiv.Perm (Fin dim)) (x : ι → T4) : ι → T4

Apply a coordinate permutation in every member of a finite tuple.

Equations

• Anderson4D.permuteT4Tuple σ x a = Anderson4D.permuteT4 σ (x a)

noncomputable def Anderson4D.coordinateFlipT4Tuple {ι : Type u_1} (i : Fin dim) (x : ι → T4) : ι → T4

Apply one coordinate flip in every member of a finite tuple.

Equations

• Anderson4D.coordinateFlipT4Tuple i x a = Anderson4D.coordinateFlipT4 i (x a)

noncomputable def Anderson4D.permuteT4TupleMeasurableEquiv {ι : Type u_1} (σ : Equiv.Perm (Fin dim)) : (ι → T4) ≃ᵐ (ι → T4)

Coordinatewise permutation bundled as a measurable equivalence of finite tuples.

Equations

• Anderson4D.permuteT4TupleMeasurableEquiv σ = MeasurableEquiv.piCongrRight fun (x : ι) => Anderson4D.permuteT4MeasurableEquiv σ

@[simp]

theorem Anderson4D.permuteT4TupleMeasurableEquiv_apply {ι : Type u_1} (σ : Equiv.Perm (Fin dim)) (x : ι → T4) : (permuteT4TupleMeasurableEquiv σ) x = permuteT4Tuple σ x

noncomputable def Anderson4D.coordinateFlipT4TupleMeasurableEquiv {ι : Type u_1} (i : Fin dim) : (ι → T4) ≃ᵐ (ι → T4)

Coordinatewise flip bundled as a measurable equivalence of finite tuples.

Equations

• Anderson4D.coordinateFlipT4TupleMeasurableEquiv i = MeasurableEquiv.piCongrRight fun (x : ι) => Anderson4D.coordinateFlipMeasurableEquiv i

@[simp]

theorem Anderson4D.coordinateFlipT4TupleMeasurableEquiv_apply {ι : Type u_1} (i : Fin dim) (x : ι → T4) : (coordinateFlipT4TupleMeasurableEquiv i) x = coordinateFlipT4Tuple i x

theorem Anderson4D.measurePreserving_permuteT4Tuple {ι : Type u_1} [Fintype ι] (σ : Equiv.Perm (Fin dim)) : MeasureTheory.MeasurePreserving (⇑(permuteT4TupleMeasurableEquiv σ)) (MeasureTheory.Measure.pi fun (x : ι) => paperMeasure) (MeasureTheory.Measure.pi fun (x : ι) => paperMeasure)

Coordinatewise permutation preserves every finite product of the paper measure.

theorem Anderson4D.measurePreserving_coordinateFlipT4Tuple {ι : Type u_1} [Fintype ι] (i : Fin dim) : MeasureTheory.MeasurePreserving (⇑(coordinateFlipT4TupleMeasurableEquiv i)) (MeasureTheory.Measure.pi fun (x : ι) => paperMeasure) (MeasureTheory.Measure.pi fun (x : ι) => paperMeasure)

Coordinatewise flip preserves every finite product of the paper measure.

theorem Anderson4D.integral_comp_permuteT4Tuple {ι : Type u_1} [Fintype ι] (σ : Equiv.Perm (Fin dim)) (F : (ι → T4) → ℝ) : (∫ (v : ι → T4), F (permuteT4Tuple σ v) ∂MeasureTheory.Measure.pi fun (x : ι) => paperMeasure) = ∫ (v : ι → T4), F v ∂MeasureTheory.Measure.pi fun (x : ι) => paperMeasure

Integral change of variables for a simultaneous tuple permutation.

theorem Anderson4D.integral_comp_coordinateFlipT4Tuple {ι : Type u_1} [Fintype ι] (i : Fin dim) (F : (ι → T4) → ℝ) : (∫ (v : ι → T4), F (coordinateFlipT4Tuple i v) ∂MeasureTheory.Measure.pi fun (x : ι) => paperMeasure) = ∫ (v : ι → T4), F v ∂MeasureTheory.Measure.pi fun (x : ι) => paperMeasure

Integral change of variables for a simultaneous tuple flip.

Equivariance of group operations and endpoint assembly

theorem Anderson4D.permuteT4_sub (σ : Equiv.Perm (Fin dim)) (x y : T4) : permuteT4 σ (x - y) = permuteT4 σ x - permuteT4 σ y

theorem Anderson4D.coordinateFlipT4_sub (i : Fin dim) (x y : T4) : coordinateFlipT4 i (x - y) = coordinateFlipT4 i x - coordinateFlipT4 i y

@[simp]

theorem Anderson4D.permuteT4_zero (σ : Equiv.Perm (Fin dim)) : permuteT4 σ 0 = 0

@[simp]

theorem Anderson4D.coordinateFlipT4_zero (i : Fin dim) : coordinateFlipT4 i 0 = 0

theorem Anderson4D.assemble_permute {m : ℕ} (σ : Equiv.Perm (Fin dim)) (z w : T4) (v : Fin m → T4) (j : Fin (m + 2)) : assemble (permuteT4 σ z) (permuteT4 σ w) (permuteT4Tuple σ v) j = permuteT4 σ (assemble z w v j)

Endpoint assembly commutes with a simultaneous coordinate permutation.

theorem Anderson4D.assemble_coordinateFlip {m : ℕ} (i : Fin dim) (z w : T4) (v : Fin m → T4) (j : Fin (m + 2)) : assemble (coordinateFlipT4 i z) (coordinateFlipT4 i w) (coordinateFlipT4Tuple i v) j = coordinateFlipT4 i (assemble z w v j)

Endpoint assembly commutes with a simultaneous coordinate flip.

theorem Anderson4D.primitiveAssemble_permute (n : ℕ) (hn : 1 ≤ n) (σ : Equiv.Perm (Fin dim)) (z w : T4) (v : Fin (2 * n - 2) → T4) (j : Fin (2 * n)) : primitiveAssemble n hn (permuteT4 σ z) (permuteT4 σ w) (permuteT4Tuple σ v) j = permuteT4 σ (primitiveAssemble n hn z w v j)

theorem Anderson4D.primitiveAssemble_coordinateFlip (n : ℕ) (hn : 1 ≤ n) (i : Fin dim) (z w : T4) (v : Fin (2 * n - 2) → T4) (j : Fin (2 * n)) : primitiveAssemble n hn (coordinateFlipT4 i z) (coordinateFlipT4 i w) (coordinateFlipT4Tuple i v) j = coordinateFlipT4 i (primitiveAssemble n hn z w v j)

Equivariance of products and diameter insertion

theorem Anderson4D.primitiveChainProduct_permute (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (σ : Equiv.Perm (Fin dim)) (x : Fin (2 * n) → T4) : primitiveChainProduct n hn G (permuteT4Tuple σ x) = primitiveChainProduct n hn G x

theorem Anderson4D.primitiveChainProduct_coordinateFlip (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (i : Fin dim) (x : Fin (2 * n) → T4) : primitiveChainProduct n hn G (coordinateFlipT4Tuple i x) = primitiveChainProduct n hn G x

theorem Anderson4D.primitiveCovarianceProduct_permute (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin (2 * n))) (σ : Equiv.Perm (Fin dim)) (x : Fin (2 * n) → T4) : primitiveCovarianceProduct ρ ε n κ (permuteT4Tuple σ x) = primitiveCovarianceProduct ρ ε n κ x

theorem Anderson4D.primitiveCovarianceProduct_coordinateFlip (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin (2 * n))) (i : Fin dim) (x : Fin (2 * n) → T4) : primitiveCovarianceProduct ρ ε n κ (coordinateFlipT4Tuple i x) = primitiveCovarianceProduct ρ ε n κ x

theorem Anderson4D.primitiveIntegrand_permute (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (κ : PartialPairing (Fin (2 * n))) (σ : Equiv.Perm (Fin dim)) (x : Fin (2 * n) → T4) : primitiveIntegrand ρ ε n hn G κ (permuteT4Tuple σ x) = primitiveIntegrand ρ ε n hn G κ x

theorem Anderson4D.primitiveIntegrand_coordinateFlip (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (κ : PartialPairing (Fin (2 * n))) (i : Fin dim) (x : Fin (2 * n) → T4) : primitiveIntegrand ρ ε n hn G κ (coordinateFlipT4Tuple i x) = primitiveIntegrand ρ ε n hn G κ x

theorem Anderson4D.torusTupleDiameterSq_permute {ι : Type u_1} [Fintype ι] [Nonempty ι] (σ : Equiv.Perm (Fin dim)) (x : ι → T4) : torusTupleDiameterSq (permuteT4Tuple σ x) = torusTupleDiameterSq x

theorem Anderson4D.torusTupleDiameterSq_coordinateFlip {ι : Type u_1} [Fintype ι] [Nonempty ι] (i : Fin dim) (x : ι → T4) : torusTupleDiameterSq (coordinateFlipT4Tuple i x) = torusTupleDiameterSq x

theorem Anderson4D.primitiveInsertedIntegrand_permute (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (κ : PartialPairing (Fin (2 * n))) (σ : Equiv.Perm (Fin dim)) (x : Fin (2 * n) → T4) : primitiveInsertedIntegrand ρ ε n hn G κ (permuteT4Tuple σ x) = primitiveInsertedIntegrand ρ ε n hn G κ x

theorem Anderson4D.primitiveInsertedIntegrand_coordinateFlip (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (κ : PartialPairing (Fin (2 * n))) (i : Fin dim) (x : Fin (2 * n) → T4) : primitiveInsertedIntegrand ρ ε n hn G κ (coordinateFlipT4Tuple i x) = primitiveInsertedIntegrand ρ ε n hn G κ x

Change of variables in the primitive kernels

theorem Anderson4D.primitiveIntegrandIntegral_permute (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (κ : PartialPairing (Fin (2 * n))) (σ : Equiv.Perm (Fin dim)) (z w : T4) : (∫ (v : Fin (2 * n - 2) → T4), primitiveIntegrand ρ ε n hn G κ (primitiveAssemble n hn (permuteT4 σ z) (permuteT4 σ w) v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = ∫ (v : Fin (2 * n - 2) → T4), primitiveIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

theorem Anderson4D.primitiveIntegrandIntegral_coordinateFlip (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (κ : PartialPairing (Fin (2 * n))) (i : Fin dim) (z w : T4) : (∫ (v : Fin (2 * n - 2) → T4), primitiveIntegrand ρ ε n hn G κ (primitiveAssemble n hn (coordinateFlipT4 i z) (coordinateFlipT4 i w) v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = ∫ (v : Fin (2 * n - 2) → T4), primitiveIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

theorem Anderson4D.primitiveInsertedIntegrandIntegral_permute (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (κ : PartialPairing (Fin (2 * n))) (σ : Equiv.Perm (Fin dim)) (z w : T4) : (∫ (v : Fin (2 * n - 2) → T4), primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn (permuteT4 σ z) (permuteT4 σ w) v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = ∫ (v : Fin (2 * n - 2) → T4), primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

theorem Anderson4D.primitiveInsertedIntegrandIntegral_coordinateFlip (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (κ : PartialPairing (Fin (2 * n))) (i : Fin dim) (z w : T4) : (∫ (v : Fin (2 * n - 2) → T4), primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn (coordinateFlipT4 i z) (coordinateFlipT4 i w) v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure) = ∫ (v : Fin (2 * n - 2) → T4), primitiveInsertedIntegrand ρ ε n hn G κ (primitiveAssemble n hn z w v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure

theorem Anderson4D.primitiveKernel_permute (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (σ : Equiv.Perm (Fin dim)) (z w : T4) : primitiveKernel ρ lam ε n hn G (permuteT4 σ z) (permuteT4 σ w) = primitiveKernel ρ lam ε n hn G z w

theorem Anderson4D.primitiveKernel_coordinateFlip (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (i : Fin dim) (z w : T4) : primitiveKernel ρ lam ε n hn G (coordinateFlipT4 i z) (coordinateFlipT4 i w) = primitiveKernel ρ lam ε n hn G z w

theorem Anderson4D.primitiveKernelInserted_permute (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (σ : Equiv.Perm (Fin dim)) (z w : T4) : primitiveKernelInserted ρ lam ε n hn G (permuteT4 σ z) (permuteT4 σ w) = primitiveKernelInserted ρ lam ε n hn G z w

theorem Anderson4D.primitiveKernelInserted_coordinateFlip (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (i : Fin dim) (z w : T4) : primitiveKernelInserted ρ lam ε n hn G (coordinateFlipT4 i z) (coordinateFlipT4 i w) = primitiveKernelInserted ρ lam ε n hn G z w

One-variable kernels belong to the paper's class 𝓔

theorem Anderson4D.primitiveKernelDiff_memE (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) : MemEClassT4 (primitiveKernelDiff ρ lam ε n hn G)

theorem Anderson4D.primitiveKernelInsertedDiff_memE (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) : MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε n hn G)