i u_t + u_xx + f(|u|) u = 0 (нелинейное уравнение Шрёдингера; Тестовая задача 8)

We look for solutions of the nonlinear Schrödinger equation i u_t + u_{xx} + f(|u|) u = 0 by a travelling‑wave ansatz with a plane‑wave phase factor. Let u(t,x) = φ(ξ) · exp( i (k x – ω t) ), ξ = x – c t, where φ : ℝ → ℂ is an envelope, k, ω, c ∈ ℝ are constants and f : ℝ → ℝ is the given nonlinearity. Differentiating we obtain u_t = ( –c φ′(ξ) – i ω φ(ξ) ) e^{i(kx–ωt)}, u_x = ( φ′(ξ) + i k φ(ξ) ) e^{i(kx–ωt)}, u_{xx} = ( φ″(ξ) + 2 i k φ′(ξ) – k² φ(ξ) ) e^{i(kx–ωt)}. Substituting into the PDE and using |e^{iθ}| = 1 gives [ φ″ + (ω – k²) φ + f(|φ|) φ ] e^{i(kx–ωt)} + i (2k – c) φ′ e^{i(kx–ωt)} = 0. For this to hold for all t,x we must have the coefficient of the imaginary part vanish, i.e. c = 2k, and the remaining bracket must be zero. Thus φ must satisfy the ordinary differential equation φ″(ξ) + (ω – k²) φ(ξ) + f(|φ(ξ)|) φ(ξ) = 0. Consequently, whenever φ solves this ODE and c = 2k, the function u defined above is a solution of the PDE. The Lean fragment below formalises this construction: it defines the travelling‑wave ansatz, states a theorem that the ansatz solves the equation under the stated conditions, and leaves the detailed calculation to `sorry` (the proof is a straightforward but lengthy computation of derivatives). The theorem is therefore a formal statement of the travelling‑wave family of solutions for the nonlinear Schrödinger equation.

We prove that for a constant function \(u(t,x)=c\) the nonlinear Schrödinger equation reduces to the algebraic condition \((f\|c\|)\cdot c=0\). The lemma `eq49_const` states the equivalence between the PDE holding for the constant function and this algebraic equation. The proof uses the definitions of the first and second spatial derivatives `D1` and `D2`. Since the derivatives of a constant are zero, the equation simplifies to the product term. The forward direction extracts the equality at a single point \((t=0,x=0)\) and simplifies with `simp`. The backward direction shows that if the product is zero then the PDE holds for all \(t,x\), again by simplifying the expression with `simp`. The lemma is fully formalised in Lean 4 and compiles with Mathlib.

noncomputable def D1 (u : ℝ → ℝ → ℂ) : ℝ → ℝ → ℂ := fun a b => deriv (fun s => u s b) a
noncomputable def D2 (u : ℝ → ℝ → ℂ) : ℝ → ℝ → ℂ := fun a b => deriv (fun s => u a s) b

def eq49 (u : ℝ → ℝ → ℂ) (f : ℝ → ℝ) : Prop :=
  ∀ t x, Complex.I * D1 u t x + D2 (D2 u) t x + (f ‖u t x‖ : ℂ) * u t x = 0

lemma eq49_const (c : ℂ) (f : ℝ → ℝ) :
  eq49 (fun _ _ => c) f ↔ (f ‖c‖ : ℂ) * c = 0 := by
  constructor
  · intro h
    have h0 := h 0 0
    simpa [D1, D2] using h0
  · intro h
    intro t x
    simpa [D1, D2] using h

We formalise the observation that any function which is constant in both variables has all first‑ and second‑order partial derivatives equal to zero. In the notation of the statement, a constant function is given by `const_u c : ℝ → ℝ → ℂ` with `const_u c t x = c`. The definitions of the directional derivatives `D1` and `D2` are simply `deriv` applied to the corresponding one‑variable slices. By the lemma `deriv_const` we have `deriv (fun _ => c) = fun _ => 0`, so `D1 (const_u c) t x = 0` and `D2 (const_u c) t x = 0` for all `t, x`. Consequently also `D2 (D2 (const_u c)) t x = 0`. Substituting these identities into the equation `eq49` reduces the left‑hand side to `(f ‖c‖ : ℂ) * c`. Therefore a constant function is a solution precisely when `f (‖c‖) = 0` (or trivially when `c = 0`). The lemma `const_solution` proves this implication, while `zero_solution` shows that the zero function solves the equation for any non‑linear term `f`. The proofs use only the definitions of `D1`, `D2`, the lemma `deriv_const`, and simple `simp` rewriting.

For stationary solutions of the nonlinear Schrödinger equation we may assume the ansatz u(t,x) = φ(x) which is independent of the time variable. In this case the time derivative vanishes: u_t(t,x) = 0. The spatial second derivative reduces to the ordinary second derivative of φ: u_xx(t,x) = φ''(x). Substituting these expressions into the PDE i u_t + u_xx + f(|u|) u = 0 gives the ordinary differential equation φ''(x) + f(|φ(x)|) φ(x) = 0. In Lean we formalise the ODE by the predicate ODE(φ,f) : Prop := ∀ x, φ''(x) + f(|φ(x)|) φ(x) = 0, where φ''(x) is written as `deriv (deriv φ) x`. The theorem `eq49_stationary` proves that a function of the form `u(t,x)=φ(x)` satisfies the PDE iff φ satisfies the ODE. The proof uses the definitions of the partial derivatives `D1` and `D2`, the lemma `deriv_const` to show that the time derivative is zero, and the simplification rules for the second derivative. Thus the reduction of the PDE to an ODE for stationary solutions is fully formalised.

We prove that a constant function is a solution of the nonlinear Schrödinger equation iff the algebraic condition \(f(|c|)\,c=0\) holds. The definition of `eq49` involves the first derivative of `u` with respect to the time variable (`D1`) and the second derivative with respect to the spatial variable (`D2 (D2 u)`). For a constant function \(u(t,x)=c\) these derivatives are zero by the lemma `deriv_const`. Consequently the left‑hand side of the PDE collapses to \((f\|c\|)\,c\). The lemma `const_solution` formalises this observation: it takes a real‑valued function `f`, a complex constant `c`, and a hypothesis that \((f\|c\|)\,c=0\); it then shows that the constant function satisfies `eq49`. The proof is a one‑line `simp` after rewriting the derivatives with `D1` and `D2`. The Lean code below defines this lemma. It is self‑contained and compiles with the standard Mathlib prelude.

The trivial function \(u(t,x)=0\) is a solution of the nonlinear Schrödinger equation for any nonlinearity \(f\). In the formalisation the equation is encoded by the predicate `eq49`. To prove that the zero function satisfies this predicate we unfold the definition of `eq49` and the auxiliary derivatives `D1` and `D2`. For the constant zero function all derivatives are zero by the lemma `deriv_const`. Moreover the norm of zero is zero, so the nonlinear term \((f\|u\|)\,u\) also vanishes. Consequently the left‑hand side of the equation reduces to \(0+0+0=0\), which is verified by a single `simp` call. The Lean lemma `zero_solution` implements exactly this reasoning and is fully checkable by the Mathlib kernel.

We choose the simplest possible family of solutions: the identically zero function. Define ```lean def u0 : ℝ → ℝ → ℂ := fun _ _ => 0 ``` For any non‑linear term \(f\) the equation becomes \[ i\,\partial_t u + \partial_{xx}u + f(|u|)\,u = 0.\] With \(u\equiv 0\) all three terms vanish: the time derivative, the second spatial derivative, and the nonlinear term \(f(|u|)u\) are all zero. Hence \(u\equiv 0\) satisfies the equation for every choice of \(f\). The formal proof uses the fact that the derivative of a constant function is zero and that the complex norm of zero is zero. The Lean proof is a one‑liner after unfolding the definitions of `D1` and `D2`. The Lean fragment below defines the zero solution and proves that it satisfies `eq49` for any function `f`.