← Mathematical handbook

def Verification.plackettN (θ u v : ℝ) : ℝ

Equations

• Verification.plackettN θ u v = 1 + (θ - 1) * (u + v - 2 * u * v)

noncomputable def Verification.plackettLogDensity (θ u v : ℝ) : ℝ

Equations

• Verification.plackettLogDensity θ u v = Real.log θ + Real.log (Verification.plackettN θ u v) - 3 / 2 * Real.log (Verification.plackettD θ u v)

noncomputable def Verification.plackettLogScore (θ u v : ℝ) : ℝ

Equations

• Verification.plackettLogScore θ u v = (θ - 1) * (1 - 2 * v) / Verification.plackettN θ u v - 3 * (θ - 1) * (Verification.plackettA θ u v - 2 * θ * v) / Verification.plackettD θ u v

theorem Verification.plackettN_pos {θ u v : ℝ} (hθ : 1 ≤ θ) (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) : 0 < plackettN θ u v

theorem Verification.plackettDensity_pos {θ u v : ℝ} (hθ : 1 ≤ θ) (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) : 0 < plackettDensity θ u v

theorem Verification.plackettLogDensity_eq {θ u v : ℝ} (hθ : 1 ≤ θ) (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) : plackettLogDensity θ u v = Real.log (plackettDensity θ u v)

theorem Verification.plackettLogDensity_deriv {θ u v : ℝ} (hN : 0 < plackettN θ u v) (hD : 0 < plackettD θ u v) : HasDerivAt (fun (x : ℝ) => plackettLogDensity θ x v) (plackettLogScore θ u v) u

theorem Verification.plackettLogScore_deriv {θ u v : ℝ} (hN : 0 < plackettN θ u v) (hD : 0 < plackettD θ u v) : HasDerivAt (plackettLogScore θ u) ((θ - 1) * plackettLogPolynomial (θ - 1) u v / (plackettN θ u v ^ 2 * plackettD θ u v ^ 2)) v