The actual Gaussian CDF as an iterated density integral #
theorem
Verification.standardNormal_affine_map
(m s : ℝ)
:
MeasureTheory.Measure.map (fun (x : ℝ) => m + s * x) (ProbabilityTheory.gaussianReal 0 1) = ProbabilityTheory.gaussianReal m (NNReal.mk (s ^ 2) ⋯)
theorem
Verification.standardNormal_affine_cdf
(m b : ℝ)
{s : ℝ}
(hs : 0 < s)
:
↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m (NNReal.mk (s ^ 2) ⋯))) b = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - m) / s)
theorem
Verification.gaussianReal_cdf_density
(m b : ℝ)
{v : NNReal}
(hv : v ≠ 0)
:
↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v)) b = ∫ (y : ℝ) in Set.Iic b, ProbabilityTheory.gaussianPDFReal m v y
theorem
Verification.gaussianBivariate_cdf_normal_density
{r : ℝ}
(hr : r ∈ Set.Ioo (-1) 1)
(a b : ℝ)
:
(gaussianBivariate r ⋯).cdf
![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b] = ∫ (x : ℝ) in Set.Iic a, ProbabilityTheory.gaussianPDFReal 0 1 x * ∫ (y : ℝ) in Set.Iic b, ProbabilityTheory.gaussianPDFReal (r * x) (1 - r ^ 2).toNNReal y
theorem
Verification.standardNormal_joint_affine_density
(r s : ℝ)
(hs : s ≠ 0)
:
MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => (p.1, r * p.1 + s * p.2))
((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) =>
ProbabilityTheory.gaussianPDF 0 1 p.1 * ProbabilityTheory.gaussianPDF (r * p.1) (NNReal.mk (s ^ 2) ⋯) p.2
theorem
Verification.gaussianBivariate_toMeasure_normal_density
{r : ℝ}
(hr : r ∈ Set.Ioo (-1) 1)
:
(gaussianBivariate r ⋯).toMeasure = MeasureTheory.Measure.map
(fun (p : ℝ × ℝ) =>
![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) p.1, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) p.2])
(MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) =>
ProbabilityTheory.gaussianPDF 0 1 p.1 * ProbabilityTheory.gaussianPDF (r * p.1) (1 - r ^ 2).toNNReal p.2)