← Mathematical handbook

Proposition 3.1 and the admissible parameter in Theorem 3.3

The cubic inverse is unique on [0,2] for target footrule in [-1/2,0]. Uniqueness among all real roots would be false, as checked below.

theorem Papers.Rockel2026XiFootrule.relaxed_coefficients_closed (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : have r := 2 / (2 + μ); Verification.relaxedFootrule μ = -2 * r ^ 2 + 6 * r - 5 + 1 / r ∧ Verification.relaxedXi μ = -4 * r ^ 2 + 20 * r - 17 + 2 / r - 1 / r ^ 2 - 12 * Real.log r

Proposition 3.1, evaluated from the source's exact integral definitions.

theorem Papers.Rockel2026XiFootrule.relaxed_coefficients_continuous : ContinuousOn Verification.relaxedFootrule (Set.Icc 0 2) ∧ ContinuousOn Verification.relaxedXi (Set.Icc 0 2)

theorem Papers.Rockel2026XiFootrule.relaxed_coefficients_strict_monotonicity : StrictAntiOn Verification.relaxedFootrule (Set.Icc 0 2) ∧ StrictMonoOn Verification.relaxedXi (Set.Icc 0 2)

theorem Papers.Rockel2026XiFootrule.relaxed_coefficients_endpoints : Verification.relaxedFootrule 0 = 0 ∧ Verification.relaxedFootrule 2 = -1 / 2 ∧ Verification.relaxedXi 0 = 0 ∧ Verification.relaxedXi 2 = 12 * Real.log 2 - 8

theorem Papers.Rockel2026XiFootrule.footrule_inverse_unique (y : ℝ) (hy : y ∈ Set.Icc (-1 / 2) 0) : ∃! μ : ℝ, μ ∈ Set.Icc 0 2 ∧ Verification.relaxedFootrule μ = y

Every nonpositive target footrule has exactly one admissible parameter.

theorem Papers.Rockel2026XiFootrule.footrule_cubic_equivalence (y μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : Verification.relaxedFootrule μ = y ↔ μ ^ 3 - (4 + 2 * y) * μ ^ 2 - (4 + 8 * y) * μ - 8 * y = 0

theorem Papers.Rockel2026XiFootrule.footrule_cubic_unique_admissible (y : ℝ) (hy : y ∈ Set.Icc (-1 / 2) 0) : ∃! μ : ℝ, μ ∈ Set.Icc 0 2 ∧ μ ^ 3 - (4 + 2 * y) * μ ^ 2 - (4 + 8 * y) * μ - 8 * y = 0

theorem Papers.Rockel2026XiFootrule.footrule_cubic_not_unique_real : Verification.footruleCubic (-1 / 2) 2 = 0 ∧ Verification.footruleCubic (-1 / 2) (-1) = 0 ∧ 2 ≠ -1

The source's phrase "unique real solution" needs the admissible interval restriction.

theorem Papers.Rockel2026XiFootrule.weighted_lower_bound_closed (C : ProbabilityTheory.Copula 2) (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : μ * Verification.footruleClosed (Verification.relaxedParameter μ) + Verification.xiClosed (Verification.relaxedParameter μ) ≤ μ * C.spearmanFootrule + C.chatterjeeXi

Theorem 3.2 with explicitly evaluated coefficients.

theorem Papers.Rockel2026XiFootrule.negative_footrule_lower_bound (C : ProbabilityTheory.Copula 2) (hy : C.spearmanFootrule ∈ Set.Icc (-1 / 2) 0) : ∃! μ : ℝ, μ ∈ Set.Icc 0 2 ∧ Verification.footruleCubic C.spearmanFootrule μ = 0 ∧ Verification.xiClosed (Verification.relaxedParameter μ) ≤ C.chatterjeeXi

Theorem 3.3's lower estimate at every nonpositive attainable footrule value.