OAI/NumberTheory/CubicMoment/Theta/CubicThetaInversionEnergyInvolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Inversion is an involutive isometry of the actual energy space and preserves its mass form. It therefore preserves every spectral kernel.

  1. lemma OAI.CubicFirstMoment.cubicThetaFullInversion_involutive line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaInversionSection_involutive line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaInversionSmooth_involutive line 31
  4. theorem OAI.CubicFirstMoment.cubicThetaInversionEnergy_involutive line 36
  5. lemma OAI.CubicFirstMoment.cubicThetaInversionEnergy_mass_norm line 47
  6. lemma OAI.CubicFirstMoment.cubicThetaInversionEnergy_mass_inner line 60
  7. lemma OAI.CubicFirstMoment.cubicThetaInversionEnergy_pencil_inner line 68
  8. theorem OAI.CubicFirstMoment.cubicThetaInversionEnergy_kernel line 81