← Copula mathematical handbook

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

noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centralMargin (α : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centralMargin α = ProbabilityTheory.Copula.RankRegion.Common.centralMargin α

noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centralSplit (α : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centralSplit α = ProbabilityTheory.Copula.RankRegion.Common.centralSplit α

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.central_weight (α : ↑unitInterval) : (1 - ↑(centralMargin α)) * ↑(centralSplit α) = ↑α

noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centeredOrdinal (C : Copula 2) (α : ↑unitInterval) : Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centeredOrdinal C α = ProbabilityTheory.Copula.RankRegion.Common.centeredOrdinal C α

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centeredOrdinal_zero (C : Copula 2) : centeredOrdinal C 0 = comonotonic 2

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centeredOrdinal_one (C : Copula 2) : centeredOrdinal C 1 = C

noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centralEmbed (α u : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.centralEmbed α u = ProbabilityTheory.Copula.RankRegion.Common.centralEmbed α u

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.coe_centralEmbed (α u : ↑unitInterval) : ↑(centralEmbed α u) = (1 - ↑α) / 2 + ↑α * ↑u

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

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

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

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