SobolevUniqueness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local uniqueness of the Sobolev interaction equation

theorem OAI.DefocusingNLS.sobolevInteractionSolution_eventually_unique line 12

Source documentation

Two Sobolev interaction solutions with the same initial datum agree near that time.

theorem sobolevInteractionSolution_eventually_unique
    (k : ℝ) (hk : 6 < k) (m : ℕ) (v w : ℝ → FourierL2)
    (J : Set ℝ) (hJ : IsOpen J) (t₀ : ℝ) (ht₀ : t₀ ∈ J)
    (hv : ∀ t ∈ J, HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t)
    (hw : ∀ t ∈ J, HasDerivAt w (schrodingerInteractionField k hk m t (w t)) t)
    (heq : v t₀ = w t₀) : v =ᶠ[𝓝 t₀] w := by
…

Mentions: OAI.DefocusingNLS.FourierL2