MetaplecticAngularOuter.lean`

3 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.

lemma OAI.CubicFirstMoment.metaplecticAngularSmoothSum_zero_of_not_squarefree line 15
lemma OAI.CubicFirstMoment.angular_level_scaling line 23

theorem OAI.CubicFirstMoment.angular_typeI_height_of_published line 30

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_of_published
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (hV : MetaplecticVoronoiInput a)
    {M : ℝ} (hMV : MontgomeryVaughanBound M) (hM : 0 ≤ M)
    {W : Eisenstein → ℝ → ℂ} (hW : UniformLogWeights W)
    (ℓ : ℤ) (hℓ : ℓ ≠ 0) {η : ℝ} (hη : 0 < η)
    (d : ℕ) {A : ℝ} (hA : 0 ≤ A) :
    ∃ (mpos mneg : ℕ) (K : ℝ), 2 ≤ mpos ∧ 2 ≤ mneg ∧ 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 →
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticVoronoiInput, OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.UniformLogWeights, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm