NormSeries.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

These elementary lattice bounds provide a quantitative tail for the Möbius residue sum after square-divisor truncation.

lemma OAI.CubicFirstMoment.eisenstein_norm_eq_sq line 18
instance OAI.CubicFirstMoment.eisenstein_discreteTopology line 21
theorem OAI.CubicFirstMoment.summable_eisenstein_norm_rpow line 39
Source documentation
The norm is the squared complex absolute value, so the convergence threshold for its negative powers is one.
```
theorem summable_eisenstein_norm_rpow {s : ℝ} (hs : 1 < s) :
    Summable (fun a : Eisenstein => norm a^(-s)) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm
lemma OAI.CubicFirstMoment.norm_rpow_tail_pointwise line 57
theorem OAI.CubicFirstMoment.eisenstein_norm_rpow_tail line 72
Source documentation
A stronger convergent exponent gives a power tail without losing a factor to the norm fibers.
```
theorem eisenstein_norm_rpow_tail {D s t : ℝ} (hD : 0 < D)
    (hs : 1 < s) (hst : s < t) :
    (∑' a : Eisenstein, if D < norm a then norm a^(-t) else 0) ≤
      D^(s-t)*(∑' a : Eisenstein, norm a^(-s)) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm