TypeIOuter.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite level summation of the uniform Type-I estimate. The actual Gauss sum removes nonsquarefree levels, and the coefficient mass remains explicit.

lemma OAI.CubicFirstMoment.metaplecticSmoothSum_zero_of_not_squarefree line 14
lemma OAI.CubicFirstMoment.dyadic_finite_norm_sum line 22

theorem OAI.CubicFirstMoment.typeI_finite_levels line 41

Source documentation

A finite dyad of levels. Only the coefficient L1 mass is needed to sum the actual original smooth sums.

theorem typeI_finite_levels {W : Eisenstein → ℝ → ℂ} (hW : UniformLogWeights W)
    {F : Eisenstein → ℂ → ℂ}
    (hF : MetaplecticContinuation F) (hGrowth : MetaplecticPolynomialGrowth F) (hHB : MetaplecticMeanSquare F)
    {ε : ℝ} (hε : 0 < ε) (hεsmall : ε < 1/12) (D : ℕ) :
    ∃ C E : ℝ, 0 ≤ C ∧ 0 ≤ E ∧ ∀ (S : Finset Eisenstein) (a : Eisenstein → ℂ)
      (R U T A : ℝ), 0 < R → 1 ≤ U → 1 ≤ T →
      (∀ r ∈ S, primary r ∧ R ≤ norm r ∧ norm r ≤ 2*R) →
      (∑ r ∈ S, ‖a r‖) ≤ A →
      ((∫ 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*U^(1/2+ε)*(2*R)^(1/4+2*ε)*Real.sqrt T+
          E*U^(5/6:ℝ)*R^(-1/6:ℝ)/T^D)*A := 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