← Mathematical handbook

Moment identities, reflection symmetry, and fixed-gamma fibres

This checks equation (28) of Lemma 3.1 and the interpolation/symmetry steps used to reduce the region problem to its upper boundary. The sign/magnitude decomposition and the optimal transport argument remain separate obligations.

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.moment_representation (C : Copula 2) : C.spearmanRho = 1 - 6 * ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂C.toMeasure ∧ C.giniGamma = 2 * ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) + ↑(x 1) - 1| - |↑(x 0) - ↑(x 1)| ∂C.toMeasure

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.reflection_pair (C : Copula 2) : (C.reflect {1}).spearmanRho = -C.spearmanRho ∧ (C.reflect {1}).giniGamma = -C.giniGamma

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.fixed_gamma_intermediate (C D : Copula 2) {g r : ℝ} (hC : C.giniGamma = g) (hD : D.giniGamma = g) (hrC : C.spearmanRho ≤ r) (hrD : r ≤ D.spearmanRho) : ∃ (E : Copula 2), E.giniGamma = g ∧ E.spearmanRho = r

def ProbabilityTheory.Copula.RankRegion.RhoGamma.region : Set (ℝ × ℝ)

The attainable set uses the source's coordinate order (rho, gamma).

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.region = Set.range fun (C : ProbabilityTheory.Copula 2) => (C.spearmanRho, C.giniGamma)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.region_convex : Convex ℝ region

The convexity assertion of Theorem 1.1, independently of its boundary formula.

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.region_centrally_symmetric {r g : ℝ} (h : (r, g) ∈ region) : (-r, -g) ∈ region

The central-symmetry assertion of Theorem 1.1.