← Mathematical handbook

def Verification.plackettLogPolynomial (p u v : ℝ) : ℝ

Numerator of the mixed log-density derivative after extracting theta-1.

Equations

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

def Verification.plackettLogCoefficients : Fin 6 → Fin 5 → Fin 5 → ℝ

Integer coefficients in the unnormalized tensor Bernstein basis of degrees (5,4,4).

Equations

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

theorem Verification.plackettLogCoefficients_nonneg (i : Fin 6) (j k : Fin 5) : 0 ≤ plackettLogCoefficients i j k

theorem Verification.plackettLogPolynomial_certificate (p u v : ℝ) : plackettLogPolynomial p u v = ∑ i : Fin 6, ∑ j : Fin 5, ∑ k : Fin 5, plackettLogCoefficients i j k * p ^ ↑i * (1 - p) ^ (5 - ↑i) * u ^ ↑j * (1 - u) ^ (4 - ↑j) * v ^ ↑k * (1 - v) ^ (4 - ↑k)

theorem Verification.plackettLogPolynomial_nonneg {p u v : ℝ} (hp : p ∈ Set.Icc 0 1) (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) : 0 ≤ plackettLogPolynomial p u v