SchrodingerNonlinearEquation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Returning from the interaction equation to the Schrödinger equation

theorem OAI.DefocusingNLS.hasDerivAt_lowerSobolev_schrodingerCurve line 14

Source documentation

A differentiable Sobolev curve under the free group loses exactly two derivatives.

theorem hasDerivAt_lowerSobolev_schrodingerCurve
    (v : ℝ → FourierL2) (v' : FourierL2) (t : ℝ) (hv : HasDerivAt v v' t) :
    HasDerivAt (fun s => schrodingerFlow s (lowerSobolevInclusion (v s)))
      (schrodingerFlow t (lowerSobolevGenerator (v t)) +
        schrodingerFlow t (lowerSobolevInclusion v')) t := by
…

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

theorem OAI.DefocusingNLS.hasDerivAt_of_schrodingerInteraction line 43

Source documentation

The local interaction solution gives the nonlinear Schrödinger equation in H^(k-2).

theorem hasDerivAt_of_schrodingerInteraction
    (k : ℝ) (hk : 6 < k) (m : ℕ) (v : ℝ → FourierL2) (t : ℝ)
    (hv : HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t) :
    HasDerivAt (fun s => lowerSobolevInclusion (schrodingerFlow s (v s)))
      (lowerSobolevGenerator (schrodingerFlow t (v t)) -
        Complex.I • lowerSobolevInclusion
          (sobolevOddPower k hk m (schrodingerFlow t (v t)))) t := by
…

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

theorem OAI.DefocusingNLS.continuousOn_schrodingerFlow_curve line 61
Source documentation
A continuous Sobolev curve remains continuous after free evolution.
```
theorem continuousOn_schrodingerFlow_curve (v : ℝ → FourierL2) (J : Set ℝ)
    (hv : ContinuousOn v J) : ContinuousOn (fun s => schrodingerFlow s (v s)) J := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2

theorem OAI.DefocusingNLS.exists_local_sobolevSchrodingerSolution line 72

Source documentation

Every initial Sobolev vector admits a local solution of the actual semilinear equation.

theorem exists_local_sobolevSchrodingerSolution
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2) :
    ∃ T : ℝ, 0 < T ∧ ∃ u : ℝ → FourierL2, u 0 = f₀ ∧
      ContinuousOn u (Ioo (-T) T) ∧
      ∀ t ∈ Ioo (-T) T,
        HasDerivAt (fun s => lowerSobolevInclusion (u s))
          (lowerSobolevGenerator (u t) -
            Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t := by
…

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

theorem OAI.DefocusingNLS.hasDerivAt_nonlinearTorusFunction line 89

Source documentation

The nonlinear Sobolev equation gives the usual time derivative at every torus point.

theorem hasDerivAt_nonlinearTorusFunction
    (k : ℝ) (hk : 8 < k) (m : ℕ) (u : ℝ → FourierL2)
    (t : ℝ) (x : SchrodingerTorus)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (lowerSobolevGenerator (u t) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k (by linarith) m (u t))) t) :
    HasDerivAt (fun s => sobolevTorusFunction k (u s) x)
      (Complex.I * torusFourierLaplacian k (u t) x -
        Complex.I * oddPowerNonlinearity m (sobolevTorusFunction k (u t) x)) t := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.lowerSobolevInclusion, OAI.DefocusingNLS.torusFourierLaplacian, OAI.DefocusingNLS.oddPowerNonlinearity

theorem OAI.DefocusingNLS.nonlinearTorusFunction_schrodinger_equation line 122

Source documentation

The ordinary twelve-torus Laplacian and the actual odd power satisfy the defocusing PDE.

theorem nonlinearTorusFunction_schrodinger_equation
    (k : ℝ) (hk : 8 < k) (m : ℕ) (u : ℝ → FourierL2)
    (t : ℝ) (x : SchrodingerTorus)
    (hu : HasDerivAt (fun s => lowerSobolevInclusion (u s))
      (lowerSobolevGenerator (u t) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k (by linarith) m (u t))) t) :
    Complex.I * deriv (fun s => sobolevTorusFunction k (u s) x) t +
      (∑ j : Fin 12, deriv (deriv
        (fun r => sobolevTorusFunction k (u t) (torusCoordinateLine x j r))) 0) -
      oddPowerNonlinearity m (sobolevTorusFunction k (u t) x) = 0 := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.lowerSobolevInclusion, OAI.DefocusingNLS.torusCoordinateLine, OAI.DefocusingNLS.oddPowerNonlinearity