CubicThetaAngularConvergence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence of the fixed-angular frequency derivatives. An explicit summable lattice majorant absorbs every fixed derivative order.

lemma OAI.CubicFirstMoment.cubicThetaFrequency_inverse_pow line 11
lemma OAI.CubicFirstMoment.cubicThetaAngular_kernel_bound line 21
lemma OAI.CubicFirstMoment.cubicThetaAngular_term_bound line 52
theorem OAI.CubicFirstMoment.cubicThetaAngular_summable line 85
Source documentation
Every fixed signed angular derivative is an absolutely convergent Fourier series at each positive height.
```
theorem cubicThetaAngular_summable {a : Eisenstein → ℂ} {C v : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
    (ℓ : ℤ) (hv : 0 < v) (z : ℂ) :
    Summable (cubicThetaSeriesTerm (cubicThetaAngularCoefficient a ℓ) z v) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicThetaSeriesTerm, OAI.CubicFirstMoment.cubicThetaAngularCoefficient