← Mathematical handbook

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

Equations

• Verification.frankDiag θ t = -Real.log (1 + (Real.exp (-θ * t) - 1) ^ 2 / (Real.exp (-θ) - 1)) / θ

theorem Verification.frankDiag_deriv_zero (θ : ℝ) : HasDerivAt (frankDiag θ) 0 0

theorem Verification.frankDiag_deriv_one {θ : ℝ} (hθ : θ ≠ 0) : HasDerivAt (frankDiag θ) 2 1

theorem Verification.frankDiag_positive (θ : ℝ) (hθ : 0 < θ) (t : ↑unitInterval) : frankDiag θ ↑t = (ProbabilityTheory.Copula.frank θ hθ).diagonal t

theorem Verification.frankDiag_negative (θ : ℝ) (hθ : θ < 0) (t : ↑unitInterval) : frankDiag θ ↑t = (ProbabilityTheory.Copula.frankNegative θ hθ).diagonal t

theorem Verification.frank_positive_tails (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.frank θ hθ).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.frank θ hθ).HasUpperTailDependence 0

theorem Verification.frank_negative_tails (θ : ℝ) (hθ : θ < 0) : (ProbabilityTheory.Copula.frankNegative θ hθ).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.frankNegative θ hθ).HasUpperTailDependence 0