DispersionExpansion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact expansion of the dispersion variance

The two independent coefficient variables produce the mixed cubic character in the lattice variable. This is the algebraic starting point for applying Poisson summation, before separating cube and noncube frequencies.

def OAI.CubicFirstMoment.dispersionAmplitude line 18
theorem OAI.CubicFirstMoment.dispersion_norm_sq_expansion line 23
Source documentation
Pointwise second moment, with the character orientation fixed by the conjugation in the definition of the row polynomial.
```
theorem dispersion_norm_sq_expansion (B : Finset Eisenstein) (β : Eisenstein → ℂ)
    (u : ℝ) (a : Eisenstein) :
    ((‖dispersionPolynomial B β u a‖ ^ 2 : ℝ) : ℂ) =
      ∑ b₁ ∈ B, ∑ b₂ ∈ B,
        dispersionAmplitude β u b₁ * star (dispersionAmplitude β u b₂) *
          mixedCubic b₂ b₁ a := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.dispersionPolynomial, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.mixedCubic
theorem OAI.CubicFirstMoment.dispersion_variance_expansion line 44
Source documentation
Weighted lattice second moment as a sum over pairs of coefficients. The finite lattice support and weight are arbitrary, so smooth lattice weights and localized cell weights both fit this identity.
```
theorem dispersion_variance_expansion (A B : Finset Eisenstein)
    (W β : Eisenstein → ℂ) (u : ℝ) :
    (∑ a ∈ A, W a * ((‖dispersionPolynomial B β u a‖ ^ 2 : ℝ) : ℂ)) =
      ∑ b₁ ∈ B, ∑ b₂ ∈ B,
        dispersionAmplitude β u b₁ * star (dispersionAmplitude β u b₂) *
          ∑ a ∈ A, W a * mixedCubic b₂ b₁ a := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.dispersionPolynomial, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.mixedCubic