The Schrödinger group on L²(E) and Nelson's product formula #
Category: 1-Mathlib (CSD-free; staged for upstream).
The real-time rung of the Feynman path integral (BACKLOG #36 (c) FC-5). The interacting
Schrödinger propagator U(t) = e^{−it(H₀ + V)} on L²(ℝ, ℂ) is the limit of alternating free
flights and potential kicks,
(U₀(t/n) · e^{−i(t/n)V})ⁿ ψ → U(t) ψ (★★ nelson),
Nelson's operator form of Feynman's finite-slice formula (E. Nelson, Feynman integrals and the
Schrödinger equation, J. Math. Phys. 5 (1964) 332; for a bounded potential it is Trotter's product
formula, and the free flights are Fresnel kernels the theorem never has to write). This is the
real-time twin of Feynman–Kac (Probability/FeynmanKac.lean): there the time slices carry the heat
kernel and the Wiener measure, here the unitary free group and unimodular phases.
Design #
- The phase group
phaseGroup hκ t = M_{e^{−itκ}}of a real measurable symbolκ: a unitary one-parameter group of multiplication operators onL². Its strong continuity is obtained from its weak continuity⟪M_t f, f⟫ → ⟪f, f⟫— a scalar dominated convergence with dominator|f|²— through the polarisation‖M_t f − f‖² = 2‖f‖² − 2 Re ⟪M_t f, f⟫; no dominated convergence inL²is needed. - The unitary group with dispersion relation
κ,fourierGroup hκ t = 𝓕⁻¹ M_{e^{−itκ}} 𝓕: the phase group conjugated by Mathlib'sL²Fourier isometryLp.fourierTransformₗᵢ. It is the groupe^{−itκ(D)},D = −i d/dx;freeSchrodingeris the Schrödinger caseκ(ξ) = 2π²ξ², the symbol ofH₀ = −½ d²/dx²in Mathlib's convention𝓕 f (ξ) = ∫ e^{−2πiξx} f(x) dx(unitsℏ = m = 1). No generator is written:e^{−itH₀}is defined by its Fourier multiplier, as the spectral theorem would define it. - The interacting propagator
schrodinger hκ VL t: the Dyson series ofBoundedPerturbation.leanaround the free group with interaction−i M_V,V ∈ L^∞, fort ≥ 0; a semigroup, strongly continuous, satisfying Duhamel's equation, all inherited. - ★
exp_eq_potential— the exponential of a multiplication operator is multiplication by the exponential, for a bounded complex multiplier (the real-time counterpart ofFeynmanKac.exp_smul_neg_potential):exp (h · (−i M_V)) = M_{e^{−ihV}}, the potential kick. - ★★
nelson— Nelson's theorem:(U_κ(t/n) · M_{e^{−i(t/n)V}})ⁿ ψ → e^{−it(κ(D)+V)} ψ, Trotter's formula ofBoundedPerturbation.leanwith the kick identified;nelson_freeSchrodingeris the Schrödinger case. Both factors are phase groups — the kinetic one in momentum space, the potential one in position space — which is exactly Feynman's alternation of free propagation ande^{−iV Δt}. - ★
norm_schrodinger_apply— probability is conserved: the propagator of a real bounded potential is an isometry ofL², inherited from its unitary Trotter approximants through Nelson's limit. - ★★
exists_linearIsometryEquiv_schrodinger— the propagator is unitary: the propagator of the reversed dynamicse^{−it(−κ(D) − V)}is a two-sided inverse (schrodinger_mul_schrodinger_neg,schrodinger_neg_mul_schrodinger). The inverse of the forward Trotter approximant(U M)ⁿisM⁻¹ (U⁻¹ M⁻¹)ⁿ M, a conjugate of the reversed approximant (mul_pow_conj); both sides converge strongly by Nelson, andχ = Xₙ Xₙ⁻¹ χpasses to the limit. With the isometry, a linear isometric bijection ofL².
The wider picture. With HeatSemigroup.lean and FeynmanKac.lean the corpus now holds both
signatures of the same dynamics: in imaginary time e^{−t(H₀+V)} is the Trotter limit of heat
steps and is the Wiener functional; in real time e^{−it(H₀+V)} is the Trotter limit of unitary
free flights and phase kicks. The Schrödinger picture (the propagator as the solution of Duhamel's
equation), the Heisenberg picture (DynamicalLocality.lean, the flow on observables) and the
Feynman picture (the time-sliced product) are each theorems about one object.
Honest scope #
⚠️ Bounded potentials, t ≥ 0. The space is any finite-dimensional real inner product space
E — ℝᵈ in particular (BACKLOG #41, 2026-09-20); the Euclidean chain lives on
EuclideanSpace ℝ ι, so Feynman–Kac and Nelson meet on the same L²(ℝᵈ). Nelson's original
theorem also covers a class of unbounded potentials through Trotter's formula for self-adjoint
generators; only the bounded case is stated. The kernel (Fresnel-integral) form of the finite-slice
formula is FC-5′ (XL). The explicit action of freeSchrodinger on Schwartz functions and its
identification with the differential operator −½ Δ are
Analysis/Semigroup/SchrodingerSchwartz.lean (FC-5″, BACKLOG #43); the free Gaussian packet
spreading into a Gaussian of complex variance is Analysis/Semigroup/GaussianPacket.lean (FC-5‴,
BACKLOG #48).
References: E. Nelson, J. Math. Phys. 5 (1964) 332; M. Reed, B. Simon, Methods of Modern
Mathematical Physics I §VIII.8 and II §X.11; Analysis/Semigroup/BoundedPerturbation.lean (FC-1);
Probability/FeynmanKac.lean (FC-4); specs/feynman-continuum-scoping.md (FC-5);
specs/BACKLOG.md #36(c); specs/future-work.md FP-1.
Multiplication operators #
The powers of a multiplication operator, pointwise.
★ The exponential of a multiplication operator is multiplication by the exponential,
complex form: if A acts on L² as multiplication by a bounded measurable m, then exp A acts
as multiplication by e^{m}. The operator series applied to f has partial sums equal almost
everywhere to the pointwise partial sums; the L² limit and the pointwise (dominated) limit are
identified on every finite-measure set.
A multiplier bounded by one is a contraction of L².
A unimodular multiplier is an isometry of L².
A power of an isometry is an isometry.
The phase group e^{−itκ} of a real symbol #
The phase e^{−itκ(ξ)}.
Equations
- SchrodingerGroup.phaseFun κ t ξ = Complex.exp (↑(-(t * κ ξ)) * Complex.I)
Instances For
Mathlib's L² Fourier transform on ℝ, as a linear isometry equivalence of L2.
Instances For
The L^∞ class of the phase e^{−itκ}.
Equations
Instances For
The phase group M_t = M_{e^{−itκ}} on L², multiplication by the unimodular phase.
Equations
Instances For
The phase group is a group.
The phase group is unitary: an isometry of L².
⟪M_t f, f⟫ = ∫ conj (e^{−itκ}) |f|².
Weak continuity of the phase group at t = 0: a scalar dominated convergence with the
integrable dominator |f|².
★ Strong continuity of the phase group at t = 0, from weak continuity and the isometry:
‖M_t f − f‖² = 2‖f‖² − 2 Re ⟪M_t f, f⟫ → 0.
★ The phase group is strongly continuous.
The unitary group of a dispersion relation #
The unitary group with dispersion relation κ, U_κ(t) = 𝓕⁻¹ M_{e^{−itκ}} 𝓕 = e^{−itκ(D)}:
the phase group conjugated by the L² Fourier isometry.
Equations
Instances For
The group law U_κ(s + t) = U_κ(s) U_κ(t).
U_κ(t) is unitary: an isometry of L².
★ U_κ is strongly continuous.
★★ The unitary group U_κ, extended by the identity to t < 0, is a strongly continuous
contraction semigroup in the sense of BoundedPerturbation.lean: the Dyson series, the Duhamel
equation and the Trotter product formula apply to it.
The interacting propagator and Nelson's formula #
The interacting propagator U(t) = e^{−it(κ(D) + V)} for a bounded potential V ∈ L^∞:
the Dyson series of BoundedPerturbation.lean around the free group U_κ with interaction
−i M_V, for t ≥ 0 (the identity for t < 0).
Equations
- SchrodingerGroup.schrodinger hκ VL t = ⋯.perturbed (-(Complex.I • HeatSemigroup.potential VL)) t
Instances For
The propagator is a semigroup: U(t + s) = U(t) U(s) for s, t ≥ 0.
★ The potential kick: the Trotter step of the propagator is a free flight followed by the
phase e^{−ihV}, U_κ(h) · exp (h · (−i M_V)) = U_κ(h) · M_{e^{−ihV}} for h ≥ 0.
★★ Nelson's theorem — Trotter's product formula for the Schrödinger propagator. For a
bounded real potential V, the interacting propagator is the limit of alternating free flights and
potential kicks,
(U_κ(t/n) · M_{e^{−i(t/n)V}})ⁿ ψ → e^{−it(κ(D) + V)} ψ in L², t ≥ 0.
With U_κ(t/n) = 𝓕⁻¹ e^{−i(t/n)κ} 𝓕, the left side is Feynman's finite-slice formula in operator
form: the momentum-space phase of the kinetic term alternating with the position-space phase of the
potential.
★ Probability is conserved: the propagator of a real bounded potential is an isometry of
L², ‖U(t) ψ‖ = ‖ψ‖, inherited from its unitary Trotter approximants through Nelson's limit.
The free Schrödinger group #
The free symbol 2π²‖ξ‖²: the Fourier symbol of H₀ = −½ Δ in Mathlib's convention
𝓕 f (ξ) = ∫ e^{−2πi⟪ξ,x⟫} f(x) dx (units ℏ = m = 1).
Instances For
The free Schrödinger group e^{−itH₀}, H₀ = −½ d²/dx², defined through its Fourier
multiplier e^{−2π²itξ²}: fourierGroup with the free symbol.
Equations
Instances For
★★ Nelson's theorem for the Schrödinger equation: for a bounded real potential V,
(e^{−i(t/n)H₀} · e^{−i(t/n)V})ⁿ ψ → e^{−it(H₀ + V)} ψ in L²(E), H₀ = −½ Δ.
Unitarity: the reversed dynamics is the inverse #
Negating the symbol reverses the phase group: M^{−κ}_s = M^{κ}_{−s}.
Negating the symbol reverses the group: U_{−κ}(s) = U_κ(−s).
★ The propagator of the reversed dynamics is an inverse: if κ₂ = −κ₁ and V₂ = −V₁,
then e^{−it(κ₁(D)+V₁)} · e^{−it(κ₂(D)+V₂)} = 1 for t ≥ 0. The forward Trotter approximants
Xₙ = (U₁ M₁)ⁿ are invertible with Xₙ⁻¹ = M₂ (U₂ M₂)ⁿ M₁, a conjugate of the reversed
approximants; both converge strongly (Nelson), and χ = Xₙ Xₙ⁻¹ χ passes to the limit.
★ U(t) · U⁻(t) = 1: the propagator of the reversed dynamics e^{−it(−κ(D) − V)} is a right
inverse of e^{−it(κ(D) + V)}, t ≥ 0.
★ U⁻(t) · U(t) = 1: the propagator of the reversed dynamics is a left inverse.
★★ The Schrödinger propagator is unitary. For a real bounded potential V and t ≥ 0,
e^{−it(κ(D) + V)} is a linear isometric bijection of L²: an isometry by
norm_schrodinger_apply, invertible with inverse the propagator of the reversed dynamics
(schrodinger_mul_schrodinger_neg, schrodinger_neg_mul_schrodinger).