theorem
Verification.gaussianBivariate_cdf_normal_rectangle
{r : ℝ}
(hr : r ∈ Set.Icc (-1) 1)
(a b : ℝ)
:
(gaussianBivariate r hr).cdf
![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b] = (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)).real
{x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ a ∧ x.ofLp 1 ≤ b}
theorem
Verification.gaussianScaleMixtureLaw_rectangle
{r : ℝ}
(hr : r ∈ Set.Icc (-1) 1)
(μ : MeasureTheory.ProbabilityMeasure ℝ)
(s : ℝ → ℝ)
(hs : Measurable s)
(hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t)
(a b : ℝ)
:
(↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation r) μ s)).real (Set.Iic ![a, b]) = ∫ (t : ℝ), (gaussianBivariate r hr).cdf
![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (a / s t), ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (b / s t)] ∂↑μ
theorem
Verification.gaussianScaleMixtureLaw_lowerOrthant
{r q : ℝ}
(hr : r ∈ Set.Icc (-1) 1)
(hq : q ∈ Set.Icc (-1) 1)
(hrq : r ≤ q)
(μ : MeasureTheory.ProbabilityMeasure ℝ)
(s : ℝ → ℝ)
(hs : Measurable s)
(hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t)
(x : Fin 2 → ℝ)
:
(↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation r) μ s)).real (Set.Iic x) ≤ (↑(ProbabilityTheory.Copula.gaussianScaleMixtureLaw (bivariateCorrelation q) μ s)).real (Set.Iic x)
theorem
Verification.gaussianScaleMixture_lowerOrthant
{r q : ℝ}
(hr : r ∈ Set.Icc (-1) 1)
(hq : q ∈ Set.Icc (-1) 1)
(hrq : r ≤ q)
(μ : MeasureTheory.ProbabilityMeasure ℝ)
(s : ℝ → ℝ)
(hs : Measurable s)
(hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t)
:
(ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp).LowerOrthantLE
(ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation q) ⋯ ⋯ μ s hs hp)