OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLogJetOperations.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Linear maps and polynomial operations on logarithmic jet bounds

These operations apply the checked scalar jet bounds to the two-channel coefficient matrices of the original radial equation.

  1. theorem OAI.DefocusingNLS.HasLogJetBound.map line 24
  2. theorem OAI.DefocusingNLS.HasLogJetBound.pair line 37
  3. theorem OAI.DefocusingNLS.HasLogJetBound.conj line 44
  4. theorem OAI.DefocusingNLS.HasLogJetBound.const_mul line 49
  5. theorem OAI.DefocusingNLS.HasLogJetBound.pow line 53
  6. theorem OAI.DefocusingNLS.HasLogJetBound.twoColumns line 61