OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousComplexCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Concrete complexification coordinates for the faithful homogeneous space

The two complex channels encode x+i y by (x+i y, J x+i J y), where J is physical conjugation. Both real coordinates are bounded by the product norm.

  1. theorem OAI.DefocusingNLS.homogeneousConjugation_complex_smul line 23
  2. def OAI.DefocusingNLS.homogeneousComplexReal line 31
  3. def OAI.DefocusingNLS.homogeneousComplexImag line 35
  4. theorem OAI.DefocusingNLS.homogeneousComplexReal_apply line 39
  5. theorem OAI.DefocusingNLS.homogeneousComplexImag_apply line 42
  6. theorem OAI.DefocusingNLS.homogeneousComplexCoordinates_first line 45
  7. theorem OAI.DefocusingNLS.homogeneousComplexCoordinates_second line 54
  8. theorem OAI.DefocusingNLS.homogeneousComplexReal_I line 64
  9. theorem OAI.DefocusingNLS.homogeneousComplexImag_I line 71
  10. theorem OAI.DefocusingNLS.homogeneousComplexReal_norm_le line 79
  11. theorem OAI.DefocusingNLS.homogeneousComplexImag_norm_le line 88