Quantitative constants for CRRA households

The equilibrium programme runs on four explicit constants: a lower bound on the secant slope of u (which drives the corner condition and the precautionary gain), an upper bound on it (which gives the value function its Lipschitz constant), a bound on saving (which gives the decline condition), and the calibration arithmetic that checks they fit together. All four were computed for Real.log, and hu : P.u = Real.log propagated through the whole chain.

The common derivative formula hasDerivAt_crraUtility covers every γ > 0, including log, so the marginal bounds also cover that case. The closed form crraSlopeBound is used only when γ ≠ 1; the logarithmic slope bound is evaluated separately as 2 log 2 / m.

The one place the shape changes

For log, marginal utility is 1/c, so the slope bound available at resources R is 1/R — it DEGRADES as resources grow, and the multiplicative bound c ≥ R / (1 + 2G) is the right output. For CES with γ < 1 marginal utility is c^{-γ}, and on a capped problem c ≤ maxConsumption, so there is a single slope maxConsumption ^ (-γ) that works everywhere. That turns the same deviation argument into a UNIFORM bound on saving — policy s ≤ K for one constant K — which is a cleaner route to the decline condition than the multiplicative bound, and the natural asset bound falls straight out of it.

policy_le_of_marginal_bound is stated for any u with a uniform slope bound, so log gets the uniform version too, with m = 1 / maxConsumption.

Rational exponents reduce to integer powers

At γ = 1 - 1/n every exponent the CES constants produce is m/n for integers m, n, and a comparison of x ^ (m/n) against a rational is equivalent to one of x ^ m against c ^ n. These two lemmas are the whole bridge, and they are what keeps γ near 1 arithmetically tractable: norm_num settles the integer form.

theorem LeanEconomics.rpow_le_of_pow_le {x c p : ℝ} {m n : ℕ} (hn : n ≠ 0) (hx : 0 ≤ x) (hc : 0 ≤ c) (hp : p = ↑m / ↑n) (h : x ^ m ≤ c ^ n) : x ^ p ≤ c

Negative exponents without a root

The gain and cost sides of the supply floor are both x ^ (-γ). When the base sits on the right side of one these need no root at all: a base above one makes the power at most one, and a base below one makes it at most the reciprocal (for γ ≤ 1). That covers the COST side of every calibration, where the base is η + income - t with t small. The GAIN side, where the base is small and the bound has to be large, is where a root is genuinely needed — le_rpow_neg_of_rpow_le hands it back to rpow_le_of_pow_le.

theorem LeanEconomics.rpow_neg_le_one_of_one_le {x γ : ℝ} (hx : 1 ≤ x) (hγ : 0 ≤ γ) : x ^ (-γ) ≤ 1

A base of at least one makes the negative power at most one.

theorem LeanEconomics.rpow_neg_le_inv_of_le_one {x γ : ℝ} (hx : 0 < x) (hx1 : x ≤ 1) (hγ : γ ≤ 1) : x ^ (-γ) ≤ x⁻¹

A base of at most one makes the negative power at most the reciprocal, when γ ≤ 1.

theorem LeanEconomics.le_rpow_neg_of_rpow_le {x q γ : ℝ} (hx : 0 < x) (hq : 0 < q) (h : x ^ γ ≤ q⁻¹) : q ≤ x ^ (-γ)

The gain side: a bound on x ^ γ from above is a bound on x ^ (-γ) from below.

theorem LeanEconomics.le_rpow_of_pow_le {x c p : ℝ} {m n : ℕ} (hn : n ≠ 0) (hx : 0 ≤ x) (hc : 0 ≤ c) (hp : p = ↑m / ↑n) (h : c ^ n ≤ x ^ m) : c ≤ x ^ p

Secant slopes of CRRA, bounded below

theorem LeanEconomics.crra_marginal_bound {γ R : ℝ} (hγ : 0 < γ) {c d : ℝ} (hd : 0 < d) (hdc : d ≤ c) (hcR : c ≤ R) : R ^ (-γ) * (c - d) ≤ crraUtility γ c - crraUtility γ d

The secant slope of CRRA on (0, R] is at least R ^ (-γ). This is log_marginal_bound for every γ > 0 at once: at γ = 1 the bound R ^ (-1) is 1 / R.

theorem LeanEconomics.crra_marginal_bound_zero {γ R : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) {c : ℝ} (hc : 0 < c) (hcR : c ≤ R) : R ^ (-γ) * (c - 0) ≤ crraUtility γ c - crraUtility γ 0

The bound reaches d = 0 when γ < 1. Utility is finite there, so the statement makes sense, and the first unit of consumption is worth at least as much as any later one. This is the case log cannot have.

theorem LeanEconomics.crra_marginal_bound_Ici {γ R : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) {c d : ℝ} (hd : d ∈ Set.Ici 0) (hdc : d ≤ c) (hcR : c ≤ R) : R ^ (-γ) * (c - d) ≤ crraUtility γ c - crraUtility γ d

The slope bound on all of Ici 0, which is the domain CES with γ < 1 uses.

theorem LeanEconomics.crra_sub_ge {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) {c d : ℝ} (hc : 0 ≤ c) (hd : 0 ≤ d) : (c + d) ^ (-γ) * d ≤ crraUtility γ (c + d) - crraUtility γ c

The gain from d extra consumption, bounded below. Taking R = c + d in crra_marginal_bound gives the CES form of log_sub_log_ge.

theorem LeanEconomics.crra_marginal_bound_above {γ : ℝ} (hγ : 0 < γ) {c d : ℝ} (hd : 0 < d) (hdc : d ≤ c) : crraUtility γ c - crraUtility γ d ≤ d ^ (-γ) * (c - d)

The secant slope of CRRA on [d, c] is at most d ^ (-γ). The mirror image of crra_marginal_bound, and what caps the COST of saving.

theorem LeanEconomics.crra_cost_of_saving {γ : ℝ} (hγ : 0 < γ) {m h R b : ℝ} (hh0 : 0 < h) (hhm : h < m) (hmR : m ≤ R) (hb0 : 0 ≤ b) (hbh : b ≤ h) : crraUtility γ (R - b) - crraUtility γ (R - h) ≤ (m - h) ^ (-γ) * h

The cost of saving h, capped uniformly in resources. Resources are at least m, so what is left after saving is at least m - h, and marginal utility there is the largest that can apply. The log form of the same bound is log (m / (m - h)).

Secant slopes of CRRA, bounded above

noncomputable def LeanEconomics.crraSlopeBound (γ m : ℝ) : ℝ

The closed form of slopeBound (crraUtility γ) at the income floor for γ ≠ 1. The literal expression below evaluates to zero at γ = 1 under total real division, so the logarithmic case uses log_slopeBoundU separately.

Equations

• LeanEconomics.crraSlopeBound γ m = 2 * m ^ (-γ) * (1 - (2 ^ (1 - γ))⁻¹) / (1 - γ)

theorem LeanEconomics.slopeBound_crraUtility {γ m : ℝ} (hγ : γ ≠ 1) (hm : 0 < m) : slopeBound (crraUtility γ) m = crraSlopeBound γ m

theorem LeanEconomics.crraSlopeBound_nonneg {γ m : ℝ} (hm : 0 ≤ m) : 0 ≤ crraSlopeBound γ m

theorem LeanEconomics.IncomeFluctuation.policy_le_of_marginal_bound {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {m : ℝ} (hm : 0 < m) (hmarg : ∀ (c d : ℝ), d ∈ P.dom → d ≤ c → c ≤ P.maxConsumption → m * (c - d) ≤ P.u c - P.u d) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : P.policy (a, z) ≤ 2 * P.deviationGap / m

A uniform bound on saving from a uniform marginal bound. Deviate to half the optimal saving: the extra consumption is worth at least m per unit, and concavity of the continuation caps what the forgone saving could have repaid at deviationGap, whatever the state.

The log development could not use this, because for log the available m at resources R is 1 / R, which is not uniform. It is stated generically anyway — log gets the version with m = 1 / maxConsumption, which is uniform after all, just weaker than what the multiplicative argument extracts. For CES with γ < 1 the uniform m = maxConsumption ^ (-γ) is all there is, and it is enough.

The oscillation gap

deviationGap = 2 β ‖V‖ is not translation-invariant. For CES, subtracting 1 / (1-γ) from c ^ (1-γ) / (1-γ) gives the normalization that tends to log c as γ → 1 for positive c; it is not an equality with log c at a fixed γ ≠ 1. A value-norm bound is sensitive to that additive utility constant. The comparisons here use DIFFERENCES of continuation values, so an oscillation bound avoids this normalization dependence: (u maxConsumption - u minConsumption) / (1 - β).

noncomputable def LeanEconomics.IncomeFluctuation.oscGap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) : ℝ

The spread of the value function, from the two constant plans.

Equations

• P.oscGap = P.oscSpread

theorem LeanEconomics.IncomeFluctuation.oscGap_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) : 0 ≤ P.oscGap

theorem LeanEconomics.IncomeFluctuation.cont_sub_le_oscGap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (z : Z) (x y : ℝ) : P.cont z x - P.cont z y ≤ P.oscGap

The continuation value moves by at most the oscillation gap, whatever the two saving levels. This is what replaces 2 ‖V‖ in every comparison.

noncomputable def LeanEconomics.IncomeFluctuation.crraLipschitz {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (γ : ℝ) : ℝ

The nonlogarithmic CRRA Lipschitz constant, mirroring logLipschitz.

Equations

• P.crraLipschitz γ = LeanEconomics.crraSlopeBound γ P.minConsumption * (1 + P.interest) / (1 - ↑P.discount * (1 + P.interest))

theorem LeanEconomics.IncomeFluctuation.crraLipschitz_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hβR : ↑P.discount * (1 + P.interest) < 1) : 0 ≤ P.crraLipschitz γ

theorem LeanEconomics.IncomeFluctuation.crra_valueFunction_lipschitz {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ : γ ≠ 1) (hu : P.u = crraUtility γ) (hβR : ↑P.discount * (1 + P.interest) < 1) (z : Z) (x : ℝ) : x ∈ Set.Icc 0 assetCap → ∀ y ∈ Set.Icc 0 assetCap, |P.toExtended.valueFunction (x, z) - P.toExtended.valueFunction (y, z)| ≤ P.crraLipschitz γ * |x - y|

The value function is Lipschitz with the explicit CRRA constant for γ ≠ 1.

theorem LeanEconomics.IncomeFluctuation.crra_policy_eq_zero_of_resources {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) (hb : P.Bounded) (hu : P.u = crraUtility γ) (hβR : ↑P.discount * (1 + P.interest) < 1) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc 0 assetCap) (hlt : ↑P.discount * P.crraLipschitz γ < P.resources s ^ (-γ)) : P.policy s = 0

The borrowing constraint binds where resources are small, CES version. The threshold is resources ^ (-γ) where the log version had 1 / resources.

theorem LeanEconomics.IncomeFluctuation.crra_policy_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) (hb : P.Bounded) (hu : P.u = crraUtility γ) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : P.policy (a, z) ≤ 2 * P.deviationGap * P.maxConsumption ^ γ

The CES saving bound in closed form. Saving never exceeds 2 · deviationGap · maxConsumption ^ γ, whatever the state.

theorem LeanEconomics.IncomeFluctuation.crra_exists_decline {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) (hb : P.Bounded) (hu : P.u = crraUtility γ) (z : Z) : ∃ (ā : ℝ), ∀ a ∈ Set.Icc 0 assetCap, ā < a → P.policy (a, z) < a

The natural asset bound for CES. A uniform cap on saving is a decline condition outright: above it, assets fall. No linear consumption bound and no exp in sight.

theorem LeanEconomics.IncomeFluctuation.crra_cont_sub_ge_gen {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hpc : P.PositiveConsumption) (z z₀ : Z) {x y : ℝ} (hx : x ∈ Set.Icc 0 assetCap) (hy : y ∈ Set.Icc 0 assetCap) (hxy : x ≤ y) : P.transitionMatrix z z₀ * ((P.income z₀ + (1 + P.interest) * y) ^ (-γ) * ((1 + P.interest) * (y - x))) ≤ P.cont z y - P.cont z x

The continuation's gain between two saving levels, CES version. Where the log form carries log (1 + R·(y-x) / (income + R·x)), this carries (income + R·y) ^ (-γ) · R·(y-x): the extra resources, valued at the marginal utility of the largest consumption they could buy.

theorem LeanEconomics.IncomeFluctuation.crra_cont_sub_ge {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hpc : P.PositiveConsumption) (z z₀ : Z) {h : ℝ} (hh : h ∈ Set.Icc 0 assetCap) : P.transitionMatrix z z₀ * ((P.income z₀ + (1 + P.interest) * h) ^ (-γ) * ((1 + P.interest) * h)) ≤ P.cont z h - P.cont z 0

The continuation's gain from zero, CES version.

The sharp decline constant

crra_policy_le bounds saving by a constant, which is enough for a natural asset bound but far too weak for the corner condition to meet it: the corner needs the threshold to be comparable to the LOW income, and an absolute bound does not shrink with it. The log development gets a PROPORTIONAL bound instead, c ≥ R / (1 + 2G), whose decline threshold is proportional to income.

The CES analogue deviates to θ times the optimal saving rather than to half of it, and prices the extra consumption at the margin where it lands: b ≤ (β · oscGap / θ) · (c + (1-θ) b) ^ γ. Taking θ near 1 makes the right-hand side nearly (β · oscGap) c ^ γ, proportional to consumption, which is the shape the decline condition needs.

theorem LeanEconomics.IncomeFluctuation.crra_policy_le_mul {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ θ : ℝ} (hγ0 : 0 < γ) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hu : P.u = crraUtility γ) (hpc : P.PositiveConsumption) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : P.policy (a, z) ≤ ↑P.discount * P.oscGap / θ * (P.consumption (a, z) (P.policy (a, z)) + (1 - θ) * P.policy (a, z)) ^ γ

The proportional CES bound on saving.

theorem LeanEconomics.IncomeFluctuation.crra_policy_lt_self {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ θ : ℝ} (hγ0 : 0 < γ) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hθr : θ ≤ 1 + P.interest) (hu : P.u = crraUtility γ) (hpc : P.PositiveConsumption) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) (hlt : ↑P.discount * P.oscGap / θ * (P.income z + (1 + P.interest - θ) * assetCap) ^ γ < a) : P.policy (a, z) < a

Assets fall above an explicit threshold, in the income state that matters. The threshold is (β · oscGap / θ) · (income z + (1 + r - θ) · assetCap) ^ γ. It depends on the income of the selected state and the residual gross return 1 + r - θ; its strict comparison with current assets is an explicit hypothesis.

The asset cap never binds

not_concaveOn_consumptionFn_of_cap_binds makes Carroll and Kimball's conclusion FALSE wherever saving reaches the cap, so the cap is the obstruction to Light's uniqueness argument, not the utility class. It can be removed by calibration rather than by weakening the theory: run crra_policy_le_mul by contradiction. If saving reached the cap then consumption would be at most maxIncome + (1 + r - θ) · assetCap. The displayed inequality makes the saving upper bound at that quantity strictly smaller than the cap.

The criterion evaluates the proportional bound at the consumption quantity implied by cap binding. The theorem retains the displayed numerical inequality as an explicit calibration hypothesis.

Related literature: Marcet, Obiols-Homs and Weil (2007), Incomplete Markets, Labor Supply and Capital Accumulation. The sufficient criterion below is specific to this capped household model: it uses the displayed quantitative inequality and positive optimal consumption. Its fixed-point and iterative versions share the same comparison argument.

theorem LeanEconomics.IncomeFluctuation.crra_policy_lt_assetCap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ θ : ℝ} (hγ0 : 0 < γ) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hu : P.u = crraUtility γ) (hpc : P.PositiveConsumption) (hlt : ↑P.discount * P.oscGap / θ * (P.maxIncome + (1 + P.interest - θ) * assetCap) ^ γ < assetCap) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : P.policy (a, z) < assetCap

Saving never reaches the asset cap.

theorem LeanEconomics.IncomeFluctuation.no_flat_at_cap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ θ : ℝ} (hγ0 : 0 < γ) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hu : P.u = crraUtility γ) (hpc : P.PositiveConsumption) (hlt : ↑P.discount * P.oscGap / θ * (P.maxIncome + (1 + P.interest - θ) * assetCap) ^ γ < assetCap) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) (z : Z) : P.policy (a, z) ≠ assetCap

The disproof of Carroll and Kimball is disarmed. Where saving never reaches the cap, the hypothesis of not_concaveOn_consumptionFn_of_cap_binds -- a flat stretch of the policy at the top of the asset region -- cannot occur, so nothing in this development contradicts concavity of the consumption function. That is not a proof of concavity; it is the removal of the obstruction that made one impossible.

theorem LeanEconomics.IncomeFluctuation.crra_policy_ge_of_gain {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ : 0 < γ) (hu : P.u = crraUtility γ) (hpc : P.PositiveConsumption) (z₁ : Z) {h : ℝ} (hh0 : 0 < h) (hhcap : h ≤ assetCap) (hhinc : h < P.income z₁) (hgain : (P.income z₁ - h) ^ (-γ) * h < ↑P.discount * (P.cont z₁ h - P.cont z₁ (h / 2))) {a : ℝ} (ha : a ∈ Set.Icc 0 assetCap) : h / 2 ≤ P.policy (a, z₁)

A quantitative CES saving floor, the form the sign-change argument consumes.

theorem LeanEconomics.IncomeFluctuation.crra_aggregateCapital_pos_of_primitives {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) [MeasurableSpace Z] [BorelSpace Z] {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hpc : P.PositiveConsumption) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) {z₁ z₀ : Z} {p₀ : ℝ} (hp0 : 0 < p₀) (hp : ∀ (z : Z), p₀ ≤ P.transitionMatrix z z₁) {h : ℝ} (hh0 : 0 < h) (hhcap : h ≤ assetCap) (hhinc : h < P.income z₁) (hgain : (P.income z₁ - h) ^ (-γ) * h < ↑P.discount * (P.transitionMatrix z₁ z₀ * ((P.income z₀ + (1 + P.interest) * h) ^ (-γ) * ((1 + P.interest) * h)))) : 0 < P.aggregateCapital μ

Positive aggregate capital for CES, from primitives alone. The log condition log (m / (m - h)) < β · P z₁ z₀ · log (1 + R h / income z₀) becomes (m - h) ^ (-γ) · h < β · P z₁ z₀ · (income z₀ + R h) ^ (-γ) · R h: the saved unit priced at the margin where consumption is lowest, against its return in the bad state.