Documentation

Papers.Rockel2025Approximation.DyadicBlocks

← Mathematical handbook

Proposition 3.3 on diagonal dyadic grids #

At depth n there are 2^n equal diagonal cells, each of mass 1/2^n. Choosing independence, M, or W inside each cell gives the checkerboard, check-min, or check-w copula for that grid. General matrices and xi formulas are not claimed here.

source
noncomputable def Papers.Rockel2025Approximation.dyadicBlocks :
ℕ → ProbabilityTheory.Copula 2 → ProbabilityTheory.Copula 2

Fill each diagonal cell of a dyadic grid with a rescaled copy of C.

Equations
Instances For
    source
    theorem Papers.Rockel2025Approximation.dyadicBlocks_cdf (n : ℕ) (C : ProbabilityTheory.Copula 2) (u v : ↑unitInterval) :
    (dyadicBlocks (n + 1) C).cdf ![u, v] = 1 / 2 * (dyadicBlocks n C).cdf ![ProbabilityTheory.Copula.OrdinalSum.lowerCoord ProbabilityTheory.Copula.unitHalf u, ProbabilityTheory.Copula.OrdinalSum.lowerCoord ProbabilityTheory.Copula.unitHalf v] + 1 / 2 * (dyadicBlocks n C).cdf ![ProbabilityTheory.Copula.OrdinalSum.upperCoord ProbabilityTheory.Copula.unitHalf u, ProbabilityTheory.Copula.OrdinalSum.upperCoord ProbabilityTheory.Copula.unitHalf v]

    Exact recursive CDF, including the edges and the midpoint.

    source
    theorem Papers.Rockel2025Approximation.dyadicBlocks_rho (n : ℕ) (C : ProbabilityTheory.Copula 2) :
    (dyadicBlocks n C).spearmanRho = 1 - (1 / 4) ^ n * (1 - C.spearmanRho)
    source
    theorem Papers.Rockel2025Approximation.dyadicBlocks_tau (n : ℕ) (C : ProbabilityTheory.Copula 2) :
    (dyadicBlocks n C).kendallTau = 1 - (1 / 2) ^ n * (1 - C.kendallTau)
    source
    theorem Papers.Rockel2025Approximation.checkerboard_rho_tau (n : ℕ) :
    (dyadicBlocks n (ProbabilityTheory.Copula.independence 2)).spearmanRho = 1 - (1 / 4) ^ n ∧ (dyadicBlocks n (ProbabilityTheory.Copula.independence 2)).kendallTau = 1 - (1 / 2) ^ n

    Proposition 3.3(i)-(ii), restricted to diagonal dyadic checkerboards.

    source
    theorem Papers.Rockel2025Approximation.checkMin_corrections (n : ℕ) :
    (dyadicBlocks n (ProbabilityTheory.Copula.comonotonic 2)).spearmanRho = (dyadicBlocks n (ProbabilityTheory.Copula.independence 2)).spearmanRho + (1 / 4) ^ n ∧ (dyadicBlocks n (ProbabilityTheory.Copula.comonotonic 2)).kendallTau = (dyadicBlocks n (ProbabilityTheory.Copula.independence 2)).kendallTau + (1 / 2) ^ n

    The check-min corrections are 1/N^2 for rho and 1/N for tau, N=2^n.

    source
    theorem Papers.Rockel2025Approximation.checkW_corrections (n : ℕ) :
    (dyadicBlocks n ProbabilityTheory.Copula.countermonotonic).spearmanRho = (dyadicBlocks n (ProbabilityTheory.Copula.independence 2)).spearmanRho - (1 / 4) ^ n ∧ (dyadicBlocks n ProbabilityTheory.Copula.countermonotonic).kendallTau = (dyadicBlocks n (ProbabilityTheory.Copula.independence 2)).kendallTau - (1 / 2) ^ n

    The check-w corrections have the opposite signs on these same grids.