OAI/NumberTheory/CubicMoment/Theta/CubicThetaPointC1Section.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The auxiliary C1 coordinates retain the literal automorphic section and its previously constructed gradient.

  1. def OAI.CubicFirstMoment.cubicThetaSectionPointC1 line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaSectionPointC1_gradient line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaSectionPointC1_automorphy line 24
  4. lemma OAI.CubicFirstMoment.cubicThetaPointC1Gradient_continuous line 34