← 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 Verification.centralMargin (α : ↑unitInterval) : ↑unitInterval

Equations

• Verification.centralMargin α = ⟨(1 - ↑α) / 2, ⋯⟩

noncomputable def Verification.centralSplit (α : ↑unitInterval) : ↑unitInterval

Equations

• Verification.centralSplit α = ⟨2 * ↑α / (1 + ↑α), ⋯⟩

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

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

Equations

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

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

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

noncomputable def Verification.centralEmbed (α u : ↑unitInterval) : ↑unitInterval

Embed a point into the central interval.

Equations

• Verification.centralEmbed α u = ProbabilityTheory.Copula.OrdinalSum.upperEmbed (Verification.centralMargin α) (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed (Verification.centralSplit α) u)

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

theorem Verification.centeredOrdinal_cdf (C : ProbabilityTheory.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 Verification.centeredOrdinal_tau (C : ProbabilityTheory.Copula 2) (α : ↑unitInterval) : (centeredOrdinal C α).kendallTau = ↑α ^ 2 * C.kendallTau + 1 - ↑α ^ 2

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

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

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