MetaplecticCoefficientMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Injective coding of the actual published theta coefficients gives the absolute dual coefficient mass with a subpower level loss.

def OAI.CubicFirstMoment.metaplecticDecode line 12
def OAI.CubicFirstMoment.metaplecticCoefficientMassTerm line 15
lemma OAI.CubicFirstMoment.metaplecticCoefficientMassTerm_nonneg line 20
lemma OAI.CubicFirstMoment.metaplectic_coefficient_codes line 25
theorem OAI.CubicFirstMoment.metaplectic_coefficient_mass_small_power line 47
Source documentation
The absolute dual coefficient sum is derived from the literal published support formula, not postulated as a Voronoi estimate.
```
theorem metaplectic_coefficient_mass_small_power
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (ha : MetaplecticCoefficientBounds a)
    {ε σ : ℝ} (hε : 0 < ε) (hσ : 0 < σ) :
    ∃ C : ℝ, 0 < C ∧ ∀ r : Eisenstein, primary r → Squarefree r →
      Summable (metaplecticCoefficientMassTerm a r σ) ∧
      (∑' n : MetaplecticDualArgument, metaplecticCoefficientMassTerm a r σ n) ≤ C*norm r^ε := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticCoefficientBounds, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticCoefficientMassTerm, OAI.CubicFirstMoment.norm