OAI/NumberTheory/CubicMoment/Theta/CubicThetaLocalizationLinear.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Real linearity of the actual localized Sobolev vectors, with their fixed compact support retained in the codomain.

  1. def OAI.CubicFirstMoment.LocalSobolev.localizedRealTest line 19
  2. def OAI.CubicFirstMoment.LocalSobolev.localizedImagTest line 38
  3. def OAI.CubicFirstMoment.LocalSobolev.localizedRealH1 line 57
  4. def OAI.CubicFirstMoment.LocalSobolev.localizedImagH1 line 61
  5. def OAI.CubicFirstMoment.LocalSobolev.localizedRealSupported line 65
  6. def OAI.CubicFirstMoment.LocalSobolev.localizedImagSupported line 71
  7. def OAI.CubicFirstMoment.LocalSobolev.localizedSupportedPair line 77
  8. lemma OAI.CubicFirstMoment.LocalSobolev.localizedSupportedPair_norm line 81