SobolevFlowNeighborhood.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Neighborhoods of the maximal Sobolev flow

def OAI.DefocusingNLS.HasSobolevFlowNeighborhood line 12
Source documentation
Existence for nearby data and times, together with joint continuity of the maximal flow.
```
def HasSobolevFlowNeighborhood (k : ℝ) (hk : 6 < k) (m : ℕ)
    (f : FourierL2) (t : ℝ) : Prop :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.hasSobolevFlowNeighborhood_zero line 17

theorem OAI.DefocusingNLS.HasSobolevFlowNeighborhood.advance line 31

Source documentation

A common local flow on a ball propagates an existence/continuity neighborhood forward.

theorem HasSobolevFlowNeighborhood.advance
    (k : ℝ) (hk : 6 < k) (m : ℕ) (R δ : ℝ) (hδ : 0 < δ)
    (hdom : ∀ g : FourierL2, ‖g‖ ≤ R →
      Ioo (-δ) δ ⊆ maximalSobolevInteractionDomain k hk m g)
    (hcont : ContinuousOn
      (fun p : FourierL2 × ℝ => maximalSobolevSchrodingerFlow k hk m p.1 p.2)
      (closedBall 0 R ×ˢ Ioo (-δ) δ))
    (f : FourierL2) (s τ : ℝ) (hs : 0 ≤ s)
    (hf : HasSobolevFlowNeighborhood k hk m f s)
    (hR : ‖maximalSobolevSchrodingerFlow k hk m f s‖ < R)
    (hτ : τ ∈ Ioo 0 δ) : HasSobolevFlowNeighborhood k hk m f (s + τ) := by
…

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