← Mathematical handbook

theorem Papers.AnsariRockel2024.student_joint_cdf (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (a b : ℝ) : (↑(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν)).real (Set.Iic ![a, b]) = ∫ (t : ℝ), (Verification.gaussianBivariate r hr).cdf ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (a * √t), ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) (b * √t)] ∂↑(ProbabilityTheory.gammaProbability (ν / 2) (ν / 2) ⋯ ⋯)

theorem Papers.AnsariRockel2024.student_lowerOrthant_monotone {r q : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hq : q ∈ Set.Icc (-1) 1) (hrq : r ≤ q) (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate r hr ν hν).LowerOrthantLE (Verification.studentBivariate q hq ν hν)

theorem Papers.AnsariRockel2024.student_kendallTau (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate r hr ν hν).kendallTau = 2 / Real.pi * Real.arcsin r

theorem Papers.AnsariRockel2024.student_lowerOrthant_iff {r q : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hq : q ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate r hr ν hν).LowerOrthantLE (Verification.studentBivariate q hq ν hν) ↔ r ≤ q

theorem Papers.AnsariRockel2024.student_reflect_second {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : Verification.studentBivariate (-r) ⋯ ν hν = (Verification.studentBivariate r hr ν hν).reflect {1}

theorem Papers.AnsariRockel2024.student_rho_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate (-r) ⋯ ν hν).spearmanRho = -(Verification.studentBivariate r hr ν hν).spearmanRho

theorem Papers.AnsariRockel2024.student_tau_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate (-r) ⋯ ν hν).kendallTau = -(Verification.studentBivariate r hr ν hν).kendallTau

theorem Papers.AnsariRockel2024.student_xi_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate (-r) ⋯ ν hν).chatterjeeXi = (Verification.studentBivariate r hr ν hν).chatterjeeXi

theorem Papers.AnsariRockel2024.student_transpose {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate r hr ν hν).transpose = Verification.studentBivariate r hr ν hν

theorem Papers.AnsariRockel2024.student_radiallySymmetric {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate r hr ν hν).IsRadiallySymmetric

theorem Papers.AnsariRockel2024.student_upperTail_iff_lowerTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (ℓ : ℝ) : (Verification.studentBivariate r hr ν hν).HasUpperTailDependence ℓ ↔ (Verification.studentBivariate r hr ν hν).HasLowerTailDependence ℓ