← Mathematical handbook

Valid approximation families and deterministic uniform convergence

These constructors allow arbitrary source copulas, including singular laws. Uniform CDF convergence is distinct from the statistical and xi convergence claims of Section 4, which require additional work.

theorem Papers.Rockel2025Approximation.bernstein_cdf (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u v : ↑unitInterval) : (C.bernstein m n hm hn).cdf ![u, v] = ∑ i : Fin (m + 1), ∑ j : Fin (n + 1), C.cdf ![bernstein.z i, bernstein.z j] * (bernstein m ↑i) u * (bernstein n ↑j) v

theorem Papers.Rockel2025Approximation.bernstein_uniform_error (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u v : ↑unitInterval) : |(C.bernstein m n hm hn).cdf ![u, v] - C.cdf ![u, v]| ≤ √(1 / (4 * ↑m)) + √(1 / (4 * ↑n))

theorem Papers.Rockel2025Approximation.bernstein_uniform_convergence (C : ProbabilityTheory.Copula 2) : TendstoUniformly (fun (k : ℕ) => (C.bernstein (k + 1) (k + 1) ⋯ ⋯).cdf) C.cdf Filter.atTop

theorem Papers.Rockel2025Approximation.rectangular_checkerboard_cdf {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (u v : ↑unitInterval) : A.checkerboard.cdf ![u, v] = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * ↑(P.coord i u) * ↑(Q.coord j v)

theorem Papers.Rockel2025Approximation.rectangular_checkMin_cdf {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (u v : ↑unitInterval) : A.checkMin.cdf ![u, v] = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * min ↑(P.coord i u) ↑(Q.coord j v)

theorem Papers.Rockel2025Approximation.rectangular_checkW_cdf {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (u v : ↑unitInterval) : A.checkW.cdf ![u, v] = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * max (↑(P.coord i u) + ↑(Q.coord j v) - 1) 0

theorem Papers.Rockel2025Approximation.patchwork_grid_interpolation (C : ProbabilityTheory.Copula 2) {m n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (D : Fin m → Fin n → ProbabilityTheory.Copula 2) (i : Fin (m + 1)) (j : Fin (n + 1)) : ((C.cellMass P Q).patchwork D).cdf ![P.point i, Q.point j] = C.cdf ![P.point i, Q.point j]

Arbitrary local fillings preserve source values at every grid vertex.

theorem Papers.Rockel2025Approximation.patchwork_uniform_convergence (C : ProbabilityTheory.Copula 2) (D : (k : ℕ) → Fin (k + 1) → Fin (k + 1) → ProbabilityTheory.Copula 2) : TendstoUniformly (fun (k : ℕ) => ((C.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯)).patchwork (D k)).cdf) C.cdf Filter.atTop

Deterministic CDF convergence, simultaneously for checkerboard, check-min and check-W fillings.