OAI/NumberTheory/CubicMoment/Theta/CubicThetaPointC1.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

C1 functions on the hyperbolic upper half-space, used only to transport the actual gradients through the finite Hecke correspondence.

  1. def OAI.CubicFirstMoment.cubicThetaPointFunction line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaPointFunction_apply line 17
  3. def OAI.CubicFirstMoment.cubicThetaPointC1 line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaPointC1_differentiable line 30
  5. def OAI.CubicFirstMoment.cubicThetaPointC1Gradient line 35
  6. lemma OAI.CubicFirstMoment.cubicThetaPointC1Gradient_norm_sq line 48
  7. def OAI.CubicFirstMoment.cubicThetaPointC1Pullback line 58
  8. lemma OAI.CubicFirstMoment.cubicThetaPointC1Pullback_function line 71
  9. lemma OAI.CubicFirstMoment.cubicThetaPointC1Pullback_gradient_norm line 79
  10. theorem OAI.CubicFirstMoment.cubicThetaPointC1Pullback_gradient_pair line 97