← Copula mathematical handbook

Exactly the zero-variance means

This closes the contact-set characterization in Proposition 1.6(iii).

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.minimum_variance_zero_iff {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : minimumVariance m = 0 ↔ m = 0 ∨ ∃ (N : ℕ), 0 < N ∧ m = 1 / (2 * ↑N)

The correction vanishes exactly at zero and the reciprocal even-integer means.

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.constant_displacement_iff {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) : (∃ (C : Copula 2), ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, |↑(x 0) - ↑(x 1)| = m) ↔ m = 0 ∨ ∃ (N : ℕ), 0 < N ∧ m = 1 / (2 * ↑N)

Theorem 2.4's constant-value classification in the equivalent uniform-copula coordinates.