← Mathematical handbook

theorem Verification.plackettDensity_continuousAt {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : ContinuousAt (fun (p : ↑unitInterval × ↑unitInterval) => plackettDensity θ ↑p.1 ↑p.2) (u, v)

theorem Verification.plackettDensity_zero {θ v : ℝ} (hθ : 0 < θ) (hv : v ∈ Set.Icc 0 1) : plackettDensity θ 0 v = θ / (1 + (θ - 1) * v) ^ 2

theorem Verification.plackettDensity_one {θ u : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Icc 0 1) : plackettDensity θ u 1 = θ / (θ - (θ - 1) * u) ^ 2

theorem Verification.plackett_minor_polynomial_nonneg {θ : ℝ} (hθ : 1 < θ) (hC : (plackett θ ⋯).HasMTP2Density) (t : ↑unitInterval) (ht : 0 < ↑t) : 0 ≤ plackettMinorPolynomial θ (θ - 1) ↑t

theorem Verification.plackett_density_tp2_requires_le_two {θ : ℝ} (hθ : 0 < θ) (hC : (plackett θ hθ).HasMTP2Density) : θ ≤ 2

theorem Verification.plackett_density_tp2_necessary {θ : ℝ} (hθ : 0 < θ) (hC : (plackett θ hθ).HasMTP2Density) : θ ∈ Set.Icc 1 2