← Copula mathematical handbook

Monotonicity, sign and limits of Kendall's tau and Spearman's rho for the Plackett family

For the Plackett copulas C_θ, θ > 0 (Copula.Families.Plackett.Basic; Nelsen 2006, §3.3.1):

• the Plackett density is positive, so every nondegenerate rectangle has positive C_θ-mass (plackettCDF_rectangle_pos) and C_θ has full support (isOpenPosMeasure_plackett);
• θ ↦ C_θ is injective (plackett_injective, via Blomqvist's beta);
• Kendall's tau and Spearman's rho are strictly increasing in θ (kendallTau_plackett_lt_iff, kendallTau_plackett_strictMono, spearmanRho_plackett_lt_iff, spearmanRho_plackett_strictMono). For tau this uses the concordance ordering plackett_lowerOrthantLE together with the strict monotonicity of tau under full support (LowerOrthantLE.kendallTau_lt_of_isOpenPosMeasure_right);
• signs: τ(C_1) = ρ(C_1) = 0, τ(C_θ) > 0 ↔ θ > 1, τ(C_θ) < 0 ↔ θ < 1, and likewise for rho; both lie in the open interval (-1, 1);
• limits: C_θ → M as θ → ∞ and C_θ → W as θ → 0⁺ pointwise, hence τ(C_θ), ρ(C_θ) → 1 as θ → ∞ and τ(C_θ), ρ(C_θ) → -1 as θ → 0⁺ (tendsto_kendallTau_plackett_atTop, tendsto_kendallTau_plackett_zero, and the rho analogues), by continuity of the coefficients under pointwise convergence (tendsto_kendallTau_of_tendsto).

The limits are stated for an arbitrary parametrization θ : α → ℝ with positive values along a countably generated filter (e.g. sequences).

Positive rectangle masses and full support

theorem ProbabilityTheory.Copula.plackettDeriv_strictMonoOn {θ v : ℝ} (hθ : 0 < θ) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : StrictMonoOn (fun (u : ℝ) => plackettDeriv θ u v) (Set.Icc 0 1)

The Plackett partial derivative ∂C_θ/∂v is strictly increasing in u.

theorem ProbabilityTheory.Copula.plackettCDF_rectangle_pos {θ : ℝ} (hθ : 0 < θ) {a b c e : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ 1) (hc : 0 ≤ c) (hce : c < e) (he : e ≤ 1) : 0 < plackettCDF θ b e - plackettCDF θ a e - plackettCDF θ b c + plackettCDF θ a c

Every nondegenerate rectangle in the unit square has positive Plackett mass.

instance ProbabilityTheory.Copula.isOpenPosMeasure_plackett (θ : ℝ) (hθ : 0 < θ) : (plackett θ hθ).toMeasure.IsOpenPosMeasure

Full support of the Plackett copula: its measure charges every nonempty open subset of the unit square.

Injectivity of the parametrization

theorem ProbabilityTheory.Copula.plackett_ne {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') (h : θ ≠ θ') : plackett θ hθ ≠ plackett θ' hθ'

Different parameters give different Plackett copulas.

theorem ProbabilityTheory.Copula.plackett_injective {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') : plackett θ hθ = plackett θ' hθ' ↔ θ = θ'

Kendall's tau: strict monotonicity and sign

theorem ProbabilityTheory.Copula.kendallTau_plackett_lt {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') (h : θ < θ') : (plackett θ hθ).kendallTau < (plackett θ' hθ').kendallTau

Kendall's tau of the Plackett family is strictly increasing in θ.

theorem ProbabilityTheory.Copula.kendallTau_plackett_strictMono : StrictMono fun (θ : ↑(Set.Ioi 0)) => (plackett ↑θ ⋯).kendallTau

theorem ProbabilityTheory.Copula.kendallTau_plackett_lt_iff {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') : (plackett θ hθ).kendallTau < (plackett θ' hθ').kendallTau ↔ θ < θ'

theorem ProbabilityTheory.Copula.kendallTau_plackett_le_iff {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') : (plackett θ hθ).kendallTau ≤ (plackett θ' hθ').kendallTau ↔ θ ≤ θ'

theorem ProbabilityTheory.Copula.kendallTau_plackett_inj {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') : (plackett θ hθ).kendallTau = (plackett θ' hθ').kendallTau ↔ θ = θ'

@[simp]

theorem ProbabilityTheory.Copula.kendallTau_plackett_one : (plackett 1 ⋯).kendallTau = 0

τ(C_1) = 0.

theorem ProbabilityTheory.Copula.kendallTau_plackett_pos_iff {θ : ℝ} (hθ : 0 < θ) : 0 < (plackett θ hθ).kendallTau ↔ 1 < θ

theorem ProbabilityTheory.Copula.kendallTau_plackett_neg_iff {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).kendallTau < 0 ↔ θ < 1

theorem ProbabilityTheory.Copula.kendallTau_plackett_eq_zero_iff {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).kendallTau = 0 ↔ θ = 1

theorem ProbabilityTheory.Copula.kendallTau_plackett_mem_Ioo {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).kendallTau ∈ Set.Ioo (-1) 1

Kendall's tau of a Plackett copula lies in the open interval (-1, 1).

Spearman's rho: strict monotonicity and sign

theorem ProbabilityTheory.Copula.spearmanRho_plackett_lt {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') (h : θ < θ') : (plackett θ hθ).spearmanRho < (plackett θ' hθ').spearmanRho

Spearman's rho of the Plackett family is strictly increasing in θ.

theorem ProbabilityTheory.Copula.spearmanRho_plackett_strictMono : StrictMono fun (θ : ↑(Set.Ioi 0)) => (plackett ↑θ ⋯).spearmanRho

theorem ProbabilityTheory.Copula.spearmanRho_plackett_lt_iff {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') : (plackett θ hθ).spearmanRho < (plackett θ' hθ').spearmanRho ↔ θ < θ'

theorem ProbabilityTheory.Copula.spearmanRho_plackett_le_iff {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') : (plackett θ hθ).spearmanRho ≤ (plackett θ' hθ').spearmanRho ↔ θ ≤ θ'

theorem ProbabilityTheory.Copula.spearmanRho_plackett_inj {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') : (plackett θ hθ).spearmanRho = (plackett θ' hθ').spearmanRho ↔ θ = θ'

theorem ProbabilityTheory.Copula.spearmanRho_plackett_pos_iff {θ : ℝ} (hθ : 0 < θ) : 0 < (plackett θ hθ).spearmanRho ↔ 1 < θ

theorem ProbabilityTheory.Copula.spearmanRho_plackett_neg_iff {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).spearmanRho < 0 ↔ θ < 1

theorem ProbabilityTheory.Copula.spearmanRho_plackett_eq_zero_iff {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).spearmanRho = 0 ↔ θ = 1

theorem ProbabilityTheory.Copula.spearmanRho_plackett_mem_Ioo {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).spearmanRho ∈ Set.Ioo (-1) 1

Spearman's rho of a Plackett copula lies in the open interval (-1, 1).

Limits

theorem ProbabilityTheory.Copula.tendsto_plackett_cdf_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l Filter.atTop) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (plackett (θ a) ⋯).cdf u) l (nhds ((comonotonic 2).cdf u))

C_θ → M pointwise along any parametrization with θ → ∞.

theorem ProbabilityTheory.Copula.tendsto_plackett_cdf_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l (nhds 0)) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (plackett (θ a) ⋯).cdf u) l (nhds (countermonotonic.cdf u))

C_θ → W pointwise along any positive parametrization with θ → 0.

theorem ProbabilityTheory.Copula.tendsto_kendallTau_plackett_atTop {α : Type u_1} {l : Filter α} [l.IsCountablyGenerated] (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l Filter.atTop) : Filter.Tendsto (fun (a : α) => (plackett (θ a) ⋯).kendallTau) l (nhds 1)

τ(C_θ) → 1 as θ → ∞.

theorem ProbabilityTheory.Copula.tendsto_kendallTau_plackett_zero {α : Type u_1} {l : Filter α} [l.IsCountablyGenerated] (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l (nhds 0)) : Filter.Tendsto (fun (a : α) => (plackett (θ a) ⋯).kendallTau) l (nhds (-1))

τ(C_θ) → -1 as θ → 0⁺.

theorem ProbabilityTheory.Copula.tendsto_spearmanRho_plackett_atTop {α : Type u_1} {l : Filter α} [l.IsCountablyGenerated] (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l Filter.atTop) : Filter.Tendsto (fun (a : α) => (plackett (θ a) ⋯).spearmanRho) l (nhds 1)

ρ(C_θ) → 1 as θ → ∞.

theorem ProbabilityTheory.Copula.tendsto_spearmanRho_plackett_zero {α : Type u_1} {l : Filter α} [l.IsCountablyGenerated] (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l (nhds 0)) : Filter.Tendsto (fun (a : α) => (plackett (θ a) ⋯).spearmanRho) l (nhds (-1))

ρ(C_θ) → -1 as θ → 0⁺.