← Copula mathematical handbook

Closedness and compactness of the set of copulas

A pointwise limit of functions satisfying the classical copula conditions again satisfies them, since every condition is a closed condition for pointwise convergence. By the classical characterization (Copula.ofClassical) such a limit is the CDF of a copula, and by Copula.Topology.Uniform the convergence is uniform. Combining this with the Arzelà–Ascoli theorem, the set of copula CDFs is a compact subset of the bounded continuous functions on the cube, so every sequence of copulas has a uniformly convergent subsequence (Nelsen, An Introduction to Copulas, 2nd ed., §2.2 and the discussion of convergence of copulas following Theorem 2.2.4).

theorem ProbabilityTheory.Copula.IsClassical.of_tendsto {d : ℕ} {ι : Type u_1} {l : Filter ι} [l.NeBot] {G : ι → (Fin d → ↑unitInterval) → ℝ} {F : (Fin d → ↑unitInterval) → ℝ} (hG : ∀ (n : ι), IsClassical (G n)) (h : ∀ (u : Fin d → ↑unitInterval), Filter.Tendsto (fun (n : ι) => G n u) l (nhds (F u))) : IsClassical F

A pointwise limit of functions satisfying the classical copula conditions satisfies them.

theorem ProbabilityTheory.Copula.isClassical_of_tendsto_cdf {d : ℕ} {ι : Type u_1} {l : Filter ι} [l.NeBot] (C : ι → Copula d) {F : (Fin d → ↑unitInterval) → ℝ} (h : ∀ (u : Fin d → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (F u))) : IsClassical F

A pointwise limit of copula CDFs satisfies the classical copula conditions.

theorem ProbabilityTheory.Copula.exists_copula_tendstoUniformly_of_tendsto {d : ℕ} {ι : Type u_1} {l : Filter ι} [l.NeBot] (C : ι → Copula d) {F : (Fin d → ↑unitInterval) → ℝ} (h : ∀ (u : Fin d → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (F u))) : ∃ (D : Copula d), D.cdf = F ∧ TendstoUniformly (fun (n : ι) => (C n).cdf) D.cdf l

A pointwise limit of copula CDFs is the CDF of a copula, and the convergence is uniform.

noncomputable def ProbabilityTheory.Copula.cdfBCF {d : ℕ} (C : Copula d) : BoundedContinuousFunction (Fin d → ↑unitInterval) ℝ

The bounded continuous function on the cube given by a copula CDF.

Equations

• C.cdfBCF = BoundedContinuousFunction.mkOfCompact { toFun := C.cdf, continuous_toFun := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.coe_cdfBCF {d : ℕ} (C : Copula d) : ⇑C.cdfBCF = C.cdf

def ProbabilityTheory.Copula.classicalSet (d : ℕ) : Set (BoundedContinuousFunction (Fin d → ↑unitInterval) ℝ)

The set of bounded continuous functions on the cube satisfying the classical copula conditions.

Equations

• ProbabilityTheory.Copula.classicalSet d = {f : BoundedContinuousFunction (Fin d → ↑unitInterval) ℝ | ProbabilityTheory.Copula.IsClassical ⇑f}

theorem ProbabilityTheory.Copula.isClosed_classicalSet {d : ℕ} : IsClosed (classicalSet d)

The set of functions satisfying the classical conditions is closed for uniform convergence.

theorem ProbabilityTheory.Copula.IsClassical.mem_Icc {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (u : Fin d → ↑unitInterval) : F u ∈ Set.Icc 0 1

Functions satisfying the classical conditions take values in [0, 1].

theorem ProbabilityTheory.Copula.isCompact_classicalSet {d : ℕ} : IsCompact (classicalSet d)

Arzelà–Ascoli: the set of copula CDFs in C(I^d, ℝ) is compact for the uniform metric.

theorem ProbabilityTheory.Copula.exists_subseq_tendstoUniformly_cdf {d : ℕ} (C : ℕ → Copula d) : ∃ (D : Copula d) (φ : ℕ → ℕ), StrictMono φ ∧ TendstoUniformly (fun (n : ℕ) => (C (φ n)).cdf) D.cdf Filter.atTop

Every sequence of copulas has a subsequence whose CDFs converge uniformly on the cube to the CDF of a copula (compactness of the set of copulas, Nelsen §2.2).