← Mathematical handbook

Chatterjee xi under diagonal localization

noncomputable def Verification.normalizedSquareMass (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : ℝ

Equations

• Verification.normalizedSquareMass C v = ∫ (u : ↑unitInterval), Verification.normalizedCDF C u v ^ 2

theorem Verification.normalizedSquareMass_eq (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : normalizedSquareMass C v = ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2

theorem Verification.normalizedSquareMass_measurable (C : ProbabilityTheory.Copula 2) : Measurable (normalizedSquareMass C)

theorem Verification.normalizedSquareMass_integrable (C : ProbabilityTheory.Copula 2) : MeasureTheory.Integrable (normalizedSquareMass C) MeasureTheory.volume

theorem Verification.normalizedSquareMass_zero (C : ProbabilityTheory.Copula 2) : normalizedSquareMass C 0 = 0

theorem Verification.normalizedSquareMass_one (C : ProbabilityTheory.Copula 2) : normalizedSquareMass C 1 = 1

theorem Verification.normalizedCDF_square_integrable (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => normalizedCDF C u v ^ 2) MeasureTheory.volume

theorem Verification.conditionalBlocks_squareMass (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), (conditionalBlocks C D a ha0 ha1).conditionalCDF u v ^ 2 = ↑a * normalizedSquareMass C (ProbabilityTheory.Copula.OrdinalSum.lowerCoord a v) + (1 - ↑a) * normalizedSquareMass D (ProbabilityTheory.Copula.OrdinalSum.upperCoord a v)

theorem Verification.conditionalBlocks_xi (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : (conditionalBlocks C D a ha0 ha1).chatterjeeXi = 1 - ↑a ^ 2 * (1 - C.chatterjeeXi) - (1 - ↑a) ^ 2 * (1 - D.chatterjeeXi)