SobolevDuhamel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Strong Sobolev solutions and the interaction equation

theorem OAI.DefocusingNLS.hasDerivAt_coordinate_of_lowerSobolev line 13
Source documentation
Differentiability in the lower Sobolev space determines each physical Fourier derivative.
```
theorem hasDerivAt_coordinate_of_lowerSobolev
    (u : ℝ → FourierL2) (g : FourierL2) (t : ℝ) (n : frequencyLattice)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s)) g t) :
    HasDerivAt (fun s => u s n) (((1 + ‖n‖ ^ 2 : ℝ) : ℂ) * g n) t := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.lowerSobolevInclusion

theorem OAI.DefocusingNLS.hasDerivAt_coordinate_schrodinger line 29

Source documentation

Every strong solution has the expected scalar Fourier differential equations.

theorem hasDerivAt_coordinate_schrodinger
    (k : ℝ) (hk : 6 < k) (m : ℕ) (u : ℝ → FourierL2)
    (t : ℝ) (n : frequencyLattice)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (lowerSobolevGenerator (u t) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t) :
    HasDerivAt (fun s => u s n)
      (-Complex.I * ((‖n‖ ^ 2 : ℝ) : ℂ) * u t n -
        Complex.I * sobolevOddPower k hk m (u t) n) t := by
…

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

theorem OAI.DefocusingNLS.hasDerivAt_interaction_coordinate line 48

Source documentation

Multiplying by the inverse free phase cancels the unbounded linear term coordinatewise.

theorem hasDerivAt_interaction_coordinate
    (k : ℝ) (hk : 6 < k) (m : ℕ) (u : ℝ → FourierL2)
    (t : ℝ) (n : frequencyLattice)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (lowerSobolevGenerator (u t) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t) :
    HasDerivAt (fun s => schrodingerFlow (-s) (u s) n)
      (((-Complex.I) • schrodingerFlow (-t) (sobolevOddPower k hk m (u t))) n) t := by
…

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