AngularFirstMoment.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The exact fixed nonzero angular comparison from the cited published inputs.

theorem OAI.CubicFirstMoment.fixedAngularPrimeComparison_of_published line 13
theorem OAI.CubicFirstMoment.angularMainResults_of_voronoi line 40
Source documentation
Both exact angular main statements, with the zero mode supplied by the radial proof.
```
theorem angularMainResults_of_voronoi
    (hpnt : PrimaryPrimePNT) (hSWRadial : KummerPrimeSiegelWalfisz)
    (hSW : AngularKummerPrimeExplicitEstimate)
    (hModel : FixedAngularPrimeExplicitEstimate)
    (hpubRadial : PrimitiveResidueHeckeInput) (hpub : PrimitiveAngularHeckeInput)
    (hHuxley : HuxleyAdditiveLargeSieve) (hperiod : CubicSupplementaryPeriodicity)
    {C : ℝ} (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C)
    (hGI : ∀ (ℓ : ℤ) (m : ℕ),
      GammaInverseFiniteOrder (1/2-(m:ℝ)+|(ℓ:ℝ)|/2) (2+|(ℓ:ℝ)|/2))
    (hGQ : ∀ (ℓ : ℤ) (m : ℕ),
      AngularGammaQuotientStripBound (|(ℓ:ℝ)|/2) (1/2-(m:ℝ)))
    {v : Eisenstein → MetaplecticDualArgument → ℂ} (hVor : MetaplecticVoronoiInput v)
…
```
Mentions: OAI.CubicFirstMoment.PrimaryPrimePNT, OAI.CubicFirstMoment.KummerPrimeSiegelWalfisz, OAI.CubicFirstMoment.AngularKummerPrimeExplicitEstimate, OAI.CubicFirstMoment.FixedAngularPrimeExplicitEstimate, OAI.CubicFirstMoment.PrimitiveResidueHeckeInput, OAI.CubicFirstMoment.PrimitiveAngularHeckeInput, OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.CubicSupplementaryPeriodicity, OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.GammaInverseFiniteOrder, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticVoronoiInput
theorem OAI.CubicFirstMoment.angularMainResults_of_polynomial line 75
theorem OAI.CubicFirstMoment.angularComparison_of_voronoi line 97
theorem OAI.CubicFirstMoment.angularComparison_of_polynomial line 116
theorem OAI.CubicFirstMoment.angularCancellation_of_voronoi line 137
theorem OAI.CubicFirstMoment.angularCancellation_of_polynomial line 156
theorem OAI.CubicFirstMoment.angularMainResults_of_published line 177
theorem OAI.CubicFirstMoment.angularComparison_of_published line 203
theorem OAI.CubicFirstMoment.angularCancellation_of_published line 228