OAI/NumberTheory/CubicMoment/Theta/CubicThetaBorelInversion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual inversion operator on quotient representatives, including the cubic phase of the chosen Borel section.

  1. def OAI.CubicFirstMoment.cubicThetaBorelInversionFunction line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaBorelInversionFunction_measurable line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaBorelInversionFunction_norm line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaBorelInversionFunction_lift line 28
  5. lemma OAI.CubicFirstMoment.cubicThetaBorelInversionFunction_memLp line 38
  6. def OAI.CubicFirstMoment.cubicThetaBorelInversionLinear line 46
  7. lemma OAI.CubicFirstMoment.cubicThetaBorelInversionLinear_norm line 84
  8. def OAI.CubicFirstMoment.cubicThetaBorelInversion line 99
  9. theorem OAI.CubicFirstMoment.cubicThetaBorelInversion_lift line 102