OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootWeylMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual conjugated inversion preserves the root-cover measure and the square norm of its sections.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeylImage_fundamental line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_map_restrict line 25
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootCoverWeyl_measurePreserving line 42
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootWeylSection_norm line 64
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeylSection_mass line 71