← Mathematical handbook

Negative-parameter bivariate Frank copulas

The negative branch is defined as the second-coordinate reflection of the positive branch with opposite parameter. This gives an exact copula and a closed-square CDF without applying logarithms to grounded zero coordinates.

noncomputable def ProbabilityTheory.Copula.frankNegative (θ : ℝ) (hθ : θ < 0) : Copula 2

The negative-parameter bivariate Frank copula.

Equations

• ProbabilityTheory.Copula.frankNegative θ hθ = (ProbabilityTheory.Copula.frank (-θ) ⋯).reflect {1}

theorem ProbabilityTheory.Copula.frankNegative_cdf_full (θ : ℝ) (hθ : θ < 0) (u v : ↑unitInterval) : (frankNegative θ hθ).cdf ![u, v] = ↑u - if u = 0 ∨ unitInterval.symm v = 0 then 0 else -Real.log (1 - (1 - Real.exp (θ * ↑u)) * (1 - Real.exp (θ * ↑(unitInterval.symm v))) / (1 - Real.exp θ)) / -θ

An exact closed-square CDF for the negative Frank branch. It uses the positive Frank logarithm at the reflected second coordinate, including all boundary cases.

theorem ProbabilityTheory.Copula.frankNegative_cdf_source (θ : ℝ) (hθ : θ < 0) (u v : ↑unitInterval) : (frankNegative θ hθ).cdf ![u, v] = -Real.log (1 + (Real.exp (-θ * ↑u) - 1) * (Real.exp (-θ * ↑v) - 1) / (Real.exp (-θ) - 1)) / θ

Table 1's Frank logarithmic CDF for every negative parameter, with all boundary values.