OAI/NumberTheory/CubicMoment/Theta/CubicThetaSpatialRegularity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual coordinate differentiability of the infinite Eisenstein series, and continuity of its constant-subtracted vertical slice.

  1. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_coordinate_hasDerivAt line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_coordinate_twice_differentiable line 33
  3. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_continuous_height line 55
  4. lemma OAI.CubicFirstMoment.cubicThetaEisensteinConstantMode_continuousAt line 65
  5. theorem OAI.CubicFirstMoment.cubicThetaEisensteinRemainder_continuous_height line 79