OAI/NumberTheory/CubicMoment/Theta/CubicThetaSupportedTangent.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported complex chart sections give actual supported real Sobolev vectors. The Euclidean Rellich theorem applies to these vectors, with the concrete transported compact support.

  1. lemma OAI.CubicFirstMoment.LocalSobolev.supported_test line 17
  2. lemma OAI.CubicFirstMoment.LocalSobolev.realTest_support line 36
  3. lemma OAI.CubicFirstMoment.LocalSobolev.imagTest_support line 43
  4. def OAI.CubicFirstMoment.LocalSobolev.realSupported line 50
  5. def OAI.CubicFirstMoment.LocalSobolev.imagSupported line 56
  6. lemma OAI.CubicFirstMoment.LocalSobolev.supported_inclusion_compact line 62