← Mathematical handbook

The open-band density convention in source equation (23)

noncomputable def Papers.AnsariRockel2026XiRho.sourceBandDensityOpen (b : ℝ) (x : Fin 2 → ↑unitInterval) : ℝ

Exactly the open-band convention in equation (23).

Equations

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

theorem Papers.AnsariRockel2026XiRho.sourceBandDensityOpen_measurable {b : ℝ} (hb : 0 < b) : Measurable (sourceBandDensityOpen b)

theorem Papers.AnsariRockel2026XiRho.sourceBandDensityOpen_ae_eq {b : ℝ} (hb : 0 < b) : sourceBandDensityOpen b =ᵐ[MeasureTheory.volume] sourceBandDensity b

The two versions differ only on a null boundary curve.

theorem Papers.AnsariRockel2026XiRho.sourceBand_toMeasure_densityOpen (b : ℝ) (hb : 0 < b) : (sourceBand b hb).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (sourceBandDensityOpen b x)

The actual copula also has precisely the source's open-band density version.

theorem Papers.AnsariRockel2026XiRho.sourceBandDensityOpen_formula (b : ℝ) (x : Fin 2 → ↑unitInterval) : sourceBandDensityOpen b x = if b * ↑(x 0) < sourceBandIntercept b (x 1) ∧ sourceBandIntercept b (x 1) < b * ↑(x 0) + 1 then if ↑(x 1) ≤ bandCut b then b / √(2 * b * ↑(x 1)) else if ↑(x 1) ≤ 1 - bandCut b then max b 1 else b / √(2 * b * (1 - ↑(x 1))) else 0

Equation (24), expressed using the source's explicit square roots.