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:

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

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) :
theorem integrable_rpow_mul_exp_neg_mul_sq {b : } (hb : 0 < b) {s : } (hs : -1 < s) :
theorem norm_cexp_neg_mul_sq (b : ) (x : ) :
cexp (-b * x ^ 2) = rexp (-b.re * x ^ 2)
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

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

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
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.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)