theorem
Verification.tawn_isCI
(θ : ℝ)
(hθ : 1 ≤ θ)
(α β : ↑unitInterval)
:
(ProbabilityTheory.Copula.tawn θ hθ α β).IsCI
theorem
Verification.tawn_schur_monotone
{θ η : ℝ}
(hθ : 1 ≤ θ)
(hθη : θ ≤ η)
(α β : ↑unitInterval)
:
(ProbabilityTheory.Copula.tawn θ hθ α β).SchurBothLE (ProbabilityTheory.Copula.tawn η ⋯ α β)