← Copula mathematical handbook

Theorem 1: the full explicit xi--rho region and unique interior boundary copulas

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.upperRhoAtXi (x : ℝ) : ℝ

Exactly M_x in equation (5), with the displayed trigonometric/radical inverse.

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.boundaryCopula (x : ℝ) (hx : 0 < x) (hx1 : x < 1) : Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.boundaryCopula x hx hx1 = ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand (ProbabilityTheory.Copula.RankRegion.XiRho.boundaryParameter x) ⋯

theorem ProbabilityTheory.Copula.RankRegion.XiRho.boundaryCopula_coefficients {x : ℝ} (hx : 0 < x) (hx1 : x < 1) : (boundaryCopula x hx hx1).chatterjeeXi = x ∧ (boundaryCopula x hx hx1).spearmanRho = upperRhoAtXi x

The original source family attains every interior positive boundary point.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sharp_absolute_rho_bound (C : Copula 2) : |C.spearmanRho| ≤ upperRhoAtXi C.chatterjeeXi

Theorem 1: the sharp two-sided bound for every bivariate copula.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.exact_region (x y : ℝ) : (∃ (C : Copula 2), C.chatterjeeXi = x ∧ C.spearmanRho = y) ↔ x ∈ Set.Icc 0 1 ∧ |y| ≤ upperRhoAtXi x

Equations (4)--(5): necessary and sufficient conditions for the full exact region.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.upper_boundary_unique (C : Copula 2) {x : ℝ} (hx : 0 < x) (hx1 : x < 1) (hC : C.chatterjeeXi = x) : C.spearmanRho = upperRhoAtXi x ↔ C = boundaryCopula x hx hx1

The positive boundary identifies the actual copula uniquely at every interior xi.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.lower_boundary_unique (C : Copula 2) {x : ℝ} (hx : 0 < x) (hx1 : x < 1) (hC : C.chatterjeeXi = x) : C.spearmanRho = -upperRhoAtXi x ↔ C = (boundaryCopula x hx hx1).reflect {1}

The reflected source copula is the unique negative-boundary optimizer.