← Mathematical handbook

The fixed-beta interpolation step in the proof of Theorem 1

Boundary constructions and the sharp inequality are separate obligations. This module proves that any two available endpoints with the same beta can be joined through every intermediate xi value, including singular endpoints.

theorem ProbabilityTheory.Copula.RankRegion.XiBeta.xi_derivative_formula (C : Copula 2) : C.chatterjeeXi = (6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.cdfSection v) ↑u ^ 2) - 2

theorem ProbabilityTheory.Copula.RankRegion.XiBeta.xi_mixture_continuous (C D : Copula 2) : Continuous fun (a : ↑unitInterval) => (C.mix D a).chatterjeeXi

theorem ProbabilityTheory.Copula.RankRegion.XiBeta.beta_mixture_fixed (C D : Copula 2) {b : ℝ} (hC : C.blomqvistBeta = b) (hD : D.blomqvistBeta = b) (a : ↑unitInterval) : (C.mix D a).blomqvistBeta = b

theorem ProbabilityTheory.Copula.RankRegion.XiBeta.fixed_beta_intermediate (C D : Copula 2) {b x : ℝ} (hC : C.blomqvistBeta = b) (hD : D.blomqvistBeta = b) (hxC : C.chatterjeeXi ≤ x) (hxD : x ≤ D.chatterjeeXi) : ∃ (E : Copula 2), E.blomqvistBeta = b ∧ E.chatterjeeXi = x

Every xi between two copulas' values is attained at their common beta.