← Copula mathematical handbook

Dependence and symmetry of a central countermonotonic block

theorem ProbabilityTheory.Copula.RankRegion.Common.centralMargin_lt_one (α : ↑unitInterval) : centralMargin α < 1

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

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

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

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

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

Equations

• ProbabilityTheory.Copula.RankRegion.Common.centralW α = ProbabilityTheory.Copula.RankRegion.Common.centeredOrdinal ProbabilityTheory.Copula.countermonotonic α

theorem ProbabilityTheory.Copula.RankRegion.Common.centralW_exchangeable (α : ↑unitInterval) : (centralW α).IsExchangeable

theorem ProbabilityTheory.Copula.RankRegion.Common.centralW_xi (α : ↑unitInterval) : (centralW α).chatterjeeXi = 1

theorem ProbabilityTheory.Copula.RankRegion.Common.centralW_beta (α : ↑unitInterval) : (centralW α).blomqvistBeta = 1 - 2 * ↑α

theorem ProbabilityTheory.Copula.RankRegion.Common.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 ProbabilityTheory.Copula.RankRegion.Common.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 ProbabilityTheory.Copula.RankRegion.Common.centralW_radiallySymmetric (α : ↑unitInterval) : (centralW α).IsRadiallySymmetric

theorem ProbabilityTheory.Copula.RankRegion.Common.centralW_pqd (α : ↑unitInterval) (hα : ↑α ≤ 1 / 2) : (centralW α).IsPQD