← Copula mathematical handbook

Quantitative Bernstein copula approximation

theorem ProbabilityTheory.Copula.bernstein_displacement_le (n : ℕ) (hn : 0 < n) (u : ↑unitInterval) : Bernstein.blend n (fun (k : Fin (n + 1)) => |↑u - ↑(bernstein.z k)|) u ≤ √(↑u * (1 - ↑u) / ↑n)

Mean absolute grid displacement is bounded by the binomial standard deviation.

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

Pointwise error controlled by the sum of coordinate binomial standard deviations.

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

A bound independent of the evaluation point; hence an explicit uniform approximation rate.

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

Bernstein copulas converge uniformly to the original copula as both degrees increase.