← Mathematical handbook

Conditional CDF and Chatterjee's xi of Nelsen's seventh family

The formula includes the singular endpoint at zero and independence at one. No density assumption is made.

noncomputable def ProbabilityTheory.Copula.nelsen7Threshold (θ v : ↑unitInterval) : ↑unitInterval

The threshold separating the zero and positive parts of a conditional CDF.

Equations

• ProbabilityTheory.Copula.nelsen7Threshold θ v = ⟨(1 - ↑θ) * (1 - ↑v) / (↑θ * ↑v + 1 - ↑θ), ⋯⟩

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

A version of the conditional CDF of the second coordinate given the first.

Equations

• ProbabilityTheory.Copula.nelsen7ConditionalCDF θ u v = (Set.Ioi (ProbabilityTheory.Copula.nelsen7Threshold θ v)).indicator (fun (x : ↑unitInterval) => ↑θ * ↑v + 1 - ↑θ) u

theorem ProbabilityTheory.Copula.integrable_nelsen7ConditionalCDF (θ v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => nelsen7ConditionalCDF θ u v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.integral_Iic_nelsen7ConditionalCDF (θ u v : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, nelsen7ConditionalCDF θ t v = (nelsen7 θ).cdf ![u, v]

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

theorem ProbabilityTheory.Copula.integral_nelsen7ConditionalCDF_sq (θ v : ↑unitInterval) : ∫ (u : ↑unitInterval), nelsen7ConditionalCDF θ u v ^ 2 = (↑θ * ↑v + 1 - ↑θ) * ↑v

theorem ProbabilityTheory.Copula.chatterjeeXi_nelsen7 (θ : ↑unitInterval) : (nelsen7 θ).chatterjeeXi = 1 - ↑θ

Table 6 of Ansari--Rockel, on the full closed parameter interval.