OAI/NumberTheory/CubicMoment/Theta/CubicThetaGlobalLocalRellich.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Compact localization of the completed global automorphic energy space in an actual injective compact chart.

  1. def OAI.CubicFirstMoment.cubicThetaGlobalEnergyTestLinear line 16
  2. lemma OAI.CubicFirstMoment.cubicThetaGlobalEnergyTestLinear_dense line 20
  3. def OAI.CubicFirstMoment.cubicThetaLocalEnergyTestLinear line 41
  4. lemma OAI.CubicFirstMoment.cubicThetaGlobalToLocal_bound line 47
  5. def OAI.CubicFirstMoment.cubicThetaGlobalToLocalEnergy line 58
  6. lemma OAI.CubicFirstMoment.cubicThetaGlobalToLocalEnergy_test line 66
  7. def OAI.CubicFirstMoment.cubicThetaGlobalLocalInclusion line 76
  8. theorem OAI.CubicFirstMoment.cubicThetaGlobalLocalInclusion_compact line 80
  9. theorem OAI.CubicFirstMoment.cubicThetaGlobalLocalInclusion_test line 86