← Mathematical handbook

Theorem 3.2: the universal Jensen lower-bound estimate

The source profile is a relaxation and is not declared to be a copula. The rank-like values are defined by exact integrals; their logarithmic closed forms from Proposition 3.1 are evaluated in ClosedCoefficients.

theorem Papers.Rockel2026XiFootrule.jensen_profile_formula (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) : (Verification.jensenLow μ v, Verification.jensenHigh μ v) = if ↑v ≤ μ / (2 + μ) then (0, ↑v / (1 - ↑v)) else if ↑v ≤ 2 / (2 + μ) then (↑v - μ / 2 * (1 - ↑v), ↑v + μ / 2 * ↑v) else (2 - 1 / ↑v, 1)

Equations (18) and (23), with the original cutoff parameters.

theorem Papers.Rockel2026XiFootrule.jensen_profile_feasible (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) : Verification.jensenLow μ v ∈ Set.Icc 0 1 ∧ Verification.jensenHigh μ v ∈ Set.Icc 0 1 ∧ ↑v * Verification.jensenLow μ v + (1 - ↑v) * Verification.jensenHigh μ v = ↑v

theorem Papers.Rockel2026XiFootrule.scalar_optimizer_minimum (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) (a b : ℝ) (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) (hm : ↑v * a + (1 - ↑v) * b = ↑v) : Verification.splitObjective μ (↑v) (Verification.jensenLow μ v) (Verification.jensenHigh μ v) ≤ Verification.splitObjective μ (↑v) a b

Equation (22): the piecewise profile is a global minimizer.

theorem Papers.Rockel2026XiFootrule.scalar_optimizer_unique (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (v : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) (a b : ℝ) (ha : a ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) (hm : ↑v * a + (1 - ↑v) * b = ↑v) : Verification.splitObjective μ (↑v) a b = Verification.splitObjective μ (↑v) (Verification.jensenLow μ v) (Verification.jensenHigh μ v) ↔ a = Verification.jensenLow μ v ∧ b = Verification.jensenHigh μ v

Uniqueness holds at every interior response threshold.

theorem Papers.Rockel2026XiFootrule.conditional_jensen_bound (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) : ↑v * Verification.conditionalBinLow C v ^ 2 + (1 - ↑v) * Verification.conditionalBinHigh C v ^ 2 ≤ ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2

Equation (20) for every copula, with no density assumption.

theorem Papers.Rockel2026XiFootrule.conditional_jensen_equality (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (hv : 0 < ↑v ∧ ↑v < 1) : ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 = ↑v * Verification.conditionalBinLow C v ^ 2 + (1 - ↑v) * Verification.conditionalBinHigh C v ^ 2 ↔ ∀ᵐ (u : ↑unitInterval), C.conditionalCDF u v = if u ≤ v then Verification.conditionalBinLow C v else Verification.conditionalBinHigh C v

noncomputable def Papers.Rockel2026XiFootrule.relaxedKernel (μ : ℝ) (u v : ↑unitInterval) : ℝ

Equation (17): the relaxed two-bin kernel.

Equations

• Papers.Rockel2026XiFootrule.relaxedKernel μ u v = Verification.twoBin v (Verification.jensenLow μ v) (Verification.jensenHigh μ v) u

noncomputable def Papers.Rockel2026XiFootrule.relaxedCDF (μ : ℝ) (u v : ↑unitInterval) : ℝ

The primitive used by the source; this is a real-valued function, not a Copula.

Equations

• Papers.Rockel2026XiFootrule.relaxedCDF μ u v = ∫ (t : ↑unitInterval) in Set.Iic u, Papers.Rockel2026XiFootrule.relaxedKernel μ t v

theorem Papers.Rockel2026XiFootrule.relaxedCDF_formula (μ : ℝ) (u v : ↑unitInterval) : relaxedCDF μ u v = Verification.jensenHigh μ v * ↑u + (Verification.jensenLow μ v - Verification.jensenHigh μ v) * min ↑u ↑v

theorem Papers.Rockel2026XiFootrule.relaxed_values_integral_form (μ : ℝ) : Verification.relaxedFootrule μ = (6 * ∫ (v : ↑unitInterval), relaxedCDF μ v v) - 2 ∧ Verification.relaxedXi μ = (6 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), relaxedKernel μ u v ^ 2) - 2

The extended coefficients use precisely the source's integral normalizations.

theorem Papers.Rockel2026XiFootrule.weighted_lower_bound (C : ProbabilityTheory.Copula 2) (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : μ * Verification.relaxedFootrule μ + Verification.relaxedXi μ ≤ μ * C.spearmanFootrule + C.chatterjeeXi

Theorem 3.2 over the parameter interval specified in Section 3.1.

theorem Papers.Rockel2026XiFootrule.xi_lower_bound_at_relaxed_footrule (C : ProbabilityTheory.Copula 2) (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (hC : C.spearmanFootrule = Verification.relaxedFootrule μ) : Verification.relaxedXi μ ≤ C.chatterjeeXi

The parameterized lower-bound consequence used in Theorem 3.3.

theorem Papers.Rockel2026XiFootrule.relaxed_family_not_copula : ¬∃ (C : ProbabilityTheory.Copula 2), ∀ (u v : ↑unitInterval), C.cdf ![u, v] = relaxedCDF 2 u v

The relaxed family cannot be treated as an attaining copula family: at μ=2 its primitive decreases in the second coordinate.