Projected covariance for the R-324 frequency route

Paper §4.2, Step 4 replaces one occurrence of the mollified noise by its projection onto modes of size at least sqrt ε / 2 times the total external shift. After Wick contraction this is a deterministic projection of one covariance Fourier series. This file constructs that countable series, proves its exact complement decomposition, and enumerates it by ℕ for the routed-reduction consumer.

noncomputable def Anderson4D.SmoothCutoff.r324CovarianceModeTerm (ρ : SmoothCutoff) (ε : ℝ) (z : T4) (k : Z4) : ℂ

One spatial Fourier mode in the complex cutoff covariance.

Equations

• ρ.r324CovarianceModeTerm ε z k = ρ.covarianceModeCoeff ε k * Anderson4D.charT4 k z

theorem Anderson4D.SmoothCutoff.norm_r324CovarianceModeTerm (ρ : SmoothCutoff) (ε : ℝ) (z : T4) (k : Z4) : ‖ρ.r324CovarianceModeTerm ε z k‖ = ‖ρ.covarianceModeCoeff ε k‖

theorem Anderson4D.SmoothCutoff.summable_r324CovarianceModeTerm (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : T4) : Summable (ρ.r324CovarianceModeTerm ε z)

def Anderson4D.SmoothCutoff.r324HighModeSet (ε L : ℝ) : Set Z4

The high-mode set selected by the truncation-length pigeonhole argument.

Equations

• Anderson4D.SmoothCutoff.r324HighModeSet ε L = {k : Anderson4D.Z4 | √ε / 2 * L ≤ ‖Anderson4D.z4EuclideanFrequency k‖}

noncomputable def Anderson4D.SmoothCutoff.r324HighCovarianceModeTerm (ρ : SmoothCutoff) (ε L : ℝ) (z : T4) (k : Z4) : ℂ

One covariance mode retained by the Step 4 high-frequency projection.

Equations

• ρ.r324HighCovarianceModeTerm ε L z k = (Anderson4D.SmoothCutoff.r324HighModeSet ε L).indicator (ρ.r324CovarianceModeTerm ε z) k

noncomputable def Anderson4D.SmoothCutoff.r324LowCovarianceModeTerm (ρ : SmoothCutoff) (ε L : ℝ) (z : T4) (k : Z4) : ℂ

The complementary low-frequency covariance mode.

Equations

• ρ.r324LowCovarianceModeTerm ε L z k = (Anderson4D.SmoothCutoff.r324HighModeSet ε L)ᶜ.indicator (ρ.r324CovarianceModeTerm ε z) k

noncomputable def Anderson4D.SmoothCutoff.r324ProjectedCovarianceC (ρ : SmoothCutoff) (ε L : ℝ) (z : T4) : ℂ

The complex covariance after projecting to routed high modes.

Equations

• ρ.r324ProjectedCovarianceC ε L z = ∑' (k : Anderson4D.Z4), ρ.r324HighCovarianceModeTerm ε L z k

noncomputable def Anderson4D.SmoothCutoff.r324LowCovarianceC (ρ : SmoothCutoff) (ε L : ℝ) (z : T4) : ℂ

The complementary low-mode covariance.

Equations

• ρ.r324LowCovarianceC ε L z = ∑' (k : Anderson4D.Z4), ρ.r324LowCovarianceModeTerm ε L z k

theorem Anderson4D.SmoothCutoff.summable_r324HighCovarianceModeTerm (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) (z : T4) : Summable (ρ.r324HighCovarianceModeTerm ε L z)

theorem Anderson4D.SmoothCutoff.summable_r324LowCovarianceModeTerm (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) (z : T4) : Summable (ρ.r324LowCovarianceModeTerm ε L z)

theorem Anderson4D.SmoothCutoff.r324Low_add_high_mode (ρ : SmoothCutoff) (ε L : ℝ) (z : T4) (k : Z4) : ρ.r324LowCovarianceModeTerm ε L z k + ρ.r324HighCovarianceModeTerm ε L z k = ρ.r324CovarianceModeTerm ε z k

theorem Anderson4D.SmoothCutoff.complexFourierCovarianceT4_eq_low_add_projected (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) (z : T4) : ρ.complexFourierCovarianceT4 ε z = ρ.r324LowCovarianceC ε L z + ρ.r324ProjectedCovarianceC ε L z

Exact low/high decomposition of the full covariance Fourier series.

theorem Anderson4D.SmoothCutoff.etaEpsT4_eq_low_add_projected (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) (z : T4) : ↑(ρ.etaEpsT4 ε z) = ρ.r324LowCovarianceC ε L z + ρ.r324ProjectedCovarianceC ε L z

Spatial covariance equals the exact low/high Fourier decomposition, with all normalization constants inherited from Poisson summation.

@[implicit_reducible]

def Anderson4D.SmoothCutoff.instDenumerableZ4 : Denumerable Z4

Canonical enumeration of ℤ⁴ by natural numbers.

Equations

• Anderson4D.SmoothCutoff.instDenumerableZ4 = Denumerable.ofEncodableOfInfinite Anderson4D.Z4

def Anderson4D.SmoothCutoff.r324NatEquivZ4 : ℕ ≃ Z4

Equations

• Anderson4D.SmoothCutoff.r324NatEquivZ4 = (Denumerable.eqv Anderson4D.Z4).symm

theorem Anderson4D.SmoothCutoff.r324ProjectedCovarianceC_eq_nat_tsum (ρ : SmoothCutoff) (ε L : ℝ) (z : T4) : ρ.r324ProjectedCovarianceC ε L z = ∑' (a : ℕ), ρ.r324HighCovarianceModeTerm ε L z (r324NatEquivZ4 a)

The projected covariance is genuinely an ℕ-indexed tsum, as required by CountableCentralRoutedMomentDecomposition.

theorem Anderson4D.SmoothCutoff.summable_r324HighCovarianceModeTerm_nat (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) (z : T4) : Summable fun (a : ℕ) => ρ.r324HighCovarianceModeTerm ε L z (r324NatEquivZ4 a)

theorem Anderson4D.SmoothCutoff.exists_r324_highCovarianceModeTerm_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε L : ℝ} {z : T4} {k : Z4}, 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → k ∈ r324HighModeSet ε L → ‖ρ.r324CovarianceModeTerm ε z k‖ ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L)

Every retained projected covariance mode carries the central Japanese-bracket payoff. The constant depends only on the fixed cutoff and includes the exact white-noise half-density squared.