← Mathematical handbook

Spearman rho dominates xi under stochastic monotonicity

The scalar estimate compares squared differences with absolute differences of an antitone function taking values in [0,1].

theorem Verification.integral_lower_integral {g : ↑unitInterval → ℝ} (hg : Measurable g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : ∫ (u : ↑unitInterval), ∫ (w : ↑unitInterval) in Set.Iic u, g w = ∫ (w : ↑unitInterval), (1 - ↑w) * g w

theorem Verification.integrable_lower_integral {g : ↑unitInterval → ℝ} (hg : Measurable g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => ∫ (w : ↑unitInterval) in Set.Iic u, g w) MeasureTheory.volume

theorem Verification.integral_abs_sub_of_antitone {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (u : ↑unitInterval) : ∫ (w : ↑unitInterval), |g u - g w| = ((2 * ∫ (w : ↑unitInterval) in Set.Iic u, g w) - ∫ (w : ↑unitInterval), g w) + g u - 2 * ↑u * g u

theorem Verification.integral_sq_le_twice_lower_integral {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : ∫ (u : ↑unitInterval), g u ^ 2 ≤ ((2 * ∫ (u : ↑unitInterval), ∫ (w : ↑unitInterval) in Set.Iic u, g w) - ∫ (u : ↑unitInterval), g u) + (∫ (u : ↑unitInterval), g u) ^ 2

theorem Verification.conditionalCDF_sq_le_cdf_integral (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 ≤ (2 * ∫ (u : ↑unitInterval), C.cdf ![u, v]) - ↑v + ↑v ^ 2

theorem Verification.spearmanRho_eq_iterated_cdf (C : ProbabilityTheory.Copula 2) : C.spearmanRho = (12 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), C.cdf ![u, v]) - 3

theorem Verification.xi_le_rho_of_isSI (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) : C.chatterjeeXi ≤ C.spearmanRho

theorem Verification.xi_le_neg_rho_of_isSD (C : ProbabilityTheory.Copula 2) (hC : C.IsSD) : C.chatterjeeXi ≤ -C.spearmanRho

theorem Verification.xi_le_abs_rho_of_stochastically_monotone (C : ProbabilityTheory.Copula 2) (hC : C.IsSI ∨ C.IsSD) : C.chatterjeeXi ≤ |C.spearmanRho|