theorem
Verification.generator_isCD_of_logconcave_neg_deriv
(g : ProbabilityTheory.Copula.BivariateGenerator)
(φ φ' ψ' : ℝ → ℝ)
(hφ : ∀ (u : ↑unitInterval), 0 < ↑u → ↑u < 1 → φ ↑u = g.invFun u)
(hφpos : ∀ u ∈ Set.Ioo 0 1, 0 < φ u)
(hφderiv : ∀ u ∈ Set.Ioo 0 1, HasDerivAt φ (φ' u) u)
(hψderiv : ∀ (t : ℝ), 0 < t → HasDerivAt g.toFun (ψ' t) t)
(hψneg : ∀ (t : ℝ), 0 < t → ψ' t < 0)
(hlog : ConcaveOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (-ψ' t))
:
A smooth strict inverse generator with log-concave negative derivative gives CD. Only interior differentiability is used; the actual copula supplies boundary continuity.