← Copula mathematical handbook

The centered ordinal-sum identities (equation 9)

The parameter here is the central width alpha=1-2a. Both zero width and full width are included, and the CDF is checked on the central square.

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

Equations

• ProbabilityTheory.Copula.RankRegion.Common.centralMargin α = ⟨(1 - ↑α) / 2, ⋯⟩

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

Equations

• ProbabilityTheory.Copula.RankRegion.Common.centralSplit α = ⟨2 * ↑α / (1 + ↑α), ⋯⟩

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

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

Equations

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

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

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

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

Embed a point into the central interval.

Equations

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

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

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

The actual CDF on the central square, including the collapsed endpoint.

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

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

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

theorem ProbabilityTheory.Copula.RankRegion.Common.centeredOrdinal_rho (C : Copula 2) (α : ↑unitInterval) : (centeredOrdinal C α).spearmanRho = ↑α ^ 3 * C.spearmanRho + 1 - ↑α ^ 3