# 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) = √(π / 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) = √π.
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)) () 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)) () 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)) () 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)) () 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 , 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) = ()
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) = () / 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.