MetaplecticLowPowers.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary small-power absorption in the polynomial scale range.

lemma OAI.CubicFirstMoment.metaplectic_low_scale_power line 9

theorem OAI.CubicFirstMoment.uniform_metaplectic_completed_subpower line 31

Source documentation

The low-height completed estimate with arbitrary small losses, for every fixed angular mode and every polynomial scale range.

theorem uniform_metaplectic_completed_subpower
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (hV : MetaplecticVoronoiInput a)
    {ι : Type*} {W : ι → ℝ → ℂ} (hW : UniformLogWeights W) (ℓ : ℤ)
    (hGamma : ∀ σ : ℝ, 0 < σ → σ < 1/10000 →
      AngularGammaQuotientStripBound (metaplecticAngularShift ℓ) (-σ-1/6))
    {ε B : ℝ} (hε : 0 < ε) (hB : 0 ≤ B) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ i r, primary r → Squarefree r →
      ∀ Y X : ℝ, 1 ≤ Y → 0 < X → norm r ≤ Y^B → Y^(-B) ≤ X →
        ‖metaplecticCompleted r ℓ (W i) X-metaplecticMain r ℓ (W i) X‖ ≤
          K*Y^ε*Real.sqrt (norm r) := 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.norm, OAI.CubicFirstMoment.metaplecticCompleted, OAI.CubicFirstMoment.metaplecticMain