mathlib documentation

analysis.special_functions.gaussian

Gaussian integral #

We prove the formula ∫ x, exp (-b * x^2) = sqrt (π / b), in integral_gaussian.

source
theorem exp_neg_mul_sq_is_o_exp_neg {b : ℝ} (hb : 0 < b) :
(λ (x : ℝ), real.exp (-b * x ^ 2)) =o[filter.at_top] λ (x : ℝ), real.exp (-x)
source
theorem rpow_mul_exp_neg_mul_sq_is_o_exp_neg {b : ℝ} (hb : 0 < b) (s : ℝ) :
(λ (x : ℝ), x ^ s * real.exp (-b * x ^ 2)) =o[filter.at_top] λ (x : ℝ), real.exp (-(1 / 2) * x)
source
theorem integrable_on_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :
measure_theory.integrable_on (λ (x : ℝ), x ^ s * real.exp (-b * x ^ 2)) (set.Ioi 0) measure_theory.measure_space.volume
source
theorem integrable_rpow_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) {s : ℝ} (hs : -1 < s) :
measure_theory.integrable (λ (x : ℝ), x ^ s * real.exp (-b * x ^ 2)) measure_theory.measure_space.volume
source
theorem integrable_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :
measure_theory.integrable (λ (x : ℝ), real.exp (-b * x ^ 2)) measure_theory.measure_space.volume
source
theorem integrable_exp_neg_mul_sq_iff {b : ℝ} :
measure_theory.integrable (λ (x : ℝ), real.exp (-b * x ^ 2)) measure_theory.measure_space.volume ↔ 0 < b
source
theorem integrable_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :
measure_theory.integrable (λ (x : ℝ), x * real.exp (-b * x ^ 2)) measure_theory.measure_space.volume
source
theorem integral_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :
∫ (r : ℝ) in set.Ioi 0, r * real.exp (-b * r ^ 2) = (2 * b)⁻¹
source
theorem integral_gaussian (b : ℝ) :
∫ (x : ℝ), real.exp (-b * x ^ 2) = real.sqrt (real.pi / b)