# 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)
• 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 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)) ()
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)) ()
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)) ()
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)
theorem integrable_exp_neg_mul_sq {b : } (hb : 0 < b) :
theorem integrable_mul_exp_neg_mul_sq {b : } (hb : 0 < b) :
MeasureTheory.Integrable fun (x : ) => x * Real.exp (-b * x ^ 2)
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)
theorem integrable_mul_cexp_neg_mul_sq {b : } (hb : 0 < b.re) :
MeasureTheory.Integrable fun (x : ) => x * Complex.exp (-b * x ^ 2)
theorem integral_mul_cexp_neg_mul_sq {b : } (hb : 0 < b.re) :
∫ (r : ) in , 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 = / 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 ()
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) = ( / b) ^ (1 / 2)
theorem integral_gaussian_complex_Ioi {b : } (hb : 0 < b.re) :
∫ (x : ) in , Complex.exp (-b * x ^ 2) = ( / b) ^ (1 / 2) / 2
theorem integral_gaussian_Ioi (b : ) :
∫ (x : ) in , Real.exp (-b * x ^ 2) = Real.sqrt () / 2

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

theorem Complex.Gamma_one_half_eq :
Complex.Gamma (1 / 2) = ^ (1 / 2)

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

## Fourier transform of the Gaussian integral #

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

Equations
Instances For
theorem GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I (b : ) (c : ) (T : ) :
Complex.exp (-b * (T + ) ^ 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 + ) ^ 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) :
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 Filter.atTop (nhds 0)
theorem GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I {b : } (hb : 0 < b.re) (c : ) :
∫ (x : ), Complex.exp (-b * (x + ) ^ 2) = ( / b) ^ (1 / 2)
theorem integral_cexp_quadratic {b : } (hb : b.re < 0) (c : ) (d : ) :
∫ (x : ), Complex.exp (b * x ^ 2 + c * x + d) = () ^ (1 / 2) * Complex.exp (d - c ^ 2 / (4 * b))
theorem fourier_transform_gaussian {b : } (hb : 0 < b.re) (t : ) :
∫ (x : ), Complex.exp ( * x) * Complex.exp (-b * x ^ 2) = ( / b) ^ (1 / 2) * Complex.exp (-t ^ 2 / (4 * b))
theorem fourier_transform_gaussian_pi' {b : } (hb : 0 < b.re) (c : ) :
(Real.fourierIntegral fun (x : ) => Complex.exp ( * x ^ 2 + 2 * * c * x)) = fun (t : ) => 1 / b ^ (1 / 2) * Complex.exp ( * (t + ) ^ 2)
theorem fourier_transform_gaussian_pi {b : } (hb : 0 < b.re) :
(Real.fourierIntegral fun (x : ) => Complex.exp ( * x ^ 2)) = fun (t : ) => 1 / b ^ (1 / 2) * Complex.exp ( * t ^ 2)

## 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[] 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)) (nhds 0)
theorem isLittleO_exp_neg_mul_sq_cocompact {a : } (ha : 0 < a.re) (s : ) :
(fun (x : ) => Complex.exp (-a * x ^ 2)) =o[] fun (x : ) => |x| ^ s
theorem Complex.tsum_exp_neg_quadratic {a : } (ha : 0 < a.re) (b : ) :
∑' (n : ), Complex.exp ( * n ^ 2 + 2 * * b * n) = 1 / a ^ (1 / 2) * ∑' (n : ), Complex.exp ( * (n + ) ^ 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 ( * n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ), Complex.exp ( * n ^ 2)
theorem Real.tsum_exp_neg_mul_int_sq {a : } (ha : 0 < a) :
∑' (n : ), Real.exp ( * n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ), Real.exp ( * n ^ 2)