OAI/NumberTheory/CubicMoment/Theta/CubicThetaMobiusSmooth.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of the literal matrix action on positive-height points.

  1. lemma OAI.CubicFirstMoment.cubicThetaMobiusDenominator_contDiff line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaMobiusNumerator_contDiff line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaMobius_contDiffAt line 28
  4. lemma OAI.CubicFirstMoment.cubicThetaMobius_contDiffOn line 38