← Mathematical handbook

noncomputable def Verification.rafteryDiag (δ t : ℝ) : ℝ

Equations

• Verification.rafteryDiag δ t = t + (1 - δ) / (1 + δ) * (t ^ (2 / (1 - δ)) - t)

theorem Verification.rafteryDiag_eq (δ : ↑unitInterval) (h1 : δ ≠ 1) (t : ↑unitInterval) : rafteryDiag ↑δ ↑t = (raftery δ).diagonal t

theorem Verification.rafteryDiag_deriv (δ : ↑unitInterval) (h1 : δ ≠ 1) (t : ℝ) : HasDerivAt (rafteryDiag ↑δ) (1 + (1 - ↑δ) / (1 + ↑δ) * (2 / (1 - ↑δ) * t ^ (2 / (1 - ↑δ) - 1) - 1)) t

theorem Verification.raftery_tails_lt_one (δ : ↑unitInterval) (h1 : δ ≠ 1) : (raftery δ).HasLowerTailDependence (2 * ↑δ / (1 + ↑δ)) ∧ (raftery δ).HasUpperTailDependence 0

theorem Verification.raftery_tails_one : (raftery 1).HasLowerTailDependence 1 ∧ (raftery 1).HasUpperTailDependence 1