OAI/NumberTheory/CubicMoment/Theta/CubicThetaContinuity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Locally uniform convergence and continuity of the actual cusp Fourier series in horizontal position and positive height.

  1. def OAI.CubicFirstMoment.cubicThetaNonconstant line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaSeriesTerm_continuousAt line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaNonconstant_continuousOn_strip line 31
  4. theorem OAI.CubicFirstMoment.cubicThetaNonconstant_continuousAt line 55

    Source documentation

    The Fourier series defines a continuous function on hyperbolic 3-space.

    theorem cubicThetaNonconstant_continuousAt {a : Eisenstein → ℂ} {C : ℝ}
    (hC : 0 ≤ C) (ha : ∀ n : Eisenstein, n ≠ 0 → ‖a n‖ ≤ C*norm n)
    {p : ℂ × ℝ} (hp : 0 < p.2) : ContinuousAt (cubicThetaNonconstant a) p := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubicThetaNonconstant