CorrectedSquareExpansion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual correction model and mixed term in the positive square. Only its first term is enlarged by the square-divisor majorant.

lemma OAI.CubicFirstMoment.correction_model_square line 12
lemma OAI.CubicFirstMoment.correction_mixed_real line 28
theorem OAI.CubicFirstMoment.corrected_dispersion_finite_majorant line 45

theorem OAI.CubicFirstMoment.corrected_dispersion_finite_error line 80

Source documentation

The three genuine model terms cancel after the positive and mixed terms have each been identified with the same squarefree mass.

theorem corrected_dispersion_finite_error (A C B : Finset Eisenstein)
    (hA : ∀ a ∈ A, primary a) (hC : ∀ c ∈ C, primary c) (h1 : 1 ∈ C)
    (W : Eisenstein → ℝ) (hW : ∀ a ∈ A, 0 ≤ W a)
    (β : Eisenstein → ℂ) (u E₁ E₂ : ℝ)
    (hpositive : |(∑ a ∈ A, (truncatedSquareDivisorSum C a)^2*W a*
        ‖dispersionPolynomial B β u a‖^2)-
      (cStar^2*‖dispersionModel B β u‖^2)*
        (∑ a ∈ A, (idealMoebius a:ℝ)^2*W a*norm a^(-1/3:ℝ))| ≤ E₁)
    (hmixed : ‖(cStar:ℂ)*star (dispersionModel B β u)*
        (∑ a ∈ A, (idealMoebius a:ℂ)^2*(W a:ℂ)*gauss a*
          ((norm a^(-1/6:ℝ):ℝ):ℂ)*dispersionPolynomial B β u a)-
      (((cStar^2*‖dispersionModel B β u‖^2)*
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.truncatedSquareDivisorSum, OAI.CubicFirstMoment.dispersionPolynomial, OAI.CubicFirstMoment.cStar, OAI.CubicFirstMoment.dispersionModel, OAI.CubicFirstMoment.idealMoebius, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss