OAI/NumberTheory/CubicMoment/Theta/CubicThetaBorelTransport.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Measurable transport of the quotient's chosen representatives back upstairs, with the actual cubic character. No smooth representative is assumed.

  1. def OAI.CubicFirstMoment.cubicThetaBorelSheet line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaBorelSheet_measurable line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaBorelSheet_cover line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaBorelSheet_disjoint line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaBorelPhase_exists line 35
  6. def OAI.CubicFirstMoment.cubicThetaBorelPhase line 43
  7. lemma OAI.CubicFirstMoment.cubicThetaBorelPhase_measurable line 46
  8. lemma OAI.CubicFirstMoment.cubicThetaBorelPhase_sheet line 49
  9. lemma OAI.CubicFirstMoment.cubicThetaBorelPhase_norm line 53
  10. lemma OAI.CubicFirstMoment.cubicThetaBorelPhase_smul line 57
  11. def OAI.CubicFirstMoment.cubicThetaBorelLift line 66
  12. lemma OAI.CubicFirstMoment.cubicThetaBorelLift_measurable line 69
  13. lemma OAI.CubicFirstMoment.cubicThetaBorelLift_norm line 73
  14. theorem OAI.CubicFirstMoment.cubicThetaBorelLift_automorphy line 77
  15. lemma OAI.CubicFirstMoment.cubicThetaBorelLift_section line 83
  16. lemma OAI.CubicFirstMoment.cubicThetaBorelLift_positive_memLp line 90