← Mathematical handbook

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

Equations

• Verification.n20Diagonal θ t = if t = 0 then 0 else Real.log (2 * Real.exp (t ^ (-θ)) - Real.exp 1) ^ (-θ⁻¹)

theorem Verification.n20Diagonal_eq {θ : ℝ} (hθ : 0 < θ) (t : ↑unitInterval) : n20Diagonal θ ↑t = (nelsen20 θ ⋯).diagonal t

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

theorem Verification.nelsen20_upperTail_pos {θ : ℝ} (hθ : 0 < θ) : (nelsen20 θ ⋯).HasUpperTailDependence 0

theorem Verification.nelsen20_lowerTail_bound {θ : ℝ} (hθ : 0 < θ) (t : ↑unitInterval) (ht : 0 < ↑t) : (1 + ↑t ^ θ * Real.log 2) ^ (-θ⁻¹) ≤ (nelsen20 θ ⋯).lowerTailRatio t

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

theorem Verification.nelsen20_tails (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen20 θ hθ).HasLowerTailDependence (if θ = 0 then 0 else 1) ∧ (nelsen20 θ hθ).HasUpperTailDependence 0