MetaplecticUniformNegativeLong.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The negative-height completed long-polynomial angular estimate, with the actual retained transform and actual discarded tail both discharged.

lemma OAI.CubicFirstMoment.sqrt_level_negative_power_negative line 17

theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_completed_negative_long_mean line 34

Source documentation

For each small loss, the far-left line is chosen once before all levels, lengths and heights. Its Gamma bounds are exactly the published bounded-strip input at that chosen line.

theorem UniformLogWeights.metaplectic_completed_negative_long_mean
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (hV : MetaplecticVoronoiInput a)
    {M : ℝ} (hMV : MontgomeryVaughanBound M) (hM : 0 ≤ M)
    {ι : Type*} {W : ι → ℝ → ℂ} (h : UniformLogWeights W) (ℓ : ℤ)
    {η B : ℝ} (hη : 0 < η) (hB : 0 ≤ B) :
    ∃ (m : ℕ) (K : ℝ), 2 ≤ m ∧ 0 ≤ K ∧
      ∀ i, ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ Y X T : ℝ, 1 ≤ Y → 0 < X → 1 ≤ T →
      norm r ≤ Y^B → T ≤ Y^B → Y^(-B) ≤ X →
      Real.sqrt (norm r)*T^2 ≤ X →
      AngularGammaQuotientStripBound (metaplecticAngularShift ℓ-1/6) (-((m:ℝ)-1/2)) →
      AngularGammaQuotientStripBound (metaplecticAngularShift ℓ+1/6) (-((m:ℝ)-1/2)) →
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticVoronoiInput, OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.UniformLogWeights, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.metaplecticAngularShift