← Copula mathematical handbook

The conditional CDF and Chatterjee's xi of FGM copulas

def ProbabilityTheory.Copula.fgmConditionalCDF (θ : ℝ) (u v : ↑unitInterval) : ℝ

The continuous version of the FGM conditional CDF, second coordinate given first.

Equations

• ProbabilityTheory.Copula.fgmConditionalCDF θ u v = ↑v + θ * (1 - 2 * ↑u) * ↑v * (1 - ↑v)

theorem ProbabilityTheory.Copula.fgmConditionalCDF_nonneg (θ : ℝ) (hθ : |θ| ≤ 1) (u v : ↑unitInterval) : 0 ≤ fgmConditionalCDF θ u v

theorem ProbabilityTheory.Copula.integral_Iic_fgmConditionalCDF (θ : ℝ) (u v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, fgmConditionalCDF θ t v = fgmCDF θ u v

theorem ProbabilityTheory.Copula.conditionalCDF_fgm (θ : ℝ) (hθ : |θ| ≤ 1) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (fgm θ hθ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => fgmConditionalCDF θ u v

theorem ProbabilityTheory.Copula.integral_unit_one_sub_two_mul : ∫ (t : ↑unitInterval), 1 - 2 * ↑t = 0

theorem ProbabilityTheory.Copula.integral_unit_one_sub_two_mul_sq : ∫ (t : ↑unitInterval), (1 - 2 * ↑t) ^ 2 = 1 / 3

theorem ProbabilityTheory.Copula.integral_fgmConditionalCDF_sq (θ : ℝ) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), fgmConditionalCDF θ u v ^ 2 = ↑v ^ 2 + θ ^ 2 / 3 * (↑v ^ 2 * (1 - ↑v) ^ 2)

theorem ProbabilityTheory.Copula.chatterjeeXi_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).chatterjeeXi = θ ^ 2 / 15