DispersionPoisson.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The exact arithmetic identity for dispersion

The existing lattice Poisson theorem is applied to the actual Gauss-sum rows. Conjugation reverses the mixed-character pair; the two normalized Gauss factors then cancel. The resulting identity retains the dispersion remainder explicitly.

def OAI.CubicFirstMoment.smoothedDispersionVariance line 20
theorem OAI.CubicFirstMoment.dispersionPolynomial_conj line 25

theorem OAI.CubicFirstMoment.smoothedDispersionVariance_gram line 33

Source documentation

The full lattice variance is precisely a finite quadratic form in primary character Gram entries.

theorem smoothedDispersionVariance_gram (B : Finset Eisenstein)
    (hB : ∀ b ∈ B, primary b) (β : Eisenstein → ℂ) (u : ℝ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W)
    {A : ℝ} (hA : 0 < A) :
    smoothedDispersionVariance B β u W A =
      ∑ p ∈ B, ∑ q ∈ B, dispersionAmplitude β u p * star (dispersionAmplitude β u q) *
        primaryCharacterGram q p W A := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.smoothedDispersionVariance, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.primaryCharacterGram

theorem OAI.CubicFirstMoment.primaryCharacterGram_self line 54
theorem OAI.CubicFirstMoment.dispersionAmplitude_mul_star line 72

theorem OAI.CubicFirstMoment.dispersion_diagonal line 82

Source documentation

The exact diagonal retains the coprimality condition in the lattice count.

theorem dispersion_diagonal (B : Finset Eisenstein) (hB : ∀ b ∈ B, primary b)
    (hsB : ∀ b ∈ B, Squarefree b) (β : Eisenstein → ℂ) (u : ℝ) (W : ℝ → ℂ) (A : ℝ) :
    (∑ b ∈ B, dispersionAmplitude β u b * star (dispersionAmplitude β u b) *
      primaryCharacterGram b b W A) =
      ∑ b ∈ B, ((‖β b‖^2 : ℝ) : ℂ) *
        ∑' a : Eisenstein, if primary a ∧ IsCoprime b a then W (norm a/A) else 0 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.primaryCharacterGram, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.dispersion_pair_poisson line 94

Source documentation

For a coprime pair, the normalized Gauss factors cancel against those in the lattice Poisson formula, leaving the explicit character frequency sum.

theorem dispersion_pair_poisson {p q : Eisenstein}
    (hp : primary p) (hq : primary q) (hsp : Squarefree p) (hsq : Squarefree q)
    (hpq : IsCoprime p q) (β : Eisenstein → ℂ) (u : ℝ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W)
    {A : ℝ} (hA : 0 < A) :
    dispersionAmplitude β u p * star (dispersionAmplitude β u q) *
      primaryCharacterGram q p W A =
      β p * star (β q) * normTwist u p * star (normTwist u q) *
        ((A / (9 * Real.sqrt (norm (q*p))) : ℝ) : ℂ) *
          ∑' h : Eisenstein, gramDualTerm q p W A h := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.primaryCharacterGram, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gramDualTerm

theorem OAI.CubicFirstMoment.smoothedDispersionVariance_split line 118

Source documentation

Exact separation of the diagonal from the off-diagonal quadratic form.

theorem smoothedDispersionVariance_split (B : Finset Eisenstein)
    (hB : ∀ b ∈ B, primary b) (hsB : ∀ b ∈ B, Squarefree b)
    (β : Eisenstein → ℂ) (u : ℝ) (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W) {A : ℝ} (hA : 0 < A) :
    smoothedDispersionVariance B β u W A =
      (∑ b ∈ B, ((‖β b‖^2 : ℝ) : ℂ) *
        ∑' a : Eisenstein, if primary a ∧ IsCoprime b a then W (norm a/A) else 0) +
      ∑ p ∈ B, ∑ q ∈ B.erase p,
        dispersionAmplitude β u p * star (dispersionAmplitude β u q) *
          primaryCharacterGram q p W A := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.smoothedDispersionVariance, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.primaryCharacterGram