Documentation

Papers.Rockel2026XiFootrule.SIRegion

← Mathematical handbook

The exact xi-footrule region for stochastically increasing copulas #

A single independence block below a comonotonic block attains the lower boundary. Mixtures with the Frechet upper boundary fill every fixed-footrule interval. All constructions include their endpoints.

noncomputable def Papers.Rockel2026XiFootrule.diagonalBoundary (a : ↑unitInterval) :

ProbabilityTheory.Copula 2

Equations

Papers.Rockel2026XiFootrule.diagonalBoundary a = (ProbabilityTheory.Copula.independence 2).ordinalSum (ProbabilityTheory.Copula.comonotonic 2) a

Instances For

theorem Papers.Rockel2026XiFootrule.diagonalBoundary_cdf (a u v : ↑unitInterval) :

(diagonalBoundary a).cdf ![u, v] = if v ≤ a then ↑v / ↑a * min ↑u ↑a else min ↑u ↑v

noncomputable def Papers.Rockel2026XiFootrule.diagonalConditional (a v u : ↑unitInterval) :

Equations

Papers.Rockel2026XiFootrule.diagonalConditional a v u = if v ≤ a then ↑v / ↑a * Verification.lowerStep a u else Verification.lowerStep v u

Instances For

theorem Papers.Rockel2026XiFootrule.diagonalConditional_primitive (a u v : ↑unitInterval) :

∫ (t : ↑unitInterval) in Set.Iic u, diagonalConditional a v t = (diagonalBoundary a).cdf ![u, v]

theorem Papers.Rockel2026XiFootrule.diagonalBoundary_isSI (a : ↑unitInterval) :

(diagonalBoundary a).IsSI

theorem Papers.Rockel2026XiFootrule.diagonalBoundary_conditionalCDF (a v : ↑unitInterval) :

(fun (u : ↑unitInterval) => (diagonalBoundary a).conditionalCDF u v) =ᵐ[MeasureTheory.volume] diagonalConditional a v

theorem Papers.Rockel2026XiFootrule.diagonalConditional_sq_integral (a v : ↑unitInterval) :

∫ (u : ↑unitInterval), diagonalConditional a v u ^ 2 = (diagonalBoundary a).cdf ![v, v]

theorem Papers.Rockel2026XiFootrule.diagonalBoundary_xi_eq_footrule (a : ↑unitInterval) :

(diagonalBoundary a).chatterjeeXi = (diagonalBoundary a).spearmanFootrule

theorem Papers.Rockel2026XiFootrule.diagonalBoundary_coefficients (a : ↑unitInterval) :

(diagonalBoundary a).chatterjeeXi = 1 - ↑a ^ 2 ∧ (diagonalBoundary a).spearmanFootrule = 1 - ↑a ^ 2

theorem Papers.Rockel2026XiFootrule.si_xi_le_footrule (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) :

C.chatterjeeXi ≤ C.spearmanFootrule

theorem Papers.Rockel2026XiFootrule.upperBoundary_isSI (a : ↑unitInterval) :

(upperBoundary a).IsSI

theorem Papers.Rockel2026XiFootrule.exact_si_xi_footrule_region (x y : ℝ) :

(∃ (C : ProbabilityTheory.Copula 2), C.IsSI ∧ C.chatterjeeXi = x ∧ C.spearmanFootrule = y) ↔ x ∈ Set.Icc 0 1 ∧ y ∈ Set.Icc 0 1 ∧ x ≤ y ∧ y ≤ √x

theorem Papers.Rockel2026XiFootrule.si_xi_le_three_quarters_tau (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) :

C.chatterjeeXi ≤ 3 / 4 * C.kendallTau + 1 / 4