← Mathematical handbook

noncomputable def Verification.plackettDiag (θ t : ℝ) : ℝ

Equations

• Verification.plackettDiag θ t = (1 + 2 * (θ - 1) * t - √(1 + 4 * (θ - 1) * t * (1 - t))) / (2 * (θ - 1))

theorem Verification.plackettDiag_eq {θ : ℝ} (hθ : 0 < θ) (hne : θ ≠ 1) (t : ↑unitInterval) : plackettDiag θ ↑t = (plackett θ hθ).diagonal t

theorem Verification.plackettDiag_deriv {θ t : ℝ} (hne : θ ≠ 1) (hD : 0 < 1 + 4 * (θ - 1) * t * (1 - t)) : HasDerivAt (plackettDiag θ) (1 - (1 - 2 * t) / √(1 + 4 * (θ - 1) * t * (1 - t))) t

theorem Verification.plackett_tails {θ : ℝ} (hθ : 0 < θ) : (plackett θ hθ).HasLowerTailDependence 0 ∧ (plackett θ hθ).HasUpperTailDependence 0