Gaussian integral

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_quadratic: general formula for ∫ (x : ℝ), exp (b * x ^ 2 + c * x + d)
• fourierIntegral_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)).
• fourierIntegral_gaussian_pi: a variant with b and t scaled to give a more symmetric statement, and formulated in terms of the Fourier transform operator 𝓕.

We also give versions of these formulas in finite-dimensional inner product spaces, see integral_cexp_neg_mul_sq_norm_add and fourierIntegral_gaussian_innerProductSpace.

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 NumberTheory.ModularForms.JacobiTheta.)

theorem exp_neg_mul_rpow_isLittleO_exp_neg {p : ℝ} {b : ℝ} (hb : 0 < b) (hp : 1 < p) : (fun (x : ℝ) => Real.exp (-b * x ^ p)) =o[Filter.atTop] fun (x : ℝ) => Real.exp (-x)

theorem exp_neg_mul_sq_isLittleO_exp_neg {b : ℝ} (hb : 0 < b) : (fun (x : ℝ) => Real.exp (-b * x ^ 2)) =o[Filter.atTop] fun (x : ℝ) => Real.exp (-x)

theorem rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg (s : ℝ) {b : ℝ} {p : ℝ} (hp : 1 < p) (hb : 0 < b) : (fun (x : ℝ) => x ^ s * Real.exp (-b * x ^ p)) =o[Filter.atTop] fun (x : ℝ) => Real.exp (-(1 / 2) * x)

theorem rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg {b : ℝ} (hb : 0 < b) (s : ℝ) : (fun (x : ℝ) => x ^ s * Real.exp (-b * x ^ 2)) =o[Filter.atTop] fun (x : ℝ) => Real.exp (-(1 / 2) * x)

theorem integrableOn_rpow_mul_exp_neg_rpow {p : ℝ} {s : ℝ} (hs : -1 < s) (hp : 1 ≤ p) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ s * Real.exp (-x ^ p)) (Set.Ioi 0) MeasureTheory.volume

theorem integrableOn_rpow_mul_exp_neg_mul_rpow {p : ℝ} {s : ℝ} {b : ℝ} (hs : -1 < s) (hp : 1 ≤ p) (hb : 0 < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ s * Real.exp (-b * x ^ p)) (Set.Ioi 0) MeasureTheory.volume

theorem integrableOn_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) : MeasureTheory.IntegrableOn (fun (x : ℝ) => x ^ s * Real.exp (-b * x ^ 2)) (Set.Ioi 0) MeasureTheory.volume

theorem integrable_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ s * Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem integrable_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem integrableOn_Ioi_exp_neg_mul_sq_iff {b : ℝ} : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-b * x ^ 2)) (Set.Ioi 0) MeasureTheory.volume ↔ 0 < b

theorem integrable_exp_neg_mul_sq_iff {b : ℝ} : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-b * x ^ 2)) MeasureTheory.volume ↔ 0 < b

theorem integrable_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (x : ℝ) => x * Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem norm_cexp_neg_mul_sq (b : ℂ) (x : ℝ) : ‖Complex.exp (-b * ↑x ^ 2)‖ = Real.exp (-b.re * x ^ 2)

theorem integrable_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (-b * ↑x ^ 2)) MeasureTheory.volume

theorem integrable_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) : MeasureTheory.Integrable (fun (x : ℝ) => ↑x * Complex.exp (-b * ↑x ^ 2)) MeasureTheory.volume

theorem integral_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) : ∫ (r : ℝ) in Set.Ioi 0, ↑r * Complex.exp (-b * ↑r ^ 2) = (2 * b)⁻¹

theorem integral_gaussian_sq_complex {b : ℂ} (hb : 0 < b.re) : (∫ (x : ℝ), Complex.exp (-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 : ℝ), Real.exp (-b * x ^ 2) = Real.sqrt (Real.pi / b)

theorem continuousAt_gaussian_integral (b : ℂ) (hb : 0 < b.re) : ContinuousAt (fun (c : ℂ) => ∫ (x : ℝ), Complex.exp (-c * ↑x ^ 2)) b

theorem integral_gaussian_complex {b : ℂ} (hb : 0 < b.re) : ∫ (x : ℝ), Complex.exp (-b * ↑x ^ 2) = (↑Real.pi / b) ^ (1 / 2)

theorem integral_gaussian_complex_Ioi {b : ℂ} (hb : 0 < b.re) : ∫ (x : ℝ) in Set.Ioi 0, Complex.exp (-b * ↑x ^ 2) = (↑Real.pi / b) ^ (1 / 2) / 2

theorem integral_gaussian_Ioi (b : ℝ) : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-b * x ^ 2) = Real.sqrt (Real.pi / b) / 2

theorem Real.Gamma_one_half_eq : Real.Gamma (1 / 2) = Real.sqrt 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 integral of Gaussian functions

def GaussianFourier.verticalIntegral (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

• GaussianFourier.verticalIntegral b c T = ∫ (y : ℝ) in 0 ..c, Complex.I * (Complex.exp (-b * (↑T + ↑y * Complex.I) ^ 2) - Complex.exp (-b * (↑T - ↑y * Complex.I) ^ 2))

theorem GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I (b : ℂ) (c : ℝ) (T : ℝ) : ‖Complex.exp (-b * (↑T + ↑c * Complex.I) ^ 2)‖ = Real.exp (-(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 GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I' {b : ℂ} (hb : b.re ≠ 0) (c : ℝ) (T : ℝ) : ‖Complex.exp (-b * (↑T + ↑c * Complex.I) ^ 2)‖ = Real.exp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))

theorem GaussianFourier.verticalIntegral_norm_le {b : ℂ} (hb : 0 < b.re) (c : ℝ) {T : ℝ} (hT : 0 ≤ T) : ‖GaussianFourier.verticalIntegral b c T‖ ≤ 2 * |c| * Real.exp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

theorem GaussianFourier.tendsto_verticalIntegral {b : ℂ} (hb : 0 < b.re) (c : ℝ) : Filter.Tendsto (GaussianFourier.verticalIntegral b c) Filter.atTop (nhds 0)

theorem GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I {b : ℂ} (hb : 0 < b.re) (c : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (-b * (↑x + ↑c * Complex.I) ^ 2)) MeasureTheory.volume

theorem GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I {b : ℂ} (hb : 0 < b.re) (c : ℝ) : ∫ (x : ℝ), Complex.exp (-b * (↑x + ↑c * Complex.I) ^ 2) = (↑Real.pi / b) ^ (1 / 2)

theorem integral_cexp_quadratic {b : ℂ} (hb : b.re < 0) (c : ℂ) (d : ℂ) : ∫ (x : ℝ), Complex.exp (b * ↑x ^ 2 + c * ↑x + d) = (↑Real.pi / -b) ^ (1 / 2) * Complex.exp (d - c ^ 2 / (4 * b))

theorem integrable_cexp_quadratic' {b : ℂ} (hb : b.re < 0) (c : ℂ) (d : ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (b * ↑x ^ 2 + c * ↑x + d)) MeasureTheory.volume

theorem integrable_cexp_quadratic {b : ℂ} (hb : 0 < b.re) (c : ℂ) (d : ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (-b * ↑x ^ 2 + c * ↑x + d)) MeasureTheory.volume

theorem fourierIntegral_gaussian {b : ℂ} (hb : 0 < b.re) (t : ℂ) : ∫ (x : ℝ), Complex.exp (Complex.I * t * ↑x) * Complex.exp (-b * ↑x ^ 2) = (↑Real.pi / b) ^ (1 / 2) * Complex.exp (-t ^ 2 / (4 * b))

@[deprecated fourierIntegral_gaussian]

theorem fourier_transform_gaussian {b : ℂ} (hb : 0 < b.re) (t : ℂ) : ∫ (x : ℝ), Complex.exp (Complex.I * t * ↑x) * Complex.exp (-b * ↑x ^ 2) = (↑Real.pi / b) ^ (1 / 2) * Complex.exp (-t ^ 2 / (4 * b))

Alias of fourierIntegral_gaussian.

theorem fourierIntegral_gaussian_pi' {b : ℂ} (hb : 0 < b.re) (c : ℂ) : (Real.fourierIntegral fun (x : ℝ) => Complex.exp (-↑Real.pi * b * ↑x ^ 2 + 2 * ↑Real.pi * c * ↑x)) = fun (t : ℝ) => 1 / b ^ (1 / 2) * Complex.exp (-↑Real.pi / b * (↑t + Complex.I * c) ^ 2)

@[deprecated fourierIntegral_gaussian_pi']

theorem fourier_transform_gaussian_pi' {b : ℂ} (hb : 0 < b.re) (c : ℂ) : (Real.fourierIntegral fun (x : ℝ) => Complex.exp (-↑Real.pi * b * ↑x ^ 2 + 2 * ↑Real.pi * c * ↑x)) = fun (t : ℝ) => 1 / b ^ (1 / 2) * Complex.exp (-↑Real.pi / b * (↑t + Complex.I * c) ^ 2)

Alias of fourierIntegral_gaussian_pi'.

theorem fourierIntegral_gaussian_pi {b : ℂ} (hb : 0 < b.re) : (Real.fourierIntegral fun (x : ℝ) => Complex.exp (-↑Real.pi * b * ↑x ^ 2)) = fun (t : ℝ) => 1 / b ^ (1 / 2) * Complex.exp (-↑Real.pi / b * ↑t ^ 2)

@[deprecated fourierIntegral_gaussian_pi]

theorem GaussianFourier.root_.fourier_transform_gaussian_pi {b : ℂ} (hb : 0 < b.re) : (Real.fourierIntegral fun (x : ℝ) => Complex.exp (-↑Real.pi * b * ↑x ^ 2)) = fun (t : ℝ) => 1 / b ^ (1 / 2) * Complex.exp (-↑Real.pi / b * ↑t ^ 2)

Alias of fourierIntegral_gaussian_pi.

theorem GaussianFourier.integrable_cexp_neg_sum_mul_add {ι : Type u_2} [Fintype ι] {b : ι → ℂ} (hb : ∀ (i : ι), 0 < (b i).re) (c : ι → ℂ) : MeasureTheory.Integrable (fun (v : ι → ℝ) => Complex.exp ((-Finset.sum Finset.univ fun (i : ι) => b i * ↑(v i) ^ 2) + Finset.sum Finset.univ fun (i : ι) => c i * ↑(v i))) MeasureTheory.volume

theorem GaussianFourier.integrable_cexp_neg_mul_sum_add {b : ℂ} {ι : Type u_2} [Fintype ι] (hb : 0 < b.re) (c : ι → ℂ) : MeasureTheory.Integrable (fun (v : ι → ℝ) => Complex.exp ((-b * Finset.sum Finset.univ fun (i : ι) => ↑(v i) ^ 2) + Finset.sum Finset.univ fun (i : ι) => c i * ↑(v i))) MeasureTheory.volume

theorem GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace {b : ℂ} {ι : Type u_2} [Fintype ι] (hb : 0 < b.re) (c : ℂ) (w : EuclideanSpace ℝ ι) : MeasureTheory.Integrable (fun (v : EuclideanSpace ℝ ι) => Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) MeasureTheory.volume

theorem GaussianFourier.integrable_cexp_neg_mul_sq_norm_add {b : ℂ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (hb : 0 < b.re) (c : ℂ) (w : V) : MeasureTheory.Integrable (fun (v : V) => Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) MeasureTheory.volume

In a real inner product space, the complex exponential of minus the square of the norm plus a scalar product is integrable. Useful when discussing the Fourier transform of a Gaussian.

theorem GaussianFourier.integral_cexp_neg_sum_mul_add {ι : Type u_2} [Fintype ι] {b : ι → ℂ} (hb : ∀ (i : ι), 0 < (b i).re) (c : ι → ℂ) : ∫ (v : ι → ℝ), Complex.exp ((-Finset.sum Finset.univ fun (i : ι) => b i * ↑(v i) ^ 2) + Finset.sum Finset.univ fun (i : ι) => c i * ↑(v i)) = Finset.prod Finset.univ fun (i : ι) => (↑Real.pi / b i) ^ (1 / 2) * Complex.exp (c i ^ 2 / (4 * b i))

theorem GaussianFourier.integral_cexp_neg_mul_sum_add {b : ℂ} {ι : Type u_2} [Fintype ι] (hb : 0 < b.re) (c : ι → ℂ) : ∫ (v : ι → ℝ), Complex.exp ((-b * Finset.sum Finset.univ fun (i : ι) => ↑(v i) ^ 2) + Finset.sum Finset.univ fun (i : ι) => c i * ↑(v i)) = (↑Real.pi / b) ^ (↑(Fintype.card ι) / 2) * Complex.exp ((Finset.sum Finset.univ fun (i : ι) => c i ^ 2) / (4 * b))

theorem GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace {b : ℂ} {ι : Type u_2} [Fintype ι] (hb : 0 < b.re) (c : ℂ) (w : EuclideanSpace ℝ ι) : ∫ (v : EuclideanSpace ℝ ι), Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ) = (↑Real.pi / b) ^ (↑(Fintype.card ι) / 2) * Complex.exp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

theorem GaussianFourier.integral_cexp_neg_mul_sq_norm_add {b : ℂ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (hb : 0 < b.re) (c : ℂ) (w : V) : ∫ (v : V), Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ) = (↑Real.pi / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * Complex.exp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

theorem GaussianFourier.integral_cexp_neg_mul_sq_norm {b : ℂ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (hb : 0 < b.re) : ∫ (v : V), Complex.exp (-b * ↑‖v‖ ^ 2) = (↑Real.pi / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2)

theorem GaussianFourier.integral_rexp_neg_mul_sq_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {b : ℝ} (hb : 0 < b) : ∫ (v : V), Real.exp (-b * ‖v‖ ^ 2) = (Real.pi / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2)

theorem fourierIntegral_gaussian_innerProductSpace' {b : ℂ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (hb : 0 < b.re) (x : V) (w : V) : Real.fourierIntegral (fun (v : V) => Complex.exp (-b * ↑‖v‖ ^ 2 + 2 * ↑Real.pi * Complex.I * ↑⟪x, v⟫_ℝ)) w = (↑Real.pi / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑‖x - w‖ ^ 2 / b)

theorem fourierIntegral_gaussian_innerProductSpace {b : ℂ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (hb : 0 < b.re) (w : V) : Real.fourierIntegral (fun (v : V) => Complex.exp (-b * ↑‖v‖ ^ 2)) w = (↑Real.pi / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑‖w‖ ^ 2 / b)

Poisson summation applied to the Gaussian

First we show that Gaussian-type functions have rapid decay along cocompact ℝ.

theorem rexp_neg_quadratic_isLittleO_rpow_atTop {a : ℝ} (ha : a < 0) (b : ℝ) (s : ℝ) : (fun (x : ℝ) => Real.exp (a * x ^ 2 + b * x)) =o[Filter.atTop] fun (x : ℝ) => x ^ s

theorem cexp_neg_quadratic_isLittleO_rpow_atTop {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) : (fun (x : ℝ) => Complex.exp (a * ↑x ^ 2 + b * ↑x)) =o[Filter.atTop] fun (x : ℝ) => x ^ s

theorem cexp_neg_quadratic_isLittleO_abs_rpow_cocompact {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) : (fun (x : ℝ) => Complex.exp (a * ↑x ^ 2 + b * ↑x)) =o[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ s

theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact {a : ℝ} (ha : 0 < a) (s : ℝ) : Filter.Tendsto (fun (x : ℝ) => |x| ^ s * Real.exp (-a * x ^ 2)) (Filter.cocompact ℝ) (nhds 0)

theorem isLittleO_exp_neg_mul_sq_cocompact {a : ℂ} (ha : 0 < a.re) (s : ℝ) : (fun (x : ℝ) => Complex.exp (-a * ↑x ^ 2)) =o[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ s

theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) : ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2 + 2 * ↑Real.pi * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * (↑n + Complex.I * b) ^ 2)

Jacobi's theta-function transformation formula for the sum of exp -Q(x), where Q is a negative definite quadratic form.

theorem Complex.tsum_exp_neg_mul_int_sq {a : ℂ} (ha : 0 < a.re) : ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * ↑n ^ 2)

theorem Real.tsum_exp_neg_mul_int_sq {a : ℝ} (ha : 0 < a) : ∑' (n : ℤ), Real.exp (-Real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Real.exp (-Real.pi / a * ↑n ^ 2)