← Copula mathematical handbook

A central copula block with comonotonic outer blocks

This endpoint-safe construction places a copula in the centered square of side length r. It is useful for fixed-median extremizing shuffles.

noncomputable def ProbabilityTheory.Copula.RankRegion.centeredEdge (r : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.centeredEdge r = ⟨(1 - ↑r) / 2, ⋯⟩

noncomputable def ProbabilityTheory.Copula.RankRegion.centeredSplit (r : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.centeredSplit r = ⟨2 * ↑r / (1 + ↑r), ⋯⟩

noncomputable def ProbabilityTheory.Copula.RankRegion.centered (C : Copula 2) (r : ↑unitInterval) : Copula 2

Insert C in the centered square of side r, with M on either side.

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.centered_rho (C : Copula 2) (r : ↑unitInterval) : (centered C r).spearmanRho = 1 - ↑r ^ 3 * (1 - C.spearmanRho)

theorem ProbabilityTheory.Copula.RankRegion.centered_tau (C : Copula 2) (r : ↑unitInterval) : (centered C r).kendallTau = 1 - ↑r ^ 2 * (1 - C.kendallTau)

theorem ProbabilityTheory.Copula.RankRegion.centered_footrule (C : Copula 2) (r : ↑unitInterval) : (centered C r).spearmanFootrule = 1 - ↑r ^ 2 * (1 - C.spearmanFootrule)

theorem ProbabilityTheory.Copula.RankRegion.centered_beta (C : Copula 2) (r : ↑unitInterval) : (centered C r).blomqvistBeta = 1 - ↑r * (1 - C.blomqvistBeta)