SievedDispersion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact assembly of the sieved dispersion variance

The positive majorant is the finite sum of the square-divisor variances. This makes the collected coefficients and the restricted Poisson formula apply to the original arithmetic polynomial.

lemma OAI.CubicFirstMoment.norm_dispersionPolynomial_le line 19
lemma OAI.CubicFirstMoment.summable_restricted_dispersion line 28
def OAI.CubicFirstMoment.sievedDispersionVariance line 46

theorem OAI.CubicFirstMoment.sievedDispersionVariance_eq line 54

Source documentation

Exact finite assembly: no error term is introduced when the squarefree positive majorant is collected by its square divisor.

theorem sievedDispersionVariance_eq (C : Finset Eisenstein)
    (hC : ∀ c ∈ C, primary c ∧ Squarefree c)
    (B : Finset Eisenstein) (hB : ∀ b ∈ B, primary b)
    (β : Eisenstein → ℂ) (u : ℝ) (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W) {A : ℝ} (hA : 0 < A) :
    sievedDispersionVariance C B β u W A =
      ∑ d ∈ (C.product C).image (fun t => primarySquarefreeJoin t.1 t.2),
        (collectedSquarefreeSieveCoefficient C d : ℂ)*
          divisorDispersionVariance d B β u W A := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.sievedDispersionVariance, OAI.CubicFirstMoment.primarySquarefreeJoin, OAI.CubicFirstMoment.collectedSquarefreeSieveCoefficient, OAI.CubicFirstMoment.divisorDispersionVariance