CubicThetaAngularOuter.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed nonzero-angular Type-I height estimate for the original Gauss sums. Finite level summation uses the actual coefficient L1 mass; its logarithmic loss is absorbed only after the common exponent is chosen.

theorem OAI.CubicFirstMoment.angular_typeI_height_proved line 17

Source documentation

The source nonzero-angular high-height estimate, with the common support threshold and the fixed far-left Gamma hypotheses explicit.

theorem angular_typeI_height_proved
    {M : ℝ} (hMV : MontgomeryVaughanBound M) (hM : 0 ≤ M)
    {W : Eisenstein → ℝ → ℂ} (hW : UniformLogWeights W)
    (ℓ : ℤ) (hℓ : ℓ ≠ 0) {η : ℝ} (hη : 0 < η)
    (d : ℕ) {A : ℝ} (hA : 0 ≤ A) :
    ∃ K : ℝ, 0 ≤ K ∧
      ∀ (S : Finset Eisenstein) (α : Eisenstein → ℂ) (R U T : ℝ),
      1 ≤ R → 1 ≤ U → max 2 (Real.exp hW.radius) ≤ R*U → 1 ≤ T →
      T ≤ (R*U)^2 →
      (∀ r ∈ S, primary r ∧ R ≤ norm r ∧ norm r ≤ 2*R) →
      (∑ r ∈ S, ‖α r‖) ≤ A*R*(Real.log (R*U))^d →
      ((∫ t in T..2*T, ∑ r ∈ S, ‖α r‖*‖metaplecticAngularSmoothSum r ℓ (W r) U t‖)+
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.UniformLogWeights, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticAngularSmoothSum