← Mathematical handbook

theorem Papers.AnsariRockel2024.student_isSklarCopula (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : ProbabilityTheory.Copula.IsSklarCopula (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) (Verification.studentBivariate r hr ν hν)

theorem Papers.AnsariRockel2024.student_one (ν : ℝ) (hν : 0 < ν) : Verification.studentBivariate 1 ⋯ ν hν = ProbabilityTheory.Copula.comonotonic 2

theorem Papers.AnsariRockel2024.student_one_isCI (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate 1 ⋯ ν hν).IsCI

theorem Papers.AnsariRockel2024.student_negative_one (ν : ℝ) (hν : 0 < ν) : Verification.studentBivariate (-1) ⋯ ν hν = ProbabilityTheory.Copula.countermonotonic

theorem Papers.AnsariRockel2024.student_negative_one_isCD (ν : ℝ) (hν : 0 < ν) : (Verification.studentBivariate (-1) ⋯ ν hν).IsCD

theorem Papers.AnsariRockel2024.student_marginal (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) : ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => (√p.2)⁻¹ * p.1) ((ProbabilityTheory.gaussianReal 0 1).prod ↑(ProbabilityTheory.gammaProbability (ν / 2) (ν / 2) ⋯ ⋯))

theorem Papers.AnsariRockel2024.student_marginal_cdf (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) (a : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i)) a = ∫ (t : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a * √t) ∂↑(ProbabilityTheory.gammaProbability (ν / 2) (ν / 2) ⋯ ⋯)

theorem Papers.AnsariRockel2024.student_marginal_cdf_strictMono (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) : StrictMono ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i))

theorem Papers.AnsariRockel2024.student_marginal_cdf_neg (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) (a : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i)) (-a) = 1 - ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (Verification.bivariateCorrelation r) ν hν) i)) a