Measures of association for approximating copulas

Verification map

Status: complete for scope. Propositions 3.1-3.3, Corollary 3.4, Lemma 4.1 and Theorem 4.2 are checked. Theorem 4.5 almost-sure consistency is checked for iid real observations with continuous marginal CDFs and 0<kappa<=1/3, using their actual ranks and the exact fractional binning matrix. The O(N log N) bound is checked for the specified unit-cost sparse-update and matrix-arithmetic schedule. Examples 4.3-4.4 and the intervening permutation counterexample are checked, including the dependence properties, actual coarse matrices and exact xi values. Numerical experiments and externally cited estimator results are outside this formal scope.

Source and conventions

Source: arXiv:2505.08045v2, 22 May 2026.

The recursive construction has N=2^n equal diagonal cells, each with mass 1/N, and zero off-diagonal masses. The CDF recurrence uses clipped rescaling and holds on cell boundaries as well. Independence in each cell gives the checkerboard, M gives check-min, and W gives check-w. Thus the source matrix is Delta=I_N/N, 1/N^2=(1/4)^n, and tr(Delta^T Delta)=1/N=(1/2)^n. The proofs below include n=0 (one cell). The newer equalGrid construction covers every N=n+1 and also checks xi for the deterministic variants and tails for all three families. RectangularRanks and RectangularXi remove the diagonal restriction for all three rank coefficients and the xi error bound. RectangularTails also checks every general-matrix tail formula.

The original dyadic declarations remain available. The equalGrid index n represents N=n+1 cells: recursively split off width 1/N and rescale the remaining N-1 equal cells. All formulas below state their diagonal-matrix restriction explicitly.

For Proposition 3.2, permutationShuffle n pi has N=n+1 equal-width increasing segments, one in each row and column prescribed by pi. The finite-sum CDF identifies the constructed copula on the entire closed square. Indices are zero-based; the source conditions pi(1)=1 and pi(N)=N become pi(0)=0 and pi(Fin.last n)=Fin.last n. The inversion count counts j<i with pi(j)>pi(i), equivalent to the source after renaming the pair. No symmetry or involution assumption is used. Functional dependence is proved with a measurable graph map, and both tail statements establish existence as well as the limit value.

Result map

Proofs are in DyadicBlocks.lean, EqualGrids.lean, BernsteinRho.lean, BernsteinRank.lean, BernsteinKendall.lean, BernsteinExact.lean, RectangularRanks.lean, RectangularXi.lean, RectangularTails.lean, ConvergenceSteps.lean, StatisticalConsistency.lean, Counterexamples.lean, and PermutationShuffles.lean, imported by Main.lean. Axioms.lean prints and enforces the standard transitive axiom allowlist for every declaration below.

| Proposition 3.3(i): rectangular checkerboard rho | Papers.Rockel2025Approximation.rectangular_checkerboard_rho | verified | Exact Omega-weighted source formula for every positive m,n and every admissible cell matrix; no diagonal or symmetry restriction. | | Proposition 3.3(i): check-min/check-W rho | Papers.Rockel2025Approximation.rectangular_checkMin_rho; Papers.Rockel2025Approximation.rectangular_checkW_rho | verified | Corrections +1/(mn) and -1/(mn), on every admissible uniform rectangular grid. | | Proposition 3.3(ii): rectangular checkerboard tau | Papers.Rockel2025Approximation.rectangular_checkerboard_tau | verified | Exact 1-tr(Xi_m Delta Xi_n Delta^T), with Xi entries 2 below the diagonal, 1 on it and 0 above. Also valid on nonuniform partitions. | | Proposition 3.3(ii): check-min/check-W tau | Papers.Rockel2025Approximation.rectangular_checkMin_tau; Papers.Rockel2025Approximation.rectangular_checkW_tau | verified | Corrections +/-tr(Delta^T Delta), including nonuniform partitions. | | Supporting general patchwork rank identities | Papers.Rockel2025Approximation.patchwork_rho_correction; Papers.Rockel2025Approximation.patchwork_tau_correction | verified | Independent arbitrary local copulas in every cell, including singular laws. Rho correction is sum of mass times both cell widths times local rho; tau correction is sum of squared mass times local tau. Actual patchwork measure is proved equal to the weighted affine local laws. |

| Proposition 3.3(iii): actual conditional CDF | Papers.Rockel2025Approximation.patchwork_conditionalCDF | verified | The cellwise normalized kernel is the actual conditional CDF almost everywhere, with arbitrary local copulas and positive nonuniform partitions. Prefix integrals recover the actual patchwork CDF. | | Proposition 3.3(iii): general finite xi formula | Papers.Rockel2025Approximation.patchwork_xi_formula; Papers.Rockel2025Approximation.patchwork_xi_correction | verified | Exact finite formula and checkerboard correction sum(width_j/width_i * mass_ij^2 * xi(C_ij)); singular and different local copulas are allowed. | | Proposition 3.3(iii): checkerboard xi trace | Papers.Rockel2025Approximation.rectangular_checkerboard_xi | verified | Exactly (6m/n) tr(Delta^T Delta M_xi)-2 with M_xi=T T^T+T^T+I/3 and T strictly upper triangular; every admissible positive rectangular grid. | | Proposition 3.3(iii): local perfect-dependence correction | Papers.Rockel2025Approximation.uniform_patchwork_xi_correction; Papers.Rockel2025Approximation.rectangular_perfect_xi | verified | Correction (m/n) tr(Delta^T Delta) when every local xi is one. The local copulas may differ across cells. Also proves the general local-xi weighted formula. | | Proposition 3.3(iii): check-min/check-W xi | Papers.Rockel2025Approximation.rectangular_checkMin_xi; Papers.Rockel2025Approximation.rectangular_checkW_xi | verified | Both corrections equal (m/n) tr(Delta^T Delta), without diagonal or symmetry restrictions. | | Corollary 3.4: rectangular xi error bound | Papers.Rockel2025Approximation.rectangular_xi_error_bound | verified | Absolute error at most m/n^2 for m<=n and 1/n otherwise; proved for every local copula filling, hence in particular every local perfect-dependence filling. |

| Proposition 3.3: both rectangular checkerboard tails | Papers.Rockel2025Approximation.rectangular_checkerboard_lower_tail; Papers.Rockel2025Approximation.rectangular_checkerboard_upper_tail | verified | Both limits exist and equal zero, for every positive rectangular grid and every admissible cell matrix. | | Proposition 3.3: both rectangular check-min tails | Papers.Rockel2025Approximation.rectangular_checkMin_lower_tail; Papers.Rockel2025Approximation.rectangular_checkMin_upper_tail | verified | Both limits exist; coefficients are respectively the first and last corner masses times min(m,n). Lean natural indices encode all positive dimensions as m+1,n+1. | | Proposition 3.3: both rectangular check-W tails | Papers.Rockel2025Approximation.rectangular_checkW_lower_tail; Papers.Rockel2025Approximation.rectangular_checkW_upper_tail | verified | Both limits exist and equal zero for every admissible rectangular matrix, with no diagonal or symmetry restriction. |

| Lemma 4.1: quadratic instance used in Theorem 4.2 | Papers.Rockel2025Approximation.majorization_sum_sq | verified | Finite decreasing comparison vector, dominance of all partial sums and equal total sums imply the square-sum inequality, by summation by parts. This row does not claim Karamata for arbitrary convex functions. | | Equation (30): estimator as average and range | Papers.Rockel2025Approximation.checkerboardEstimator_eq_average; Papers.Rockel2025Approximation.checkerboardEstimator_mem | verified | The exact square-matrix estimator equals the mean of actual checkerboard and check-min xi values, and lies in [0,1], for every positive order. | | Theorem 4.5 proof step: deterministic correction bound | Papers.Rockel2025Approximation.checkerboardEstimator_correction_bounds | verified | Estimator minus checkerboard xi lies between zero and 1/(2K), for every admissible K-by-K matrix. | | Theorem 4.5 proof step: vanishing correction | Papers.Rockel2025Approximation.checkerboardEstimator_correction_tendsto; Papers.Rockel2025Approximation.checkerboardEstimator_tendsto_iff | verified | For any sequence of admissible matrices with order tending to infinity, the correction tends to zero, and estimator convergence is equivalent to checkerboard-xi convergence. This deterministic transfer theorem is used by the statistical consistency proof below. |

| Theorem 4.2: MTP2 checkerboard xi bound | Papers.Rockel2025Approximation.checkerboard_xi_le_of_mtp2 | verified | Every positive rectangular grid, the actual cell masses of the source copula, and its MTP2 density. Establishes xi(checkerboard)<=xi(C) without assuming conditional increase or the integral inequality. | | Theorem 4.2: stronger CI comparison | Papers.Rockel2025Approximation.checkerboard_xi_le_of_isCI | verified | All conditionally increasing copulas, including singular laws, with uniform predictor bins and arbitrary response partitions. Uses row-average Jensen, finite majorization and the actual checkerboard conditional CDF. | | Theorem 4.2: density-to-order implication | Papers.Rockel2025Approximation.mtp2_isCI | verified | Integration of the MTP2 density over ordered rectangles proves conditional increase in both directions. |

| Theorem 4.5 proof step: population checkerboard convergence | Papers.Rockel2025Approximation.checkerboard_xi_tendsto | verified | Every copula, including singular laws, has xi convergence along its square uniform checkerboards. Proves L1 convergence of predictor-cell averages by continuous approximation, controls response interpolation, and applies dominated convergence. | | Theorem 4.5 proof step: CDF stability | Papers.Rockel2025Approximation.checkerboard_xi_stability | verified | Uniform CDF error epsilon changes checkerboard xi by at most 24mepsilon, for arbitrary predictor and response partitions with m predictor cells. | | Theorem 4.5 proof step: quantitative consistency criterion | Papers.Rockel2025Approximation.checkerboard_xi_tendsto_of_cdf_error; Papers.Rockel2025Approximation.checkerboardEstimator_tendsto_of_cdf_error | verified | If the grid order tends to infinity and order times an eventual uniform CDF error tends to zero, both re-binned xi and the corrected estimator converge. The rank-sample rate is proved separately below. |

| Lemma 4.1: full Karamata inequality | Papers.Rockel2025Approximation.majorization_sum_convex | verified | Every real convex function on the real line, decreasing comparison vector, prefix-sum dominance and equal totals; no differentiability assumption. | | Theorem 4.5: exact fractional rank binning | Papers.Rockel2025Approximation.rankCopula_cellMass | verified | The actual rank-copula cell masses equal N times the sum of products of half-open interval overlaps, for every pair of rank permutations and arbitrary coarse partitions. | | Theorem 4.5: almost-sure rank CDF rate | Papers.Rockel2025Approximation.sampleRankCopula_ae_rate | verified | iid samples from any copula: eventually the uniform CDF error is at most 3 sqrt(8 log(N+1)/N)+8/N almost surely. Proved by concentration, a growing grid, Borel-Cantelli and no-ties rank comparison. | | Theorem 4.5: consistency for copula observations | Papers.Rockel2025Approximation.sampleCheckerboardEstimator_ae_tendsto | verified | Actual rank samples from every copula, including singular laws, and K=floor(N^kappa), 0<kappa<=1/3. The exact Equation (30) estimator converges almost surely to xi. | | Theorem 4.5: consistency for real observations | Papers.Rockel2025Approximation.realSampleCheckerboardEstimator_ae_tendsto | verified | iid real bivariate observations with continuous marginal CDFs, 0<kappa<=1/3. Original sample ranks are preserved by the probability integral transform even when marginal CDFs have flat intervals. No statistical convergence is assumed. | | Theorem 4.5: sparse matrix construction | Papers.Rockel2025Approximation.rankCopula_cellMass_four_slots | verified | For K<=N, each observation contributes to at most four explicitly computed candidate cells; their updates reconstruct the exact fractional rank-binning matrix. | | Theorem 4.5: operation bound | Papers.Rockel2025Approximation.checkerboardEstimatorWork_isBigO | verified | O(N log N) for the defined work schedule: two merge sorts, four candidate updates per observation, three dense K-by-K products, initialization and traces, with K=floor(N^kappa), 0<=kappa<=1/3. Arithmetic, comparisons and indexed updates have unit cost. This is not a bit-complexity or machine-runtime claim. |

The verified subset consists only of the explicitly mapped statements and proof steps. Pending rows are not implied by a successful build. Numerical experiments and plots are not counted as formal proofs.

Latest package integration

The dependency is pinned to copula commit 5926399c46f83d307127fd34b3aa2e416c940786. New proof modules: Constructors.lean. Every mapped declaration is compiled and transitively audited against the standard Lean axiom allowlist. Uniqueness of a numerical boundary value does not imply uniqueness of its copula witness.