OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalizationSobolevBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform Sobolev bounds for the actual localized sections. Together with the proved supported compact inclusion, these control the core localization by its hyperbolic energy graph norm.

  1. lemma OAI.CubicFirstMoment.LocalSobolev.functionEnergy_integrable line 16
  2. lemma OAI.CubicFirstMoment.LocalSobolev.compact_sobolev_bound line 30
  3. def OAI.CubicFirstMoment.LocalSobolev.localizedPair line 43
  4. lemma OAI.CubicFirstMoment.LocalSobolev.localizedPair_bound line 53