← Mathematical handbook

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

Equations

• Verification.gaussianNegSecond = ↑(EuclideanSpace.equiv (Fin 2) ℝ).symm ∘SL ContinuousLinearMap.pi fun (i : Fin 2) => ![1, -1] i • EuclideanSpace.proj i

theorem Verification.gaussianNegSecond_apply (x : EuclideanSpace ℝ (Fin 2)) (i : Fin 2) : (gaussianNegSecond x).ofLp i = ![1, -1] i * x.ofLp i

theorem Verification.map_gaussianNegSecond {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (⇑gaussianNegSecond) (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)) = ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation (-r))

theorem Verification.standardNormalCDF_neg (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (-x) = 1 - ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x

theorem Verification.standardNormalCDFUnit_neg (x : ℝ) : ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (-x) = unitInterval.symm (ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) x)

theorem Verification.gaussianBivariate_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : gaussianBivariate (-r) ⋯ = (gaussianBivariate r hr).reflect {1}

theorem Verification.gaussianBivariate_negative_one : gaussianBivariate (-1) ⋯ = ProbabilityTheory.Copula.countermonotonic

theorem Verification.gaussianBivariate_xi_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate (-r) ⋯).chatterjeeXi = (gaussianBivariate r hr).chatterjeeXi

theorem Verification.gaussianBivariate_rho_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate (-r) ⋯).spearmanRho = -(gaussianBivariate r hr).spearmanRho

theorem Verification.gaussianBivariate_tau_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate (-r) ⋯).kendallTau = -(gaussianBivariate r hr).kendallTau

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

Equations

• Verification.gaussianPrintedXi r = 3 / Real.pi * Real.arcsin (Verification.gaussianPrintedXiArgument r) - 1 / 2

theorem Verification.gaussianPrintedXi_negative_half : gaussianPrintedXi (-(1 / 2)) = 1

theorem Verification.gaussianPrintedXi_half_lt_one : gaussianPrintedXi (1 / 2) < 1

theorem Verification.gaussian_printed_xi_formula_false : ¬∀ (r : ℝ) (hr : r ∈ Set.Icc (-1) 1), (gaussianBivariate r hr).chatterjeeXi = gaussianPrintedXi r