← Mathematical handbook

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

Equations

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

noncomputable def Verification.bernsteinDensity (C : ProbabilityTheory.Copula 2) (m n : ℕ) (x : Fin 2 → ↑unitInterval) : ℝ

Equations

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

theorem Verification.bernsteinKernel_mono (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u : ↑unitInterval) : Monotone (bernsteinKernel C m n u)

theorem Verification.bernsteinDensity_nonneg (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (x : Fin 2 → ↑unitInterval) : 0 ≤ bernsteinDensity C m n x

theorem Verification.integral_Iic_bernsteinDerivative (m i : ℕ) (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, bernsteinDerivative m (i + 1) t = (bernstein m (i + 1)) u

theorem Verification.integral_Iic_bernsteinDensity (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (u : Fin 2 → ↑unitInterval) : ∫ (x : Fin 2 → ↑unitInterval) in Set.Iic u, bernsteinDensity C m n x = (C.bernstein m n hm hn).cdf u

theorem Verification.toMeasure_bernstein_density (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) : (C.bernstein m n hm hn).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (bernsteinDensity C m n x)

theorem Verification.integral_bernstein_density (C : ProbabilityTheory.Copula 2) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (f : (Fin 2 → ↑unitInterval) → ℝ) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(C.bernstein m n hm hn).toMeasure = ∫ (x : Fin 2 → ↑unitInterval), bernsteinDensity C m n x * f x