← Copula mathematical handbook

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

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.smallXiParameter (x : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.smallXiParameter x = √(6 * x) / (2 * Real.cos (Real.arccos (-3 * √(6 * x) / 5) / 3))

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.largeXiParameter (x : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.largeXiParameter x = (5 + √(5 * (6 * x - 1))) / (10 * (1 - x))

theorem ProbabilityTheory.Copula.RankRegion.XiRho.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 ProbabilityTheory.Copula.RankRegion.XiRho.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 ProbabilityTheory.Copula.RankRegion.XiRho.boundaryParameter (x : ℝ) : ℝ

Exactly the b_x displayed in equation (5).

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.boundaryParameter_inverse {x : ℝ} (hx : 0 < x) (hx1 : x < 1) : 0 < boundaryParameter x ∧ bandXi (boundaryParameter x) = x