← Mathematical handbook

noncomputable def Verification.diagonalHoleLower (α β : ℝ) (u : ↑unitInterval) : ℝ

The source's piecewise lower edge, with its natural alpha=1/2 extension.

Equations

• Verification.diagonalHoleLower α β u = if ↑u ≤ α then 0 else if 1 - α ≤ ↑u then 1 - β else (1 - β) / (1 - 2 * α) * (↑u - α)

theorem Verification.diagonalHoleLower_measurable (α β : ℝ) : Measurable (diagonalHoleLower α β)

theorem Verification.diagonalHoleLower_mem (α β : ℝ) (_hα : α ∈ Set.Icc 0 (1 / 2)) (hβ : β ∈ Set.Icc 0 (1 / 2)) (u : ↑unitInterval) : diagonalHoleLower α β u ∈ Set.Icc 0 (1 - β)

noncomputable def Verification.diagonalHoleBand (α β : ℝ) (hα : α ∈ Set.Icc 0 (1 / 2)) (hβ : β ∈ Set.Icc 0 (1 / 2)) : ExclusionBand

Equations

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

noncomputable def Verification.diagonalHoleCopula (α β : ℝ) (hα : α ∈ Set.Icc 0 (1 / 2)) (hβ : β ∈ Set.Icc 0 (1 / 2)) : ProbabilityTheory.Copula 2

Rank standardization of the joint uniform density outside the diagonal hole.

Equations

• Verification.diagonalHoleCopula α β hα hβ = (Verification.diagonalHoleBand α β hα hβ).copula

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

The finite-mu path in Equation (33).

Equations

• Verification.diagonalHoleAlpha μ = if μ ≤ 2 then 3 / 20 * μ else 1 / 2 - 2 / (5 * μ)

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

Equations

• Verification.diagonalHoleBeta μ = 1 / 4 * min μ 2

theorem Verification.diagonalHolePath_mem (μ : ℝ) (hμ : 0 ≤ μ) : diagonalHoleAlpha μ ∈ Set.Icc 0 (1 / 2) ∧ diagonalHoleBeta μ ∈ Set.Icc 0 (1 / 2)