MaximalSobolevEndpoint.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite endpoints of the maximal Sobolev solution

theorem OAI.DefocusingNLS.maximalSobolevInteractionFlow_not_continuable line 13

Source documentation

A finite right boundary of the maximal solution domain cannot be continued across.

theorem maximalSobolevInteractionFlow_not_continuable
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2) (a T : ℝ)
    (ha : a < 0) (hT : 0 < T)
    (hsub : Ioo a T ⊆ maximalSobolevInteractionDomain k hk m f₀)
    (hnot : T ∉ maximalSobolevInteractionDomain k hk m f₀) :
    ¬ HasSobolevInteractionContinuation k hk m (maximalSobolevInteractionFlow k hk m f₀) T := by
…

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

theorem OAI.DefocusingNLS.maximalSobolevInteractionFlow_norm_tendsto_atTop line 62

Source documentation

The Sobolev norm diverges at a finite right boundary of the actual maximal solution.

theorem maximalSobolevInteractionFlow_norm_tendsto_atTop
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2) (a T : ℝ)
    (ha : a < 0) (hT : 0 < T)
    (hsub : Ioo a T ⊆ maximalSobolevInteractionDomain k hk m f₀)
    (hnot : T ∉ maximalSobolevInteractionDomain k hk m f₀) :
    Tendsto (fun t => ‖maximalSobolevInteractionFlow k hk m f₀ t‖) (𝓝[<] T) atTop := by
…

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

def OAI.DefocusingNLS.maximalSobolevSchrodingerFlow line 74
Source documentation
Return the maximal interaction solution to the physical Schrödinger variable.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:232 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.maximalSobolevSchrodingerFlow@path.
```
noncomputable def maximalSobolevSchrodingerFlow (k : ℝ) (hk : 6 < k) (m : ℕ)
    (f₀ : FourierL2) (t : ℝ) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.maximalSobolevSchrodingerFlow_initial line 78
theorem OAI.DefocusingNLS.hasDerivAt_maximalSobolevSchrodingerFlow line 82
theorem OAI.DefocusingNLS.maximalSobolevSchrodingerFlow_norm_tendsto_atTop line 91

theorem OAI.DefocusingNLS.bounded_maximalSobolevDomain_endpoint line 101

Source documentation

If the maximal time domain is bounded above, its supremum is a positive excluded endpoint.

theorem bounded_maximalSobolevDomain_endpoint (k : ℝ) (hk : 6 < k) (m : ℕ)
    (f₀ : FourierL2) (hb : BddAbove (maximalSobolevInteractionDomain k hk m f₀)) :
    ∃ a : ℝ, a < 0 ∧ 0 < sSup (maximalSobolevInteractionDomain k hk m f₀) ∧
      Ioo a (sSup (maximalSobolevInteractionDomain k hk m f₀)) ⊆
        maximalSobolevInteractionDomain k hk m f₀ ∧
      sSup (maximalSobolevInteractionDomain k hk m f₀) ∉
        maximalSobolevInteractionDomain k hk m f₀ := by
…

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

theorem OAI.DefocusingNLS.maximalSobolevSchrodingerFlow_finite_lifespan_blowup line 129

Source documentation

A finite maximal forward lifespan has divergent Sobolev norm at its endpoint.

theorem maximalSobolevSchrodingerFlow_finite_lifespan_blowup
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2)
    (hb : BddAbove (maximalSobolevInteractionDomain k hk m f₀)) :
    Tendsto (fun t => ‖maximalSobolevSchrodingerFlow k hk m f₀ t‖)
      (𝓝[<] (sSup (maximalSobolevInteractionDomain k hk m f₀))) atTop := by
…

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

theorem OAI.DefocusingNLS.maximalSobolevInteractionDomain_global_of_unbounded line 138

Source documentation

An unbounded maximal forward time domain contains every nonnegative time.

theorem maximalSobolevInteractionDomain_global_of_unbounded
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2)
    (hb : ¬ BddAbove (maximalSobolevInteractionDomain k hk m f₀))
    (t : ℝ) (ht : 0 ≤ t) : t ∈ maximalSobolevInteractionDomain k hk m f₀ := by
…

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