← Mathematical handbook

theorem Verification.studentBivariate_lowerTail_raw {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r ⋯ ν hν).HasLowerTailDependence (2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation 0) (ν + 1) ⋯) 0)) (-(1 - r) / √((1 - r ^ 2) / (ν + 1))))

theorem Verification.student_tail_threshold_standard {r ν : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (hν : 0 < ν) : (1 - r) / √((1 - r ^ 2) / (ν + 1)) = √((ν + 1) * (1 - r) / (1 + r))

theorem Verification.studentBivariate_lowerTail_interior {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r ⋯ ν hν).HasLowerTailDependence (2 - 2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation 0) (ν + 1) ⋯) 0)) √((ν + 1) * (1 - r) / (1 + r)))

theorem Verification.studentBivariate_upperTail_interior {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r ⋯ ν hν).HasUpperTailDependence (2 - 2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation 0) (ν + 1) ⋯) 0)) √((ν + 1) * (1 - r) / (1 + r)))

theorem Verification.studentBivariate_lowerTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r hr ν hν).HasLowerTailDependence (if r = 1 then 1 else if r = -1 then 0 else 2 - 2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation 0) (ν + 1) ⋯) 0)) √((ν + 1) * (1 - r) / (1 + r)))

theorem Verification.studentBivariate_upperTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentBivariate r hr ν hν).HasUpperTailDependence (if r = 1 then 1 else if r = -1 then 0 else 2 - 2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation 0) (ν + 1) ⋯) 0)) √((ν + 1) * (1 - r) / (1 + r)))