Fourier configurations of an R-324 covariance product

For one full doubled pairing, the covariance part of the deterministic moment integrand is a finite product of cutoff covariances. This file expands that product as one absolutely convergent tsum over a finite assignment of lattice modes. It is the concrete Fourier-configuration space used in paper §4.2, Step 4.

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324PairIndex {m : ℕ} (κ : PartialPairing (Fin (2 * m))) : Type

The lower endpoints used to count every pair exactly once.

Equations

• Anderson4D.SmoothCutoff.R324PairIndex κ = ↥({j ∈ κ.pairSupport | j < κ j})

noncomputable def Anderson4D.SmoothCutoff.r324PairFinEquiv {m : ℕ} (κ : PartialPairing (Fin (2 * m))) : Fin {j ∈ κ.pairSupport | j < κ j}.card ≃ R324PairIndex κ

A deterministic enumeration of the lower endpoints of a pairing.

Equations

• Anderson4D.SmoothCutoff.r324PairFinEquiv κ = {j ∈ κ.pairSupport | j < κ j}.equivFin.symm

noncomputable def Anderson4D.SmoothCutoff.r324PairModeTerm (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) (j : Fin {i ∈ κ.pairSupport | i < κ i}.card) (k : Z4) : ℂ

The covariance Fourier mode attached to one enumerated pair.

Equations

• ρ.r324PairModeTerm ε κ v j k = ρ.r324CovarianceModeTerm ε (v ↑((Anderson4D.SmoothCutoff.r324PairFinEquiv κ) j) - v (κ ↑((Anderson4D.SmoothCutoff.r324PairFinEquiv κ) j))) k

noncomputable def Anderson4D.SmoothCutoff.r324CovarianceFourierConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) : ℂ

One Fourier configuration of a complete covariance product.

Equations

• ρ.r324CovarianceFourierConfigurationTerm ε κ v q = Anderson4D.finSeriesAssignmentTerm {i ∈ κ.pairSupport | i < κ i}.card (ρ.r324PairModeTerm ε κ v) q

theorem Anderson4D.SmoothCutoff.summable_norm_r324PairModeTerm (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) (j : Fin {i ∈ κ.pairSupport | i < κ i}.card) : Summable fun (k : Z4) => ‖ρ.r324PairModeTerm ε κ v j k‖

Every individual pair-mode series is absolutely convergent.

theorem Anderson4D.SmoothCutoff.summable_norm_r324CovarianceFourierConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) : Summable fun (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) => ‖ρ.r324CovarianceFourierConfigurationTerm ε κ v q‖

The full configuration series is absolutely convergent.

theorem Anderson4D.SmoothCutoff.summable_r324CovarianceFourierConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) : Summable (ρ.r324CovarianceFourierConfigurationTerm ε κ v)

In particular the complex configuration series is summable.

theorem Anderson4D.SmoothCutoff.primitiveCovarianceProduct_eq_r324_configuration_tsum (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) : ↑(primitiveCovarianceProduct ρ ε m κ v) = ∑' (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4), ρ.r324CovarianceFourierConfigurationTerm ε κ v q

Exact Fourier expansion of every covariance factor in a doubled pairing. No Fubini across physical integration is used here: this is a pointwise, absolutely convergent identity.