SobolevForwardDomain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Openness and continuous dependence throughout the forward lifespan

theorem OAI.DefocusingNLS.hasSobolevFlowNeighborhood_of_nonneg line 13
Source documentation
Finitely many uniform local restarts propagate continuous dependence to every nonnegative time in a maximal solution's lifespan.
```
theorem hasSobolevFlowNeighborhood_of_nonneg
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f : FourierL2) (T : ℝ) (hT : 0 ≤ T)
    (hdom : T ∈ maximalSobolevInteractionDomain k hk m f) :
    HasSobolevFlowNeighborhood k hk m f T := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.maximalSobolevInteractionDomain, OAI.DefocusingNLS.HasSobolevFlowNeighborhood
theorem OAI.DefocusingNLS.isOpen_sobolevForwardExistenceSet line 67
Source documentation
Existence up to any prescribed forward time is an open condition on the initial datum.
```
theorem isOpen_sobolevForwardExistenceSet
    (k : ℝ) (hk : 6 < k) (m : ℕ) (T : ℝ) (hT : 0 ≤ T) :
    IsOpen {f : FourierL2 | T ∈ maximalSobolevInteractionDomain k hk m f} := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.maximalSobolevInteractionDomain

theorem OAI.DefocusingNLS.continuousOn_maximalSobolevForwardFlow line 76

Source documentation

The maximal physical flow is jointly continuous throughout its forward existence domain.

theorem continuousOn_maximalSobolevForwardFlow
    (k : ℝ) (hk : 6 < k) (m : ℕ) :
    ContinuousOn (fun p : FourierL2 × ℝ => maximalSobolevSchrodingerFlow k hk m p.1 p.2)
      {p | 0 ≤ p.2 ∧ p.2 ∈ maximalSobolevInteractionDomain k hk m p.1} := by
…

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