The two-parameter family in Section 3.2 #
The displayed density is identified with an actual copula law. The proof uses probability-integral transforms and almost-everywhere quantile inversion, so zero marginal densities and the closed-square parameter endpoints are covered.
noncomputable def
Papers.Rockel2026XiFootrule.twoParameter
(α β : ℝ)
(hα : α ∈ Set.Icc 0 (1 / 2))
(hβ : β ∈ Set.Icc 0 (1 / 2))
:
Equations
- Papers.Rockel2026XiFootrule.twoParameter α β hα hβ = Verification.diagonalHoleCopula α β hα hβ
Instances For
theorem
Papers.Rockel2026XiFootrule.twoParameter_raw_marginals
(α β : ℝ)
(hα : α ∈ Set.Icc 0 (1 / 2))
(hβ : β ∈ Set.Icc 0 (1 / 2))
:
have B := Verification.diagonalHoleBand α β hα hβ;
MeasureTheory.Measure.map Prod.fst B.measure = MeasureTheory.volume ∧ MeasureTheory.Measure.map Prod.snd B.measure = MeasureTheory.volume.withDensity fun (t : ↑unitInterval) => ENNReal.ofReal (B.columnDensity t)
The pre-standardization law has the claimed two marginal distributions.
theorem
Papers.Rockel2026XiFootrule.twoParameter_marginal_density
(α β : ℝ)
(hα : α ∈ Set.Icc 0 (1 / 2))
(hβ : β ∈ Set.Icc 0 (1 / 2))
(t : ↑unitInterval)
:
have B := Verification.diagonalHoleBand α β hα hβ;
B.columnDensity t = (1 - B.holeLength t) / (1 - β)
Equation (31) evaluates the actual second marginal, rather than a candidate normalization.
theorem
Papers.Rockel2026XiFootrule.twoParameter_density
(α β : ℝ)
(hα : α ∈ Set.Icc 0 (1 / 2))
(hβ : β ∈ Set.Icc 0 (1 / 2))
:
have B := Verification.diagonalHoleBand α β hα hβ;
(twoParameter α β hα hβ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) =>
ENNReal.ofReal
(if B.lower (x 0) ≤ ↑(ProbabilityTheory.unitQuantile B.marginal (x 1)) ∧ ↑(ProbabilityTheory.unitQuantile B.marginal (x 1)) ≤ B.lower (x 0) + β then
0
else 1 / ((1 - β) * B.columnDensity (ProbabilityTheory.unitQuantile B.marginal (x 1))))
Proposition 3.5 and Equation (32), including both parameter endpoints.
A zero-width hole gives independence along the entire bottom parameter edge.
The upper corner is the same actual checkerboard as in Theorem 3.4.
theorem
Papers.Rockel2026XiFootrule.twoParameter_corner_coefficients :
(twoParameter (1 / 2) (1 / 2) ⋯ ⋯).chatterjeeXi = 1 / 2 ∧ (twoParameter (1 / 2) (1 / 2) ⋯ ⋯).spearmanFootrule = -1 / 2
The corner's exact rank values; no numerical evaluation.
theorem
Papers.Rockel2026XiFootrule.twoParameter_path_admissible
(μ : ℝ)
(hμ : 0 ≤ μ)
:
Verification.diagonalHoleAlpha μ ∈ Set.Icc 0 (1 / 2) ∧ Verification.diagonalHoleBeta μ ∈ Set.Icc 0 (1 / 2)
Equation (33) stays inside the proved closed parameter square for every finite mu.