Feynman-Kac formula

In plain terms

Feynman's path integral says that a quantum amplitude is a sum over all histories, each contributing a phase. It's the most intuitive statement in quantum mechanics and the hardest to make mathematically respectable, since the sum is over an infinite-dimensional space of paths and the phases refuse to settle down.

Kac noticed that the difficulty is the phase rather than the sum. Replace time by imaginary time and the oscillating phases become decaying weights, and the resulting integral over paths is a perfectly ordinary average with respect to the measure that describes Brownian motion, which mathematics already had. The formula that comes out says: to solve a diffusion equation with a potential, start a Brownian path at your point, follow it for the given time, weight it by the exponential of minus the potential accumulated along the way, and average.

This is the workhorse behind quantum Monte Carlo methods, behind the modern treatment of Schrodinger operators, and behind option pricing in finance, which is the same equation wearing different clothes. The real-time path integral remains a formal device, and the imaginary-time version is a theorem.

In CSD

The programme's claim is that the formulations of quantum mechanics agree, so the path integral had to be proved rather than gestured at, and the corpus builds it in a chain of rows. The perturbed heat semigroup comes first, as a Dyson series around the free semigroup with the potential as the interaction and no generator written down. The time-sliced Wiener functional comes next. The formula is then the statement that the two limits of the same time-sliced expression agree, one converging by the Trotter product formula and one by the convergence of Riemann sums along a continuous path.

The same chain supports the rest of the programme's Feynman row: a unitary Schrodinger propagator on square-integrable functions, the heat semigroup, and the Nelson result that connects the diffusion picture to the Schrodinger equation. The honest boundary is that a Brownian motion is a hypothesis rather than a construction, since the Mathlib pin doesn't build one, and that the potential is bounded and continuous.

Mathematically

For a Brownian motion B with almost surely continuous paths, bounded continuous V and bounded f in L2 of d-dimensional space, feynmanKac states that the perturbed heat semigroup applied to f at x equals the expectation of f(x + B_t) times exp(minus the integral of V(x + B_s) over [0, t]), for almost every x. The operator side converges by tendsto_trotter_perturbedHeat once exp_smul_neg_potential identifies the exponential of a multiplication operator with multiplication by the exponential; the Wiener side is the time-sliced functional of TimeSlicedWiener.lean with tendsto_riemannSum and domination; the two limits agree because their integrals over every finite-measure set agree.

IsBrownianVec B P is a hypothesis (BrownianVec.lean); the extension to f in L2 alone is FeynmanKacL2.lean. The real-time path integral is not claimed anywhere in the corpus; the unitary propagator is obtained from the semigroup route instead.

The name

Mark Kac heard Feynman describe the path integral at a Cornell seminar in the late 1940s and recognised his own Wiener-integral formulas in it, which is how the formula came to carry both names although the two men worked on different problems. Kac's paper that year is about distributions of Wiener functionals and never mentions quantum mechanics.

Richard Feynman's thesis of 1942 and his 1948 paper introduced the sum over histories as a reformulation of quantum mechanics, and it remains the language of quantum field theory, where the imaginary-time version is what lattice calculations actually compute.

Related entries

• Lie-Trotter product formulaAlternate many tiny steps of two operations that don't commute and the result converges to the exponential of their sum, with an error that shrinks like one over the number of steps, and CSD proves this in textbook generality, in a form ready for the Mathlib library, because its open-systems tier needed it and nothing on the shelf existed.
• Schrodinger equationIn CSD the Schrodinger equation isn't postulated, as it's what any continuous motion that preserves the measurable relations between quantum states is forced to look like.
• Nelson stochastic mechanicsNelson derived the Schrodinger equation from a diffusion, so the same continuity equation that lets Bohm read a velocity off the wavefunction lets Nelson read a drift with noise against it, and the Born density solves both.
• Stone's theoremAsk only that time evolution never jumps, and differentiability, a generator and the Hamiltonian all follow for free.
• Gibbs stateThe state a system settles into at a given temperature is the unique solution to a trade-off between energy and disorder.