OAI/NumberTheory/CubicMoment/Theta/CubicThetaTangentSobolev.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The local complex energy has genuine real and imaginary Sobolev components in Euclidean Sobolev space. The change from product coordinates to the Hilbert tangent space preserves volume.

  1. lemma OAI.CubicFirstMoment.LocalSobolev.tangentCoordinates_measurePreserving line 17
  2. def OAI.CubicFirstMoment.LocalSobolev.tangentBorelVolume line 21
  3. instance OAI.CubicFirstMoment.LocalSobolev.tangentBorelVolume_finiteOnCompacts line 26
  4. def OAI.CubicFirstMoment.LocalSobolev.realTest line 34
  5. def OAI.CubicFirstMoment.LocalSobolev.imagTest line 40
  6. def OAI.CubicFirstMoment.LocalSobolev.realH1 line 46
  7. def OAI.CubicFirstMoment.LocalSobolev.imagH1 line 51
  8. lemma OAI.CubicFirstMoment.LocalSobolev.realTest_fderiv line 56
  9. lemma OAI.CubicFirstMoment.LocalSobolev.imagTest_fderiv line 65
  10. lemma OAI.CubicFirstMoment.LocalSobolev.gradient_norm_sq line 74