TypeIFinal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The Type-I height bound with the paper's exponents, obtained by absorbing the fixed logarithmic coefficient loss.

lemma OAI.CubicFirstMoment.typeI_log_power_bound line 12
lemma OAI.CubicFirstMoment.typeI_principal_log_bound line 38

theorem OAI.CubicFirstMoment.typeI_height_of_published line 54

Source documentation

The literal zero-angular Type-I height estimate. The coefficient hypothesis is its explicit divisor-bounded L1 consequence; all analytic inputs are the cited published continuation and HB estimates.

theorem typeI_height_of_published {W : Eisenstein → ℝ → ℂ} (hW : UniformLogWeights W)
    {F : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) (hGrowth : MetaplecticPolynomialGrowth F) (hHB : MetaplecticMeanSquare F)
    {ε : ℝ} (hε : 0 < ε) (D B : ℕ) {K : ℝ} (hK : 0 ≤ K) :
    ∃ C E : ℝ, 0 ≤ C ∧ 0 ≤ E ∧ ∀ (S : Finset Eisenstein) (a : Eisenstein → ℂ)
      (R U T : ℝ), 1 ≤ R → 1 ≤ U → 1 ≤ T →
      (∀ r ∈ S, primary r ∧ R ≤ norm r ∧ norm r ≤ 2*R) →
      (∑ r ∈ S, ‖a r‖) ≤ K*R*(Real.log (R*U))^B →
      ((∫ t in T..2*T, ∑ r ∈ S, ‖a r‖*‖metaplecticSmoothSum r (W r) U t‖)+
       (∫ t in -(2*T)..(-T), ∑ r ∈ S, ‖a r‖*‖metaplecticSmoothSum r (W r) U t‖))/T ≤
        C*(R*U)^(1/2+ε)*R^(3/4:ℝ)*Real.sqrt T+
        E*(R*U)^(5/6:ℝ)*(Real.log (R*U))^B/T^D := by
…

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