OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalEnergyRellich.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Rellich compactness on the completion of the actual local energy graph. No independent value and derivative data are introduced.

  1. lemma OAI.CubicFirstMoment.LocalSobolev.supported_closed line 20
  2. instance OAI.CubicFirstMoment.LocalSobolev.supported_complete line 27
  3. def OAI.CubicFirstMoment.LocalSobolev.localEnergyTest line 61
  4. lemma OAI.CubicFirstMoment.LocalSobolev.localEnergyTest_norm line 66
  5. lemma OAI.CubicFirstMoment.LocalSobolev.localEnergyTest_dense line 69
  6. lemma OAI.CubicFirstMoment.LocalSobolev.localizedSupportedPair_bound line 83
  7. def OAI.CubicFirstMoment.LocalSobolev.localEnergyToSupported line 95
  8. lemma OAI.CubicFirstMoment.LocalSobolev.localEnergyToSupported_test line 120
  9. def OAI.CubicFirstMoment.LocalSobolev.localEnergyInclusion line 148
  10. theorem OAI.CubicFirstMoment.LocalSobolev.localEnergyInclusion_compact line 151