OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeInvariantDilation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Scalar integration for the actual dilation. This is used for the invariant derivative energy as well as the mass density.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeDilation_inversion_atkin line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeScalarAtkin_integrable line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeScalarAtkin_integral line 32
  4. lemma OAI.CubicFirstMoment.cubicThetaScalarInversion_invariant line 43
  5. lemma OAI.CubicFirstMoment.cubicThetaScalarInversion_integrable line 49
  6. lemma OAI.CubicFirstMoment.cubicThetaScalarInversion_integral line 58
  7. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeScalarDilation_integrable line 68
  8. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeScalarDilation_integral line 80