OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoordinateRegularity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Twice continuous coordinate differentiability of the literal Eisenstein sum, from the existing local summable derivative bounds.

  1. lemma OAI.CubicFirstMoment.cubicTheta_twice_contDiffAt_tsum line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_coordinate_contDiffAt line 35