← Mathematical handbook

theorem Verification.nelsen19_lowerTail_bound {θ : ℝ} (hθ : 0 < θ) (t : ↑unitInterval) (ht : 0 < ↑t) : θ / (θ + ↑t * Real.log 2) ≤ (nelsen19 θ ⋯).lowerTailRatio t

theorem Verification.nelsen19_lowerTail_pos {θ : ℝ} (hθ : 0 < θ) : (nelsen19 θ ⋯).HasLowerTailDependence 1

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

Equations

• Verification.n19Diagonal θ t = if t = 0 then 0 else θ / Real.log (2 * Real.exp (θ / t) - Real.exp θ)

theorem Verification.n19Diagonal_eq {θ : ℝ} (hθ : 0 < θ) (t : ↑unitInterval) : n19Diagonal θ ↑t = (nelsen19 θ ⋯).diagonal t

theorem Verification.n19Diagonal_deriv_one {θ : ℝ} (hθ : 0 < θ) : HasDerivAt (n19Diagonal θ) 2 1

theorem Verification.nelsen19_upperTail_pos {θ : ℝ} (hθ : 0 < θ) : (nelsen19 θ ⋯).HasUpperTailDependence 0

theorem Verification.nelsen19_tails (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen19 θ hθ).HasLowerTailDependence (if θ = 0 then 1 / 2 else 1) ∧ (nelsen19 θ hθ).HasUpperTailDependence 0