← Mathematical handbook

Kendall tau as the product of the two conditional CDFs

The identity uses disintegration and Fubini, so it applies to singular copulas as well as those admitting a Lebesgue density.

theorem Verification.integral_copula_conditionalKernel (C : ProbabilityTheory.Copula 2) (f : (Fin 2 → ↑unitInterval) → ℝ) (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂C.toMeasure = ∫ (u : ↑unitInterval), ∫ (v : ↑unitInterval), f ![u, v] ∂C.conditionalKernel u

theorem Verification.integral_unit_primitive (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure μ] (g : ↑unitInterval → ℝ) (hg : Measurable g) (hb : ∀ (t : ↑unitInterval), g t ∈ Set.Icc 0 1) : ∫ (v : ↑unitInterval), ∫ (t : ↑unitInterval) in Set.Iic v, g t ∂μ = ∫ (t : ↑unitInterval), g t * (1 - μ.real (Set.Iic t))

Integrating a bounded nonnegative primitive against a probability law.

theorem Verification.crossConditional_integrable (C : ProbabilityTheory.Copula 2) : MeasureTheory.Integrable (fun (p : ↑unitInterval × ↑unitInterval) => C.conditionalCDF p.1 p.2 * C.transpose.conditionalCDF p.2 p.1) MeasureTheory.volume

theorem Verification.kendallTau_conditional_product (C : ProbabilityTheory.Copula 2) : C.kendallTau = 1 - 4 * ∫ (u : ↑unitInterval) (v : ↑unitInterval), C.conditionalCDF u v * C.transpose.conditionalCDF v u