Fourier Transforms for QFT

This file contains Fourier transform identities needed for the Gaussian Free Field, particularly for proving reflection positivity of the free covariance.

Main Results

• fourier_lorentzian_1d: The 1D Fourier transform of the Lorentzian 1/(k² + μ²) gives exponential decay: ∫ dk e^{ikx} / (k² + μ²) = (π/μ) e^{-μ|x|}

• fourier_exponential_decay: The inverse transform - Fourier transform of e^{-μ|x|} gives the Lorentzian: ∫ dx e^{-ikx} e^{-μ|x|} = 2μ/(k² + μ²)

• exp_factorization_reflection: Key factorization for reflection positivity

Mathematical Background

The key identity for reflection positivity is:

C(x - y) = ∫ d⁴k / (2π)⁴ · e^{ik·(x-y)} / (k² + m²)

For the time direction k₀, we need:

∫ dk₀ e^{ik₀(x₀ - y₀)} / (k₀² + μ²) = (π/μ) e^{-μ|x₀ - y₀|}

where μ² = |pbar|² + m² (with pbar the spatial momentum).

When x₀ > 0 and y₀ < 0 (positive and negative time respectively), we have x₀ - y₀ > 0, so the exponential is e^{-μ(x₀ - y₀)} which factorizes as e^{-μx₀} · e^{μy₀}, enabling the reflection positivity argument.

Proof Strategy

The 1D result follows from Fourier inversion:

1. Compute half-line integrals using the fundamental theorem of calculus
2. Sum to get FT[e^{-μ|x|}] = 2μ/(k² + μ²)
3. Apply Fourier inversion to derive the Lorentzian result

Dependencies

No axioms declared in this file.

theorem fubini_triple_reorder {α : Type u_1} [MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume] {F : α → α → α → ℂ} (hF : MeasureTheory.Integrable (fun (p : α × α × α) => F p.1 p.2.1 p.2.2) (MeasureTheory.volume.prod (MeasureTheory.volume.prod MeasureTheory.volume))) : ∫ (x : α) (y : α) (k : α), F x y k = ∫ (k : α) (x : α) (y : α), F x y k

Fubini reordering for triple integrals.

For integrable functions on α × α × α, we can reorder the integration from ∫x ∫y ∫k to ∫k ∫x ∫y.

This follows from Fubini-Tonelli: if F is integrable on the product space, then we can integrate in any order.

theorem integrable_exponential_decay (μ : ℝ) (hμ : 0 < μ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-μ * |x|)) MeasureTheory.volume

The exponential decay function is integrable when μ > 0. Proof: Split ℝ into (-∞, 0] ∪ (0, ∞) and use:

• integrableOn_exp_mul_Iic for exp(μx) on (-∞, 0] (since μ > 0)
• integrableOn_exp_mul_Ioi for exp(-μx) on (0, ∞) (since -μ < 0)

theorem integrable_exponential_decay_fourier (μ : ℝ) (hμ : 0 < μ) (k : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (Complex.I * ↑k * ↑x) * ↑(Real.exp (-μ * |x|))) MeasureTheory.volume

The Fourier integrand of exponential decay is integrable. Proof: |exp(ikx)| = 1, so the norm of the integrand equals exp(-μ|x|), which is integrable by integrable_exponential_decay.

Half-Line Integrals and Antiderivatives

The half-line integrals are the fundamental building blocks. We compute these using the fundamental theorem of calculus for improper integrals, then combine them to get the Fourier transform of e^{-μ|x|}, and finally use Fourier inversion to derive the Lorentzian result.

theorem ik_add_ne_zero (α : ℝ) (hα : α ≠ 0) (k : ℝ) : Complex.I * ↑k + ↑α ≠ 0

The coefficient ik + α is nonzero when α ≠ 0 (since Re(ik + α) = α ≠ 0).

theorem antideriv_exp_complex_linear (α : ℝ) (hα : α ≠ 0) (k x : ℝ) : HasDerivAt (fun (t : ℝ) => Complex.exp ((Complex.I * ↑k + ↑α) * ↑t) / (Complex.I * ↑k + ↑α)) (Complex.exp ((Complex.I * ↑k + ↑α) * ↑x)) x

The antiderivative of e^{(ik+α)x} for α ≠ 0. This is the indefinite integral: ∫ e^{(ik+α)x} dx = e^{(ik+α)x} / (ik + α)

The denominator ik + α is never zero since Re(ik + α) = α ≠ 0.

Special cases:

• α = -μ (μ > 0): gives decay on [0,∞), converges at +∞
• α = +μ (μ > 0): gives growth on (-∞,0], converges at -∞

theorem tendsto_cexp_atTop_zero {c : ℂ} (hc : c.re < 0) : Filter.Tendsto (fun (x : ℝ) => Complex.exp (c * ↑x)) Filter.atTop (nhds 0)

Complex exponential e^{cx} tends to 0 as x → +∞ when Re(c) < 0. Proof: ‖e^{cx}‖ = e^{Re(c)·x} → 0 since Re(c) < 0 and x → +∞.

theorem tendsto_cexp_atBot_zero {c : ℂ} (hc : c.re > 0) : Filter.Tendsto (fun (x : ℝ) => Complex.exp (c * ↑x)) Filter.atBot (nhds 0)

Complex exponential e^{cx} tends to 0 as x → -∞ when Re(c) > 0. Proof: ‖e^{cx}‖ = e^{Re(c)·x} → 0 since Re(c) > 0 and x → -∞.

theorem integrableOn_exp_decay_Ioi (μ : ℝ) (hμ : 0 < μ) (k : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Complex.exp ((Complex.I * ↑k - ↑μ) * ↑x)) (Set.Ioi 0) MeasureTheory.volume

The integrand e^{(ik-μ)x} is integrable on [0, ∞) when μ > 0. This follows from the exponential decay since Re(ik - μ) = -μ < 0.

theorem exp_pos_integrableOn_Iio (a : ℝ) {b : ℝ} (h : 0 < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (b * x)) (Set.Iio a) MeasureTheory.volume

Exponential e^{bx} is integrable on (-∞, a) when b > 0. Proved by change of variables from exp_neg_integrableOn_Ioi.

theorem exp_pos_integrableOn_Iic (a : ℝ) {b : ℝ} (h : 0 < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (b * x)) (Set.Iic a) MeasureTheory.volume

Exponential e^{bx} is integrable on (-∞, a] when b > 0. Follows from Iio version since measure of a point is 0.

theorem integrableOn_exp_growth_Iic (μ : ℝ) (hμ : 0 < μ) (k : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Complex.exp ((Complex.I * ↑k + ↑μ) * ↑x)) (Set.Iic 0) MeasureTheory.volume

The integrand e^{(ik+μ)x} is integrable on (-∞, 0] when μ > 0. This follows from the exponential decay since Re(ik + μ) = μ > 0.

theorem ik_sub_ne_zero (μ : ℝ) (hμ : μ ≠ 0) (k : ℝ) : Complex.I * ↑k - ↑μ ≠ 0

ik - μ is nonzero when μ ≠ 0 (since Re(ik - μ) = -μ ≠ 0).

theorem fourier_exp_decay_positive_halfline (μ : ℝ) (hμ : 0 < μ) (k : ℝ) : ∫ (x : ℝ) in Set.Ioi 0, Complex.exp (Complex.I * ↑k * ↑x) * ↑(Real.exp (-μ * x)) = 1 / (↑μ - Complex.I * ↑k)

The integral over the positive half-line [0, ∞): ∫₀^∞ e^{ikx} e^{-μx} dx = 1/(μ - ik)

Proof: Use FTC with antiderivative e^{(ik-μ)x}/(ik-μ). At +∞: e^{(ik-μ)x} → 0 since Re(ik-μ) = -μ < 0. At 0: e^0/(ik-μ) = 1/(ik-μ). Result: 0 - 1/(ik-μ) = -1/(ik-μ) = 1/(μ-ik).

theorem fourier_exp_decay_negative_halfline (μ : ℝ) (hμ : 0 < μ) (k : ℝ) : ∫ (x : ℝ) in Set.Iic 0, Complex.exp (Complex.I * ↑k * ↑x) * ↑(Real.exp (μ * x)) = 1 / (↑μ + Complex.I * ↑k)

The integral over the negative half-line (-∞, 0]: ∫_{-∞}^0 e^{ikx} e^{μx} dx = 1/(μ + ik)

Proof: Use FTC with antiderivative e^{(ik+μ)x}/(ik+μ). At -∞: e^{(ik+μ)x} → 0 since Re(ik+μ) = μ > 0. At 0: e^0/(ik+μ) = 1/(ik+μ) = 1/(μ+ik).

theorem fourier_exponential_decay_split (μ : ℝ) (hμ : 0 < μ) (k : ℝ) : (∫ (x : ℝ) in Set.Iic 0, Complex.exp (Complex.I * ↑k * ↑x) * ↑(Real.exp (μ * x))) + ∫ (x : ℝ) in Set.Ioi 0, Complex.exp (Complex.I * ↑k * ↑x) * ↑(Real.exp (-μ * x)) = 2 * ↑μ / (↑k ^ 2 + ↑μ ^ 2)

The full integral as sum of half-line integrals. This is the key decomposition: ∫{-∞}^∞ e^{ikx} e^{-μ|x|} dx = ∫{-∞}^0 e^{ikx} e^{μx} dx + ∫_0^∞ e^{ikx} e^{-μx} dx = 1/(μ+ik) + 1/(μ-ik) = 2μ/(k² + μ²)

Fourier Transform of Exponential Decay

The Fourier transform of e^{-μ|x|} gives the Lorentzian 2μ/(k² + μ²). This is the "forward" direction of the Fourier pair.

theorem fourier_exponential_decay' (μ : ℝ) (hμ : 0 < μ) (k : ℝ) : ∫ (x : ℝ), Complex.exp (Complex.I * ↑k * ↑x) * ↑(Real.exp (-μ * |x|)) = 2 * ↑μ / (↑k ^ 2 + ↑μ ^ 2)

The Fourier transform of the exponential decay function e^{-μ|x|}. ∫_{-∞}^{∞} e^{ikx} e^{-μ|x|} dx = 2μ/(k² + μ²)

This follows from splitting at x = 0 (see fourier_exponential_decay_split).

theorem fourier_exponential_decay (μ : ℝ) (hμ : 0 < μ) (k : ℝ) : ∫ (x : ℝ), Complex.exp (-Complex.I * ↑k * ↑x) * ↑(Real.exp (-μ * |x|)) = 2 * ↑μ / (↑k ^ 2 + ↑μ ^ 2)

Variant with negative frequency convention e^{-ikx}.

Fourier Inversion and the Lorentzian Transform

By the Fourier inversion theorem, if FTf = g(k), then IFTg = f(x). Since FTe^{-μ|x|} = 2μ/(k² + μ²), the inverse gives: (1/2π) ∫ e^{ikx} · 2μ/(k² + μ²) dk = e^{-μ|x|} Rearranging: ∫ e^{ikx} / (k² + μ²) dk = (π/μ) e^{-μ|x|}

Relation to Mathlib's Fourier Transform

Mathlib's Fourier transform uses the convention: FT_mathlib(f)(ξ) = ∫ exp(2πi⟨x,ξ⟩) f(x) dx

For ℝ with standard inner product ⟨x,ξ⟩ = xξ, this becomes: FT_mathlib(f)(ξ) = ∫ exp(2πixξ) f(x) dx

Our convention uses: FT(f)(k) = ∫ exp(ikx) f(x) dx

The relationship is: FT(f)(k) = FT_mathlib(f)(k/(2π))

Mathlib provides MeasureTheory.Integrable.fourierInv_fourier_eq which says: If f is integrable, FT(f) is integrable, and f is continuous at x, then IFT(FT(f))(x) = f(x)

noncomputable def expDecayFun (μ : ℝ) : ℝ → ℂ

The exponential decay function e^{-μ|x|} as a function ℝ → ℂ.

Equations

• expDecayFun μ x = ↑(Real.exp (-μ * |x|))

theorem continuous_expDecayFun (μ : ℝ) : Continuous (expDecayFun μ)

The exponential decay function is continuous.

theorem integrable_expDecayFun (μ : ℝ) (hμ : 0 < μ) : MeasureTheory.Integrable (expDecayFun μ) MeasureTheory.volume

The exponential decay function is integrable over ℝ.

theorem fourierIntegral_expDecayFun_eq (μ : ℝ) (hμ : 0 < μ) (ξ : ℝ) : FourierTransform.fourier (expDecayFun μ) ξ = 2 * ↑μ / (4 * ↑Real.pi ^ 2 * ↑ξ ^ 2 + ↑μ ^ 2)

Mathlib's Fourier transform of expDecayFun equals the scaled Lorentzian. FT_mathlib(e^{-μ|x|})(ξ) = 2μ/(4π²ξ² + μ²) This follows from fourier_exponential_decay' via the substitution k = -2πξ.

theorem integrable_fourierIntegral_expDecayFun (μ : ℝ) (hμ : 0 < μ) : MeasureTheory.Integrable (FourierTransform.fourier (expDecayFun μ)) MeasureTheory.volume

The Mathlib Fourier transform of expDecayFun is integrable.

theorem fourier_inversion_exp_decay (μ : ℝ) (hμ : 0 < μ) (x : ℝ) : 1 / (2 * ↑Real.pi) * ∫ (k : ℝ), Complex.exp (Complex.I * ↑k * ↑x) * (2 * ↑μ / (↑k ^ 2 + ↑μ ^ 2)) = ↑(Real.exp (-μ * |x|))

Fourier inversion theorem for the exponential decay / Lorentzian pair. If FTe^{-μ|x|} = 2μ/(k² + μ²), then the inverse transform gives: (1/2π) ∫ e^{ikx} · 2μ/(k² + μ²) dk = e^{-μ|x|}

This follows from Mathlib's Fourier inversion theorem applied to the exponential decay function, combined with the explicit formula for its Fourier transform and a change of variables.

The Lorentzian Fourier Transform (Main Result)

We derive the Lorentzian Fourier transform from the Fourier inversion theorem.

theorem fourier_lorentzian_1d (μ : ℝ) (hμ : 0 < μ) (x : ℝ) : ∫ (k : ℝ), Complex.exp (Complex.I * ↑k * ↑x) / (↑k ^ 2 + ↑μ ^ 2) = ↑Real.pi / ↑μ * ↑(Real.exp (-μ * |x|))

The 1D Fourier transform of the Lorentzian/Cauchy distribution. This is the fundamental identity: ∫_{-∞}^{∞} e^{ikx} / (k² + μ²) dk = (π/μ) e^{-μ|x|}

Derivation from Fourier inversion: From fourier_inversion_exp_decay: (1/2π) ∫ e^{ikx} · 2μ/(k² + μ²) dk = e^{-μ|x|} Multiply both sides by π/μ: (1/2π) · (π/μ) · 2μ ∫ e^{ikx} / (k² + μ²) dk = (π/μ) e^{-μ|x|} ∫ e^{ikx} / (k² + μ²) dk = (π/μ) e^{-μ|x|}

theorem exp_factorization_reflection (μ x y : ℝ) (hx : 0 ≤ x) (hy : y ≤ 0) : Real.exp (-μ * |x - y|) = Real.exp (-μ * x) * Real.exp (μ * y)

The exponential from the Lorentzian Fourier transform factorizes. For x, y with x ≥ 0 and y ≤ 0, we have |x - y| = x - y = x + |y|, so e^{-μ|x-y|} = e^{-μx} · e^{-μ|y|} = e^{-μx} · e^{μy}.

theorem fourier_lorentzian_1d_neg (μ : ℝ) (hμ : 0 < μ) (x : ℝ) : ∫ (k : ℝ), Complex.exp (-Complex.I * ↑k * ↑x) / (↑k ^ 2 + ↑μ ^ 2) = ↑Real.pi / ↑μ * ↑(Real.exp (-μ * |x|))

Negative phase variant: ∫ e^{-ikx} / (k² + μ²) dk = (π/μ) e^{-μ|x|}

This follows from fourier_lorentzian_1d by the substitution k ↦ -k. Since (-k)² = k² and the integral over ℝ is symmetric, we get the same result.

Application to Free Field Propagator

The free field propagator in d=4 Euclidean dimensions is:

C(x) = ∫ d⁴k/(2π)⁴ · e^{ik·x} / (k² + m²)

We can split this into time and spatial parts. After integrating over the time component k₀, we get an exponential factor e^{-μ|x₀|} where μ = √(|pbar|² + m²).

Proof Strategy: Fourier Inversion Approach

Overview

The main result fourier_lorentzian_1d is derived via Fourier inversion:

1. Half-line integrals (FTC): Compute ∫₀^∞ e^{(ik-μ)x} dx and ∫_{-∞}^0 e^{(ik+μ)x} dx using the fundamental theorem of calculus for improper integrals.

2. Fourier transform of e^{-μ|x|}: Split into half-lines and sum: FTe^{-μ|x|} = 2μ/(k² + μ²)

3. Fourier inversion: Apply (1/2π) ∫ e^{ikx} · FTf dk = f(x) to get: (1/2π) ∫ e^{ikx} · 2μ/(k² + μ²) dk = e^{-μ|x|}

4. Lorentzian result: Rearrange to obtain: ∫ e^{ikx} / (k² + μ²) dk = (π/μ) e^{-μ|x|}

Key Lemmas (in dependency order)

1. antideriv_exp_complex_linear: d/dx[e^{cx}/c] = e^{cx}
2. tendsto_cexp_atTop_zero, tendsto_cexp_atBot_zero: Limits at ±∞
3. integrableOn_exp_decay_Ioi, integrableOn_exp_growth_Iic: Integrability
4. fourier_exp_decay_positive_halfline, fourier_exp_decay_negative_halfline: Half-line integrals
5. fourier_exponential_decay_split: Sum to get 2μ/(k² + μ²)
6. fourier_inversion_exp_decay: Inversion gives e^{-μ|x|}
7. fourier_lorentzian_1d: Main result

Bridge to OS3

The lemma contour_integral_propagator in OS3 has a negative phase convention. To prove it, use fourier_lorentzian_1d with substitution k ↦ -k:

theorem fourier_lorentzian_1d_neg (μ : ℝ) (hμ : 0 < μ) (x : ℝ) :
    ∫ k : ℝ, Complex.exp (-Complex.I * k * x) / (k^2 + μ^2) = (π / μ) * Real.exp (-μ * |x|)

Then coerce to complex exponential and instantiate with μ = omega m k.

Integrability Lemmas