OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingScaleTransfer.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Canonical transfer between expanding-torus norms

The transfer keeps the physical Fourier coefficients in normalized coordinates and has the exact growth bound (M / L)^a when 1 ≤ L ≤ M.

  1. theorem OAI.DefocusingNLS.expandingSobolevWeightSq_scale_le line 15
  2. theorem OAI.DefocusingNLS.expandingSobolevWeight_scale_le line 38
  3. def OAI.DefocusingNLS.expandingScaleRatio line 56
  4. theorem OAI.DefocusingNLS.expandingScaleRatio_nonneg line 59
  5. theorem OAI.DefocusingNLS.expandingScaleRatio_le line 65
  6. def OAI.DefocusingNLS.expandingTransferVector line 71
  7. theorem OAI.DefocusingNLS.expandingTransferVector_apply line 82
  8. theorem OAI.DefocusingNLS.expandingTransferVector_norm_le line 88
  9. def OAI.DefocusingNLS.expandingScaleTransfer line 106

    Source documentation

    Continuous complex-linear transfer with the physical coefficients fixed.

    noncomputable def expandingScaleTransfer (a k L M : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hLM : L ≤ M) : FourierL2 →L[ℂ] FourierL2 :=
…

    Mentions: OAI.DefocusingNLS.FourierL2

  10. theorem OAI.DefocusingNLS.expandingScaleTransfer_norm_le line 121
  11. theorem OAI.DefocusingNLS.expandingScaleTransfer_coefficient line 128
  12. theorem OAI.DefocusingNLS.expandingScaleTransfer_function line 144

    Source documentation

    Transfer represents the same function in normalized torus coordinates.

    theorem expandingScaleTransfer_function (a k L M : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (hLM : L ≤ M)
    (f : FourierL2) :
    expandingTorusFunction a k M (expandingScaleTransfer a k L M ha hk hL hLM f) =
      expandingTorusFunction a k L f := by
…

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.expandingScaleTransfer

  13. theorem OAI.DefocusingNLS.expandingCoefficient_injective line 153
  14. theorem OAI.DefocusingNLS.expandingScaleTransfer_self line 161
  15. theorem OAI.DefocusingNLS.expandingScaleTransfer_comp line 171

    Source documentation

    Canonical scale changes compose without an additional normalization.

    theorem expandingScaleTransfer_comp (a k L M N : ℝ)
    (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L) (hLM : L ≤ M) (hMN : M ≤ N) :
    (expandingScaleTransfer a k M N ha hk (hL.trans hLM) hMN).comp
        (expandingScaleTransfer a k L M ha hk hL hLM) =
      expandingScaleTransfer a k L N ha hk hL (hLM.trans hMN) := by
…

    Mentions: OAI.DefocusingNLS.expandingScaleTransfer