← Copula mathematical handbook

Kendall's tau of the Plackett family: a one-dimensional integral

Starting from the rational representation kendallTau_plackett_eq_rational (Copula.Families.Plackett.Kendall), the inner integral is elementary: for 0 < v < 1 write x = (θ-1)u + 1 - (θ+1)v (PlackettKendall.shift) and s = 2√θ √(v(1-v)) (PlackettKendall.arcScale); then disc = x² + s² and the numerator is 1 + (θ-1)(u+v-2uv) = (1-2v) x + 2(θ+1) v(1-v), so the u-integrand has the primitive ((1-2v)/2 · log disc + (θ+1)/√θ · √(v(1-v)) · arctan(x/s)) / (θ-1) (PlackettKendall.hasDerivAt_ratPrimitive). The boundary terms are symmetric under v ↦ 1 - v, and the logarithmic part integrates in closed form. The result is (kendallTau_plackett_eq_arctan, θ ≠ 1)

τ(C_θ) = (θ+1)/(θ-1) - 2θ(θ² - 1 - 2θ log θ)/(θ-1)⁴ + 4(θ+1)√θ/(θ-1)² · J(θ),

J(θ) = ∫₀¹ √(v(1-v)) arctan((1 - (θ+1)v) / (2√θ √(v(1-v)))) dv (plackettTauIntegral),

equivalently, with Mardia's ρ(C_θ) = (θ² - 1 - 2θ log θ)/(θ-1)² (spearmanRho_plackett),

τ(C_θ) = (θ+1)/(θ-1) - 2θ ρ(C_θ)/(θ-1)² + 4(θ+1)√θ/(θ-1)² · J(θ) (kendallTau_plackett_eq_spearmanRho_arctan).

There is no elementary closed form for J; the formula reduces the computation of τ(C_θ) to one bounded one-dimensional integral (checked numerically, e.g. τ(C_2) ≈ 0.15305, τ(C_5) ≈ 0.34550, τ(C_{20}) ≈ 0.59166).

def ProbabilityTheory.Copula.PlackettKendall.shift (θ u v : ℝ) : ℝ

x(u,v) = (θ-1)u + 1 - (θ+1)v, so that disc(u,v) = x² + 4θv(1-v).

Equations

• ProbabilityTheory.Copula.PlackettKendall.shift θ u v = (θ - 1) * u + 1 - (θ + 1) * v

noncomputable def ProbabilityTheory.Copula.PlackettKendall.arcScale (θ v : ℝ) : ℝ

s(v) = 2√θ √(v(1-v)), so that disc(u,v) = x(u,v)² + s(v)².

Equations

• ProbabilityTheory.Copula.PlackettKendall.arcScale θ v = 2 * √θ * √(v * (1 - v))

theorem ProbabilityTheory.Copula.PlackettKendall.plackettDisc_eq_shift (θ u v : ℝ) : plackettDisc θ u v = shift θ u v ^ 2 + 4 * θ * v * (1 - v)

theorem ProbabilityTheory.Copula.PlackettKendall.arcScale_sq {θ v : ℝ} (hθ : 0 ≤ θ) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : arcScale θ v ^ 2 = 4 * θ * v * (1 - v)

theorem ProbabilityTheory.Copula.PlackettKendall.arcScale_pos {θ v : ℝ} (hθ : 0 < θ) (hv0 : 0 < v) (hv1 : v < 1) : 0 < arcScale θ v

theorem ProbabilityTheory.Copula.PlackettKendall.plackettDisc_pos_of_mem {θ v : ℝ} (hθ : 0 < θ) (hv0 : 0 < v) (hv1 : v < 1) (u : ℝ) : 0 < plackettDisc θ u v

noncomputable def ProbabilityTheory.Copula.PlackettKendall.ratPrimitive (θ v u : ℝ) : ℝ

The primitive in u of the rational part (1 + (θ-1)(u+v-2uv))/disc.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.PlackettKendall.hasDerivAt_ratPrimitive {θ v : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) (hv0 : 0 < v) (hv1 : v < 1) (u : ℝ) : HasDerivAt (ratPrimitive θ v) (plackettRatPart θ u v) u

theorem ProbabilityTheory.Copula.PlackettKendall.continuous_plackettRatPart_left {θ v : ℝ} (hθ : 0 < θ) (hv0 : 0 < v) (hv1 : v < 1) : Continuous fun (u : ℝ) => plackettRatPart θ u v

theorem ProbabilityTheory.Copula.PlackettKendall.integral_plackettRatPart_left {θ v : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) (hv0 : 0 < v) (hv1 : v < 1) : ∫ (u : ℝ) in 0..1, plackettRatPart θ u v = ratPrimitive θ v 1 - ratPrimitive θ v 0

The u-integral of the rational part, by the fundamental theorem of calculus.

noncomputable def ProbabilityTheory.Copula.PlackettKendall.logPart (θ v : ℝ) : ℝ

The logarithmic part (1 - 2v) log(1 + (θ-1)v).

Equations

• ProbabilityTheory.Copula.PlackettKendall.logPart θ v = (1 - 2 * v) * Real.log (1 + (θ - 1) * v)

noncomputable def ProbabilityTheory.Copula.PlackettKendall.arcPart (θ v : ℝ) : ℝ

The arctangent part √(v(1-v)) arctan((1 - (θ+1)v)/(2√θ√(v(1-v)))).

Equations

• ProbabilityTheory.Copula.PlackettKendall.arcPart θ v = √(v * (1 - v)) * Real.arctan ((1 - (θ + 1) * v) / ProbabilityTheory.Copula.PlackettKendall.arcScale θ v)

noncomputable def ProbabilityTheory.Copula.PlackettKendall.half (θ v : ℝ) : ℝ

Half of the boundary term: ∫₀¹ ratPart(u,v) du = half(v) + half(1-v).

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.PlackettKendall.ratPrimitive_sub (θ v : ℝ) : ratPrimitive θ v 1 - ratPrimitive θ v 0 = half θ v + half θ (1 - v)

theorem ProbabilityTheory.Copula.PlackettKendall.measurable_arcPart (θ : ℝ) : Measurable (arcPart θ)

theorem ProbabilityTheory.Copula.PlackettKendall.abs_arcPart_le {θ v : ℝ} (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : |arcPart θ v| ≤ Real.pi / 2

theorem ProbabilityTheory.Copula.PlackettKendall.integrable_arcPart (θ : ℝ) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => arcPart θ ↑v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.PlackettKendall.one_add_mul_pos {θ v : ℝ} (hθ : 0 < θ) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) : 0 < 1 + (θ - 1) * v

theorem ProbabilityTheory.Copula.PlackettKendall.continuousOn_logPart {θ : ℝ} (hθ : 0 < θ) : ContinuousOn (logPart θ) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.PlackettKendall.integrable_logPart {θ : ℝ} (hθ : 0 < θ) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => logPart θ ↑v) MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.PlackettKendall.logPrimitive (θ v : ℝ) : ℝ

A primitive of the logarithmic part.

Equations

• ProbabilityTheory.Copula.PlackettKendall.logPrimitive θ v = v ^ 2 / 2 - v * (v - 1) * Real.log (1 + (θ - 1) * v) - v * θ / (θ - 1) + θ * Real.log (1 + (θ - 1) * v) / (θ - 1) ^ 2

theorem ProbabilityTheory.Copula.PlackettKendall.hasDerivAt_logPrimitive {θ v : ℝ} (hθ1 : θ ≠ 1) (hv : 0 < 1 + (θ - 1) * v) : HasDerivAt (logPrimitive θ) (logPart θ v) v

theorem ProbabilityTheory.Copula.PlackettKendall.integral_logPart {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) : ∫ (v : ↑unitInterval), logPart θ ↑v = 1 / 2 - θ / (θ - 1) + θ * Real.log θ / (θ - 1) ^ 2

theorem ProbabilityTheory.Copula.PlackettKendall.integrable_half {θ : ℝ} (hθ : 0 < θ) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => half θ ↑v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.PlackettKendall.integral_plackettRatPart {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) : ∫ (v : ↑unitInterval) (u : ↑unitInterval), plackettRatPart θ ↑u ↑v = 2 * ∫ (v : ↑unitInterval), half θ ↑v

The double integral of the rational part as twice the integral of half.

noncomputable def ProbabilityTheory.Copula.plackettTauIntegral (θ : ℝ) : ℝ

The arctangent integral J(θ) = ∫₀¹ √(v(1-v)) arctan((1 - (θ+1)v)/(2√θ √(v(1-v)))) dv appearing in Kendall's tau of the Plackett copula.

Equations

• ProbabilityTheory.Copula.plackettTauIntegral θ = ∫ (v : ℝ) in 0..1, √(v * (1 - v)) * Real.arctan ((1 - (θ + 1) * v) / (2 * √θ * √(v * (1 - v))))

theorem ProbabilityTheory.Copula.kendallTau_plackett_eq_arctan {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) : (plackett θ hθ).kendallTau = (θ + 1) / (θ - 1) - 2 * θ * (θ ^ 2 - 1 - 2 * θ * Real.log θ) / (θ - 1) ^ 4 + 4 * (θ + 1) * √θ / (θ - 1) ^ 2 * plackettTauIntegral θ

Kendall's tau of the Plackett copula as a one-dimensional integral (θ ≠ 1): τ(C_θ) = (θ+1)/(θ-1) - 2θ(θ² - 1 - 2θ log θ)/(θ-1)⁴ + 4(θ+1)√θ/(θ-1)² · J(θ).

theorem ProbabilityTheory.Copula.kendallTau_plackett_eq_spearmanRho_arctan {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≠ 1) : (plackett θ hθ).kendallTau = (θ + 1) / (θ - 1) - 2 * θ * (plackett θ hθ).spearmanRho / (θ - 1) ^ 2 + 4 * (θ + 1) * √θ / (θ - 1) ^ 2 * plackettTauIntegral θ

Kendall's tau of the Plackett copula in terms of Spearman's rho and J(θ) (θ ≠ 1): τ(C_θ) = (θ+1)/(θ-1) - 2θ ρ(C_θ)/(θ-1)² + 4(θ+1)√θ/(θ-1)² · J(θ).