← Mathematical handbook

theorem Verification.convex_increment_pos {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ioi 0) f) {a b c e : ℝ} (ha : 0 < a) (hc : 0 ≤ c) (hab : a ≤ b) (hce : c ≤ e) : 0 ≤ f (b + e) - f (a + e) - f (b + c) + f (a + c)

theorem Verification.generator_isCI_of_logconvex_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 : ConvexOn ℝ (Set.Ioi 0) fun (t : ℝ) => Real.log (-ψ' t)) : g.copula.IsCI

A smooth strict inverse generator with log-convex negative derivative gives CI. Only interior differentiability is used; the actual copula supplies boundary continuity.