Symmetry of the first primitive kernel

The analytic base bounds and the symmetry conclusion of Proposition 4.1 are deliberately separated. Here the latter follows from closure of the hyperoctahedral class under products and the periodized covariance symmetry.

theorem Anderson4D.MemEClassT4.mul {f g : T4 → ℝ} (hf : MemEClassT4 f) (hg : MemEClassT4 g) : MemEClassT4 fun (z : T4) => f z * g z

The torus symmetry class is closed under pointwise multiplication.

theorem Anderson4D.MemEClassT4.const_mul {f : T4 → ℝ} (hf : MemEClassT4 f) (c : ℝ) : MemEClassT4 fun (z : T4) => c * f z

Multiplication by a scalar preserves the torus symmetry class.

theorem Anderson4D.torusDistSq_memE : MemEClassT4 torusDistSq

The canonical squared torus distance is hyperoctahedrally invariant.

theorem Anderson4D.add_torusDistSq_memE (ε : ℝ) : MemEClassT4 fun (z : T4) => ε ^ 2 + torusDistSq z

The diameter factor in the inserted base kernel is symmetric.

theorem Anderson4D.primitiveKernelDiff_one_memE (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin 1 → T4 → ℝ) (hG : MemEClassT4 (G 0)) : MemEClassT4 (primitiveKernelDiff ρ lam ε 1 ⋯ G)

The ordinary first primitive kernel belongs to 𝓔.

theorem Anderson4D.primitiveKernelInsertedDiff_one_memE (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin 1 → T4 → ℝ) (hG : MemEClassT4 (G 0)) : MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε 1 ⋯ G)

The diameter-inserted first primitive kernel belongs to 𝓔.

theorem Anderson4D.exists_uniform_prop41BoundPredicate_one (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ (lam ε orderConstant : ℝ) (G : Fin 1 → T4 → ℝ), Prop41BoundPredicate ρ lam ε 1 ⋯ G orderConstant supportConstant C

Fully uniform Proposition 4.1 predicate at the base order, including both symmetry conclusions and both analytic estimates.