← Mathematical handbook

theorem Papers.AnsariRockel2024.student_cdf_continuous (ν : ℝ) (hν : 0 < ν) (u : Fin 2 → ↑unitInterval) : Continuous fun (r : ↑(Set.Icc (-1) 1)) => (Verification.studentBivariate ↑r ⋯ ν hν).cdf u

theorem Papers.AnsariRockel2024.laplace_cdf_continuous (u : Fin 2 → ↑unitInterval) : Continuous fun (r : ↑(Set.Icc (-1) 1)) => (Verification.laplaceBivariate ↑r ⋯).cdf u

theorem Papers.AnsariRockel2024.student_cdf_tendsto_one (ν : ℝ) (hν : 0 < ν) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (Verification.studentBivariate ↑r ⋯ ν hν).cdf u) (nhds ⟨1, ⋯⟩) (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))

theorem Papers.AnsariRockel2024.student_cdf_tendsto_negative_one (ν : ℝ) (hν : 0 < ν) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (Verification.studentBivariate ↑r ⋯ ν hν).cdf u) (nhds ⟨-1, ⋯⟩) (nhds (ProbabilityTheory.Copula.countermonotonic.cdf u))

theorem Papers.AnsariRockel2024.laplace_cdf_tendsto_one (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (Verification.laplaceBivariate ↑r ⋯).cdf u) (nhds ⟨1, ⋯⟩) (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))

theorem Papers.AnsariRockel2024.laplace_cdf_tendsto_negative_one (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (Verification.laplaceBivariate ↑r ⋯).cdf u) (nhds ⟨-1, ⋯⟩) (nhds (ProbabilityTheory.Copula.countermonotonic.cdf u))