OAI/NumberTheory/CubicMoment/Theta/CubicThetaSpatialDerivativeBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A joint Frechet derivative bound for the actual Eisenstein summands. The three proved coordinate bounds control the product-space operator norm.

  1. lemma OAI.CubicFirstMoment.cubicThetaComplexProduct_opNorm_le line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaFDeriv_coordinates line 36
  3. lemma OAI.CubicFirstMoment.cubicThetaEisensteinTerm_contDiffAt line 57
  4. lemma OAI.CubicFirstMoment.cubicThetaEisensteinGridTerm_contDiffAt line 63
  5. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGridTerm_fderiv_bound line 76