← Copula mathematical handbook

Order and limits of the Plackett family

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

• the family is positively ordered: θ ≤ θ' implies C_θ ≤ C_θ' pointwise (plackett_lowerOrthantLE); the proof only uses the cross-product ratio equation and the Fréchet–Hoeffding bounds. Consequently C_θ is PQD for θ ≥ 1 and NQD for θ ≤ 1;
• quantitative Fréchet–Hoeffding limits: 0 ≤ M(u,v) - C_θ(u,v) ≤ 1/√θ and 0 ≤ C_θ(u,v) - W(u,v) ≤ √θ, hence C_θ → M as θ → ∞ and C_θ → W as θ → 0⁺ (tendsto_plackettCDF_atTop, tendsto_plackettCDF_zero);
• Blomqvist's beta (√θ - 1)/(√θ + 1) is strictly increasing in θ.

theorem ProbabilityTheory.Copula.plackettCDF_bounds {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : 0 ≤ plackettCDF θ ↑u ↑v ∧ ↑u + ↑v - 1 ≤ plackettCDF θ ↑u ↑v ∧ plackettCDF θ ↑u ↑v ≤ ↑u ∧ plackettCDF θ ↑u ↑v ≤ ↑v

The Fréchet–Hoeffding bounds for the Plackett formula on the unit square.

theorem ProbabilityTheory.Copula.plackettCDF_cross_ratio {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : plackettCDF θ ↑u ↑v * (1 - ↑u - ↑v + plackettCDF θ ↑u ↑v) = θ * (↑u - plackettCDF θ ↑u ↑v) * (↑v - plackettCDF θ ↑u ↑v)

The cross-product ratio equation for the Plackett formula.

theorem ProbabilityTheory.Copula.plackettCDF_mono {θ θ' : ℝ} (hθ : 0 < θ) (hθθ' : θ ≤ θ') (u v : ↑unitInterval) : plackettCDF θ ↑u ↑v ≤ plackettCDF θ' ↑u ↑v

The Plackett formula is nondecreasing in the parameter.

theorem ProbabilityTheory.Copula.plackett_lowerOrthantLE {θ θ' : ℝ} (hθ : 0 < θ) (hθ' : 0 < θ') (hθθ' : θ ≤ θ') : (plackett θ hθ).LowerOrthantLE (plackett θ' hθ')

The Plackett family is positively ordered (Nelsen 2006, §3.3.1).

theorem ProbabilityTheory.Copula.isPQD_plackett {θ : ℝ} (hθ : 0 < θ) (h1 : 1 ≤ θ) : (plackett θ hθ).IsPQD

C_θ is positively quadrant dependent for θ ≥ 1.

theorem ProbabilityTheory.Copula.isNQD_plackett {θ : ℝ} (hθ : 0 < θ) (h1 : θ ≤ 1) : (plackett θ hθ).IsNQD

C_θ is negatively quadrant dependent for θ ≤ 1.

theorem ProbabilityTheory.Copula.min_sub_plackettCDF_le {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : 0 ≤ min ↑u ↑v - plackettCDF θ ↑u ↑v ∧ min ↑u ↑v - plackettCDF θ ↑u ↑v ≤ 1 / √θ

Quantitative convergence to the upper Fréchet–Hoeffding bound: 0 ≤ min(u,v) - C_θ(u,v) ≤ 1/√θ.

theorem ProbabilityTheory.Copula.plackettCDF_sub_max_le {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : 0 ≤ plackettCDF θ ↑u ↑v - max 0 (↑u + ↑v - 1) ∧ plackettCDF θ ↑u ↑v - max 0 (↑u + ↑v - 1) ≤ √θ

Quantitative convergence to the lower Fréchet–Hoeffding bound: 0 ≤ C_θ(u,v) - max(0, u + v - 1) ≤ √θ.

theorem ProbabilityTheory.Copula.tendsto_plackettCDF_atTop (u v : ↑unitInterval) : Filter.Tendsto (fun (θ : ℝ) => plackettCDF θ ↑u ↑v) Filter.atTop (nhds ((comonotonic 2).cdf ![u, v]))

C_θ → M pointwise as θ → ∞ (Nelsen 2006, §3.3.1).

theorem ProbabilityTheory.Copula.tendsto_plackettCDF_zero (u v : ↑unitInterval) : Filter.Tendsto (fun (θ : ℝ) => plackettCDF θ ↑u ↑v) (nhdsWithin 0 (Set.Ioi 0)) (nhds (countermonotonic.cdf ![u, v]))

C_θ → W pointwise as θ → 0⁺ (Nelsen 2006, §3.3.1).

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

Blomqvist's beta of the Plackett copula is strictly increasing in θ.