theorem
Papers.AnsariRockel2024.student_diagonal_integral
(r : ℝ)
(hr : r ∈ Set.Ioo (-1) 1)
(ν : ℝ)
(hν : 0 < ν)
(a : ℝ)
:
(Verification.studentBivariate r ⋯ ν hν).diagonal
(ProbabilityTheory.cdfUnit
(ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0)
a) = 2 * ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf
(ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0))
((x - r * x) / √((ν + x ^ 2) * (1 - r ^ 2) / (ν + 1))) ∂ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0
theorem
Papers.AnsariRockel2024.student_lowerTailRatio_integral
(r : ℝ)
(hr : r ∈ Set.Ioo (-1) 1)
(ν : ℝ)
(hν : 0 < ν)
(a : ℝ)
:
(Verification.studentBivariate r ⋯ ν hν).lowerTailRatio
(ProbabilityTheory.cdfUnit
(ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0)
a) = (2 * ∫ (x : ℝ) in Set.Iic a, ↑(ProbabilityTheory.cdf
(ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0))
((x - r * x) / √((ν + x ^ 2) * (1 - r ^ 2) / (ν + 1))) ∂ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0) / ↑(ProbabilityTheory.cdf
(ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) 0))
a
theorem
Papers.AnsariRockel2024.student_lowerTail_interior
(r : ℝ)
(hr : r ∈ Set.Ioo (-1) 1)
(ν : ℝ)
(hν : 0 < ν)
:
(Verification.studentBivariate r ⋯ ν hν).HasLowerTailDependence
(2 - 2 * ↑(ProbabilityTheory.cdf
(ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0))
√((ν + 1) * (1 - r) / (1 + r)))
theorem
Papers.AnsariRockel2024.student_upperTail_interior
(r : ℝ)
(hr : r ∈ Set.Ioo (-1) 1)
(ν : ℝ)
(hν : 0 < ν)
:
(Verification.studentBivariate r ⋯ ν hν).HasUpperTailDependence
(2 - 2 * ↑(ProbabilityTheory.cdf
(ProbabilityTheory.Copula.marginal
(ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0))
√((ν + 1) * (1 - r) / (1 + r)))
theorem
Papers.AnsariRockel2024.student_lowerTail
(r : ℝ)
(hr : r ∈ Set.Icc (-1) 1)
(ν : ℝ)
(hν : 0 < ν)
:
(Verification.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 (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0))
√((ν + 1) * (1 - r) / (1 + r)))
theorem
Papers.AnsariRockel2024.student_upperTail
(r : ℝ)
(hr : r ∈ Set.Icc (-1) 1)
(ν : ℝ)
(hν : 0 < ν)
:
(Verification.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 (Verification.bivariateCorrelation 0) (ν + 1) ⋯) 0))
√((ν + 1) * (1 - r) / (1 + r)))