theorem
Verification.copula_limit_comonotonic_of_diagonal
{ι : Type u_1}
{l : Filter ι}
(C : ι → ProbabilityTheory.Copula 2)
(h : ∀ (t : ↑unitInterval), Filter.Tendsto (fun (i : ι) => (C i).diagonal t) l (nhds ↑t))
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (C i).cdf u) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))
theorem
Verification.copula_limit_comonotonic_of_powerDiagonal
{ι : Type u_1}
{l : Filter ι}
(C : ι → ProbabilityTheory.Copula 2)
(κ : ι → ℝ)
(hκ : ∀ (i : ι), (C i).HasPowerDiagonal (κ i))
(hk : Filter.Tendsto κ l (nhds 1))
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (C i).cdf u) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))