Feynman's kernel for the free propagator

Category: 1-Mathlib (CSD-free; staged for upstream).

Analysis/Semigroup/SchrodingerSchwartz.lean builds the free propagator U₀(t) = e^{−itH₀}, H₀ = −½ d²/dx², as a Fourier multiplier: U₀(t) = 𝓕⁻¹ e^{−2π²itξ²} 𝓕. This module (BACKLOG #44, FC-5′) writes the kernel of that operator — the one the path integral is built from — by analytic continuation of the heat kernel in the time variable:

• the kernel at complex time w, fresnelKernel w x = (4πw)^{−1/2} e^{−x²/(4w)}, is a Schwartz function for Re w > 0 (fresnelS, on top of GaussianPacket.lean's complex-parameter Gaussian) and its Fourier transform is the multiplier e^{−4π²wξ²} (★ fourier_fresnelS): the amplitude (4πw)^{−1/2} is exactly what cancels the a^{−1/2} of the Gaussian transform;
• the operator fresnelOp w is convolution with that kernel, so it has both the kernel form ∫ K_w(x − y) ψ(y) dy (★ fresnelOp_apply) and the multiplier form (★ fourier_fresnelOp); it is a semigroup in the complex time (★★ fresnelOp_fresnelOp), and therefore every time-slicing is exact: n+1 slices of w/(n+1) compose to w (★★ fresnelOp_iterate_div), each slice one kernel integral (★ fresnelOp_iterate_succ_apply);
• ★★★ tendsto_fresnelOp — the Gaussian-regularised Fresnel integral is the propagator: (U₀(t)ψ)(x) = lim_{ε ↓ 0} ∫ K_{ε + it/2}(x − y) ψ(y) dy, by dominated convergence on the Fourier side (|e^{−4π²(ε+it/2)ξ²}| ≤ 1, 𝓕ψ integrable). This is the continuation t ↦ it of the heat kernel, taken where it converges absolutely and carried to the imaginary axis;
• ★ fresnelKernel_I_mul — at w = it/2 the kernel is Feynman's (2πit)^{−1/2} e^{ix²/(2t)}, of constant modulus (norm_fresnelKernel_I_mul): it does not decay, which is why the integral is improper for general L² data — and absolutely convergent against the L¹ Schwartz functions used here (★ integrable_fresnelKernel_mul);
• ★★★ freeSchrodingerS_eq_integral_fresnel — Feynman's kernel formula, exactly: (U₀(t)ψ)(x) = (2πit)^{−1/2} ∫ e^{i(x−y)²/(2t)} ψ(y) dy for t ≠ 0 and Schwartz ψ, with no regularisation left in the statement. The regularised integrals converge both to the propagator and to this integral, and limits are unique;
• ★★ freeSchrodingerS_iterate — U₀(t) = (U₀(t/(n+1)))^{n+1}, so the n-slice iterated Feynman integral is exact for every n; and ★★★ prod_fresnelKernel_eq_exp_discreteAction — the product of the n kernels in that iterated integral is ((2πit/n)^{−1/2})^n e^{iS_n} with S_n the discrete action ∑ (q_{k+1} − q_k)²/(2Δt) of the sampled path (discreteAction). The phase of the path integral is a theorem here, not a notation.

Honest scope

⚠️ One dimension, Schwartz data. The scoping note's ψ ∈ L¹ ∩ L² is not claimed: Fourier inversion at this pin is the Schwartz theorem, and for ψ ∈ L² \ L¹ the Feynman integral is genuinely improper — it needs oscillatory-integral technology the pin does not have (MATHLIB-ABSENT(fresnelIntegral)). Nothing here evaluates an oscillatory integral as a limit of truncations ∫_{−R}^{R}; the ε ↓ 0 regularisation is the whole method.

⚠️ The n-slice identity is exact for every n, so no limit over paths is taken and none is claimed: there is no measure on path space here, and no statement that S_n converges to the classical action. The imaginary-time counterpart, where the path measure does exist, is the corpus's Feynman–Kac chain.

⚠️ fresnelS is defined by a dite on Re w > 0, following Mathlib's own SchwartzMap.smulLeftCLM: off the half-plane the kernel is not Schwartz, and every lemma carries the hypothesis.

References: M. Reed, B. Simon, Methods of Modern Mathematical Physics II §IX.7; R. P. Feynman, A. R. Hibbs, Quantum Mechanics and Path Integrals (1965) §2-2, §3-1; Analysis/Semigroup/SchrodingerSchwartz.lean (FC-5″), GaussianPacket.lean (FC-5‴); specs/feynman-continuum-scoping.md §5 and §8 D4; specs/BACKLOG.md #44; specs/future-work.md FP-1.

The kernel at complex time

noncomputable def SchrodingerGroup.fresnelAmp (w : ℂ) : ℂ

The amplitude (4πw)^{−1/2} of the heat kernel at complex time w.

Equations

• SchrodingerGroup.fresnelAmp w = (4 * ↑Real.pi * w) ^ (-1 / 2)

noncomputable def SchrodingerGroup.fresnelKernel (w : ℂ) (x : ℝ) : ℂ

The heat kernel at complex time w: (4πw)^{−1/2} e^{−x²/(4w)}. At w = it/2 this is Feynman's kernel (2πit)^{−1/2} e^{ix²/(2t)} (fresnelKernel_I_mul).

Equations

• SchrodingerGroup.fresnelKernel w x = SchrodingerGroup.fresnelAmp w * Complex.exp (-↑x ^ 2 / (4 * w))

noncomputable def SchrodingerGroup.fresnelSymbol (w : ℂ) (ξ : ℝ) : ℂ

The Fourier multiplier of the complex-time kernel: e^{−4π²wξ²}. At w = it/2 this is the free Schrödinger phase e^{−2π²itξ²} (fresnelSymbol_I_mul).

Equations

• SchrodingerGroup.fresnelSymbol w ξ = Complex.exp (-(4 * ↑Real.pi ^ 2 * w) * ↑ξ ^ 2)

theorem SchrodingerGroup.re_four_pi_mul (w : ℂ) : (4 * ↑Real.pi * w).re = 4 * Real.pi * w.re

theorem SchrodingerGroup.four_pi_mul_ne_zero {w : ℂ} (hw : w ≠ 0) : 4 * ↑Real.pi * w ≠ 0

theorem SchrodingerGroup.ne_zero_of_re_pos {w : ℂ} (hw : 0 < w.re) : w ≠ 0

theorem SchrodingerGroup.re_fresnelParam_pos {w : ℂ} (hw : 0 < w.re) : 0 < (4 * ↑Real.pi * w)⁻¹.re

The Gaussian parameter of the kernel, a = (4πw)⁻¹, has positive real part.

theorem SchrodingerGroup.arg_four_pi_mul_ne_pi {w : ℂ} (hw : 0 < w.re) : (4 * ↑Real.pi * w).arg ≠ Real.pi

theorem SchrodingerGroup.norm_fresnelSymbol (w : ℂ) (ξ : ℝ) : ‖fresnelSymbol w ξ‖ = Real.exp (-(4 * Real.pi ^ 2 * w.re * ξ ^ 2))

The modulus of the multiplier: |e^{−4π²wξ²}| = e^{−4π²(Re w)ξ²}, which is ≤ 1 for Re w ≥ 0 — the bound that drives every dominated convergence below.

theorem SchrodingerGroup.norm_fresnelSymbol_le_one {w : ℂ} (hw : 0 ≤ w.re) (ξ : ℝ) : ‖fresnelSymbol w ξ‖ ≤ 1

theorem SchrodingerGroup.norm_exp_fresnel_le_one {w : ℂ} (hw : 0 ≤ w.re) (hw0 : w ≠ 0) (x : ℝ) : ‖Complex.exp (-↑x ^ 2 / (4 * w))‖ ≤ 1

The modulus of the Gaussian factor of the kernel is ≤ 1 when Re w ≥ 0: the exponent's real part is −x²(Re w)/(4|w|²).

noncomputable def SchrodingerGroup.fresnelS (w : ℂ) : SchwartzMap ℝ ℂ

The kernel at complex time w, Re w > 0, as a Schwartz function: the Gaussian e^{−πax²} of parameter a = (4πw)⁻¹, scaled by (4πw)^{−1/2}. The dite follows Mathlib's own SchwartzMap.smulLeftCLM: outside the half-plane the Gaussian is not Schwartz, and every lemma below carries 0 < w.re.

Equations

• SchrodingerGroup.fresnelS w = if hw : 0 < w.re then SchrodingerGroup.fresnelAmp w • SchrodingerGroup.gaussianS (4 * ↑Real.pi * w)⁻¹ ⋯ else 0

theorem SchrodingerGroup.fresnelS_eq {w : ℂ} (hw : 0 < w.re) : fresnelS w = fresnelAmp w • gaussianS (4 * ↑Real.pi * w)⁻¹ ⋯

theorem SchrodingerGroup.coe_fresnelS {w : ℂ} (hw : 0 < w.re) : ⇑(fresnelS w) = fresnelKernel w

The Schwartz function is the kernel.

theorem SchrodingerGroup.fourier_fresnelS {w : ℂ} (hw : 0 < w.re) : ⇑(FourierTransform.fourier (fresnelS w)) = fresnelSymbol w

★ The Fourier transform of the complex-time kernel is the multiplier e^{−4π²wξ²}: the amplitude (4πw)^{−1/2} is exactly what cancels the a^{−1/2} of the Gaussian transform.

The operator

noncomputable def SchrodingerGroup.fresnelOp (w : ℂ) : SchwartzMap ℝ ℂ →L[ℂ] SchwartzMap ℝ ℂ

Convolution with the complex-time kernel, on Schwartz functions: e^{−wH₀} for H₀ = −½ d²/dx², read through Re w > 0 (heat) and continued to w = it/2 (Schrödinger).

Equations

• SchrodingerGroup.fresnelOp w = (SchwartzMap.convolution (ContinuousLinearMap.mul ℂ ℂ)) (SchrodingerGroup.fresnelS w)

theorem SchrodingerGroup.fresnelOp_apply {w : ℂ} (hw : 0 < w.re) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ((fresnelOp w) ψ) x = ∫ (y : ℝ), fresnelKernel w (x - y) * ψ y

★ The kernel form of the operator: (fresnelOp w ψ) x = ∫ K_w(x − y) ψ(y) dy, an absolutely convergent integral (Mathlib's Schwartz convolution).

theorem SchrodingerGroup.fourier_fresnelOp {w : ℂ} (hw : 0 < w.re) (ψ : SchwartzMap ℝ ℂ) (ξ : ℝ) : (FourierTransform.fourier ((fresnelOp w) ψ)) ξ = fresnelSymbol w ξ * (FourierTransform.fourier ψ) ξ

★ The multiplier form: the Fourier transform of the operator is multiplication by e^{−4π²wξ²}.

theorem SchrodingerGroup.apply_eq_integral_fourier (f : SchwartzMap ℝ ℂ) (x : ℝ) : f x = ∫ (ξ : ℝ), Real.fourierChar (inner ℝ ξ x) • (FourierTransform.fourier f) ξ

Fourier inversion, pointwise: a Schwartz function is the inverse transform of its transform.

theorem SchrodingerGroup.fresnelOp_apply_eq_integral_symbol {w : ℂ} (hw : 0 < w.re) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ((fresnelOp w) ψ) x = ∫ (ξ : ℝ), Real.fourierChar (inner ℝ ξ x) • (fresnelSymbol w ξ * (FourierTransform.fourier ψ) ξ)

theorem SchrodingerGroup.fresnelSymbol_add (w₁ w₂ : ℂ) (ξ : ℝ) : fresnelSymbol (w₁ + w₂) ξ = fresnelSymbol w₁ ξ * fresnelSymbol w₂ ξ

The multiplier is a one-parameter semigroup in the complex time.

theorem SchrodingerGroup.fresnelOp_fresnelOp {w₁ w₂ : ℂ} (h₁ : 0 < w₁.re) (h₂ : 0 < w₂.re) (ψ : SchwartzMap ℝ ℂ) : (fresnelOp w₁) ((fresnelOp w₂) ψ) = (fresnelOp (w₁ + w₂)) ψ

★★ The complex-time semigroup: two slices compose into one, fresnelOp w₁ ∘ fresnelOp w₂ = fresnelOp (w₁ + w₂). On the Fourier side it is e^{−4π²w₁ξ²} e^{−4π²w₂ξ²} = e^{−4π²(w₁+w₂)ξ²}; on the kernel side it is the Gaussian convolution identity, continued in the time.

theorem SchrodingerGroup.re_natCast_add_one_mul (n : ℕ) (w : ℂ) : ((↑n + 1) * w).re = (↑n + 1) * w.re

theorem SchrodingerGroup.fresnelOp_iterate {w : ℂ} (hw : 0 < w.re) (n : ℕ) (ψ : SchwartzMap ℝ ℂ) : (⇑(fresnelOp w))^[n + 1] ψ = (fresnelOp ((↑n + 1) * w)) ψ

★ n equal slices compose: iterating the complex-time operator n+1 times is the operator at (n+1)w.

theorem SchrodingerGroup.re_div_natCast_add_one (w : ℂ) (n : ℕ) : (w / (↑n + 1)).re = w.re / (↑n + 1)

theorem SchrodingerGroup.fresnelOp_iterate_div {w : ℂ} (hw : 0 < w.re) (n : ℕ) (ψ : SchwartzMap ℝ ℂ) : (⇑(fresnelOp (w / (↑n + 1))))^[n + 1] ψ = (fresnelOp w) ψ

★★ Every time-slicing is exact: n+1 slices of complex time w/(n+1) compose to the single slice w.

theorem SchrodingerGroup.fresnelOp_iterate_succ_apply {w : ℂ} (hw : 0 < w.re) (n : ℕ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ((⇑(fresnelOp w))^[n + 1] ψ) x = ∫ (y : ℝ), fresnelKernel w (x - y) * ((⇑(fresnelOp w))^[n] ψ) y

★ The time-slicing recursion: each slice is one kernel integral, so the n+1-slice operator is an n+1-fold iterated kernel integral.

The free propagator is the ε ↓ 0 limit

theorem SchrodingerGroup.re_ofReal_add_I_mul (ε t : ℝ) : (↑ε + Complex.I * ↑t / 2).re = ε

The real part of the regularised time ε + it/2 is the regulariser (simp knows this; the name is here because the positivity hypothesis is rewritten with it everywhere below).

theorem SchrodingerGroup.ofReal_add_I_mul_ne_zero {ε : ℝ} (hε : 0 < ε) (t : ℝ) : ↑ε + Complex.I * ↑t / 2 ≠ 0

theorem SchrodingerGroup.fresnelSymbol_I_mul (t ξ : ℝ) : fresnelSymbol (Complex.I * ↑t / 2) ξ = phaseFun freeSymbol t ξ

At purely imaginary time the multiplier is the free Schrödinger phase e^{−2π²itξ²}.

theorem SchrodingerGroup.fourier_freeSchrodingerS (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (ξ : ℝ) : (FourierTransform.fourier ((freeSchrodingerS t) ψ)) ξ = fresnelSymbol (Complex.I * ↑t / 2) ξ * (FourierTransform.fourier ψ) ξ

The Fourier transform of the free propagator applied to a Schwartz function.

theorem SchrodingerGroup.freeSchrodingerS_apply_eq_integral (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ((freeSchrodingerS t) ψ) x = ∫ (ξ : ℝ), Real.fourierChar (inner ℝ ξ x) • (fresnelSymbol (Complex.I * ↑t / 2) ξ * (FourierTransform.fourier ψ) ξ)

theorem SchrodingerGroup.continuous_fourierChar_inner (x : ℝ) : Continuous fun (ξ : ℝ) => Real.fourierChar (inner ℝ ξ x)

theorem SchrodingerGroup.continuous_ofReal_add_I_mul (t : ℝ) : Continuous fun (ε : ℝ) => ↑ε + Complex.I * ↑t / 2

theorem SchrodingerGroup.tendsto_ofReal_add_I_mul (t : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ↑ε + Complex.I * ↑t / 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Complex.I * ↑t / 2))

theorem SchrodingerGroup.tendsto_fresnelOp (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ((fresnelOp (↑ε + Complex.I * ↑t / 2)) ψ) x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (((freeSchrodingerS t) ψ) x))

★★★ The Gaussian-regularised Fresnel integral is the free propagator: for Schwartz data, (U₀(t)ψ)(x) = lim_{ε ↓ 0} (e^{−(ε + it/2)H₀} ψ)(x), every term on the left an absolutely convergent kernel integral. The proof is dominated convergence on the Fourier side: the multiplier e^{−4π²(ε + it/2)ξ²} has modulus ≤ 1 and tends pointwise to the free phase, and 𝓕ψ is integrable.

theorem SchrodingerGroup.tendsto_integral_fresnelKernel_freeSchrodingerS (t : ℝ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (y : ℝ), fresnelKernel (↑ε + Complex.I * ↑t / 2) (x - y) * ψ y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (((freeSchrodingerS t) ψ) x))

★★★ The same limit as the kernel integral the physics writes: (U₀(t)ψ)(x) = lim_{ε ↓ 0} ∫ (4π(ε + it/2))^{−1/2} e^{−(x−y)²/(4(ε + it/2))} ψ(y) dy.

theorem SchrodingerGroup.tendsto_fresnelOp_iterate (t : ℝ) (n : ℕ) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ((⇑(fresnelOp ((↑ε + Complex.I * ↑t / 2) / (↑n + 1))))^[n + 1] ψ) x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (((freeSchrodingerS t) ψ) x))

★★ Feynman's time-slicing, regularised: for every number of slices the n+1-fold iterated kernel integral has the same ε ↓ 0 limit, the propagator.

Feynman's kernel

theorem SchrodingerGroup.fresnelKernel_I_mul {t : ℝ} (ht : t ≠ 0) (x : ℝ) : fresnelKernel (Complex.I * ↑t / 2) x = (2 * ↑Real.pi * Complex.I * ↑t) ^ (-1 / 2) * Complex.exp (Complex.I * ↑x ^ 2 / (2 * ↑t))

★ Feynman's kernel: at purely imaginary time w = it/2 the complex-time kernel is (2πit)^{−1/2} e^{ix²/(2t)}, the kernel of the path integral.

theorem SchrodingerGroup.norm_fresnelKernel_I_mul {t : ℝ} (ht : t ≠ 0) (x : ℝ) : ‖fresnelKernel (Complex.I * ↑t / 2) x‖ = ‖fresnelAmp (Complex.I * ↑t / 2)‖

The Feynman kernel has constant modulus: it does not decay, which is why the Fresnel integral is improper for general L² data — and why it is nevertheless absolutely convergent against the L¹ Schwartz functions used here.

theorem SchrodingerGroup.integrable_fresnelKernel_mul {t : ℝ} (ht : t ≠ 0) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : MeasureTheory.Integrable (fun (y : ℝ) => fresnelKernel (Complex.I * ↑t / 2) (x - y) * ψ y) MeasureTheory.volume

★ The Feynman integral converges absolutely for Schwartz data: the kernel is bounded and ψ is integrable.

theorem SchrodingerGroup.tendsto_integral_fresnelKernel {t : ℝ} (ht : t ≠ 0) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (y : ℝ), fresnelKernel (↑ε + Complex.I * ↑t / 2) (x - y) * ψ y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (y : ℝ), fresnelKernel (Complex.I * ↑t / 2) (x - y) * ψ y))

The ε ↓ 0 limit of the regularised kernel integrals is the Feynman integral: the amplitude converges by continuity of the principal square root off the cut, and the Gaussian factor by dominated convergence (its modulus is ≤ 1 for Re w ≥ 0).

theorem SchrodingerGroup.freeSchrodingerS_eq_integral_fresnel {t : ℝ} (ht : t ≠ 0) (ψ : SchwartzMap ℝ ℂ) (x : ℝ) : ((freeSchrodingerS t) ψ) x = (2 * ↑Real.pi * Complex.I * ↑t) ^ (-1 / 2) * ∫ (y : ℝ), Complex.exp (Complex.I * ↑(x - y) ^ 2 / (2 * ↑t)) * ψ y

★★★ Feynman's kernel formula, exactly: for Schwartz data and t ≠ 0, (U₀(t)ψ)(x) = (2πit)^{−1/2} ∫ e^{i(x−y)²/(2t)} ψ(y) dy, an absolutely convergent integral — no regularisation is left in the statement. The Gaussian regularisation proves it: the regularised integrals converge to the propagator (tendsto_fresnelOp) and to this integral (tendsto_integral_fresnelKernel), and limits in ℂ are unique.

theorem SchrodingerGroup.freeSchrodingerS_add (t₁ t₂ : ℝ) (ψ : SchwartzMap ℝ ℂ) : (freeSchrodingerS t₁) ((freeSchrodingerS t₂) ψ) = (freeSchrodingerS (t₁ + t₂)) ψ

The free propagator is a one-parameter group on Schwartz functions.

theorem SchrodingerGroup.freeSchrodingerS_iterate_eq (s : ℝ) (n : ℕ) (ψ : SchwartzMap ℝ ℂ) : (⇑(freeSchrodingerS s))^[n + 1] ψ = (freeSchrodingerS ((↑n + 1) * s)) ψ

theorem SchrodingerGroup.freeSchrodingerS_iterate (t : ℝ) (n : ℕ) (ψ : SchwartzMap ℝ ℂ) : (⇑(freeSchrodingerS (t / (↑n + 1))))^[n + 1] ψ = (freeSchrodingerS t) ψ

★★ The propagator is its own n-slice product: U₀(t) = (U₀(t/(n+1)))^{n+1}, so the n-slice iterated Feynman integral is exact for every n, not only in a limit.

The discrete action

noncomputable def SchrodingerGroup.discreteAction (t : ℝ) (n : ℕ) (q : ℕ → ℝ) : ℝ

The discrete action of a path q : ℕ → ℝ sampled at n steps of duration t/n: S_n = ∑_{k<n} (q_{k+1} − q_k)²/(2Δt), the Riemann sum of ∫ ½ q̇² ds for the free Lagrangian.

Equations

• SchrodingerGroup.discreteAction t n q = ∑ k ∈ Finset.range n, (q (k + 1) - q k) ^ 2 / (2 * (t / ↑n))

theorem SchrodingerGroup.prod_fresnelKernel_eq_exp_discreteAction {t : ℝ} (ht : t ≠ 0) (n : ℕ) (hn : n ≠ 0) (q : ℕ → ℝ) : ∏ k ∈ Finset.range n, fresnelKernel (Complex.I * (↑t / ↑n) / 2) (q (k + 1) - q k) = fresnelAmp (Complex.I * (↑t / ↑n) / 2) ^ n * Complex.exp (Complex.I * ↑(discreteAction t n q))

★★★ e^{iS_n} is the integrand: the product of the n Feynman kernels that make up the n-slice iterated integral is ((2πit/n)^{−1/2})^n e^{iS_n}, with S_n the discrete action of the sampled path. The phase of the path integral is a theorem, not a notation.