OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeAtkinMeasure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The prime normalizer preserves the actual measure on the finite arithmetic cover. The proof transports the constructed fundamental domain.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkinImage_fundamental line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeAtkin_map_restrict line 26
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeCoverAtkin_measurePreserving line 43