DivisorDispersion.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Dispersion after a square-divisor restriction

The squarefree majorant introduces d² ∣ a. Expanding the actual variance and changing variables produces a Gram kernel at scale A / N(d)², with the precise cubic-character factor retained.

def OAI.CubicFirstMoment.divisorCharacterGram line 20
def OAI.CubicFirstMoment.divisorDispersionVariance line 24
lemma OAI.CubicFirstMoment.divisorCharacterGram_scale line 29

theorem OAI.CubicFirstMoment.divisorDispersionVariance_gram line 39

Source documentation

The restricted variance is still the exact finite Gram quadratic form.

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

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.divisorDispersionVariance, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.divisorCharacterGram

theorem OAI.CubicFirstMoment.divisorDispersionVariance_scaled line 80

Source documentation

The d² restriction has norm cost N(d)² and the expected character phase. No coprimality condition is dropped in this identity.

theorem divisorDispersionVariance_scaled {d : Eisenstein} (hd : primary d)
    (B : Finset Eisenstein) (hB : ∀ b ∈ B, primary b) (β : Eisenstein → ℂ) (u : ℝ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W)
    {A : ℝ} (hA : 0 < A) :
    divisorDispersionVariance d B β u W A =
      ∑ p ∈ B, ∑ q ∈ B, dispersionAmplitude β u p*star (dispersionAmplitude β u q)*
        mixedSymbol q p (d^2)*primaryCharacterGram q p W (A/(norm d)^2) := by
…

theorem OAI.CubicFirstMoment.divisor_dispersion_common_pair_poisson line 97

Source documentation

Exact off-diagonal Poisson formula after the square-divisor sieve. The fixed d² character factor is retained even when it vanishes.

theorem divisor_dispersion_common_pair_poisson {d k a b : Eisenstein}
    (hd : primary d) (hk : primary k) (ha : primary a) (hb : primary b)
    (hsk : Squarefree k) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (β : Eisenstein → ℂ) (u : ℝ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W)
    {A : ℝ} (hA : 0 < A) :
    dispersionAmplitude β u (k*a) * star (dispersionAmplitude β u (k*b)) *
      divisorCharacterGram d (k*b) (k*a) W A =
      ∑ s ∈ (primaryPrimeFactors k).powerset,
        let m := ∏ p ∈ s, p
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.divisorCharacterGram, OAI.CubicFirstMoment.primaryPrimeFactors