← Mathematical handbook

def Verification.bivariateCorrelation (r : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

Equations

• Verification.bivariateCorrelation r = !![1, r; r, 1]

theorem Verification.bivariateCorrelation_posSemidef {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateCorrelation r).PosSemidef

noncomputable def Verification.gaussianBivariate (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) : ProbabilityTheory.Copula 2

Equations

• Verification.gaussianBivariate r hr = ProbabilityTheory.Copula.gaussian (Verification.bivariateCorrelation r) ⋯ ⋯

theorem Verification.gaussianBivariate_zero : gaussianBivariate 0 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Verification.gaussianBivariate_one : gaussianBivariate 1 ⋯ = ProbabilityTheory.Copula.comonotonic 2

theorem Verification.gaussianBivariate_transpose {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).transpose = gaussianBivariate r hr

theorem Verification.bivariateCorrelation_posSemidef_iff (r : ℝ) : (bivariateCorrelation r).PosSemidef ↔ r ∈ Set.Icc (-1) 1

noncomputable def Verification.gaussianPrintedXiArgument (r : ℝ) : ℝ

The literal argument printed in arXiv v3 Table 6.

Equations

• Verification.gaussianPrintedXiArgument r = 1 / 2 + r ^ 2 / (1 + r)

theorem Verification.gaussianPrintedXiArgument_gt_one {r : ℝ} (hr : r ∈ Set.Ioo (-1) (-(1 / 2))) : 1 < gaussianPrintedXiArgument r

theorem Verification.gaussianPrintedXiArgument_counterexample : gaussianPrintedXiArgument (-(3 / 4)) = 11 / 4 ∧ gaussianPrintedXiArgument (-(3 / 4)) ∉ Set.Icc (-1) 1