OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousComplexification.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Complexification of actual real-linear operators on Y

The doubled complex space uses its existing product norm. The factor two in the norm estimate is harmless for the later fixed long-time contraction.

  1. def OAI.DefocusingNLS.homogeneousComplexificationReal line 22
  2. theorem OAI.DefocusingNLS.homogeneousComplexificationReal_apply line 27
  3. theorem OAI.DefocusingNLS.homogeneousComplexificationReal_I line 31
  4. def OAI.DefocusingNLS.homogeneousComplexification line 42
  5. theorem OAI.DefocusingNLS.homogeneousComplexification_apply line 66
  6. theorem OAI.DefocusingNLS.homogeneousComplexification_real line 70
  7. theorem OAI.DefocusingNLS.homogeneousComplexification_imag line 77
  8. theorem OAI.DefocusingNLS.homogeneousComplexification_id line 86
  9. theorem OAI.DefocusingNLS.homogeneousComplexification_comp line 96
  10. theorem OAI.DefocusingNLS.homogeneousComplexification_add line 109
  11. theorem OAI.DefocusingNLS.homogeneousComplexification_apply_norm_le line 119
  12. theorem OAI.DefocusingNLS.homogeneousComplexification_norm_le line 136