← Mathematical handbook

Dependence and symmetry of a central countermonotonic block

theorem Verification.centralMargin_lt_one (α : ↑unitInterval) : centralMargin α < 1

theorem Verification.central_top (α : ↑unitInterval) : ProbabilityTheory.Copula.OrdinalSum.upperEmbed (centralMargin α) (centralSplit α) = unitInterval.symm (centralMargin α)

theorem Verification.centeredOrdinal_cdf_below (C : ProbabilityTheory.Copula 2) (α u v : ↑unitInterval) (huv : u ≤ v) (hu : u ≤ centralMargin α) : (centeredOrdinal C α).cdf ![u, v] = ↑u

theorem Verification.centeredOrdinal_cdf_above (C : ProbabilityTheory.Copula 2) (α u v : ↑unitInterval) (huv : u ≤ v) (hv : unitInterval.symm (centralMargin α) ≤ v) : (centeredOrdinal C α).cdf ![u, v] = ↑u

theorem Verification.centralEmbed_surjectiveOn (α u : ↑unitInterval) (hu : centralMargin α ≤ u) (hv : u ≤ unitInterval.symm (centralMargin α)) : ∃ (t : ↑unitInterval), centralEmbed α t = u

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

Equations

• Verification.centralW α = Verification.centeredOrdinal ProbabilityTheory.Copula.countermonotonic α

theorem Verification.centralW_exchangeable (α : ↑unitInterval) : (centralW α).IsExchangeable

theorem Verification.centralW_xi (α : ↑unitInterval) : (centralW α).chatterjeeXi = 1

theorem Verification.centralW_beta (α : ↑unitInterval) : (centralW α).blomqvistBeta = 1 - 2 * ↑α

theorem Verification.centralW_cdf_inside (α u v : ↑unitInterval) (hu : centralMargin α ≤ u) (hu' : u ≤ unitInterval.symm (centralMargin α)) (hv : centralMargin α ≤ v) (hv' : v ≤ unitInterval.symm (centralMargin α)) : (centralW α).cdf ![u, v] = ↑(centralMargin α) + max 0 (↑u + ↑v - 1)

theorem Verification.centralW_cdf_ordered (α u v : ↑unitInterval) (huv : u ≤ v) : (centralW α).cdf ![u, v] = if u ≤ centralMargin α ∨ unitInterval.symm (centralMargin α) ≤ v then ↑u else ↑(centralMargin α) + max 0 (↑u + ↑v - 1)

A pointwise formula covering the central square and both outer identity strips.

theorem Verification.centralW_radiallySymmetric (α : ↑unitInterval) : (centralW α).IsRadiallySymmetric

theorem Verification.centralW_pqd (α : ↑unitInterval) (hα : ↑α ≤ 1 / 2) : (centralW α).IsPQD