MaximalSobolevFlow.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The maximal Sobolev interaction solution

Local solutions through the same initial datum agree on overlapping time intervals. Their union therefore defines one classical solution on an open, connected domain, containing every other solution interval through that datum.

structure OAI.DefocusingNLS.SobolevInteractionPatch line 18
Source documentation
A classical solution patch on an open interval containing the initial time.
Also declared: ComparatorChallenges/DefocusingNLS.lean:210 (same declaration text).
```
structure SobolevInteractionPatch (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2) where
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevInteractionPatch_nonempty line 28
def OAI.DefocusingNLS.maximalSobolevInteractionDomain line 34
Source documentation
The union of every classical solution interval through the prescribed datum.
Also declared: ComparatorChallenges/DefocusingNLS.lean:220 (same declaration text).
```
def maximalSobolevInteractionDomain (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2) : Set ℝ :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
def OAI.DefocusingNLS.maximalSobolevInteractionFlow line 38
Source documentation
The unique value supplied by any classical solution patch containing the time.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:223 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.maximalSobolevInteractionFlow@path.
```
noncomputable def maximalSobolevInteractionFlow (k : ℝ) (hk : 6 < k) (m : ℕ)
    (f₀ : FourierL2) (t : ℝ) : FourierL2 := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2

theorem OAI.DefocusingNLS.SobolevInteractionPatch.eqOn_overlap line 46

Source documentation

Any two local patches agree wherever their intervals overlap.

theorem SobolevInteractionPatch.eqOn_overlap
    {k : ℝ} {hk : 6 < k} {m : ℕ} {f₀ : FourierL2}
    (P Q : SobolevInteractionPatch k hk m f₀) :
    EqOn P.curve Q.curve (Ioo (max P.left Q.left) (min P.right Q.right)) := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SobolevInteractionPatch

theorem OAI.DefocusingNLS.maximalSobolevInteractionFlow_eq_patch line 62

Source documentation

The maximal solution agrees with each of its classical patches.

theorem maximalSobolevInteractionFlow_eq_patch
    {k : ℝ} {hk : 6 < k} {m : ℕ} {f₀ : FourierL2}
    (P : SobolevInteractionPatch k hk m f₀) {t : ℝ} (ht : t ∈ Ioo P.left P.right) :
    maximalSobolevInteractionFlow k hk m f₀ t = P.curve t := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SobolevInteractionPatch

theorem OAI.DefocusingNLS.isOpen_maximalSobolevInteractionDomain line 72
theorem OAI.DefocusingNLS.zero_mem_maximalSobolevInteractionDomain line 76
theorem OAI.DefocusingNLS.isPreconnected_maximalSobolevInteractionDomain line 81
theorem OAI.DefocusingNLS.maximalSobolevInteractionFlow_initial line 89

theorem OAI.DefocusingNLS.hasDerivAt_maximalSobolevInteractionFlow line 95

Source documentation

The union is a classical solution at every point of its maximal open domain.

theorem hasDerivAt_maximalSobolevInteractionFlow (k : ℝ) (hk : 6 < k) (m : ℕ)
    (f₀ : FourierL2) {t : ℝ} (ht : t ∈ maximalSobolevInteractionDomain k hk m f₀) :
    HasDerivAt (maximalSobolevInteractionFlow k hk m f₀)
      (schrodingerInteractionField k hk m t (maximalSobolevInteractionFlow k hk m f₀ t)) t := by
…

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

theorem OAI.DefocusingNLS.SobolevInteractionPatch.subset_maximalDomain line 107
Source documentation
Every solution interval through the datum is contained in this domain.
```
theorem SobolevInteractionPatch.subset_maximalDomain
    {k : ℝ} {hk : 6 < k} {m : ℕ} {f₀ : FourierL2}
    (P : SobolevInteractionPatch k hk m f₀) :
    Ioo P.left P.right ⊆ maximalSobolevInteractionDomain k hk m f₀ := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SobolevInteractionPatch, OAI.DefocusingNLS.maximalSobolevInteractionDomain