← Mathematical handbook

Exact Spearman rho of the Cuadras–Augé family

theorem Verification.integral_unit_rpow_nonneg (p : ℝ) (hp : 0 ≤ p) : ∫ (u : ↑unitInterval), ↑u ^ p = 1 / (p + 1)

theorem Verification.integral_unit_Iic_rpow_nonneg (p : ℝ) (hp : 0 ≤ p) (v : ↑unitInterval) : ∫ (u : ↑unitInterval) in Set.Iic v, ↑u ^ p = ↑v ^ (p + 1) / (p + 1)

theorem Verification.cuadrasAuge_cdf_of_le (δ u v : ↑unitInterval) (h : u ≤ v) : (ProbabilityTheory.Copula.cuadrasAuge δ).cdf ![u, v] = ↑u * ↑v ^ (1 - ↑δ)

theorem Verification.cuadrasAuge_cdf_of_ge (δ u v : ↑unitInterval) (h : v ≤ u) : (ProbabilityTheory.Copula.cuadrasAuge δ).cdf ![u, v] = ↑u ^ (1 - ↑δ) * ↑v

theorem Verification.integral_cuadrasAuge_section (δ v : ↑unitInterval) : ∫ (u : ↑unitInterval), (ProbabilityTheory.Copula.cuadrasAuge δ).cdf ![u, v] = ↑v ^ (3 - ↑δ) / 2 + ↑v / (2 - ↑δ) - ↑v ^ (3 - ↑δ) / (2 - ↑δ)

theorem Verification.integral_cuadrasAuge_cdf (δ : ↑unitInterval) : ∫ (x : Fin 2 → ↑unitInterval), (ProbabilityTheory.Copula.cuadrasAuge δ).cdf x = 1 / (4 - ↑δ)

theorem Verification.cuadrasAuge_spearmanRho (δ : ↑unitInterval) : (ProbabilityTheory.Copula.cuadrasAuge δ).spearmanRho = 3 * ↑δ / (4 - ↑δ)