OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalRellich.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The two supported real Sobolev components give a compact complex L2 inclusion on every concrete compact coordinate set.

  1. abbrev OAI.CubicFirstMoment.LocalSobolev.Supported line 15
  2. abbrev OAI.CubicFirstMoment.LocalSobolev.TangentComplexL2 line 19
  3. def OAI.CubicFirstMoment.LocalSobolev.realSupportedInclusion line 21
  4. def OAI.CubicFirstMoment.LocalSobolev.complexInclusion line 26
  5. theorem OAI.CubicFirstMoment.LocalSobolev.complexInclusion_compact line 33