Gaussian Moments and Fourier Properties

This file contains lemmas about moments of Gaussian functions and their Fourier transforms, specifically supporting the frame condition proof in exists_golden_peak_proof.

def Frourio.normalizedGaussianLp (δ : ℝ) (hδ : 0 < δ) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Equations

• Frourio.normalizedGaussianLp δ hδ = Classical.choose ⋯

theorem Frourio.div_sqrt_mul_delta {A : ℂ} {δ : ℝ} (hδ : 0 < δ) : A / ↑√δ * ↑δ = A * ↑√δ

A helper lemma showing that A / √δ * δ = A * √δ for positive δ. This simplifies the algebraic manipulation in the Gaussian Fourier transform proof.

theorem Frourio.delta_sq_inv_sq {δ : ℝ} (hδ : 0 < δ) : ↑δ * ↑δ * ((↑δ)⁻¹ * (↑δ)⁻¹) = 1

Helper lemma: δ² * δ⁻² = 1 in complex numbers

theorem Frourio.complete_square_simplify {δ : ℝ} (hδ : 0 < δ) (ξ t : ℝ) : -↑Real.pi / ↑δ ^ 2 * (↑t + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2 + ↑Real.pi / ↑δ ^ 2 * -1 * (↑δ ^ 2) ^ 2 * ↑ξ ^ 2 = -↑Real.pi / ↑δ ^ 2 * (↑t + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2 - ↑Real.pi * ↑δ ^ 2 * ↑ξ ^ 2

Helper lemma for completing the square calculation. Shows that -π/δ² * (t + Iδ²ξ)² + π/δ² * (-1) * (δ²)² * ξ² = -π/δ² * (t + Iδ²ξ)² - πδ²ξ²

theorem Frourio.gaussian_exponent_complete_square {δ : ℝ} (hδ : 0 < δ) (ξ t : ℝ) : -↑Real.pi / ↑δ ^ 2 * ↑t ^ 2 - 2 * ↑Real.pi * Complex.I * ↑ξ * ↑t = -↑Real.pi / ↑δ ^ 2 * (↑t + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2 - ↑Real.pi * ↑δ ^ 2 * ↑ξ ^ 2

Complete the square in the exponent appearing in Gaussian integrals. This is the algebraic identity -π/δ² * t² - 2π I ξ t = -π/δ² (t + I δ² ξ)² - π δ² ξ² over the complex numbers.

theorem Frourio.complex_gaussian_contour_shift {δ : ℝ} (hδ : 0 < δ) (ξ : ℝ) : ∫ (a : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * (↑a + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2) = ∫ (s : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * ↑s ^ 2)

Complex contour shift for Gaussian integrals. For a Gaussian function, shifting the integration contour by a purely imaginary constant doesn't change the integral value. This is a consequence of Cauchy's theorem for entire functions with sufficient decay.

@[simp]

theorem Frourio.integral_ofReal' {f : ℝ → ℝ} : ∫ (x : ℝ), ↑(f x) = ↑(∫ (x : ℝ), f x)

Helper lemma for integral_ofReal with specific type signatures.

theorem Frourio.gaussian_integral_complex {δ : ℝ} (hδ : 0 < δ) : ∫ (s : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * ↑s ^ 2) = ↑δ

Standard complex Gaussian integral. The integral of exp(-π/δ² * s²) over ℝ equals δ. This is the complex version of the standard Gaussian integral formula.

theorem Frourio.shifted_gaussian_integral {δ : ℝ} (hδ : 0 < δ) (ξ : ℝ) : ∫ (t : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * (↑t + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2) = ↑δ

Shifted Gaussian integral formula. The integral of exp(-π/δ²(t + Iδ²ξ)²) over ℝ equals δ. This represents a Gaussian shifted by a pure imaginary amount.

theorem Frourio.complex_shifted_gaussian_integral {δ : ℝ} (hδ : 0 < δ) (ξ : ℝ) : ∫ (t : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * (↑t + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2) = ↑δ

Complex shifted Gaussian integral formula. The integral of exp(-π/δ²(t + Iδ²ξ)²) over ℝ equals δ.

theorem Frourio.gaussian_fourier_real_exp {δ : ℝ} (hδ : 0 < δ) (ξ : ℝ) : ∫ (t : ℝ), Complex.exp (↑(-2 * Real.pi * ξ * t) * Complex.I) * ↑(Real.exp (-Real.pi * t ^ 2 / δ ^ 2)) = ↑δ * Complex.exp (-↑Real.pi * ↑δ ^ 2 * ↑ξ ^ 2)

The Fourier transform of a Gaussian with real exponential form. This variant uses Real.exp with coercion to complex numbers.

theorem Frourio.gaussian_fourier_transform {δ : ℝ} (hδ : 0 < δ) : Real.fourierIntegral ↑↑(normalizedGaussianLp δ hδ) = fun (ξ : ℝ) => 2 ^ (1 / 4) * ↑√δ * Complex.exp (-↑Real.pi * ↑δ ^ 2 * ↑ξ ^ 2)

Explicit formula for the Fourier transform of a normalized Gaussian. The Fourier transform of a Gaussian is another Gaussian with reciprocal width.