OAI/NumberTheory/CubicMoment/Theta/CubicThetaInversionSmooth.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Inversion acts on the actual compact smooth sections. Both their pointwise differential and quotient norm are transported geometrically.

  1. lemma OAI.CubicFirstMoment.cubicThetaInversionSection_norm line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaInversionSection_function line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaInversionSection_smooth line 29
  4. def OAI.CubicFirstMoment.cubicThetaInversionSmooth line 36
  5. lemma OAI.CubicFirstMoment.cubicThetaInversionSection_differential line 44
  6. lemma OAI.CubicFirstMoment.cubicThetaInversionSection_energy line 69