OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevLocalFlow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local Sobolev solutions in the Schrödinger interaction representation

The actual polynomial field satisfies the Banach-space Picard–Lindelöf hypotheses. This establishes local existence without treating the nonlinear Cauchy theory as an external assumption.

  1. theorem OAI.DefocusingNLS.exists_sobolevInteractionSolution line 19

    Source documentation

    Local existence for the actual interaction equation in H^k.

    theorem exists_sobolevInteractionSolution (k : ℝ) (hk : 6 < k) (m : ℕ)
    (f₀ : FourierL2) :
    ∃ T : ℝ, 0 < T ∧ ∃ v : ℝ → FourierL2, v 0 = f₀ ∧
      ∀ t ∈ Ioo (-T) T, HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t := by
…

    Mentions: OAI.DefocusingNLS.FourierL2