Grid constructions, shuffles and Bernstein copulas¶
Import Copula.Checkerboard, Copula.Shuffle, Copula.Bernstein, or the
umbrella Copula. All constructors below return actual measure-based
Copula 2 values. Their uniform marginals and nonnegative rectangle
increments are proved, with no extra copula-validity assumption on callers.
Coverage¶
| Construction | Formalized scope and guarantees |
|---|---|
| Ordinal sums | Existing binary API, arbitrary finite partitions, countably many adjacent blocks exhausting [0,1], and general families of disjoint intervals with M on the gaps; see ordinal sums |
| Ordinal sums of Π | ordinalSumPi and countableOrdinalSumPi, with explicit CDF formulas |
| Shuffles of min | Arbitrary finite positive strip widths, a length-matching permutation, and an independent reflection choice for each segment |
| Weight shuffles and shuffle density | Straight shuffles from weight vectors with zero entries; grid shuffles interpolating any copula; density of shuffles of M in the uniform metric |
| Checkerboard | Rectangular, nonuniform grids; arbitrary nonnegative cell probabilities with the specified row and column sums |
| Check-min | Same grids and matrices, using comonotonic local coordinates |
| Bernstein | Arbitrary positive degrees in each coordinate, the tensor polynomial formula, copula validity, independence preservation and uniform convergence |
These are bivariate constructions. Closed-form rank-coefficient formulas for these new families and higher-dimensional grid and Bernstein constructors are not asserted here. The binary ordinal-sum rank results remain available in their existing modules.
Partitions and cell probabilities¶
IntervalPartition n contains n+1 strictly increasing knots, beginning
at zero and ending at one. Its width i is positive. Its clipped local
coordinate is
IntervalPartition.uniform n hn constructs equal-width cells from
hn : 0 < n. The endpoint requirements rule out an empty partition;
zero-width cells are excluded rather than silently divided by zero.
CellMass P Q stores an m × n matrix of probabilities, with
nonnegative entries, row sums P.width i and column sums Q.width j.
On a uniform grid these sums are 1/m and 1/n, respectively. Zero
entries are allowed. CellMass.product P Q is the product of the width
vectors. Its checkerboard is exactly independence.
C.cellMass P Q constructs the matrix directly from the rectangle
increments of any copula C. Matrix admissibility, including both
marginal identities, is proved by two-increasingness and telescoping.
Local copulas and exact interpolation¶
Given A : CellMass P Q and local copulas D i j, A.patchwork D has CDF
The specializations are:
A.checkerboard: eachD_ij = Π, so the local factor is a product.A.checkMin: eachD_ij = M, so the local factor is a minimum.A.checkW: eachD_ij = W, so the local factor ismax(s+t-1,0).
The same formulas cover cell boundaries and the outer boundary.
CellMass.cellMass_patchwork proves that sampling the result recovers
exactly A.mass i j, independently of the local copulas.
CellMass.checkerboard_le_checkMin gives their pointwise comparison.
For a source copula, C.checkerboard P Q and C.checkMin P Q first
sample its cell probabilities. cdf_cellMass_patchwork_point proves
that every local filling agrees with C at every grid vertex.
The convenient specializations are cdf_checkerboard_point and
cdf_checkMin_point.
abs_cdf_cellMass_patchwork_sub_le_mesh bounds the CDF error everywhere
by dx + dy when the row and column widths are at most dx and dy.
In particular, abs_cdf_checkerboard_uniform_sub_le and
abs_cdf_checkMin_uniform_sub_le bound the error by 1/m + 1/n.
The bound holds for singular source copulas as well.
tendstoUniformly_checkerboard and tendstoUniformly_checkMin prove
uniform convergence along refining uniform grids, as a consequence of the
general tendstoUniformly_cellMass_patchwork theorem.
Shuffles of min¶
shuffleOfMin P Q perm hwidth flipped uses one segment in each strip
pair (i, perm i). hwidth states that matched strips have the same
length; each segment has that length as probability mass. flipped i
selects decreasing (true) or increasing (false) orientation.
cdf_shuffleOfMin gives the weighted sum of the corresponding local
W or M CDFs. uniformShuffleOfMin n hn perm is the convenient
straight equal-width case. shuffleOfMin_refl identifies the straight
identity shuffle with M.
Shuffle density¶
Shuffle.Weights describes a straight shuffle by a weight vector
w : Fin M → ℝ (nonnegative, summing to one, zero entries allowed) listing
the source intervals from left to right, and a permutation π giving the
target order. Piece k is the diagonal of
[s_k, s_k + w_k] × [t_k, t_k + w_k] with s_k = Σ_{j<k} w_j and
t_k = Σ_{π j < π k} w_j. weightShuffle w hw0 hw1 π discards the zero
pieces, enumerates the positive ones in increasing order and is by
definition a shuffleOfMin. cdf_weightShuffle gives
IsShuffleOfMin and IsStraightShuffleOfMin name the classes of shuffles
of M (with and without reflected segments).
Shuffle.Density proves Nelsen's Theorem 3.2.2 (Mikusiński, Sherwood and
Taylor). For a partition P and a matrix of cell masses A : CellMass P P,
A.shuffle splits the vertical strip i into pieces of lengths
A.mass i 0, A.mass i 1, … and the horizontal strip j into pieces of
lengths A.mass 0 j, A.mass 1 j, …, and matches piece (i,j) of both.
For C.gridShuffle P = (C.cellMass P P).shuffle this gives exact agreement
with C at every grid vertex:
abs_cdf_sub_le_of_eq_on_grid turns grid agreement into the error bound
dx + dy, so uniformCDFDistance_gridShuffle_le gives d∞ ≤ 2/n on the
uniform n-grid. Consequently tendstoUniformly_gridShuffle,
exists_isStraightShuffleOfMin_uniformCDFDistance_lt and the density
statements for the metric uniformMetricSpace 2 hold:
dense_isShuffleOfMin is the same statement for all shuffles of M.
Bernstein copulas¶
For positive m,n, C.bernstein m n hm hn has the CDF
bernsteinCDF_eq_sum connects the constructor to mathlib's Bernstein
basis. The proof of isClassical_bernsteinCDF uses the derivative
identity for Bernstein combinations to establish monotonicity from
ordered coefficients, then applies it to copula rectangle increments.
Degree zero is deliberately excluded from the copula constructor.
bernstein_independence proves that smoothing Π returns Π.
bernstein_one_one proves that degree (1,1) returns Π for every source.
The public examples also check the nontrivial value B_{2,2}(M)(1/2,1/2)=5/16.
abs_bernsteinCDF_sub_le bounds the error at (u,v) by
sqrt(u(1-u)/m) + sqrt(v(1-v)/n). Its uniform specialization bounds it by
sqrt(1/(4m)) + sqrt(1/(4n)). Finally, tendstoUniformly_bernstein proves
uniform convergence along degrees (k+1,k+1).
Modules¶
| Module | Content |
|---|---|
Patchwork.Basic |
General finite validity and monotonicity under local CDF order |
Patchwork.Partition |
Nonuniform partitions, clipping and telescoping |
Patchwork.Grid |
Cell matrices, sampling, local fillings and named families |
Patchwork.Approximation |
Grid interpolation, cell recovery and uniform error bounds |
OrdinalSum.Finite |
Finite sums, Π specialization and binary compatibility |
OrdinalSum.Countable |
Increasing countable partitions, summability and CDF series |
Shuffle |
Unequal-width signed shuffles and straight uniform shuffles |
Shuffle.Weights |
Shuffle classes, weight vectors with zero entries and their CDF formula |
Shuffle.Density |
Grid shuffles, exact grid interpolation, 2/n error bound and density (Nelsen Thm 3.2.2) |
Bernstein.Basis |
Bernstein derivative and shape-preservation lemmas |
Bernstein.Basic |
Tensor formula, validity and benchmark identities |
Bernstein.Approximation |
Error bounds and uniform convergence |
For the conventional family definitions and terminology, see Rockel, Measures of association for approximating copulas, §2 and Cottin–Pfeifer, From Bernstein polynomials to Bernstein copulas.
Library revision: fe53ea2f · Lean 4.34.0