OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/BlowupRate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A nonzero self-similar amplitude prevents continuous continuation

A positive self-similar amplitude excludes continuous continuation through the singular time.

  1. theorem OAI.DefocusingNLS.vanishing_rescaled_norm_of_left_limit line 18

    Source documentation

    A positive power times a function with a finite left limit tends to zero.

    theorem vanishing_rescaled_norm_of_left_limit {E : Type*} [NormedAddCommGroup E]
    (u : ℝ β†’ E) (T a : ℝ) (ha : 0 < a) (v : E)
    (hu : Tendsto u (𝓝[<] T) (𝓝 v)) :
    Tendsto (fun t => (T - t) ^ a * β€–u tβ€–) (𝓝[<] T) (𝓝 0) := by
…
  2. theorem OAI.DefocusingNLS.no_left_limit_of_positive_rescaled_norm line 32

    Source documentation

    In particular, the positive rescaled limit in the paper excludes a finite left limit.

    theorem no_left_limit_of_positive_rescaled_norm {E : Type*} [NormedAddCommGroup E]
    (u : ℝ β†’ E) (T a c : ℝ) (ha : 0 < a) (hc : 0 < c)
    (hblowup : Tendsto (fun t => (T - t) ^ a * β€–u tβ€–) (𝓝[<] T) (𝓝 c)) :
    Β¬ βˆƒ v, Tendsto u (𝓝[<] T) (𝓝 v) := by
…
  3. theorem OAI.DefocusingNLS.no_continuous_extension_of_positive_rescaled_norm line 43

    Source documentation

    Continuous observations of a continuously extendible trajectory have a finite left limit. Hence a positive self-similar pointwise amplitude rules out such an extension.

    theorem no_continuous_extension_of_positive_rescaled_norm
    {E F : Type*} [TopologicalSpace E] [NormedAddCommGroup F]
    (u : ℝ β†’ E) (observe : E β†’ F) (T a c : ℝ)
    (ha : 0 < a) (hc : 0 < c) (hobs : Continuous observe)
    (hblowup : Tendsto (fun t => (T - t) ^ a * β€–observe (u t)β€–)
      (𝓝[<] T) (𝓝 c)) :
    Β¬ ContinuousWithinAt u (Set.Iio T) T := by
…