OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeAtkinEnergyInvolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The prime Atkin pullback is involutive on actual sections and their energy completion. It preserves the mass and derivative sesquilinear forms.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinMatrix_eq line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinPoint_involutive line 25
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinSection_involutive line 36
  4. theorem OAI.CubicFirstMoment.cubicThetaPrimeAtkinEnergy_involutive line 45
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinEnergy_mass_norm line 58
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinEnergy_mass_inner line 66
  7. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinEnergy_derivative_norm line 75
  8. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinEnergy_derivative_inner line 85