OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevDuhamelIntegral.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.inverseSchrodingerCurve line 12
2. def OAI.DefocusingNLS.physicalSchrodingerForcing line 15
3. theorem OAI.DefocusingNLS.continuousOn_physicalSchrodingerForcing line 19
4. theorem OAI.DefocusingNLS.sobolevDuhamel_identity line 29

   Source documentation

   Strong solutions satisfy the H^k-valued Duhamel identity, proved by their Fourier coordinates.

   theorem sobolevDuhamel_identity
       (k : ℝ) (hk : 6 < k) (m : ℕ) (u : ℝ → FourierL2) (a b t₀ t : ℝ)
       (huc : ContinuousOn u (Ioo a b))
       (hu : ∀ s ∈ Ioo a b, HasDerivAt (fun r => lowerSobolevInclusion (u r))
         (lowerSobolevGenerator (u s) -
           Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u s))) s)
       (ht₀ : t₀ ∈ Ioo a b) (ht : t ∈ Ioo a b) :
       inverseSchrodingerCurve u t = inverseSchrodingerCurve u t₀ +
         ∫ s in t₀..t, physicalSchrodingerForcing k hk m u s := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion, OAI.DefocusingNLS.inverseSchrodingerCurve, OAI.DefocusingNLS.physicalSchrodingerForcing

5. theorem OAI.DefocusingNLS.hasDerivAt_inverseSchrodingerCurve line 62

   Source documentation

   A strong Sobolev solution becomes a classical H^k interaction solution.

   theorem hasDerivAt_inverseSchrodingerCurve
       (k : ℝ) (hk : 6 < k) (m : ℕ) (u : ℝ → FourierL2) (a b t : ℝ)
       (huc : ContinuousOn u (Ioo a b))
       (hu : ∀ s ∈ Ioo a b, HasDerivAt (fun r => lowerSobolevInclusion (u r))
         (lowerSobolevGenerator (u s) -
           Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u s))) s)
       (ht : t ∈ Ioo a b) :
       HasDerivAt (inverseSchrodingerCurve u)
         (schrodingerInteractionField k hk m t (inverseSchrodingerCurve u t)) t := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion, OAI.DefocusingNLS.inverseSchrodingerCurve

6. theorem OAI.DefocusingNLS.sobolevSchrodingerSolution_unique_on_interval line 90

   Source documentation

   Strong H^k solutions of the actual Schrödinger equation are unique on a common interval.

   theorem sobolevSchrodingerSolution_unique_on_interval
       (k : ℝ) (hk : 6 < k) (m : ℕ) (u v : ℝ → FourierL2) (a b t₀ : ℝ)
       (ht₀ : t₀ ∈ Ioo a b) (huc : ContinuousOn u (Ioo a b)) (hvc : ContinuousOn v (Ioo a b))
       (hu : ∀ t ∈ Ioo a b, HasDerivAt (fun s => lowerSobolevInclusion (u s))
         (lowerSobolevGenerator (u t) -
           Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t)
       (hv : ∀ t ∈ Ioo a b, HasDerivAt (fun s => lowerSobolevInclusion (v s))
         (lowerSobolevGenerator (v t) -
           Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (v t))) t)
       (heq : u t₀ = v t₀) : EqOn u v (Ioo a b) := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion