mathlib3 documentation

analysis.special_functions.gaussian

Gaussian integral #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove various versions of the formula for the Gaussian integral:

integral_gaussian: for real b we have ∫ x:ℝ, exp (-b * x^2) = sqrt (π / b).
integral_gaussian_complex: for complex b with 0 < re b we have ∫ x:ℝ, exp (-b * x^2) = (π / b) ^ (1 / 2).
integral_gaussian_Ioi and integral_gaussian_complex_Ioi: variants for integrals over Ioi 0.
complex.Gamma_one_half_eq: the formula Γ (1 / 2) = √π.

We also prove, more generally, that the Fourier transform of the Gaussian is another Gaussian:

integral_cexp_neg_mul_sq_add_const: for all complex b and c with 0 < re b we have ∫ (x : ℝ), exp (-b * (x + c) ^ 2) = (π / b) ^ (1 / 2).
fourier_transform_gaussian: for all complex b and t with 0 < re b, we have ∫ x:ℝ, exp (I * t * x) * exp (-b * x^2) = (π / b) ^ (1 / 2) * exp (-t ^ 2 / (4 * b)).
fourier_transform_gaussian_pi: a variant with b and t scaled to give a more symmetric statement, and formulated in terms of the Fourier transform operator 𝓕.

As an application, in real.tsum_exp_neg_mul_int_sq and complex.tsum_exp_neg_mul_int_sq, we use Poisson summation to prove the identity ∑' (n : ℤ), exp (-π * a * n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), exp (-π / a * n ^ 2) for positive real a, or complex a with positive real part. (See also number_theory.modular_forms.jacobi_theta.)

theorem exp_neg_mul_sq_is_o_exp_neg {b : ℝ} (hb : 0 < b) :

(λ (x : ℝ), rexp (-b * x ^ 2)) =o[filter.at_top ] λ (x : ℝ), rexp (-x)

theorem rpow_mul_exp_neg_mul_sq_is_o_exp_neg {b : ℝ} (hb : 0 < b) (s : ℝ) :

(λ (x : ℝ), x ^ s * rexp (-b * x ^ 2)) =o[filter.at_top ] λ (x : ℝ), rexp (-(1 / 2) * x)

theorem integrable_on_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :

measure_theory.integrable_on (λ (x : ℝ), x ^ s * rexp (-b * x ^ 2)) (set.Ioi 0) measure_theory.measure_space.volume

theorem integrable_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :

measure_theory.integrable (λ (x : ℝ), x ^ s * rexp (-b * x ^ 2)) measure_theory.measure_space.volume

theorem integrable_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :

measure_theory.integrable (λ (x : ℝ), rexp (-b * x ^ 2)) measure_theory.measure_space.volume

theorem integrable_on_Ioi_exp_neg_mul_sq_iff {b : ℝ} :

measure_theory.integrable_on (λ (x : ℝ), rexp (-b * x ^ 2)) (set.Ioi 0) measure_theory.measure_space.volume ↔ 0 < b

theorem integrable_exp_neg_mul_sq_iff {b : ℝ} :

measure_theory.integrable (λ (x : ℝ), rexp (-b * x ^ 2)) measure_theory.measure_space.volume ↔ 0 < b

theorem integrable_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :

measure_theory.integrable (λ (x : ℝ), x * rexp (-b * x ^ 2)) measure_theory.measure_space.volume

theorem norm_cexp_neg_mul_sq (b : ℂ) (x : ℝ) :

‖cexp (-b * ↑x ^ 2)‖ = rexp (-b.re * x ^ 2)

theorem integrable_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :

measure_theory.integrable (λ (x : ℝ), cexp (-b * ↑x ^ 2)) measure_theory.measure_space.volume

theorem integrable_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :

measure_theory.integrable (λ (x : ℝ), ↑x * cexp (-b * ↑x ^ 2)) measure_theory.measure_space.volume

theorem integral_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :

∫ (r : ℝ) in set.Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹

theorem integral_gaussian_sq_complex {b : ℂ} (hb : 0 < b.re) :

(∫ (x : ℝ), cexp (-b * ↑x ^ 2)) ^ 2 = ↑real.pi / b

The square of the Gaussian integral ∫ x:ℝ, exp (-b * x^2) is equal to π / b.

theorem integral_gaussian (b : ℝ) :

∫ (x : ℝ), rexp (-b * x ^ 2) = √ (real.pi / b)

theorem continuous_at_gaussian_integral (b : ℂ) (hb : 0 < b.re) :

continuous_at (λ (c : ℂ), ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b

theorem integral_gaussian_complex {b : ℂ} (hb : 0 < b.re) :

∫ (x : ℝ), cexp (-b * ↑x ^ 2) = (↑real.pi / b) ^ (1 / 2)

theorem integral_gaussian_complex_Ioi {b : ℂ} (hb : 0 < b.re) :

∫ (x : ℝ) in set.Ioi 0, cexp (-b * ↑x ^ 2) = (↑real.pi / b) ^ (1 / 2) / 2

theorem integral_gaussian_Ioi (b : ℝ) :

∫ (x : ℝ) in set.Ioi 0, rexp (-b * x ^ 2) = √ (real.pi / b) / 2

theorem real.Gamma_one_half_eq :

real.Gamma (1 / 2) = √ real.pi

The special-value formula Γ(1/2) = √π, which is equivalent to the Gaussian integral.

theorem complex.Gamma_one_half_eq :

complex.Gamma (1 / 2) = ↑real.pi ^ (1 / 2)

The special-value formula Γ(1/2) = √π, which is equivalent to the Gaussian integral.

Fourier transform of the Gaussian integral #

noncomputable def gaussian_fourier.vertical_integral (b : ℂ) (c T : ℝ) :

The integral of the Gaussian function over the vertical edges of a rectangle with vertices at (±T, 0) and (±T, c).

Equations

gaussian_fourier.vertical_integral b c T = ∫ (y : ℝ) in 0..c, complex.I * (cexp (-b * (↑T + ↑y * complex.I) ^ 2) - cexp (-b * (↑T - ↑y * complex.I) ^ 2))

theorem gaussian_fourier.norm_cexp_neg_mul_sq_add_mul_I (b : ℂ) (c T : ℝ) :

‖cexp (-b * (↑T + ↑c * complex.I) ^ 2)‖ = rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))

Explicit formula for the norm of the Gaussian function along the vertical edges.

theorem gaussian_fourier.norm_cexp_neg_mul_sq_add_mul_I' {b : ℂ} (hb : b.re ≠ 0) (c T : ℝ) :

‖cexp (-b * (↑T + ↑c * complex.I) ^ 2)‖ = rexp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))

theorem gaussian_fourier.vertical_integral_norm_le {b : ℂ} (hb : 0 < b.re) (c : ℝ) {T : ℝ} (hT : 0 ≤ T) :

‖gaussian_fourier.vertical_integral b c T‖ ≤ 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im | * |c| * T - b.re * c ^ 2))

theorem gaussian_fourier.tendsto_vertical_integral {b : ℂ} (hb : 0 < b.re) (c : ℝ) :

filter.tendsto (gaussian_fourier.vertical_integral b c) filter.at_top (nhds 0)

theorem gaussian_fourier.integrable_cexp_neg_mul_sq_add_real_mul_I {b : ℂ} (hb : 0 < b.re) (c : ℝ) :

measure_theory.integrable (λ (x : ℝ), cexp (-b * (↑x + ↑c * complex.I) ^ 2)) measure_theory.measure_space.volume

theorem gaussian_fourier.integral_cexp_neg_mul_sq_add_real_mul_I {b : ℂ} (hb : 0 < b.re) (c : ℝ) :

∫ (x : ℝ), cexp (-b * (↑x + ↑c * complex.I) ^ 2) = (↑real.pi / b) ^ (1 / 2)

theorem integral_cexp_neg_mul_sq_add_const {b : ℂ} (hb : 0 < b.re) (c : ℂ) :

∫ (x : ℝ), cexp (-b * (↑x + c) ^ 2) = (↑real.pi / b) ^ (1 / 2)

theorem fourier_transform_gaussian {b : ℂ} (hb : 0 < b.re) (t : ℂ) :

∫ (x : ℝ), cexp (complex.I * t * ↑x) * cexp (-b * ↑x ^ 2) = cexp (-t ^ 2 / (4 * b)) * (↑real.pi / b) ^ (1 / 2)

theorem fourier_transform_gaussian_pi {b : ℂ} (hb : 0 < b.re) :

real.fourier_integral (λ (x : ℝ), cexp (-↑real.pi * b * ↑x ^ 2)) = λ (t : ℝ), 1 / b ^ (1 / 2) * cexp (-↑real.pi / b * ↑t ^ 2)

Poisson summation applied to the Gaussian #

theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact {a : ℝ} (ha : 0 < a) (s : ℝ) :

filter.tendsto (λ (x : ℝ), |x| ^ s * rexp (-a * x ^ 2)) (filter.cocompact ℝ) (nhds 0)

theorem is_o_exp_neg_mul_sq_cocompact {a : ℂ} (ha : 0 < a.re) (s : ℝ) :

(λ (x : ℝ), cexp (-a * ↑x ^ 2)) =o[filter.cocompact ℝ] λ (x : ℝ), |x| ^ s

theorem complex.tsum_exp_neg_mul_int_sq {a : ℂ} (ha : 0 < a.re) :

∑' (n : ℤ), cexp (-↑real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑real.pi / a * ↑n ^ 2)

theorem real.tsum_exp_neg_mul_int_sq {a : ℝ} (ha : 0 < a) :

∑' (n : ℤ), rexp (-real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), rexp (-real.pi / a * ↑n ^ 2)