← Mathematical handbook

Measurable equality classification for the SI xi-footrule bound

The cut functions are the lengths of the one and positive level sets of the conditional CDF. Both are nondecreasing in the response threshold. The middle level is recovered from the uniform marginal.

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

Equations

• Verification.conditionalOneCut C v = ⟨∫ (u : ↑unitInterval), Verification.oneLevel (fun (t : ↑unitInterval) => C.conditionalCDF t v) u, ⋯⟩

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

Equations

• Verification.conditionalPositiveCut C v = ⟨∫ (u : ↑unitInterval), Verification.positiveLevel (fun (t : ↑unitInterval) => C.conditionalCDF t v) u, ⋯⟩

theorem Verification.conditionalOneCut_le (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : conditionalOneCut C v ≤ v

theorem Verification.le_conditionalPositiveCut (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : v ≤ conditionalPositiveCut C v

theorem Verification.conditionalOneCut_monotone (C : ProbabilityTheory.Copula 2) : Monotone (conditionalOneCut C)

theorem Verification.conditionalPositiveCut_monotone (C : ProbabilityTheory.Copula 2) : Monotone (conditionalPositiveCut C)

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

Equations

• Verification.conditionalMiddle C v = ⟨(↑v - ↑(Verification.conditionalOneCut C v)) / (↑(Verification.conditionalPositiveCut C v) - ↑(Verification.conditionalOneCut C v)), ⋯⟩

theorem Verification.measurable_conditionalMiddle (C : ProbabilityTheory.Copula 2) : Measurable (conditionalMiddle C)

theorem Verification.ae_diagonal_moment_eq_iff (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanFootrule ↔ ∀ᵐ (v : ↑unitInterval), ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 = C.cdf ![v, v]

theorem Verification.conditionalCDF_threeLevel_of_diagonal_moment_eq (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (v : ↑unitInterval) (heq : ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 = C.cdf ![v, v]) : (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] threeLevel (conditionalOneCut C v) (conditionalPositiveCut C v) ↑(conditionalMiddle C v)

theorem Verification.xi_eq_footrule_of_threeLevel (C : ProbabilityTheory.Copula 2) (A B a : ↑unitInterval → ↑unitInterval) (hAB : ∀ (v : ↑unitInterval), A v ≤ B v) (hr : ∀ᵐ (v : ↑unitInterval), (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] threeLevel (A v) (B v) ↑(a v)) : C.chatterjeeXi = C.spearmanFootrule

A three-level representation with ordered cuts implies equality even without separately assuming SI.

theorem Verification.si_xi_eq_footrule_iff_ordered_threeLevel (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanFootrule ↔ ∃ (A : ↑unitInterval → ↑unitInterval) (B : ↑unitInterval → ↑unitInterval) (a : ↑unitInterval → ↑unitInterval), Monotone A ∧ Monotone B ∧ Measurable A ∧ Measurable B ∧ Measurable a ∧ (∀ (v : ↑unitInterval), A v ≤ B v) ∧ ∀ᵐ (v : ↑unitInterval), (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] threeLevelOpen (A v) (B v) ↑(a v)

Proposition 2.2 with canonical measurable, nondecreasing cut functions.

theorem Verification.xi_eq_footrule_of_threeLevelOpen (C : ProbabilityTheory.Copula 2) (A B a : ↑unitInterval → ↑unitInterval) (hr : ∀ᵐ (v : ↑unitInterval), (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] threeLevelOpen (A v) (B v) ↑(a v)) : C.chatterjeeXi = C.spearmanFootrule

The open-interval representation implies equality without an ordering hypothesis on the supplied cuts: replace B with max A B.

theorem Verification.si_xi_eq_footrule_iff_threeLevel (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanFootrule ↔ ∃ (A : ↑unitInterval → ↑unitInterval) (B : ↑unitInterval → ↑unitInterval) (a : ↑unitInterval → ↑unitInterval), Monotone A ∧ Monotone B ∧ Measurable A ∧ Measurable B ∧ Measurable a ∧ ∀ᵐ (v : ↑unitInterval), (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] threeLevelOpen (A v) (B v) ↑(a v)

The exact existential representation in Proposition 2.2.

theorem Verification.si_xi_eq_footrule_iff_derivative_threeLevel (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi = C.spearmanFootrule ↔ ∃ (A : ↑unitInterval → ↑unitInterval) (B : ↑unitInterval → ↑unitInterval) (a : ↑unitInterval → ↑unitInterval), Monotone A ∧ Monotone B ∧ Measurable A ∧ Measurable B ∧ Measurable a ∧ ∀ᵐ (v : ↑unitInterval), (fun (u : ↑unitInterval) => deriv (C.cdfSection v) ↑u) =ᵐ[MeasureTheory.volume] threeLevelOpen (A v) (B v) ↑(a v)