OAI/NumberTheory/CubicMoment/Theta/CubicThetaInversionFiniteEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Global inversion on actual finite-energy C1 sections. This bridges the completed inversion to the literal functions occurring in the Hecke trace.

  1. lemma OAI.CubicFirstMoment.cubicThetaInversionSection_c1 line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaInversionPointC1 line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaInversionSection_C1energy line 23
  4. def OAI.CubicFirstMoment.cubicThetaInversionFinite line 34
  5. def OAI.CubicFirstMoment.cubicThetaInversionFiniteLinear line 44
  6. lemma OAI.CubicFirstMoment.cubicThetaInversionFinite_value_norm line 49
  7. lemma OAI.CubicFirstMoment.cubicThetaInversionFinite_gradient_norm line 55
  8. lemma OAI.CubicFirstMoment.cubicThetaInversionFinite_embedding_norm line 64