← Mathematical handbook

theorem Verification.plackett_odds_equation {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : θ * (↑u - (plackett θ hθ).cdf ![u, v]) * (↑v - (plackett θ hθ).cdf ![u, v]) = (plackett θ hθ).cdf ![u, v] * (1 - ↑u - ↑v + (plackett θ hθ).cdf ![u, v])

The defining cross-product odds equation holds even at independence and on the boundary.

theorem Verification.plackett_lowerOrthant_monotone {θ η : ℝ} (hθ : 0 < θ) (hθη : θ ≤ η) : (plackett θ hθ).LowerOrthantLE (plackett η ⋯)

theorem Verification.plackett_schur_above_one {θ η : ℝ} (hθ : 0 < θ) (h1 : 1 ≤ θ) (hθη : θ ≤ η) : (plackett θ hθ).SchurBothLE (plackett η ⋯)

theorem Verification.plackett_schur_below_one {θ η : ℝ} (hθ : 0 < θ) (hη : η ≤ 1) (hθη : θ ≤ η) : (plackett η ⋯).SchurBothLE (plackett θ hθ)

theorem Verification.plackett_lowerOrthant_iff {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) : (plackett θ hθ).LowerOrthantLE (plackett η hη) ↔ θ ≤ η