OAI/NumberTheory/CubicMoment/Transform/MetaplecticTailCoefficient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The literal grouped coefficient in the long inverse-completion tail. Its angular and coprimality phases are retained, while the remaining Möbius divisor sum is bounded by a proved small norm power.

  1. def OAI.CubicFirstMoment.metaplecticTailPairs line 15
  2. def OAI.CubicFirstMoment.metaplecticTailMoebius line 18
  3. def OAI.CubicFirstMoment.metaplecticTailCoefficient line 21
  4. lemma OAI.CubicFirstMoment.metaplecticTailCoefficient_factor line 26
  5. theorem OAI.CubicFirstMoment.metaplecticTailCoefficient_collect line 45

    Source documentation

    Exact collection of the two actual completion divisors into their product, for any remaining norm-weighted Gauss sum.

    theorem metaplecticTailCoefficient_collect (r : Eisenstein) (ℓ : ℤ) (C F : ℝ)
    (g : Eisenstein → ℂ) :
    (∑ c ∈ primaryElementBall F, ∑ d ∈ primaryElementBall F,
      (if C < norm c then (idealMoebius c:ℂ)*metaplecticCompletionWeight r ℓ 0 c*
        metaplecticCompletionWeight r ℓ 0 d else 0)*g (c*d)) =
      ∑ e ∈ ((primaryElementBall F).product (primaryElementBall F)).image
        (fun cd => cd.1*cd.2), metaplecticTailCoefficient r ℓ C F e*g e := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealMoebius, OAI.CubicFirstMoment.metaplecticCompletionWeight, OAI.CubicFirstMoment.metaplecticTailCoefficient

  6. lemma OAI.CubicFirstMoment.metaplecticTailMoebius_zero line 68
  7. lemma OAI.CubicFirstMoment.metaplecticTailCoefficient_zero line 76
  8. theorem OAI.CubicFirstMoment.metaplecticTailMoebius_bound line 81
  9. theorem OAI.CubicFirstMoment.metaplecticTailCoefficient_bound line 105