Fourier facts for the smooth cutoff

These are the normalization and reality identities needed by the white-noise Fourier series. They are proved directly from the project's unnormalized Euclidean Fourier convention.

theorem Anderson4D.fourierR4_neg_eq_conj (f : R4 → ℝ) (ξ : R4) : fourierR4 f (-ξ) = (starRingEnd ℂ) (fourierR4 f ξ)

The Fourier transform of a real-valued function has the usual conjugate symmetry.

@[simp]

theorem Anderson4D.SmoothCutoff.symbol_neg (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ρ.symbol ε (-k) = (starRingEnd ℂ) (ρ.symbol ε k)

The mollifier multiplier obeys the reality constraint needed to pair the modes k and -k.

@[simp]

theorem Anderson4D.SmoothCutoff.symbol_zero (ρ : SmoothCutoff) (ε : ℝ) : ρ.symbol ε 0 = 1

The zero Fourier mode is one, with the exact normalization inherited from ∫ρ = 1.

theorem Anderson4D.SmoothCutoff.norm_symbol_le_one (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ‖ρ.symbol ε k‖ ≤ 1

Every cutoff multiplier lies in the closed unit disk.