← Mathematical handbook

Table 4: the Plackett copula and its actual Lebesgue density

theorem Papers.AnsariRockel2024.plackett_cdf {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) (u v : ↑unitInterval) : (Verification.plackett θ hθ).cdf ![u, v] = (1 + (θ - 1) * (↑u + ↑v) - √((1 + (θ - 1) * (↑u + ↑v)) ^ 2 - 4 * θ * (θ - 1) * ↑u * ↑v)) / (2 * (θ - 1))

theorem Papers.AnsariRockel2024.plackett_one : Verification.plackett 1 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.plackett_density {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) : (Verification.plackett θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.plackettDensity θ ↑(x 0) ↑(x 1))

theorem Papers.AnsariRockel2024.plackett_ci_iff {θ : ℝ} (hθ : 0 < θ) : (Verification.plackett θ hθ).IsCI ↔ 1 ≤ θ

theorem Papers.AnsariRockel2024.plackett_cd_iff {θ : ℝ} (hθ : 0 < θ) : (Verification.plackett θ hθ).IsCD ↔ θ ≤ 1

theorem Papers.AnsariRockel2024.plackett_pqd_iff {θ : ℝ} (hθ : 0 < θ) : (Verification.plackett θ hθ).IsPQD ↔ 1 ≤ θ

theorem Papers.AnsariRockel2024.plackett_nqd_iff {θ : ℝ} (hθ : 0 < θ) : (Verification.plackett θ hθ).IsNQD ↔ θ ≤ 1

theorem Papers.AnsariRockel2024.plackett_tails {θ : ℝ} (hθ : 0 < θ) : (Verification.plackett θ hθ).HasLowerTailDependence 0 ∧ (Verification.plackett θ hθ).HasUpperTailDependence 0

theorem Papers.AnsariRockel2024.plackett_cdf_rationalized {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : (Verification.plackett θ hθ).cdf ![u, v] = 2 * θ * ↑u * ↑v / (Verification.plackettA θ ↑u ↑v + √(Verification.plackettD θ ↑u ↑v))

theorem Papers.AnsariRockel2024.plackett_tendsto_parameter {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hθ : ∀ (a : A), 0 < θ a) {η : ℝ} (hη : 0 < η) (ht : Filter.Tendsto θ l (nhds η)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : A) => (Verification.plackett (θ a) ⋯).cdf ![u, v]) l (nhds ((Verification.plackett η hη).cdf ![u, v]))

theorem Papers.AnsariRockel2024.plackett_tendsto_zero {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hθ : ∀ (a : A), 0 < θ a) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : A) => (Verification.plackett (θ a) ⋯).cdf ![u, v]) l (nhds (ProbabilityTheory.Copula.countermonotonic.cdf ![u, v]))

theorem Papers.AnsariRockel2024.plackett_tendsto_atTop {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hθ : ∀ (a : A), 0 < θ a) (ht : Filter.Tendsto θ l Filter.atTop) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : A) => (Verification.plackett (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf ![u, v]))

theorem Papers.AnsariRockel2024.plackett_lowerOrthant_iff {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) : (Verification.plackett θ hθ).LowerOrthantLE (Verification.plackett η hη) ↔ θ ≤ η

theorem Papers.AnsariRockel2024.plackett_schur_above_one {θ η : ℝ} (hθ : 0 < θ) (h1 : 1 ≤ θ) (hθη : θ ≤ η) : (Verification.plackett θ hθ).SchurBothLE (Verification.plackett η ⋯)

theorem Papers.AnsariRockel2024.plackett_schur_below_one {θ η : ℝ} (hθ : 0 < θ) (hη : η ≤ 1) (hθη : θ ≤ η) : (Verification.plackett η ⋯).SchurBothLE (Verification.plackett θ hθ)

theorem Papers.AnsariRockel2024.plackett_density_tp2_necessary {θ : ℝ} (hθ : 0 < θ) (hC : (Verification.plackett θ hθ).HasMTP2Density) : θ ∈ Set.Icc 1 2

theorem Papers.AnsariRockel2024.plackett_not_density_tp2_above_two {θ : ℝ} (hθ : 2 < θ) : ¬(Verification.plackett θ ⋯).HasMTP2Density

theorem Papers.AnsariRockel2024.plackett_density_tp2_iff {θ : ℝ} (hθ : 0 < θ) : (Verification.plackett θ hθ).HasMTP2Density ↔ θ ∈ Set.Icc 1 2

theorem Papers.AnsariRockel2024.plackett_spearmanRho {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) : (Verification.plackett θ hθ).spearmanRho = (θ + 1) / (θ - 1) - 2 * θ * Real.log θ / (θ - 1) ^ 2

Corrected Table 6 formula, derived from the actual copula measure.

theorem Papers.AnsariRockel2024.plackett_spearmanRho_one : (Verification.plackett 1 ⋯).spearmanRho = 0

theorem Papers.AnsariRockel2024.plackett_printed_rho_false : (Verification.plackett 2 ⋯).spearmanRho ≠ (2 + 1) / (2 - 1) - 2 * (2 * 2 / (2 - 1) ^ 2) * Real.log 2