← Copula 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 ProbabilityTheory.Copula.RankRegion.RhoGamma.rankMagnitude (u : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.rankMagnitude u = ⟨|2 * ↑u - 1|, ⋯⟩

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.continuous_rankMagnitude : Continuous rankMagnitude

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.rankMagnitude_uniform : MeasureTheory.Measure.map rankMagnitude MeasureTheory.volume = MeasureTheory.volume

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.magnitudeCopula (C : Copula 2) : Copula 2

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.rankSign (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.rankSign x = ↑(SignType.sign ((2 * ↑(x 0) - 1) * (2 * ↑(x 1) - 1)))

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.sign_product_identity (x : Fin 2 → ↑unitInterval) : rankSign x * ↑(rankMagnitude (x 0)) * ↑(rankMagnitude (x 1)) = (2 * ↑(x 0) - 1) * (2 * ↑(x 1) - 1)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.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 ProbabilityTheory.Copula.RankRegion.RhoGamma.sign_magnitude_rho (C : Copula 2) : C.spearmanRho = 3 * ∫ (x : Fin 2 → ↑unitInterval), rankSign x * ↑(rankMagnitude (x 0)) * ↑(rankMagnitude (x 1)) ∂C.toMeasure

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