CubicThetaCompletedLong.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual nonzero-angular long-height estimate at the exact fixed primal dilation. Coefficient, retained and tail bounds are all proved.

lemma OAI.CubicFirstMoment.sqrt_level_negative_power line 16
Also declared: OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialLong.lean:17 (same declaration text), OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialNegativeLong.lean:18 (same declaration text), OAI/NumberTheory/CubicMoment/Theta/CubicThetaUniformLong.lean:17 (same declaration text), OAI/NumberTheory/CubicMoment/Theta/CubicThetaUniformNegativeLong.lean:18 (same declaration text), OAI/NumberTheory/CubicMoment/Transform/MetaplecticUniformLong.lean:17 (same declaration text).

theorem OAI.CubicFirstMoment.cubicTheta_completed_dilated_long_mean line 33

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 cubicTheta_completed_dilated_long_mean
    {M : ℝ} (hMV : MontgomeryVaughanBound M) (hM : 0 ≤ M)
    {ℓ : ℤ} (hℓ : ℓ≠0) (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Ioi 0) (hsm : ContDiff ℝ ∞ W)
    {η B : ℝ} (hη : 0 < η) (hB : 0 ≤ B) :
    ∃ (m : ℕ) (K : ℝ), 2 ≤ m ∧ 0 ≤ K ∧
      ∀ 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.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.metaplecticAngularShift