CRRA utility, and where it fits

This file compares two conditions on the CRRA utility family:

• Tendsto u (𝓝[>] 0) atBot, which gives unbounded-below utility at zero consumption;
• Light's relative-risk-aversion bound RelativeRiskAversionLeOne.

For CRRA the first holds exactly when γ ≥ 1 and the second exactly when γ ≤ 1. crra_pinch records that both hold only for log utility, γ = 1. For γ < 1, not_tendsto_atBot_crraUtility proves utility is bounded below; for γ > 1, strictConcaveOn_crra_comp_exp rules out the relative-risk-aversion bound.

The household structure itself supports both cases. Its utility domain can be Ioi 0 or Ici 0, with continuity of the extended reward in place of an unconditional divergence assumption. IncomeFluctuation.Unbounded recovers divergence in the open-domain case. BoundedIncomeFluctuation supplies a bounded-utility CES model, and the later iteration machinery obtains its positive consumption from a marginal Inada condition. Thus the pinch restricts the unbounded-below CRRA subclass, rather than every household model in the library.

The single derivative formula

hasDerivAt_crraUtility gives u' c = c ^ (-γ) for every γ, log included, since log' c = c⁻¹ is the γ = 1 case. Monotonicity, strict concavity and the Inada condition are all read off it, so the two branches of the definition are only ever separated once.

noncomputable def LeanEconomics.crraUtility (γ c : ℝ) : ℝ

CRRA period utility. Power utility for γ ≠ 1, with the usual logarithmic convention at γ = 1. For positive c, subtracting 1 / (1 - γ) from the power branch gives the normalization whose limit as γ → 1 is log c; the raw branch does not have a finite limit.

Equations

• LeanEconomics.crraUtility γ c = if γ = 1 then Real.log c else c ^ (1 - γ) / (1 - γ)

theorem LeanEconomics.crraUtility_of_ne {γ : ℝ} (h : γ ≠ 1) (c : ℝ) : crraUtility γ c = c ^ (1 - γ) / (1 - γ)

@[simp]

theorem LeanEconomics.crraUtility_one : crraUtility 1 = Real.log

theorem LeanEconomics.crraUtility_two : crraUtility 2 = fun (c : ℝ) => -c⁻¹

The existing non-vacuity witness u c = -c⁻¹ is CRRA with γ = 2.

The derivative, and everything read off it

theorem LeanEconomics.hasDerivAt_crraUtility (γ : ℝ) {c : ℝ} (hc : 0 < c) : HasDerivAt (crraUtility γ) (c ^ (-γ)) c

Marginal utility is c ^ (-γ), log included.

theorem LeanEconomics.deriv_crraUtility (γ : ℝ) {c : ℝ} (hc : 0 < c) : deriv (crraUtility γ) c = c ^ (-γ)

theorem LeanEconomics.continuousOn_crraUtility (γ : ℝ) : ContinuousOn (crraUtility γ) (Set.Ioi 0)

theorem LeanEconomics.strictMonoOn_crraUtility (γ : ℝ) : StrictMonoOn (crraUtility γ) (Set.Ioi 0)

theorem LeanEconomics.monotoneOn_crraUtility (γ : ℝ) : MonotoneOn (crraUtility γ) (Set.Ioi 0)

theorem LeanEconomics.strictConcaveOn_crraUtility {γ : ℝ} (hγ : 0 < γ) : StrictConcaveOn ℝ (Set.Ioi 0) (crraUtility γ)

The Inada condition holds exactly for γ ≥ 1

theorem LeanEconomics.tendsto_atBot_crraUtility {γ : ℝ} (hγ : 1 ≤ γ) : Filter.Tendsto (crraUtility γ) (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

theorem LeanEconomics.not_tendsto_atBot_crraUtility {γ : ℝ} (hγ : γ < 1) : ¬Filter.Tendsto (crraUtility γ) (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

For γ < 1 the Inada condition fails, and not for want of an argument: period utility is then bounded below by zero, so it cannot tend to -∞ along any filter that is not trivial.

The pinch

theorem LeanEconomics.relativeRiskAversionLeOne_crraUtility_iff {γ : ℝ} : RelativeRiskAversionLeOne (crraUtility γ) ↔ γ ≤ 1

Relative risk aversion at most one holds for CRRA exactly when γ ≤ 1.

theorem LeanEconomics.crra_pinch {γ : ℝ} : Filter.Tendsto (crraUtility γ) (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot ∧ RelativeRiskAversionLeOne (crraUtility γ) ↔ γ = 1

The unbounded-domain requirements pinch CRRA to log utility. Divergence to -∞ at zero forces γ ≥ 1, while relative risk aversion at most one forces γ ≤ 1. This conjunction does not restrict the separate bounded-domain treatment of 0 < γ < 1.

theorem LeanEconomics.not_relativeRiskAversionLeOne_neg_inv : ¬RelativeRiskAversionLeOne fun (c : ℝ) => -c⁻¹

The existing witness fails Light's condition, as γ = 2 > 1 requires.

A log-utility economy

The pinch is not vacuous: γ = 1 really is an income fluctuation problem. This is NonVacuity.impatient with its -c⁻¹ — which is γ = 2 by crraUtility_two — replaced by log, so the two witnesses sit on either side of Light's condition, and every utility axiom is now discharged by a single lemma about the CRRA family.

noncomputable def LeanEconomics.logImpatient : IncomeFluctuation (Fin 2) 0 1

An impatient household with log utility: β = 1/100, r = 0, income in {1, 2}, cap 1.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanEconomics.logImpatient_u : logImpatient.u = Real.log

theorem LeanEconomics.logImpatient_relativeRiskAversionLeOne : RelativeRiskAversionLeOne logImpatient.u

The log economy satisfies Light's condition, and by crra_pinch it is the only CRRA economy that can.