MetaplecticCompletedLow.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The low-height completed angular estimate, derived from the actual published Voronoi identity, coefficient support, and Gamma strip bound.

lemma OAI.CubicFirstMoment.norm_tsum_le_separated line 12
lemma OAI.CubicFirstMoment.metaplectic_d_weight_summable line 32
lemma OAI.CubicFirstMoment.metaplecticDualTerm_tsum_norm_bound line 39
theorem OAI.CubicFirstMoment.uniform_metaplectic_completed_low line 60
Source documentation
All constants are chosen before the weight index, level and scale. This is the explicit form before absorbing the arbitrarily small powers.
```
theorem uniform_metaplectic_completed_low
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (hV : MetaplecticVoronoiInput a)
    {ι : Type*} {W : ι → ℝ → ℂ} (hW : UniformLogWeights W)
    (ℓ : ℤ) {ε σ : ℝ} (hε : 0 < ε) (hσ : 0 < σ) (hσs : σ < 1/10000)
    (hGamma : AngularGammaQuotientStripBound (metaplecticAngularShift ℓ) (-σ-1/6)) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ i r, primary r → Squarefree r → ∀ X : ℝ, 0 < X →
      ‖metaplecticCompleted r ℓ (W i) X-metaplecticMain r ℓ (W i) X‖ ≤
        K*Real.sqrt (norm r)*norm r^(ε+2*σ)*X^(-σ) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticVoronoiInput, OAI.CubicFirstMoment.UniformLogWeights, OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.metaplecticAngularShift, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticCompleted, OAI.CubicFirstMoment.metaplecticMain, OAI.CubicFirstMoment.norm