← Mathematical handbook

Exact evaluation of the relaxed xi-footrule coefficients

noncomputable def Verification.relaxedParameter (μ : ℝ) : ℝ

Equations

• Verification.relaxedParameter μ = 2 / (2 + μ)

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

Equations

• Verification.footruleClosed r = -2 * r ^ 2 + 6 * r - 5 + 1 / r

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

Equations

• Verification.xiClosed r = -4 * r ^ 2 + 20 * r - 17 + 2 / r - 1 / r ^ 2 - 12 * Real.log r

theorem Verification.relaxedParameter_mem (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : relaxedParameter μ ∈ Set.Icc (1 / 2) 1

theorem Verification.relaxedParameter_inverse (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : μ = 2 / relaxedParameter μ - 2

theorem Verification.relaxedFootrule_closed (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : relaxedFootrule μ = footruleClosed (relaxedParameter μ)

Proposition 3.1: exact footrule evaluation, including both parameter endpoints.

theorem Verification.relaxedXi_closed (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) : relaxedXi μ = xiClosed (relaxedParameter μ)

Proposition 3.1: exact xi evaluation, with the logarithmic term.