← Mathematical handbook

The Cauchy-Schwarz equality case and every discrete contact point

The exact variance defect gives equation (22). Equal blocks of a half-turn shuffle attain all the contact points x_N=1-3/(2N), N>=1.

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.quadratic_defect (C : Copula 2) : 1 - 2 / 3 * (1 - C.spearmanFootrule) ^ 2 - C.spearmanRho = 6 * ∫ (x : Fin 2 → ↑unitInterval), (|↑(x 0) - ↑(x 1)| - (1 - C.spearmanFootrule) / 3) ^ 2 ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.quadratic_equality_iff (C : Copula 2) : C.spearmanRho = 1 - 2 / 3 * (1 - C.spearmanFootrule) ^ 2 ↔ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, |↑(x 0) - ↑(x 1)| = (1 - C.spearmanFootrule) / 3

Equation (22): equality is exactly constant absolute displacement.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.halfTurn : Copula 2

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.halfTurn_rho : halfTurn.spearmanRho = -1 / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.halfTurn_footrule : halfTurn.spearmanFootrule = -1 / 2

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.contactCopula (n : ℕ) : Copula 2

Index n means N=n+1, covering every positive integer contact index.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoFootrule.contactCopula n = ProbabilityTheory.Copula.RankRegion.equalBlocks n ProbabilityTheory.Copula.RankRegion.RhoFootrule.halfTurn

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.contactCopula_coefficients (n : ℕ) : (contactCopula n).spearmanFootrule = 1 - 3 / (2 * (↑n + 1)) ∧ (contactCopula n).spearmanRho = 1 - 3 / (2 * (↑n + 1) ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.contactCopula_maximizes_rho (n : ℕ) (C : Copula 2) (hC : C.spearmanFootrule = 1 - 3 / (2 * (↑n + 1))) : C.spearmanRho ≤ (contactCopula n).spearmanRho

These are genuine global maxima at fixed footrule, not just benchmark values.

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.contactCopula_constant_displacement (n : ℕ) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(contactCopula n).toMeasure, |↑(x 0) - ↑(x 1)| = 1 / (2 * (↑n + 1))