OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevIntervalUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.sobolevInteractionSolution_unique_of_bounded line 13

   Source documentation

   On an interval where both curves are bounded, one initial value determines the solution.

   theorem sobolevInteractionSolution_unique_of_bounded
       (k : ℝ) (hk : 6 < k) (m : ℕ) (v w : ℝ → FourierL2)
       (a b t₀ R : ℝ) (hR : 0 ≤ R) (ht₀ : t₀ ∈ Ioo a b)
       (hv : ∀ t ∈ Ioo a b, HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t)
       (hw : ∀ t ∈ Ioo a b, HasDerivAt w (schrodingerInteractionField k hk m t (w t)) t)
       (hvb : ∀ t ∈ Ioo a b, ‖v t‖ ≤ R) (hwb : ∀ t ∈ Ioo a b, ‖w t‖ ≤ R)
       (heq : v t₀ = w t₀) : EqOn v w (Ioo a b) := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2

2. theorem OAI.DefocusingNLS.sobolevInteractionSolution_unique_on_interval line 38

   Source documentation

   Two classical Sobolev interaction solutions agree on their entire common interval.

   theorem sobolevInteractionSolution_unique_on_interval
       (k : ℝ) (hk : 6 < k) (m : ℕ) (v w : ℝ → FourierL2)
       (a b t₀ : ℝ) (ht₀ : t₀ ∈ Ioo a b)
       (hv : ∀ t ∈ Ioo a b, HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t)
       (hw : ∀ t ∈ Ioo a b, HasDerivAt w (schrodingerInteractionField k hk m t (w t)) t)
       (heq : v t₀ = w t₀) : EqOn v w (Ioo a b) := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2