CubicThetaUniformLong.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The uniform actual nonzero-angular long-height estimate, with its exact primal dilation and proved coefficient bounds.

lemma OAI.CubicFirstMoment.sqrt_level_negative_power line 17
Also declared: OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompletedLong.lean:16 (same declaration text), OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialLong.lean:17 (same declaration text), OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialNegativeLong.lean:18 (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.UniformLogWeights.cubicTheta_completed_dilated_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.cubicTheta_completed_dilated_long_mean
    {M : ℝ} (hMV : MontgomeryVaughanBound M) (hM : 0 ≤ M)
    {ι : Type*} {W : ι → ℝ → ℂ} (h : UniformLogWeights W) {ℓ : ℤ} (hℓ : ℓ≠0)
    {η 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)) →
      (∫ t in T..2*T, ‖metaplecticHeightCompleted r ℓ (W i) (729*X) t‖)/T ≤
…

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