OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingGlobalTrajectory.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A global similarity solution identifies the actual maximal physical flow

A path satisfying the nonlinear mild equation on every finite similarity slab determines the maximal Sobolev flow, including its point observation and endpoint.

  1. def OAI.DefocusingNLS.expandingSlabRestriction line 17
  2. theorem OAI.DefocusingNLS.exists_expanding_physical_slab line 21
  3. theorem OAI.DefocusingNLS.expandingGlobal_mem_maximal line 48
  4. theorem OAI.DefocusingNLS.expandingGlobal_maximal_observation line 61
  5. theorem OAI.DefocusingNLS.expandingGlobal_rescaled_limit line 82

    Source documentation

    A stable similarity orbit transfers to a physical solution with finite-time blowup and its prescribed limiting point observation.

    theorem expandingGlobal_rescaled_limit
    (q : ℝ → FourierL2) (x : SchrodingerTorus) (c : ℂ)
    (hq : ∀ s, 0 ≤ s → expandingTorusFunction a k (expandingRadius L s) (q s) x = c)
    (hdecay : Tendsto (fun s => ‖u s - q s‖) atTop (𝓝 0)) :
    Tendsto (fun t => (L ^ (-2 : ℝ) - t) ^ a *
      ‖sobolevTorusFunction k (maximalSobolevSchrodingerFlow k (by linarith) m f₀ t) x‖)
      (𝓝[<] (L ^ (-2 : ℝ))) (𝓝 ‖c‖) := by
…

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.expandingRadius

  6. theorem OAI.DefocusingNLS.expandingGlobal_lifespan line 96