← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.lower_threshold (A : AuxiliaryCertificate) (x : Fin 2 → ↑unitInterval) : (thresholdSign A.t fun (i : Fin 2) => OrdinalSum.lowerEmbed A.a (x i)) = false

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper_threshold (A : AuxiliaryCertificate) (u v : ↑unitInterval) (hc : A.h ↑u + A.h ↑v = (↑u - ↑v) ^ 2 - A.s * |↑u - ↑v|) : A.t ≤ max ↑(OrdinalSum.upperEmbed A.a u) ↑(OrdinalSum.upperEmbed A.a v)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.upper_threshold_ae (A : AuxiliaryCertificate) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂A.D.toMeasure, (thresholdSign A.t fun (i : Fin 2) => OrdinalSum.upperEmbed A.a (x i)) = true

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.signed_integral (A : AuxiliaryCertificate) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), (if thresholdSign A.t x = true then 1 else -1) * f x ∂A.magnitudes.toMeasure = (-↑A.a * ∫ (u : ↑unitInterval), f fun (x : Fin 2) => OrdinalSum.lowerEmbed A.a u) + A.z * ∫ (x : Fin 2 → ↑unitInterval), f fun (i : Fin 2) => OrdinalSum.upperEmbed A.a (x i) ∂A.D.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.integral_min (D : Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), min ↑(x 0) ↑(x 1) ∂D.toMeasure = (D.spearmanFootrule + 2) / 6

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.integral_lower_min (A : AuxiliaryCertificate) : ∫ (u : ↑unitInterval), min ↑(OrdinalSum.lowerEmbed A.a u) ↑(OrdinalSum.lowerEmbed A.a u) = ↑A.a / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.integral_upper_min (A : AuxiliaryCertificate) : ∫ (x : Fin 2 → ↑unitInterval), min ↑(OrdinalSum.upperEmbed A.a (x 0)) ↑(OrdinalSum.upperEmbed A.a (x 1)) ∂A.D.toMeasure = ↑A.a + A.z * (A.D.spearmanFootrule + 2) / 6

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.gamma (A : AuxiliaryCertificate) : A.copula.giniGamma = 1 - 2 * ↑A.a ^ 2 - A.z ^ 2 * (1 - A.D.spearmanFootrule) / 3

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.integral_lower_product (A : AuxiliaryCertificate) : ∫ (u : ↑unitInterval), ↑(OrdinalSum.lowerEmbed A.a u) * ↑(OrdinalSum.lowerEmbed A.a u) = ↑A.a ^ 2 / 3

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.integral_upper_product (A : AuxiliaryCertificate) : ∫ (x : Fin 2 → ↑unitInterval), ↑(OrdinalSum.upperEmbed A.a (x 0)) * ↑(OrdinalSum.upperEmbed A.a (x 1)) ∂A.D.toMeasure = ↑A.a ^ 2 + ↑A.a * A.z + A.z ^ 2 * (A.D.spearmanRho + 3) / 12

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.rho (A : AuxiliaryCertificate) : A.copula.spearmanRho = 1 - 2 * ↑A.a ^ 3 - A.z ^ 3 * (1 - A.D.spearmanRho) / 4

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate.maximizes_rho (A : AuxiliaryCertificate) (C : Copula 2) (h : C.giniGamma = A.copula.giniGamma) : C.spearmanRho ≤ A.copula.spearmanRho