The interacting Schrödinger equation on the domain of the free Hamiltonian

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #129 (out of #64(iii)).

SchrodingerGroup.schrodinger is the interacting propagator U(t) = e^{−it(H₀ + V)} for a bounded potential, built as the Dyson series around the free group — a mild solution. PhaseGenerator.lean has the free Schrödinger equation on the domain of H₀ (hasDerivAt_fourierGroup_freePositionOp), and PerturbedGenerator.lean has the abstract theorem that a bounded perturbation's mild solution is classical on the generator's domain. This file puts the two together.

• ★ hasGeneratorAt_freeGroup: a vector ψ = 𝓕⁻¹ f of the domain of H₀ is in the domain of the generator of the free group, with value −i H₀ ψ — the free equation at t = 0, read as a right derivative.
• ★★★ hasDerivAt_schrodinger: the interacting Schrödinger equation, d/dt U(t)ψ = −i U(t)(H₀ψ + Vψ) at every t > 0, for every such ψ; hasDerivAt_schrodinger_addCLM writes the right-hand side with the operator H₀ + V of FreeHamiltonian.lean (freePositionOp.addCLM (potential VL)); hasDerivWithinAt_schrodinger_zero is the same at t = 0.
• ★★ hasGeneratorAt_freeGroup_schrodinger: the orbit U(t)ψ stays in the domain of the free generator, with −i H₀ (U(t)ψ) = −i U(t)(H₀ + V)ψ + i V U(t)ψ, so the equation also reads i ∂ₜ U(t)ψ = (H₀ + V)(U(t)ψ) with H₀ acting on the orbit (★★★ schrodinger_classical).

Honest scope

• The domain of H₀ enters as a hypothesis on the initial vector, in the form PhaseGenerator.lean uses: ψ = 𝓕⁻¹ f with f in the momentum domain and the membership of ψ in freePositionOp.domain supplied. The orbit is shown to lie in the domain of the free generator (the right derivative of the free orbit exists), which is the semigroup-theoretic domain. That this coincides with the concretely described freePositionOp.domain — the converse of phaseGroup_mem_mulDomain, "a right-differentiable free orbit has κ·f ∈ L²", a Fatou argument — is not proved here and is recorded as a separate row. Until it is, "U(t)ψ ∈ dom H₀" is a statement about the generator, not about the multiplication domain.
• The potential is the bounded multiplier potential VL for VL ∈ L^∞, as in schrodinger itself. The self-adjoint schrodingerOp of FreeHamiltonian.lean takes a real V through mulCLM; identifying the two operators is a coeFn statement about potential that this file does not make, so the equation is stated with potential VL and the addCLM form uses it too.
• One dimension, κ = freeSymbol, as in FreeHamiltonian.lean.

References: Engel–Nagel III.1, Pazy Thm 3.1.1; PerturbedGenerator.lean (hasDerivAt_perturbed, hasGeneratorAt_of_perturbed, perturbed_classical), PhaseGenerator.lean (hasDerivAt_fourierGroup_freePositionOp, phaseGroup_mem_mulDomain), SchrodingerGroup.lean (schrodinger, isContractionSemigroup_fourierGroup), FreeHamiltonian.lean (freePositionOp, schrodingerOp); specs/BACKLOG.md #129, #64.

The free generator on the domain of H₀

theorem SchrodingerGroup.hasGeneratorAt_freeGroup (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) : HasGeneratorAt (fun (t : ℝ) => if 0 ≤ t then fourierGroup ⋯ t else 1) (fourierL2.symm ↑f) (-Complex.I • ↑freePositionOp ⟨fourierL2.symm ↑f, h⟩)

★ A vector of the domain of H₀ is in the domain of the free group's generator, with value −i H₀ ψ: the free Schrödinger equation at t = 0, read as a right derivative.

The interacting equation

theorem SchrodingerGroup.hasDerivAt_schrodinger (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => (schrodinger ⋯ VL s) (fourierL2.symm ↑f)) (-Complex.I • (schrodinger ⋯ VL t) (↑freePositionOp ⟨fourierL2.symm ↑f, h⟩ + (HeatSemigroup.potential VL) (fourierL2.symm ↑f))) t

★★★ The interacting Schrödinger equation on the domain of H₀: for a bounded potential and every ψ = 𝓕⁻¹ f with f in the momentum domain, d/dt U(t)ψ = −i U(t)(H₀ψ + Vψ) at every t > 0.

theorem SchrodingerGroup.hasDerivAt_schrodinger_addCLM (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => (schrodinger ⋯ VL s) (fourierL2.symm ↑f)) (-Complex.I • (schrodinger ⋯ VL t) (↑(freePositionOp.addCLM (HeatSemigroup.potential VL)) ⟨fourierL2.symm ↑f, h⟩)) t

The same equation with the right-hand side written through the operator H₀ + V of FreeHamiltonian.lean.

theorem SchrodingerGroup.hasDerivWithinAt_schrodinger_zero (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) : HasDerivWithinAt (fun (s : ℝ) => (schrodinger ⋯ VL s) (fourierL2.symm ↑f)) (-Complex.I • (↑freePositionOp ⟨fourierL2.symm ↑f, h⟩ + (HeatSemigroup.potential VL) (fourierL2.symm ↑f))) (Set.Ici 0) 0

The equation at t = 0, within [0, ∞): the derivative is −i (H₀ψ + Vψ).

The orbit stays in the domain of the free generator

theorem SchrodingerGroup.hasGeneratorAt_freeGroup_schrodinger (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) {t : ℝ} (ht : 0 ≤ t) : HasGeneratorAt (fun (t : ℝ) => if 0 ≤ t then fourierGroup ⋯ t else 1) ((schrodinger ⋯ VL t) (fourierL2.symm ↑f)) ((schrodinger ⋯ VL t) (-Complex.I • ↑freePositionOp ⟨fourierL2.symm ↑f, h⟩ + (-(Complex.I • HeatSemigroup.potential VL)) (fourierL2.symm ↑f)) - (-(Complex.I • HeatSemigroup.potential VL)) ((schrodinger ⋯ VL t) (fourierL2.symm ↑f)))

★★ The orbit U(t)ψ stays in the domain of the free generator, with −i H₀(U(t)ψ) = −i U(t)(H₀ψ + Vψ) + i V (U(t)ψ).

theorem SchrodingerGroup.schrodinger_classical (VL : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)) (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) {t : ℝ} (ht : 0 < t) : ∃ (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), HasGeneratorAt (fun (t : ℝ) => if 0 ≤ t then fourierGroup ⋯ t else 1) ((schrodinger ⋯ VL t) (fourierL2.symm ↑f)) w ∧ HasDerivAt (fun (s : ℝ) => (schrodinger ⋯ VL s) (fourierL2.symm ↑f)) (w - Complex.I • (HeatSemigroup.potential VL) ((schrodinger ⋯ VL t) (fourierL2.symm ↑f))) t

★★★ The classical equation along the orbit: at every t > 0, U(t)ψ lies in the domain of the free generator with a named value w (that is, w = −i H₀ (U(t)ψ) in generator form), and d/dt U(t)ψ = w − i V (U(t)ψ) — i.e. i ∂ₜ U(t)ψ = (H₀ + V)(U(t)ψ) with H₀ acting on the orbit.