OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeEnergyRestriction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Original compact smooth sections restrict to finite-energy prime sections. Both mass and derivative energy scale by the exact covering degree.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeSmoothC1 line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeSmoothC1_energy line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeSmoothC1_gradient_memLp line 31
  4. def OAI.CubicFirstMoment.cubicThetaPrimeSmoothEnergyRestriction line 44
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeSmoothEnergy_gradient_norm_sq line 52
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimeSmoothEnergyRestriction_norm_sq line 67