Decreasing increments of a concave function

Numbered Light references use the October 31, 2018 author draft, printed page 13: https://www.researchgate.net/publication/314238962

A concave function's increment over an interval of fixed length shrinks as the interval slides right. In economics this is the increasing-differences (supermodularity) condition that monotone-comparative-statics arguments run on, usually stated as a cross partial -u'' > 0. Stated this way it needs no derivatives and no smoothness at all.

The proof is two applications of concavity. Writing L = (c₂ + Δ) - c₁, the two interior points c₁ + Δ and c₂ are complementary convex combinations of the endpoints c₁ and c₂ + Δ: the weights on c₂ + Δ are Δ / L and (c₂ - c₁) / L, which sum to one. Adding the two concavity inequalities makes the weights cancel.

theorem ConcaveOn.sub_le_sub_of_shift {s : Set ℝ} {u : ℝ → ℝ} (hu : ConcaveOn ℝ s u) {c₁ c₂ Δ : ℝ} (h₁ : c₁ ∈ s) (h₂ : c₂ + Δ ∈ s) (hc : c₁ ≤ c₂) (hΔ : 0 ≤ Δ) : u (c₂ + Δ) - u (c₁ + Δ) ≤ u c₂ - u c₁

Decreasing increments. For a concave u, sliding an interval to the right by Δ cannot increase the increment of u across it.

Lipschitz away from the left endpoint

A concave function on Ioi 0 need not be Lipschitz there -- utility functions used in economics are exactly the ones that are not, diverging at zero -- but it IS Lipschitz on [δ, ∞) for any δ > 0, with a constant read off a single secant. No differentiability is needed: the bound comes from antitonicity of secant slopes.

This is what lets a marginal argument be run without a derivative. Where the textbook argument bounds the marginal utility of consumption by u'(δ), this bounds it by the slope of u across [δ/2, δ], which is available from concavity alone.

noncomputable def slopeBound (u : ℝ → ℝ) (δ : ℝ) : ℝ

The secant slope of u across [δ/2, δ], which bounds every slope further right.

Equations

• slopeBound u δ = (u δ - u (δ / 2)) / (δ / 2)

theorem slopeBound_nonneg {u : ℝ → ℝ} (hmono : MonotoneOn u (Set.Ioi 0)) {δ : ℝ} (hδ : 0 < δ) : 0 ≤ slopeBound u δ

theorem ConcaveOn.sub_le_slopeBound_mul {u : ℝ → ℝ} (hu : ConcaveOn ℝ (Set.Ioi 0) u) {δ : ℝ} (hδ : 0 < δ) {a b : ℝ} (ha : δ ≤ a) (hab : a ≤ b) : u b - u a ≤ slopeBound u δ * (b - a)

The one-sided bound: moving right from a ≥ δ raises u by at most the slope bound times the distance.

theorem ConcaveOn.abs_sub_le_slopeBound_mul {u : ℝ → ℝ} (hu : ConcaveOn ℝ (Set.Ioi 0) u) (hmono : MonotoneOn u (Set.Ioi 0)) {δ : ℝ} (hδ : 0 < δ) {x y : ℝ} (hx : δ ≤ x) (hy : δ ≤ y) : |u x - u y| ≤ slopeBound u δ * |x - y|

A concave function is Lipschitz away from the left endpoint, with an explicit constant and no appeal to differentiability.

Scaling a concave function

For a concave, strictly positive z, the ratio α / z (α x) rises with α. This is Lemma 4 of Light (2018), one of the three ingredients of his Theorem 1 (savings rise with the interest rate when relative risk aversion is at most one).

Like the increments lemma above, it needs no derivative: α₁ x is a convex combination of 0 and α₂ x with weight α₁ / α₂, so concavity gives the inequality directly, and strict positivity at the origin is what turns it from weak into the stated form.

theorem ConcaveOn.div_le_div_of_scale {z : ℝ → ℝ} {s : Set ℝ} (hz : ConcaveOn ℝ s z) (h0 : 0 ∈ s) (hz0 : 0 < z 0) {α₁ α₂ x : ℝ} (h1 : 0 < α₁) (h12 : α₁ ≤ α₂) (hm2 : α₂ * x ∈ s) (hp2 : 0 < z (α₂ * x)) : α₁ / z (α₁ * x) ≤ α₂ / z (α₂ * x)

Light (2018), Lemma 4, on any convex set containing the origin. In the application z is the consumption function, which is concave on the asset region and nowhere else, so the original statement over [0, ∞) would not reach it. Positivity is needed only at the origin and at the far point: concavity carries it to everything in between.