OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoreRestriction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual global restriction to the arithmetic compact core is compact from the energy space to L2. The finite bump inequality gives norm domination by the already compact family of localizations.

  1. lemma OAI.CubicFirstMoment.indicatorOne_bound line 13
  2. def OAI.CubicFirstMoment.cubicThetaGlobalRestriction line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaGlobalRestriction_ae line 22
  4. def OAI.CubicFirstMoment.cubicThetaCoreRestriction line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaCoreMass_integral line 37
  6. lemma OAI.CubicFirstMoment.cubicThetaCoreMass_density_integrable line 47
  7. lemma OAI.CubicFirstMoment.cubicThetaCoreRestriction_norm_sq_le line 57
  8. theorem OAI.CubicFirstMoment.cubicThetaCoreRestriction_compact line 80