Documentation

Copula.Bernstein.Basis

← Copula mathematical handbook

Shape preservation for Bernstein polynomials #

The derivative is a nonnegative Bernstein combination of consecutive coefficient differences. In particular, ordered coefficients give a monotone function. This is the key step in proving that the tensor Bernstein approximation of a copula is a copula.

source
noncomputable def ProbabilityTheory.Copula.Bernstein.polynomial (n : ℕ) (f : Fin (n + 1) → ℝ) :
Polynomial ℝ

Polynomial with prescribed Bernstein coefficients.

Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.Bernstein.blend (n : ℕ) (f : Fin (n + 1) → ℝ) (u : ↑unitInterval) :
    ℝ

    Evaluation of a Bernstein combination on the unit interval.

    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.Bernstein.eval_polynomial (n : ℕ) (f : Fin (n + 1) → ℝ) (u : ↑unitInterval) :
      Polynomial.eval (↑u) (polynomial n f) = blend n f u
      source
      theorem ProbabilityTheory.Copula.Bernstein.derivative_polynomial (n : ℕ) (f : Fin (n + 2) → ℝ) :
      Polynomial.derivative (polynomial (n + 1) f) = Polynomial.C (↑n + 1) * polynomial n fun (k : Fin (n + 1)) => f k.succ - f k.castSucc
      source
      theorem ProbabilityTheory.Copula.Bernstein.blend_mono (n : ℕ) (f : Fin (n + 1) → ℝ) (hf : Monotone f) :
      Monotone (blend n f)
      source
      @[simp]
      theorem ProbabilityTheory.Copula.Bernstein.blend_zero (n : ℕ) (f : Fin (n + 1) → ℝ) :
      blend n f 0 = f 0
      source
      @[simp]
      theorem ProbabilityTheory.Copula.Bernstein.blend_one (n : ℕ) (f : Fin (n + 1) → ℝ) :
      blend n f 1 = f (Fin.last n)
      source
      theorem ProbabilityTheory.Copula.Bernstein.blend_const (n : ℕ) (a : ℝ) (u : ↑unitInterval) :
      blend n (fun (x : Fin (n + 1)) => a) u = a
      source
      theorem ProbabilityTheory.Copula.Bernstein.blend_sub (n : ℕ) (f g : Fin (n + 1) → ℝ) (u : ↑unitInterval) :
      blend n (fun (k : Fin (n + 1)) => f k - g k) u = blend n f u - blend n g u
      source
      theorem ProbabilityTheory.Copula.Bernstein.blend_nonneg (n : ℕ) (f : Fin (n + 1) → ℝ) (hf : ∀ (k : Fin (n + 1)), 0 ≤ f k) (u : ↑unitInterval) :
      0 ≤ blend n f u
      source
      theorem ProbabilityTheory.Copula.Bernstein.blend_id (n : ℕ) (hn : 0 < n) (u : ↑unitInterval) :
      blend n (fun (k : Fin (n + 1)) => ↑(bernstein.z k)) u = ↑u

      Bernstein polynomials reproduce the identity for every positive degree.