OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeTraceEnergyBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual differential of the finite trace has the degree bound obtained from the sheet isometries and finite Cauchy--Schwarz.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeTraceCoordinateTerm line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceCoordinateTerm_differentiable line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeTraceCoordinateTerm_energy line 29
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeTraceSection_energy_le line 52