← Copula mathematical handbook

The bridge from conditional CDFs to the classical partial derivative

noncomputable def ProbabilityTheory.Copula.cdfSection (C : Copula 2) (v : ↑unitInterval) (u : ℝ) : ℝ

The CDF section extended constantly outside the unit interval.

Equations

• C.cdfSection v u = C.cdf ![Set.projIcc 0 1 ProbabilityTheory.Copula.cdfSection._proof_1 u, v]

theorem ProbabilityTheory.Copula.integral_Iic_unit_eq_interval (f : ↑unitInterval → ℝ) (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, f t = ∫ (t : ℝ) in 0..↑u, f (Set.projIcc 0 1 ⋯ t)

theorem ProbabilityTheory.Copula.conditionalCDF_eq_deriv (C : Copula 2) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => deriv (C.cdfSection v) ↑u

For each threshold, the classical first partial derivative equals the conditional CDF almost everywhere in the conditioning coordinate. No density is required.

theorem ProbabilityTheory.Copula.chatterjeeXi_eq_integral_deriv (C : Copula 2) : C.chatterjeeXi = (6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.cdfSection v) ↑u ^ 2) - 2

Chatterjee's population coefficient in the derivative convention of the articles.