theorem
Verification.generator_isCD_of_antitone_derivative_ratio
(g : ProbabilityTheory.Copula.BivariateGenerator)
(φ φ' ψ' : ℝ → ℝ)
(J : Set ℝ)
(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φmem : ∀ u ∈ Set.Ioo 0 1, φ u ∈ J)
(hψneg : ∀ t ∈ J, ψ' t < 0)
(hratio : ∀ (k : ℝ), 0 ≤ k → AntitoneOn (fun (t : ℝ) => ψ' (t + k) / ψ' t) J)
:
A derivative-ratio criterion allowing a finite-zero inverse generator. Strict negativity is needed only on the image of interior generator values.