← Mathematical handbook

The relaxed lower curve lies strictly inside the absolute square-root bound

noncomputable def Verification.footruleSquareDefect (r : ℝ) : ℝ

Equations

• Verification.footruleSquareDefect r = Verification.xiClosed r - Verification.footruleClosed r ^ 2

theorem Verification.hasDerivAt_footruleSquareDefect (r : ℝ) (hr : r ≠ 0) : HasDerivAt footruleSquareDefect (-4 * (1 - r) ^ 3 * (2 * r - 1) * (-2 * r ^ 2 + 2 * r + 1) / r ^ 3) r

theorem Verification.strictAntiOn_footruleSquareDefect : StrictAntiOn footruleSquareDefect (Set.Icc (1 / 2) 1)

theorem Verification.relaxed_footrule_sq_lt_xi (μ : ℝ) (hμ : μ ∈ Set.Ioc 0 2) : relaxedFootrule μ ^ 2 < relaxedXi μ

theorem Verification.negative_footrule_sq_lt_xi (C : ProbabilityTheory.Copula 2) (hC : C.spearmanFootrule < 0) : C.spearmanFootrule ^ 2 < C.chatterjeeXi

A negative footrule cannot attain the absolute square-root bound.