← Mathematical handbook

theorem Verification.plackettP_deriv_first {θ u v : ℝ} (hD : 0 < plackettD θ u v) : HasDerivAt (fun (x : ℝ) => plackettP θ x v) (-2 * θ * (θ - 1) * v * (1 - v) / √(plackettD θ u v) ^ 3) u

theorem Verification.plackett_transpose (θ : ℝ) (hθ : 0 < θ) : (plackett θ hθ).transpose = plackett θ hθ

theorem Verification.plackett_isCI {θ : ℝ} (hθ : 0 < θ) (hθ1 : 1 ≤ θ) : (plackett θ hθ).IsCI

theorem Verification.plackett_isCD {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) : (plackett θ hθ).IsCD

theorem Verification.plackett_midpoint {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf] = √θ / (2 * (√θ + 1))

theorem Verification.plackett_pqd_iff {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).IsPQD ↔ 1 ≤ θ

theorem Verification.plackett_nqd_iff {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).IsNQD ↔ θ ≤ 1

theorem Verification.plackett_ci_iff {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).IsCI ↔ 1 ≤ θ

theorem Verification.plackett_cd_iff {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).IsCD ↔ θ ≤ 1