← Mathematical handbook

Lemma 5.1 (iii): the maximal completion maximizes ξ among SI copulas with the same

median section

For a stochastically increasing copula C with median section A, ξ(C) ≤ ξ(Q_A), with equality iff C = Q_A.

theorem Papers.OrendayLaresRockel2026XiBeta.integrable_of_abs_le_one {f : ↑unitInterval → ℝ} (hf : Measurable f) (hb : ∀ (u : ↑unitInterval), |f u| ≤ 1) : MeasureTheory.Integrable f MeasureTheory.volume

theorem Papers.OrendayLaresRockel2026XiBeta.kernel_sq_gap (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (s : MedianSection) (hs : ∀ (u : ↑unitInterval), s.A ↑u = C.cdf ![u, ProbabilityTheory.Copula.unitHalf]) (v : ↑unitInterval) : ∃ (g : ↑unitInterval → ℝ), Antitone g ∧ (∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) ∧ (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] g ∧ ∫ (u : ↑unitInterval), (s.kernelCDF v u - g u) ^ 2 ≤ (∫ (u : ↑unitInterval), s.kernelCDF v u ^ 2) - ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2

For each threshold v: the conditional CDF of C has an antitone version g and ∫ (k - g)² ≤ ∫ k² - ∫ h².

theorem Papers.OrendayLaresRockel2026XiBeta.xi_le_completion (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (s : MedianSection) (hs : ∀ (u : ↑unitInterval), s.A ↑u = C.cdf ![u, ProbabilityTheory.Copula.unitHalf]) : C.chatterjeeXi ≤ s.completion.chatterjeeXi

Lemma 5.1 (iii): ξ(C) ≤ ξ(Q_A), with equality iff C = Q_A.

theorem Papers.OrendayLaresRockel2026XiBeta.eq_completion_of_xi_eq (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) (s : MedianSection) (hs : ∀ (u : ↑unitInterval), s.A ↑u = C.cdf ![u, ProbabilityTheory.Copula.unitHalf]) (hxi : C.chatterjeeXi = s.completion.chatterjeeXi) : C = s.completion