HARA utility

Hyperbolic absolute risk aversion: absolute risk tolerance -u' / u'' is affine in consumption. Toda's November 2020 draft studies concavity uniformly over arbitrary return and income laws, under its regularity hypotheses with borrowing permitted. That necessity result does not exclude concavity outside HARA in a particular capped model.

The definition

Stating "risk tolerance is affine" needs second derivatives. Since risk tolerance a + c scaled by 1/γ integrates to a shifted CRRA, the family can instead be given by its members, which is derivative-free and is what every proof below actually uses:

u c = k · (a + c) ^ (1 - γ) / (1 - γ) + l, and the γ = 1 logarithm,

with k > 0. This is the b ≠ 0 branch of HARA -- the one that contains CRRA, and the one macroeconomics uses. The quadratic branch (b < 0) is excluded because it satiates, and that exclusion is now a theorem rather than a remark: Models.Quadratic.no_incomeFluctuation_quadUtility shows no economy in this development can have quadratic utility, for any bliss point, since the structure asks for monotone utility on the whole of dom and a quadratic falls beyond its bliss point. Models.Quadratic also records what the branch would give if it could be hosted — Hall's certainty equivalence, the aggregator being the plain weighted mean.

CARA (b = 0) is NOT excluded, and an earlier version of this docstring was wrong about why it might be: u c = -exp (-α c) / α is bounded above by 0 and equals -1/α at zero consumption, so a capped model admits it -- Models.IncomeFluctuationCARA.caraWitness is one. What CARA does not have is Light's condition, since relative risk aversion α c is unbounded (not_monotoneOn_mul_deriv_caraUtility). It is covered separately because its Carroll--Kimball step needs a different aggregator, the soft minimum of Analysis.SoftMin rather than a power mean; see Models.IncomeFluctuationCARA.

The shift a is the subsistence level of Stone and Geary. a = 0 is CRRA exactly.

The result that matters

relativeRiskAversionLeOne_haraUtility: HARA with a NONNEGATIVE shift and γ ≤ 1 satisfies Light's condition. Relative risk aversion of the shifted family is γ c / (a + c), which for a ≥ 0 is at most γ; a negative shift (genuine subsistence) pushes it above γ and can break the condition however small γ is, so the sign of the shift is not a technicality.

The proof is derivative-free in the sense that matters: it factors

c · u' c = c ^ (1 - γ) · (c / (a + c)) ^ γ

into two nonnegative nondecreasing factors, which is exactly u' c · c nondecreasing, which is relative risk aversion at most one.

noncomputable def LeanEconomics.haraUtility (γ a c : ℝ) : ℝ

Shifted CRRA: the b ≠ 0 branch of HARA, with subsistence level a.

Equations

• LeanEconomics.haraUtility γ a c = LeanEconomics.crraUtility γ (a + c)

@[simp]

theorem LeanEconomics.haraUtility_zero_shift (γ : ℝ) : haraUtility γ 0 = crraUtility γ

def LeanEconomics.IsHARA (u : ℝ → ℝ) : Prop

HARA, as a class of functions: a positive affine transformation of a shifted CRRA.

Equations

• LeanEconomics.IsHARA u = ∃ (γ : ℝ) (a : ℝ) (k : ℝ) (l : ℝ), 0 < γ ∧ 0 < k ∧ ∀ (c : ℝ), u c = k * LeanEconomics.haraUtility γ a c + l

theorem LeanEconomics.isHARA_haraUtility {γ : ℝ} (hγ : 0 < γ) (a : ℝ) : IsHARA (haraUtility γ a)

theorem LeanEconomics.isHARA_crraUtility {γ : ℝ} (hγ : 0 < γ) : IsHARA (crraUtility γ)

CRRA is HARA, with no shift.

theorem LeanEconomics.isHARA_log : IsHARA Real.log

Log utility is HARA, as the γ = 1 member.

theorem LeanEconomics.hasDerivAt_haraUtility (γ : ℝ) {a c : ℝ} (hac : 0 < a + c) : HasDerivAt (haraUtility γ a) ((a + c) ^ (-γ)) c

Light's condition

theorem LeanEconomics.mul_rpow_neg_eq {γ a c : ℝ} (hc : 0 < c) (hac : 0 < a + c) : c * (a + c) ^ (-γ) = c ^ (1 - γ) * (c / (a + c)) ^ γ

The factorisation used for Light's condition: when the shift is nonnegative and 0 < γ ≤ 1, both factors are nonnegative and nondecreasing on positive consumption.

theorem LeanEconomics.relativeRiskAversionLeOne_haraUtility {γ a : ℝ} (hγ0 : 0 < γ) (hγ1 : γ ≤ 1) (ha : 0 ≤ a) : RelativeRiskAversionLeOne (haraUtility γ a)

HARA with a nonnegative shift and γ ≤ 1 satisfies Light's condition.

theorem LeanEconomics.IsHARA.relativeRiskAversionLeOne {u : ℝ → ℝ} {γ a k l : ℝ} (hγ0 : 0 < γ) (hγ1 : γ ≤ 1) (ha : 0 ≤ a) (hk : 0 < k) (hu : ∀ (c : ℝ), u c = k * haraUtility γ a c + l) : RelativeRiskAversionLeOne u

The same for the whole class, since a positive affine transformation preserves convexity in log consumption.

theorem LeanEconomics.haraUtility_rra_gt_one_of_neg_shift {γ a c : ℝ} (hac : 0 < a + c) (hnear : a + c < γ * c) : 1 < γ * c / (a + c)

A negative shift breaks it, however small γ is: relative risk aversion γ c / (a + c) exceeds one as consumption approaches the subsistence level from above. Recorded to show that 0 ≤ a in the theorem above is doing work.