← Copula mathematical handbook

Coverage and ordering of the Schreyer–Paulin–Trutschnig arcs

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.continuous_arcTau (n : ℕ) : Continuous (arcTau n)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.continuous_arcRho (n : ℕ) : Continuous (arcRho n)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.strictMono_arcTau (n : ℕ) : StrictMono fun (s : ↑unitInterval) => arcTau n ↑s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.strictMono_arcRho (n : ℕ) : StrictMono fun (s : ↑unitInterval) => arcRho n ↑s

inductive ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter : Type

• endpoint : LowerParameter
• arc (n : ℕ) (s : ↑unitInterval) : LowerParameter

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.tau : LowerParameter → ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.endpoint.tau = -1
• (ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.arc n s).tau = ProbabilityTheory.Copula.RankRegion.RhoTau.arcTau n ↑s

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.rho : LowerParameter → ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.endpoint.rho = -1
• (ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.arc n s).rho = ProbabilityTheory.Copula.RankRegion.RhoTau.arcRho n ↑s

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.copula : LowerParameter → Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.endpoint.copula = ProbabilityTheory.Copula.countermonotonic
• (ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.arc n s).copula = ProbabilityTheory.Copula.RankRegion.RhoTau.arcCopula n s

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.coefficients (p : LowerParameter) : p.copula.kendallTau = p.tau ∧ p.copula.spearmanRho = p.rho

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.tau_mem (p : LowerParameter) : p.tau ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.LowerParameter.rho_mem (p : LowerParameter) : p.rho ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.joined_arcs_cover {f : ℕ → ↑unitInterval → ℝ} {j : ℕ → ℝ} {l x : ℝ} (hc : ∀ (n : ℕ), Continuous (f n)) (hzero : ∀ (n : ℕ), f n 0 = j (n + 1)) (hone : ∀ (n : ℕ), f n 1 = j n) (hj : Filter.Tendsto j Filter.atTop (nhds l)) (hl : l < x) (hx : x ≤ j 0) : ∃ (n : ℕ) (s : ↑unitInterval), f n s = x

Consecutive continuous arcs cover every point above their limiting junction.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tau_junction_tendsto : Filter.Tendsto (fun (n : ℕ) => -1 + 2 / (↑n + 1)) Filter.atTop (nhds (-1))

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.rho_junction_tendsto : Filter.Tendsto (fun (n : ℕ) => -1 + 2 / (↑n + 1) ^ 2) Filter.atTop (nhds (-1))

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.lowerParameter_tau_exists {t : ℝ} (ht : t ∈ Set.Icc (-1) 1) : ∃ (p : LowerParameter), p.tau = t

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.lowerParameter_rho_exists {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : ∃ (p : LowerParameter), p.rho = r

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.prototype_interval_attainable (a b : LowerParameter) {r t : ℝ} (ha : a.rho = r) (hb : -b.rho = r) (hl : -b.tau ≤ t) (hu : t ≤ a.tau) : (r, t) ∈ attainable Coefficient.rho Coefficient.tau

Filling the horizontal sections uses only actual prototype copulas and continuity of Kendall's tau along mixtures.