OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingSobolevEquiv.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Coefficient-preserving identification of fixed expanding and Sobolev norms

  1. def OAI.DefocusingNLS.boundedRealDiagonalVector line 11
  2. theorem OAI.DefocusingNLS.boundedRealDiagonalVector_norm_le line 20
  3. def OAI.DefocusingNLS.boundedRealDiagonal line 33
  4. def OAI.DefocusingNLS.standardSobolevWeight line 49
  5. theorem OAI.DefocusingNLS.standardSobolevWeight_pos line 52
  6. def OAI.DefocusingNLS.expandingToSobolevRatio line 55
  7. def OAI.DefocusingNLS.sobolevToExpandingRatio line 58
  8. theorem OAI.DefocusingNLS.expandingToSobolevRatio_bounds line 61
  9. theorem OAI.DefocusingNLS.sobolevToExpandingRatio_bounds line 71
  10. def OAI.DefocusingNLS.expandingToSobolev line 82

    Source documentation

    The physical Fourier coefficients are unchanged; only their weights change.

    noncomputable def expandingToSobolev (a k : ℝ) (ha1 : a < 1) (hk : 8 < k) :
    FourierL2 →L[ℂ] FourierL2 :=
…

    Mentions: OAI.DefocusingNLS.FourierL2

  11. def OAI.DefocusingNLS.sobolevToExpanding line 87
  12. theorem OAI.DefocusingNLS.expandingToSobolev_apply line 92
  13. theorem OAI.DefocusingNLS.sobolevToExpanding_apply line 96
  14. theorem OAI.DefocusingNLS.sobolevToExpanding_expandingToSobolev line 100
  15. theorem OAI.DefocusingNLS.expandingToSobolev_sobolevToExpanding line 112
  16. def OAI.DefocusingNLS.expandingSobolevEquiv line 124
  17. theorem OAI.DefocusingNLS.expandingToSobolev_coefficient line 134