← Mathematical handbook

noncomputable def Verification.gaussianMix (r : ℝ) : EuclideanSpace ℝ (Fin 2) →L[ℝ] EuclideanSpace ℝ (Fin 2)

Equations

• Verification.gaussianMix r = ↑(EuclideanSpace.equiv (Fin 2) ℝ).symm ∘SL ContinuousLinearMap.pi ![EuclideanSpace.proj 0, r • EuclideanSpace.proj 0 + √(1 - r ^ 2) • EuclideanSpace.proj 1]

noncomputable def Verification.gaussianMixRow (r : ℝ) (i : Fin 2) : EuclideanSpace ℝ (Fin 2)

Equations

• Verification.gaussianMixRow r i = WithLp.toLp 2 (!![1, 0; r, √(1 - r ^ 2)] i)

theorem Verification.gaussianMix_inner (r : ℝ) (i : Fin 2) : (fun (u : EuclideanSpace ℝ (Fin 2)) => inner ℝ ((EuclideanSpace.basisFun (Fin 2) ℝ).toBasis i) u) ∘ ⇑(gaussianMix r) = fun (u : EuclideanSpace ℝ (Fin 2)) => inner ℝ (gaussianMixRow r i) u

theorem Verification.map_gaussianMix {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (⇑(gaussianMix r)) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin 2))) = ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)

theorem Verification.gaussianBivariate_toMeasure_independent {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).toMeasure = MeasureTheory.Measure.map (fun (x : Fin 2 → ℝ) => ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (x 0), ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (r * x 0 + √(1 - r ^ 2) * x 1)]) (MeasureTheory.Measure.pi fun (x : Fin 2) => ProbabilityTheory.gaussianReal 0 1)

theorem Verification.gaussianBivariate_rho_normal_integral {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).spearmanRho = (12 * ∫ (x : Fin 2 → ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (x 0) * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (r * x 0 + √(1 - r ^ 2) * x 1) ∂MeasureTheory.Measure.pi fun (x : Fin 2) => ProbabilityTheory.gaussianReal 0 1) - 3