TypeICompleted.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual dyadic Type-I height mean, from the original smooth Gauss sum. The residue and shifted integral are derived rather than assumed. The estimate applies to one fixed smooth weight.

lemma OAI.CubicFirstMoment.metaplecticSmoothSum_continuous line 15
lemma OAI.CubicFirstMoment.dyadic_interval_decomposition_bound line 38
lemma OAI.CubicFirstMoment.dyadic_decomposition_mean line 61

theorem OAI.CubicFirstMoment.metaplectic_dyadic_height_of_published line 86

Source documentation

The actual zero-angular Type-I height estimate for one smooth weight, uniform in the squarefree level and in U,T. The residue retains its precise level decay. All analytic assumptions are published inputs.

theorem metaplectic_dyadic_height_of_published {F : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) (hGrowth : MetaplecticPolynomialGrowth F) (hHB : MetaplecticMeanSquare F)
    {ε : ℝ} (hε : 0 < ε) (hεsmall : ε < 1/12)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) (D : ℕ) :
    ∃ C E : ℝ, 0 ≤ C ∧ 0 ≤ E ∧ ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ U : ℝ, 1 ≤ U → ∀ T : ℝ, 1 ≤ T →
      ((∫ t in T..2*T, ‖metaplecticSmoothSum r W U t‖)+
       (∫ t in -(2*T)..(-T), ‖metaplecticSmoothSum r W U t‖))/T ≤
        C*U^(1/2+ε)*norm r^(1/4+2*ε)*Real.sqrt T+
        E*U^(5/6:ℝ)*norm r^(-1/6:ℝ)/T^D := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticContinuation, OAI.CubicFirstMoment.MetaplecticPolynomialGrowth, OAI.CubicFirstMoment.MetaplecticMeanSquare, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticSmoothSum, OAI.CubicFirstMoment.norm