OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalEnergyGraph.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The local graph of genuine compact smooth sections and its closed Hilbert energy space. The value and derivative entries remain tied to the same localized section throughout the construction.

  1. abbrev OAI.CubicFirstMoment.CubicThetaLocalEnergyAmbient line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyJet_add line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaLocalEnergyJet_smul line 22
  4. lemma OAI.CubicFirstMoment.cubicThetaTestLocalization_add line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaTestLocalization_smul line 35
  6. lemma OAI.CubicFirstMoment.cubicThetaLocalSectionJet_memLp line 41
  7. def OAI.CubicFirstMoment.cubicThetaLocalEnergyGraph line 49
  8. def OAI.CubicFirstMoment.cubicThetaLocalEnergySpace line 77
  9. instance OAI.CubicFirstMoment.cubicThetaLocalEnergySpace_complete line 83