← Mathematical handbook

Lemma 3.1: uniform magnitudes and the sign decomposition

The sign is zero on either median. Both transformed marginals are proved uniform, and the two moment identities use the original copula measure.

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.rankMagnitude (u : ↑unitInterval) : ↑unitInterval

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.rankMagnitude u = ⟨|2 * ↑u - 1|, ⋯⟩

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.continuous_rankMagnitude : Continuous rankMagnitude

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.rankMagnitude_uniform : MeasureTheory.Measure.map rankMagnitude MeasureTheory.volume = MeasureTheory.volume

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.magnitude_marginal (C : ProbabilityTheory.Copula 2) (i : Fin 2) : MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => rankMagnitude (x i)) C.toMeasure = MeasureTheory.volume

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.magnitudeCopula (C : ProbabilityTheory.Copula 2) : ProbabilityTheory.Copula 2

Equations

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

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.rankSign (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.rankSign x = ↑(SignType.sign ((2 * ↑(x 0) - 1) * (2 * ↑(x 1) - 1)))

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sign_product_identity (x : Fin 2 → ↑unitInterval) : rankSign x * ↑(rankMagnitude (x 0)) * ↑(rankMagnitude (x 1)) = (2 * ↑(x 0) - 1) * (2 * ↑(x 1) - 1)

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sign_min_magnitude_identity (x : Fin 2 → ↑unitInterval) : rankSign x * min ↑(rankMagnitude (x 0)) ↑(rankMagnitude (x 1)) = |↑(x 0) + ↑(x 1) - 1| - |↑(x 0) - ↑(x 1)|

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sign_magnitude_rho (C : ProbabilityTheory.Copula 2) : C.spearmanRho = 3 * ∫ (x : Fin 2 → ↑unitInterval), rankSign x * ↑(rankMagnitude (x 0)) * ↑(rankMagnitude (x 1)) ∂C.toMeasure

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sign_magnitude_gamma (C : ProbabilityTheory.Copula 2) : C.giniGamma = 2 * ∫ (x : Fin 2 → ↑unitInterval), rankSign x * min ↑(rankMagnitude (x 0)) ↑(rankMagnitude (x 1)) ∂C.toMeasure