OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousOutgoingMatrix.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Bounded normalized inverse for the actual outgoing value matrix

The two physical channel factors have the same modulus. Consequently conjugation by their diagonal does not enlarge an operator norm. No derivative of the inverse matrix is used in the high-derivative estimate.

  1. theorem OAI.DefocusingNLS.homogeneousTwoColumns_norm line 20
  2. def OAI.DefocusingNLS.homogeneousDiagonal line 33
  3. theorem OAI.DefocusingNLS.homogeneousDiagonal_apply line 36
  4. theorem OAI.DefocusingNLS.homogeneousDiagonal_norm line 42
  5. theorem OAI.DefocusingNLS.homogeneousDiagonal_inv_apply line 49
  6. theorem OAI.DefocusingNLS.homogeneousDiagonal_columns line 54
  7. theorem OAI.DefocusingNLS.homogeneousDiagonal_det line 61
  8. theorem OAI.DefocusingNLS.homogeneousDiagonal_valueInverse line 67
  9. theorem OAI.DefocusingNLS.homogeneousDiagonal_conjugate_norm line 86
  10. theorem OAI.DefocusingNLS.homogeneousDiagonal_remainder_norm line 102
  11. theorem OAI.DefocusingNLS.homogeneousDiagonal_commute line 120
  12. theorem OAI.DefocusingNLS.homogeneousDiagonal_robin_difference line 129
  13. theorem OAI.DefocusingNLS.homogeneousDiagonal_robin_bound line 159
  14. theorem OAI.DefocusingNLS.homogeneousValueInverse_tendsto line 173
  15. theorem OAI.DefocusingNLS.homogeneousNormalizedInverse_bound line 187