← Mathematical handbook

Bernstein copulas

The tensor Bernstein polynomial of a copula is again a copula for arbitrary positive degrees in the two coordinates. Copula validity is proved from the polynomial formula, using monotonicity of Bernstein combinations of ordered coefficients; no admissibility proof is required from the caller.

noncomputable def ProbabilityTheory.Copula.bernsteinCDF (C : Copula 2) (m n : ℕ) (u v : ↑unitInterval) : ℝ

Tensor Bernstein polynomial of the sampled copula CDF.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.isClassical_bernsteinCDF (C : Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : IsClassical fun (u : Fin 2 → ↑unitInterval) => C.bernsteinCDF m n (u 0) (u 1)

The classical copula conditions hold for every pair of positive degrees.

noncomputable def ProbabilityTheory.Copula.bernstein (C : Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : Copula 2

The Bernstein copula with positive coordinate degrees m and n.

Equations

• C.bernstein m n hm hn = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => C.bernsteinCDF m n (u 0) (u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_bernstein (C : Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u : Fin 2 → ↑unitInterval) : (C.bernstein m n hm hn).cdf u = C.bernsteinCDF m n (u 0) (u 1)

theorem ProbabilityTheory.Copula.bernsteinCDF_eq_sum (C : Copula 2) (m n : ℕ) (u v : ↑unitInterval) : C.bernsteinCDF m n u v = ∑ i : Fin (m + 1), ∑ j : Fin (n + 1), C.cdf ![bernstein.z i, bernstein.z j] * (_root_.bernstein m ↑i) u * (_root_.bernstein n ↑j) v

The usual tensor-product Bernstein formula, with indices including both endpoints.

@[simp]

theorem ProbabilityTheory.Copula.bernstein_independence (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (independence 2).bernstein m n hm hn = independence 2

Bernstein smoothing fixes independence at every pair of positive degrees.

@[simp]

theorem ProbabilityTheory.Copula.bernstein_one_one (C : Copula 2) : C.bernstein 1 1 ⋯ ⋯ = independence 2

The degree (1,1) Bernstein approximation of every copula is independence.