← Mathematical handbook

Equation (5): verification of the explicit inverse boundary parameter

noncomputable def Papers.AnsariRockel2026XiRho.smallXiParameter (x : ℝ) : ℝ

Equations

• Papers.AnsariRockel2026XiRho.smallXiParameter x = √(6 * x) / (2 * Real.cos (Real.arccos (-3 * √(6 * x) / 5) / 3))

noncomputable def Papers.AnsariRockel2026XiRho.largeXiParameter (x : ℝ) : ℝ

Equations

• Papers.AnsariRockel2026XiRho.largeXiParameter x = (5 + √(5 * (6 * x - 1))) / (10 * (1 - x))

theorem Papers.AnsariRockel2026XiRho.smallXiParameter_inverse {x : ℝ} (hx : 0 < x) (hx1 : x ≤ 3 / 10) : 0 < smallXiParameter x ∧ smallXiParameter x ≤ 1 ∧ bandXi (smallXiParameter x) = x

The trigonometric cubic inverse lies in (0,1] and has exactly the requested xi.

theorem Papers.AnsariRockel2026XiRho.largeXiParameter_inverse {x : ℝ} (hx : 3 / 10 < x) (hx1 : x < 1) : 1 < largeXiParameter x ∧ bandXi (largeXiParameter x) = x

The radical quadratic inverse lies above 1 and has exactly the requested xi.

noncomputable def Papers.AnsariRockel2026XiRho.boundaryParameter (x : ℝ) : ℝ

Exactly the b_x displayed in equation (5).

Equations

• Papers.AnsariRockel2026XiRho.boundaryParameter x = if x ≤ 3 / 10 then Papers.AnsariRockel2026XiRho.smallXiParameter x else Papers.AnsariRockel2026XiRho.largeXiParameter x

theorem Papers.AnsariRockel2026XiRho.boundaryParameter_inverse {x : ℝ} (hx : 0 < x) (hx1 : x < 1) : 0 < boundaryParameter x ∧ bandXi (boundaryParameter x) = x