OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingInitialData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Physical initial data as a continuous linear equivalence

For a fixed starting scale this map restores the physical amplitude and changes the exact expanding Fourier norm to the standard Sobolev norm.

  1. def OAI.DefocusingNLS.expandingPhysicalInitialEquiv line 15
  2. theorem OAI.DefocusingNLS.expandingPhysicalInitialEquiv_apply line 23
  3. theorem OAI.DefocusingNLS.expandingSchrodingerTrajectory_initial_equiv line 29
  4. theorem OAI.DefocusingNLS.expandingPhysicalInitialEquiv_isOpen_image line 37

    Source documentation

    Open sets in the exact starting norm give open sets of physical H^k data.

    theorem expandingPhysicalInitialEquiv_isOpen_image (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L)
    (V : Set FourierL2) (hV : IsOpen V) :
    IsOpen (expandingPhysicalInitialEquiv a k L ha ha1 hk hL '' V) :=
…

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingPhysicalInitialEquiv

  5. theorem OAI.DefocusingNLS.expandingPhysicalInitialEquiv_nonempty_image line 43