SobolevContinuation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform local lifespans and continuation of Sobolev interaction solutions

theorem OAI.DefocusingNLS.exists_uniform_sobolevInteraction_time line 12

Source documentation

Every bounded set of initial data has one common positive local lifespan, at every time.

theorem exists_uniform_sobolevInteraction_time (k : ℝ) (hk : 6 < k) (m : ℕ)
    (R : ℝ) (hR : 0 ≤ R) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (t₀ : ℝ) (f₀ : FourierL2), ‖f₀‖ ≤ R →
      ∃ v : ℝ → FourierL2, v t₀ = f₀ ∧
        ∀ t ∈ Ioo (t₀ - δ) (t₀ + δ),
          HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t := by
…

Mentions: OAI.DefocusingNLS.FourierL2

def OAI.DefocusingNLS.HasSobolevInteractionContinuation line 72
Source documentation
A right continuation is a classical solution across the endpoint agreeing on a left neighborhood.
```
def HasSobolevInteractionContinuation (k : ℝ) (hk : 6 < k) (m : ℕ)
    (v : ℝ → FourierL2) (T : ℝ) : Prop :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2

theorem OAI.DefocusingNLS.sobolevInteraction_continuation_from_overlap line 80

Source documentation

A local solution started before the endpoint and lasting beyond it continues the original one.

theorem sobolevInteraction_continuation_from_overlap
    (k : ℝ) (hk : 6 < k) (m : ℕ) (v w : ℝ → FourierL2)
    (a T t₀ δ : ℝ) (ht₀ : t₀ ∈ Ioo a T) (hT : T < t₀ + δ)
    (hv : ∀ t ∈ Ioo a T, HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t)
    (hw : ∀ t ∈ Ioo (t₀ - δ) (t₀ + δ),
      HasDerivAt w (schrodingerInteractionField k hk m t (w t)) t)
    (heq : v t₀ = w t₀) : HasSobolevInteractionContinuation k hk m v T := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.HasSobolevInteractionContinuation

theorem OAI.DefocusingNLS.sobolevInteraction_continuation_of_bounded line 116

Source documentation

A finite right endpoint with bounded Sobolev norm is extendible.

theorem sobolevInteraction_continuation_of_bounded
    (k : ℝ) (hk : 6 < k) (m : ℕ) (v : ℝ → FourierL2)
    (a T R : ℝ) (haT : a < T) (hR : 0 ≤ R)
    (hv : ∀ t ∈ Ioo a T, HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t)
    (hb : ∀ t ∈ Ioo a T, ‖v t‖ ≤ R) : HasSobolevInteractionContinuation k hk m v T := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.HasSobolevInteractionContinuation

theorem OAI.DefocusingNLS.sobolevInteraction_norm_tendsto_atTop line 139

Source documentation

A nonextendible finite endpoint forces the Sobolev norm to diverge.

theorem sobolevInteraction_norm_tendsto_atTop
    (k : ℝ) (hk : 6 < k) (m : ℕ) (v : ℝ → FourierL2)
    (a T : ℝ) (haT : a < T)
    (hv : ∀ t ∈ Ioo a T, HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t)
    (hmax : ¬ HasSobolevInteractionContinuation k hk m v T) :
    Tendsto (fun t => ‖v t‖) (𝓝[<] T) atTop := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.HasSobolevInteractionContinuation