← Mathematical handbook

theorem Verification.copula_rectangle_frontier_null (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : C.toMeasure (frontier (Set.Iic ![u, v])) = 0

Lower rectangles are continuity sets for every copula, including singular laws.

theorem Verification.copula_cdf_tendsto_of_weak (C : ℕ → ProbabilityTheory.Copula 2) (D : ProbabilityTheory.Copula 2) (hC : Filter.Tendsto (fun (n : ℕ) => (C n).measure) Filter.atTop (nhds D.measure)) (u v : ↑unitInterval) : Filter.Tendsto (fun (n : ℕ) => (C n).cdf ![u, v]) Filter.atTop (nhds (D.cdf ![u, v]))

theorem Verification.exists_copula_subsequence (C : ℕ → ProbabilityTheory.Copula 2) : ∃ (D : ProbabilityTheory.Copula 2) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (fun (n : ℕ) => (C (φ n)).measure) Filter.atTop (nhds D.measure) ∧ ∀ (u v : ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => (C (φ n)).cdf ![u, v]) Filter.atTop (nhds (D.cdf ![u, v]))

Every sequence has a weak copula subsequential limit, with pointwise CDF convergence.