← Mathematical handbook

Equation (9): source-facing names for the shared centered ordinal sum

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.centralMargin (α : ↑unitInterval) : ↑unitInterval

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.centralMargin α = Verification.centralMargin α

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.centralSplit (α : ↑unitInterval) : ↑unitInterval

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.centralSplit α = Verification.centralSplit α

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.central_weight (α : ↑unitInterval) : (1 - ↑(centralMargin α)) * ↑(centralSplit α) = ↑α

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.centeredOrdinal (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) : ProbabilityTheory.Copula 2

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.centeredOrdinal C α = Verification.centeredOrdinal C α

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.centeredOrdinal_zero (C : ProbabilityTheory.Copula 2) : centeredOrdinal C 0 = ProbabilityTheory.Copula.comonotonic 2

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.centeredOrdinal_one (C : ProbabilityTheory.Copula 2) : centeredOrdinal C 1 = C

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.centralEmbed (α u : ↑unitInterval) : ↑unitInterval

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.centralEmbed α u = Verification.centralEmbed α u

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.coe_centralEmbed (α u : ↑unitInterval) : ↑(centralEmbed α u) = (1 - ↑α) / 2 + ↑α * ↑u

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.centeredOrdinal_cdf (C : ProbabilityTheory.Copula 2) (α u v : ↑unitInterval) : (centeredOrdinal C α).cdf ![centralEmbed α u, centralEmbed α v] = (1 - ↑α) / 2 + ↑α * C.cdf ![u, v]

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.centeredOrdinal_tau (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) : (centeredOrdinal C α).kendallTau = ↑α ^ 2 * C.kendallTau + 1 - ↑α ^ 2

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.centeredOrdinal_footrule (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) : (centeredOrdinal C α).spearmanFootrule = ↑α ^ 2 * C.spearmanFootrule + 1 - ↑α ^ 2

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.centeredOrdinal_beta (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) : (centeredOrdinal C α).blomqvistBeta = ↑α * C.blomqvistBeta + 1 - ↑α