theorem
Verification.bernstein_lower_tail
(C : ProbabilityTheory.Copula 2)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
:
(C.bernstein m n hm hn).HasLowerTailDependence 0
theorem
Verification.bernstein_upper_tail
(C : ProbabilityTheory.Copula 2)
(m n : ℕ)
(hm : 0 < m)
(hn : 0 < n)
:
(C.bernstein m n hm hn).HasUpperTailDependence 0