← Mathematical handbook

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

Equations

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

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

Equations

• Verification.plackettD θ u v = Verification.plackettA θ u v ^ 2 - 4 * θ * (θ - 1) * u * v

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

Equations

• Verification.plackettF θ u v = (Verification.plackettA θ u v - √(Verification.plackettD θ u v)) / (2 * (θ - 1))

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

Equations

• Verification.plackettP θ u v = (1 - (Verification.plackettA θ u v - 2 * θ * v) / √(Verification.plackettD θ u v)) / 2

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

Equations

• Verification.plackettDensity θ u v = θ * (1 + (θ - 1) * (u + v - 2 * u * v)) / √(Verification.plackettD θ u v) ^ 3

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

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

theorem Verification.plackettF_deriv {θ u v : ℝ} (hθ : θ ≠ 1) (hD : 0 < plackettD θ u v) : HasDerivAt (fun (x : ℝ) => plackettF θ x v) (plackettP θ u v) u

theorem Verification.plackettP_deriv {θ u v : ℝ} (hD : 0 < plackettD θ u v) : HasDerivAt (plackettP θ u) (plackettDensity θ u v) v