OAI/NumberTheory/CubicMoment/Theta/CubicThetaHyperbolicMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The actual invariant hyperbolic measure on positive-height points. Its density is v^-3, and arithmetic invariance follows from the proved Jacobian, not from an assumed invariant measure.

  1. def OAI.CubicFirstMoment.cubicThetaHyperbolicDensity line 20
  2. def OAI.CubicFirstMoment.cubicThetaHyperbolicMeasure line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicDensity_transform line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaHyperbolic_lintegral_change line 33
  5. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicMeasure_image line 48
  6. def OAI.CubicFirstMoment.cubicThetaPointCoordinates line 55
  7. lemma OAI.CubicFirstMoment.cubicThetaPointInclusion_measurableEmbedding line 57
  8. def OAI.CubicFirstMoment.cubicThetaPointMeasure line 63
  9. lemma OAI.CubicFirstMoment.cubicThetaPointMeasure_apply line 66
  10. lemma OAI.CubicFirstMoment.cubicThetaPointMeasure_image line 71
  11. instance OAI.CubicFirstMoment.cubicThetaPointMeasure_invariant line 87
  12. def OAI.CubicFirstMoment.cubicThetaQuotientMeasure line 101