← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.copula_rectangle_frontier_null (C : 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.copula_cdf_tendsto_of_weak (C : ℕ → Copula 2) (D : 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.exists_copula_subsequence (C : ℕ → Copula 2) : ∃ (D : 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.