OAI/NumberTheory/CubicMoment/Theta/CubicThetaComplexLocalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The compact chart inclusion also respects the complex scalar action. The extension is identified on the dense genuine smooth sections.

  1. theorem OAI.CubicFirstMoment.valueMemLp line 21
  2. def OAI.CubicFirstMoment.cubicThetaLocalValue line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaLocalValue_apply line 52
  4. lemma OAI.CubicFirstMoment.cubicThetaLocalValue_bound line 64
  5. def OAI.CubicFirstMoment.cubicThetaComplexLocalInclusion line 70
  6. lemma OAI.CubicFirstMoment.cubicThetaComplexLocalInclusion_test line 77
  7. theorem OAI.CubicFirstMoment.cubicThetaComplexLocalInclusion_eq line 85
  8. theorem OAI.CubicFirstMoment.cubicThetaComplexLocalInclusion_compact line 98