← Copula mathematical handbook

Convexity lemmas for inverse generators of Nelsen's Table 4.1

Several families of Nelsen (An Introduction to Copulas, second edition, Table 4.1, families 19 and 20) have an inverse generator of the form c / f t or (f t) ^ p with f t = log (t + c') concave and positive and p ≤ 0. Such a composite of a convex decreasing power with a concave function is convex. These elementary lemmas isolate that argument.

theorem ProbabilityTheory.Copula.convexOn_rpow_Ioi_of_nonpos {p : ℝ} (hp : p ≤ 0) : ConvexOn ℝ (Set.Ioi 0) fun (z : ℝ) => z ^ p

The power z ↦ z ^ p is convex on (0, ∞) for every nonpositive exponent p.

theorem ProbabilityTheory.Copula.convexOn_rpow_comp_nonpos {f : ℝ → ℝ} {p : ℝ} (hp : p ≤ 0) (hf : ConcaveOn ℝ (Set.Ici 0) f) (hpos : ∀ x ∈ Set.Ici 0, 0 < f x) : ConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => f x ^ p

A positive concave function raised to a nonpositive power is convex.

theorem ProbabilityTheory.Copula.convexOn_div_comp {f : ℝ → ℝ} {c : ℝ} (hc : 0 ≤ c) (hf : ConcaveOn ℝ (Set.Ici 0) f) (hpos : ∀ x ∈ Set.Ici 0, 0 < f x) : ConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => c / f x

A nonnegative constant divided by a positive concave function is convex.

theorem ProbabilityTheory.Copula.concaveOn_log_add {c : ℝ} (hc : 0 < c) : ConcaveOn ℝ (Set.Ici 0) fun (s : ℝ) => Real.log (s + c)

The logarithm of a positive translate is concave on [0, ∞).

theorem ProbabilityTheory.Copula.le_log_add_exp {t : ℝ} (ht : 0 ≤ t) (c : ℝ) : c ≤ Real.log (t + Real.exp c)

c ≤ log (t + exp c) for nonnegative t.