CubicThetaAngularContinuity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Locally uniform convergence for the fixed-angular theta expansion.

lemma OAI.CubicFirstMoment.cubicThetaAngular_continuousOn_strip line 9
theorem OAI.CubicFirstMoment.cubicThetaAngular_continuousAt line 41
Source documentation
The fixed signed angular Fourier expansion is a continuous function at every point of the upper half-space.
```
theorem cubicThetaAngular_continuousAt {a : Eisenstein → ℂ} {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
    (ℓ : ℤ) {p : ℂ × ℝ} (hp : 0 < p.2) :
    ContinuousAt (cubicThetaNonconstant (cubicThetaAngularCoefficient a ℓ)) p := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicThetaNonconstant, OAI.CubicFirstMoment.cubicThetaAngularCoefficient