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)) (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.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.pi / b) / 2

theorem Real.Gamma_one_half_eq : Real.Gamma (1 / 2) = √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.

theorem Real.Gamma_nat_add_one_add_half (k : ℕ) : Real.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.

theorem Real.Gamma_nat_add_half (k : ℕ) : Real.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.