OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalRellichValue.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The compact local energy inclusion has the original localized complex section as its value, rather than an unrelated Sobolev vector.

  1. lemma OAI.CubicFirstMoment.LocalSobolev.tangentFunction_memLp line 16
  2. def OAI.CubicFirstMoment.LocalSobolev.tangentFunctionL2 line 21
  3. theorem OAI.CubicFirstMoment.LocalSobolev.complexInclusion_value line 24
  4. theorem OAI.CubicFirstMoment.LocalSobolev.localEnergyInclusion_test line 51