ExpandingBlowupTransfer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From a decaying similarity perturbation to a finite maximal endpoint

A decaying similarity perturbation gives an unbounded physical point observation as the physical time approaches its finite endpoint.

theorem OAI.DefocusingNLS.expandingSchrodingerTrajectory_observation line 15
theorem OAI.DefocusingNLS.expanding_profile_rescaled_limit line 42

theorem OAI.DefocusingNLS.maximalSobolev_lifespan_of_forward_rescaled_observation line 60

Source documentation

The forward maximal-flow formulation only needs existence on [0,T). Continuity of the observation excludes the endpoint itself.

theorem maximalSobolev_lifespan_of_forward_rescaled_observation
    {F : Type*} [NormedAddCommGroup F]
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2)
    (T β c : ℝ) (hT : 0 < T) (hβ : 0 < β) (hc : 0 < c)
    (hsub : Ico 0 T ⊆ maximalSobolevInteractionDomain k hk m f₀)
    (observe : FourierL2 → F) (hobs : Continuous observe)
    (hblowup : Tendsto (fun t => (T - t) ^ β *
      ‖observe (maximalSobolevSchrodingerFlow k hk m f₀ t)‖) (𝓝[<] T) (𝓝 c)) :
    BddAbove (maximalSobolevInteractionDomain k hk m f₀) ∧
      sSup (maximalSobolevInteractionDomain k hk m f₀) = T := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.maximalSobolevInteractionDomain