← Mathematical handbook

theorem Verification.integral_gaussian_radial {b : ℝ} (hb : 0 < b) : ∫ (x : ℝ) in Set.Ioi 0, x * Real.exp (-b * x ^ 2) = 1 / (2 * b)

theorem Verification.integral_gaussian_wedge {a : ℝ} (ha : 0 ≤ a) : (∫ (x : ℝ) (y : ℝ) in Set.Ioi 0, if y ≤ a * x then Real.exp (-(x ^ 2 + y ^ 2) / 2) else 0) = Real.arctan a

theorem Verification.setIntegral_standardGaussian (f : ℝ → ℝ) {s : Set ℝ} (hs : MeasurableSet s) : ∫ (x : ℝ) in s, f x ∂ProbabilityTheory.gaussianReal 0 1 = ∫ (x : ℝ) in s, ProbabilityTheory.gaussianPDFReal 0 1 x * f x

theorem Verification.standardGaussian_pdf_product (x y : ℝ) : ProbabilityTheory.gaussianPDFReal 0 1 x * ProbabilityTheory.gaussianPDFReal 0 1 y = 1 / (2 * Real.pi) * Real.exp (-(x ^ 2 + y ^ 2) / 2)

theorem Verification.standardGaussian_wedge {a : ℝ} (ha : 0 ≤ a) : ∫ (x : ℝ) in Set.Ioi 0, ∫ (y : ℝ) in Set.Ioi 0, if y ≤ a * x then 1 else 0 ∂ProbabilityTheory.gaussianReal 0 1 ∂ProbabilityTheory.gaussianReal 0 1 = Real.arctan a / (2 * Real.pi)

theorem Verification.standardGaussian_cdf_zero : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) 0 = 1 / 2

theorem Verification.standardGaussian_cdf_nonneg {b : ℝ} (hb : 0 ≤ b) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) b = 1 / 2 + ∫ (y : ℝ) in Set.Ioi 0, if y ≤ b then 1 else 0 ∂ProbabilityTheory.gaussianReal 0 1

theorem Verification.integral_standardGaussian_cdf_nonneg {a : ℝ} (ha : 0 ≤ a) : ∫ (x : ℝ) in Set.Ioi 0, ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a * x) ∂ProbabilityTheory.gaussianReal 0 1 = 1 / 4 + Real.arctan a / (2 * Real.pi)

theorem Verification.integral_standardGaussian_cdf (a : ℝ) : ∫ (x : ℝ) in Set.Ioi 0, ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a * x) ∂ProbabilityTheory.gaussianReal 0 1 = 1 / 4 + Real.arctan a / (2 * Real.pi)