← Mathematical handbook

Nelsen 7: exact conditional law, xi, CI region and Schur parameter order

theorem Papers.AnsariRockel2024.nelsen7_conditionalCDF (θ v : ↑unitInterval) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.nelsen7 θ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => ProbabilityTheory.Copula.nelsen7ConditionalCDF θ u v

theorem Papers.AnsariRockel2024.nelsen7_derivative (θ v : ↑unitInterval) : (fun (u : ↑unitInterval) => deriv ((ProbabilityTheory.Copula.nelsen7 θ).cdfSection v) ↑u) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => ProbabilityTheory.Copula.nelsen7ConditionalCDF θ u v

theorem Papers.AnsariRockel2024.nelsen7_xi (θ : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).chatterjeeXi = 1 - ↑θ

theorem Papers.AnsariRockel2024.nelsen7_ci_iff (θ : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).IsCI ↔ θ = 1

theorem Papers.AnsariRockel2024.nelsen7_schur_iff (θ η : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).SchurBothLE (ProbabilityTheory.Copula.nelsen7 η) ↔ η ≤ θ