# 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) = √π`.

source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
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
source
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
source
theorem integrable_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :
MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-b * x ^ 2)) MeasureTheory.volume
source
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
source
theorem integrable_exp_neg_mul_sq_iff {b : ℝ} :
MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-b * x ^ 2)) MeasureTheory.volume ↔ 0 < b
source
theorem integrable_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :
MeasureTheory.Integrable (fun (x : ℝ) => x * Real.exp (-b * x ^ 2)) MeasureTheory.volume
source
theorem norm_cexp_neg_mul_sq (b : ℂ) (x : ℝ) :
‖Complex.exp (-b * ↑x ^ 2)‖ = Real.exp (-b.re * x ^ 2)
source
theorem integrable_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :
MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (-b * ↑x ^ 2)) MeasureTheory.volume
source
theorem integrable_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :
MeasureTheory.Integrable (fun (x : ℝ) => ↑x * Complex.exp (-b * ↑x ^ 2)) MeasureTheory.volume
source
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)⁻¹
source
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`.

source
theorem integral_gaussian (b : ℝ) :
∫ (x : ℝ), Real.exp (-b * x ^ 2) = √(Real.pi / b)
source
theorem continuousAt_gaussian_integral (b : ℂ) (hb : 0 < b.re) :
ContinuousAt (fun (c : ℂ) => ∫ (x : ℝ), Complex.exp (-c * ↑x ^ 2)) b
source
theorem integral_gaussian_complex {b : ℂ} (hb : 0 < b.re) :
∫ (x : ℝ), Complex.exp (-b * ↑x ^ 2) = (↑Real.pi / b) ^ (1 / 2)
source
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
source
theorem integral_gaussian_Ioi (b : ℝ) :
∫ (x : ℝ) in Set.Ioi 0, Real.exp (-b * x ^ 2) = √(Real.pi / b) / 2
source
theorem Real.Gamma_one_half_eq :
Gamma (1 / 2) = √Real.pi

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

source
theorem Complex.Gamma_one_half_eq :
Gamma (1 / 2) = ↑Real.pi ^ (1 / 2)

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

source
theorem Real.Gamma_nat_add_one_add_half (k : ℕ) :
Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1).doubleFactorial * √Real.pi / 2 ^ (k + 1)

The special-value formula `Γ(k + 1 + 1/2) = (2 * k + 1)‼ * √π / (2 ^ (k + 1))` for half-integer values of the gamma function in terms of `Nat.doubleFactorial`.

source
theorem Real.Gamma_nat_add_half (k : ℕ) :
Gamma (↑k + 1 / 2) = ↑(2 * k - 1).doubleFactorial * √Real.pi / 2 ^ k

The special-value formula `Γ(k + 1/2) = (2 * k - 1)‼ * √π / (2 ^ k))` for half-integer values of the gamma function in terms of `Nat.doubleFactorial`.