← Mathematical handbook

Exact grid interpolation by local-copula patchworks

theorem ProbabilityTheory.Copula.IntervalPartition.coord_point {n : ℕ} (P : IntervalPartition n) (i : Fin n) (k : Fin (n + 1)) : P.coord i (P.point k) = if ↑i < ↑k then 1 else 0

A clipped coordinate at a grid point is an exact step function.

theorem ProbabilityTheory.Copula.IntervalPartition.sum_prefix_differences {n : ℕ} (f : Fin (n + 1) → ℝ) (k : Fin (n + 1)) : (∑ i : Fin n, if ↑i < ↑k then f i.succ - f i.castSucc else 0) = f k - f 0

Telescoping a prefix without introducing a second finite index type.

theorem ProbabilityTheory.Copula.CellMass.cdf_patchwork_point {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (D : Fin m → Fin n → Copula 2) (k : Fin (m + 1)) (l : Fin (n + 1)) : (A.patchwork D).cdf ![P.point k, Q.point l] = ∑ i : Fin m, if ↑i < ↑k then ∑ j : Fin n, if ↑j < ↑l then A.mass i j else 0 else 0

All local choices interpolate the same cumulative cell probabilities.

theorem ProbabilityTheory.Copula.cdf_cellMass_patchwork_point {m n : ℕ} (C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) (D : Fin m → Fin n → Copula 2) (k : Fin (m + 1)) (l : Fin (n + 1)) : ((C.cellMass P Q).patchwork D).cdf ![P.point k, Q.point l] = C.cdf ![P.point k, Q.point l]

A sampled patchwork agrees with the original copula at every grid vertex.

@[simp]

theorem ProbabilityTheory.Copula.cdf_checkerboard_point {m n : ℕ} (C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) (k : Fin (m + 1)) (l : Fin (n + 1)) : (C.checkerboard P Q).cdf ![P.point k, Q.point l] = C.cdf ![P.point k, Q.point l]

@[simp]

theorem ProbabilityTheory.Copula.cdf_checkMin_point {m n : ℕ} (C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) (k : Fin (m + 1)) (l : Fin (n + 1)) : (C.checkMin P Q).cdf ![P.point k, Q.point l] = C.cdf ![P.point k, Q.point l]

theorem ProbabilityTheory.Copula.CellMass.cellMass_patchwork {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (D : Fin m → Fin n → Copula 2) (i : Fin m) (j : Fin n) : ((A.patchwork D).cellMass P Q).mass i j = A.mass i j

Sampling any filled grid recovers exactly the original cell probabilities.

theorem ProbabilityTheory.Copula.IntervalPartition.exists_cell {m : ℕ} (P : IntervalPartition m) (u : ↑unitInterval) : ∃ (i : Fin m), P.point i.castSucc ≤ u ∧ u ≤ P.point i.succ

Every unit-interval point is contained in a closed grid cell.

theorem ProbabilityTheory.Copula.abs_cdf_cellMass_patchwork_sub_le {m n : ℕ} (C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) (D : Fin m → Fin n → Copula 2) (u v : ↑unitInterval) (i : Fin m) (j : Fin n) (hu : P.point i.castSucc ≤ u ∧ u ≤ P.point i.succ) (hv : Q.point j.castSucc ≤ v ∧ v ≤ Q.point j.succ) : |((C.cellMass P Q).patchwork D).cdf ![u, v] - C.cdf ![u, v]| ≤ P.width i + Q.width j

Any local filling has CDF error at most the sum of the containing cell widths.

theorem ProbabilityTheory.Copula.abs_cdf_cellMass_patchwork_sub_le_mesh {m n : ℕ} (C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) (D : Fin m → Fin n → Copula 2) (dx dy : ℝ) (hx : ∀ (i : Fin m), P.width i ≤ dx) (hy : ∀ (j : Fin n), Q.width j ≤ dy) (u v : ↑unitInterval) : |((C.cellMass P Q).patchwork D).cdf ![u, v] - C.cdf ![u, v]| ≤ dx + dy

Uniform mesh bound, independent of the choice of local copulas.

theorem ProbabilityTheory.Copula.abs_cdf_checkerboard_uniform_sub_le (C : Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u v : ↑unitInterval) : |(C.checkerboard (IntervalPartition.uniform m hm) (IntervalPartition.uniform n hn)).cdf ![u, v] - C.cdf ![u, v]| ≤ 1 / ↑m + 1 / ↑n

Checkerboard approximation error on an m × n uniform grid.

theorem ProbabilityTheory.Copula.abs_cdf_checkMin_uniform_sub_le (C : Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u v : ↑unitInterval) : |(C.checkMin (IntervalPartition.uniform m hm) (IntervalPartition.uniform n hn)).cdf ![u, v] - C.cdf ![u, v]| ≤ 1 / ↑m + 1 / ↑n

Check-min approximation has the same uniform CDF error guarantee.

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

Every choice of local copulas converges uniformly as the uniform grid is refined.

theorem ProbabilityTheory.Copula.tendstoUniformly_checkerboard (C : Copula 2) : TendstoUniformly (fun (k : ℕ) => (C.checkerboard (IntervalPartition.uniform (k + 1) ⋯) (IntervalPartition.uniform (k + 1) ⋯)).cdf) C.cdf Filter.atTop

Checkerboard copulas converge uniformly along refining uniform grids.

theorem ProbabilityTheory.Copula.tendstoUniformly_checkMin (C : Copula 2) : TendstoUniformly (fun (k : ℕ) => (C.checkMin (IntervalPartition.uniform (k + 1) ⋯) (IntervalPartition.uniform (k + 1) ⋯)).cdf) C.cdf Filter.atTop

Check-min copulas converge uniformly along refining uniform grids.