Consumption and savings with period utility unbounded below

Period utility may fall to -∞ at zero consumption, which covers σ ≥ 1 in the CES family and log utility. Assets are capped.

This file used to use a floor

It replaced u by max floor u to keep the reward real-valued and bounded, and then had to prove the floor never binds: bounds on the value function above and below, then floor_lt_rewardFn_optimal, then cFloor_le_consumption_optimal. Four structure fields (floor, cFloor, u_cFloor_le_floor, floor_lt) and about a hundred and fifty lines of proof existed only to establish that a device introduced for technical reasons was invisible in the answer.

With LeanEconomics.DynamicProgramming.Extended the reward is simply -∞ there. All of that machinery is gone. What replaces it is a single hypothesis, tendsto_atBot_u, saying utility falls to -∞ at zero consumption -- which is not an extra assumption at all, since it is precisely the situation that forced the floor.

Positive consumption at the optimum now comes for free. It used to be the conclusion of the floor argument. Now it follows from the value function being real: if the optimal action left zero consumption the reward would be -∞, so the value would be -∞, and it is not. That is exists_optimal_saving, which returns 0 < consumption as part of its conclusion rather than requiring a separate development.

What is unchanged

Consumption is still clamped above, and assets are still capped. Neither has anything to do with -∞; both are the ordinary requirement that the reward be bounded above, which the weighted theory addresses separately.

Cash on hand is now computed from max 0 a rather than a. With a floor, a state with negative cash on hand received the floor value; without one it would receive -∞, which the framework does not allow. Reading assets as nonnegative keeps the value finite everywhere, and changes nothing on [0, assetCap], which is where the results are stated.

theorem LeanEconomics.strictConcaveOn_neg_inv : StrictConcaveOn ℝ (Set.Ioi 0) fun (c : ℝ) => -c⁻¹

c ↦ -1/c, that is CES utility at σ = 2, is strictly concave on the positives. Mathlib has no convexity lemma for x⁻¹, and its rpow convexity results cover only exponents ≥ 1, so this is proved by hand: the difference of the two sides is a * b * (x - y)² / (x * y * (a * x + b * y)).

structure LeanEconomics.ConsumptionSavingsUnbounded : Type

A consumption-savings problem whose period utility is unbounded below.

• income : ℝ

  Constant labour income.

• interest : ℝ

  The interest rate on assets.

• assetCap : ℝ

  The upper bound imposed on asset holdings.

• discount : NNReal

  The discount factor.

• u : ℝ → ℝ

  Period utility, required to behave only on positive consumption.

• income_pos : 0 < self.income
• interest_gt_neg_one : 0 < 1 + self.interest
• assetCap_nonneg : 0 ≤ self.assetCap
• discount_lt_one : self.discount < 1
• continuousOn_u : ContinuousOn self.u (Set.Ioi 0)
• monotoneOn_u : MonotoneOn self.u (Set.Ioi 0)
• tendsto_atBot_u : Filter.Tendsto self.u (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

  Utility falls to -∞ as consumption vanishes. This single hypothesis replaces the four fields the floored version needed.

• strictConcaveOn_u : StrictConcaveOn ℝ (Set.Ioi 0) self.u

  Diminishing marginal utility. Needed for a unique optimal policy, hence for an agent distribution to be a well-defined object.

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.resources (P : ConsumptionSavingsUnbounded) (a : ℝ) : ℝ

Cash on hand, with assets read as nonnegative.

Equations

• P.resources a = P.income + (1 + P.interest) * max 0 a

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.maxConsumption (P : ConsumptionSavingsUnbounded) : ℝ

The largest consumption the capped problem allows.

Equations

• P.maxConsumption = P.income + (1 + P.interest) * P.assetCap

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.maxSaving (P : ConsumptionSavingsUnbounded) (a : ℝ) : ℝ

The largest asset holding that can be carried forward.

Equations

• P.maxSaving a = max 0 (min P.assetCap (P.resources a))

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.consumption (P : ConsumptionSavingsUnbounded) (a a' : ℝ) : ℝ

Consumption on the budget line.

Equations

• P.consumption a a' = P.resources a - a'

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.rewardFn (P : ConsumptionSavingsUnbounded) (p : ℝ × ℝ) : EReal

The reward: utility of consumption clamped above, and -∞ where consumption vanishes. No floor.

Equations

• P.rewardFn p = LeanEconomics.extendBot P.u (min P.maxConsumption (P.consumption p.1 p.2))

theorem LeanEconomics.ConsumptionSavingsUnbounded.income_le_resources (P : ConsumptionSavingsUnbounded) (a : ℝ) : P.income ≤ P.resources a

theorem LeanEconomics.ConsumptionSavingsUnbounded.resources_pos (P : ConsumptionSavingsUnbounded) (a : ℝ) : 0 < P.resources a

theorem LeanEconomics.ConsumptionSavingsUnbounded.income_le_maxConsumption (P : ConsumptionSavingsUnbounded) : P.income ≤ P.maxConsumption

theorem LeanEconomics.ConsumptionSavingsUnbounded.maxConsumption_pos (P : ConsumptionSavingsUnbounded) : 0 < P.maxConsumption

theorem LeanEconomics.ConsumptionSavingsUnbounded.continuous_resources (P : ConsumptionSavingsUnbounded) : Continuous P.resources

theorem LeanEconomics.ConsumptionSavingsUnbounded.continuous_maxSaving (P : ConsumptionSavingsUnbounded) : Continuous P.maxSaving

theorem LeanEconomics.ConsumptionSavingsUnbounded.continuous_rewardFn (P : ConsumptionSavingsUnbounded) : Continuous P.rewardFn

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.toExtended (P : ConsumptionSavingsUnbounded) : ExtendedProgram ℝ ℝ

The problem as a dynamic program with an extended-real reward.

Equations

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

@[simp]

theorem LeanEconomics.ConsumptionSavingsUnbounded.feasible_eq (P : ConsumptionSavingsUnbounded) (a : ℝ) : P.toExtended.feasible a = Set.Icc 0 (P.maxSaving a)

theorem LeanEconomics.ConsumptionSavingsUnbounded.consumption_le_maxConsumption (P : ConsumptionSavingsUnbounded) {a a' : ℝ} (ha : a ∈ Set.Icc 0 P.assetCap) (ha' : 0 ≤ a') : P.consumption a a' ≤ P.maxConsumption

theorem LeanEconomics.ConsumptionSavingsUnbounded.exists_optimal_saving (P : ConsumptionSavingsUnbounded) {a : ℝ} (ha : a ∈ Set.Icc 0 P.assetCap) : ∃ a' ∈ Set.Icc 0 (P.maxSaving a), 0 < P.consumption a a' ∧ P.toExtended.valueFunction a = P.u (P.consumption a a') + ↑P.discount * P.toExtended.valueFunction a'

The Bellman equation, with honest utility and positive consumption. That consumption is positive at the optimum is not assumed and not separately proved: a zero would make the reward -∞ and hence the value -∞, and the value is real.

Concavity and the optimal policy

The σ < 1 model gets concavity from the general criterion in LeanEconomics.DynamicProgramming.Bellman. That criterion is stated for a real-valued reward and does not apply here, because ConcaveOn over EReal would need an ordered module structure that does not sit well. The way round is that the -∞ never appears where it matters: at an optimum consumption is strictly positive, so every value the argument touches is finite, and the reasoning can be carried out in the reals.

theorem LeanEconomics.ConsumptionSavingsUnbounded.resources_eq_affine (P : ConsumptionSavingsUnbounded) {x : ℝ} (hx : 0 ≤ x) : P.resources x = P.income + (1 + P.interest) * x

theorem LeanEconomics.ConsumptionSavingsUnbounded.resources_affine_comb (P : ConsumptionSavingsUnbounded) {x y θ φ : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hθ : 0 ≤ θ) (hφ : 0 ≤ φ) (hθφ : θ + φ = 1) : P.resources (θ * x + φ * y) = θ * P.resources x + φ * P.resources y

theorem LeanEconomics.ConsumptionSavingsUnbounded.maxSaving_le_assetCap (P : ConsumptionSavingsUnbounded) (a : ℝ) : P.maxSaving a ≤ P.assetCap

theorem LeanEconomics.ConsumptionSavingsUnbounded.feasible_subset_region (P : ConsumptionSavingsUnbounded) {x a : ℝ} (ha : a ∈ P.toExtended.feasible x) : a ∈ Set.Icc 0 P.assetCap

theorem LeanEconomics.ConsumptionSavingsUnbounded.maxSaving_eq (P : ConsumptionSavingsUnbounded) (x : ℝ) : P.maxSaving x = min P.assetCap (P.resources x)

theorem LeanEconomics.ConsumptionSavingsUnbounded.feasible_convex (P : ConsumptionSavingsUnbounded) {x y : ℝ} (hx : x ∈ Set.Icc 0 P.assetCap) (hy : y ∈ Set.Icc 0 P.assetCap) {ax ay θ φ : ℝ} (hax : ax ∈ P.toExtended.feasible x) (hay : ay ∈ P.toExtended.feasible y) (hθ : 0 ≤ θ) (hφ : 0 ≤ φ) (hθφ : θ + φ = 1) : θ * ax + φ * ay ∈ P.toExtended.feasible (θ * x + φ * y)

theorem LeanEconomics.ConsumptionSavingsUnbounded.consumption_pos_of_ne_bot (P : ConsumptionSavingsUnbounded) {x a : ℝ} (h : P.toExtended.reward (x, a) ≠ ⊥) : 0 < P.consumption x a

A finite reward means strictly positive consumption.

theorem LeanEconomics.ConsumptionSavingsUnbounded.reward_eq_coe (P : ConsumptionSavingsUnbounded) {x a : ℝ} (hx : x ∈ Set.Icc 0 P.assetCap) (ha : a ∈ P.toExtended.feasible x) (hc : 0 < P.consumption x a) : P.toExtended.reward (x, a) = ↑(P.u (P.consumption x a))

Where consumption is positive the reward is an ordinary real utility.

theorem LeanEconomics.ConsumptionSavingsUnbounded.bellmanFn_eq_of_optimal (P : ConsumptionSavingsUnbounded) {v : BoundedContinuousFunction ℝ ℝ} {x a : ℝ} (hx : x ∈ Set.Icc 0 P.assetCap) (ha : a ∈ P.toExtended.feasible x) (heq : P.toExtended.objectiveE v x a = ↑(P.toExtended.bellmanFn v x)) : 0 < P.consumption x a ∧ P.toExtended.bellmanFn v x = P.u (P.consumption x a) + ↑P.discount * v a

At an optimum consumption is positive and the value is an ordinary real expression.

theorem LeanEconomics.ConsumptionSavingsUnbounded.concaveOn_bellman (P : ConsumptionSavingsUnbounded) (v : BoundedContinuousFunction ℝ ℝ) (hv : ConcaveOn ℝ (Set.Icc 0 P.assetCap) ⇑v) : ConcaveOn ℝ (Set.Icc 0 P.assetCap) ⇑(P.toExtended.bellman v)

The Bellman operator preserves concavity on the region.

theorem LeanEconomics.ConsumptionSavingsUnbounded.concaveOn_valueFunction (P : ConsumptionSavingsUnbounded) : ConcaveOn ℝ (Set.Icc 0 P.assetCap) ⇑P.toExtended.valueFunction

The value function is concave on [0, assetCap], for utility unbounded below.

theorem LeanEconomics.ConsumptionSavingsUnbounded.optimal_action_unique (P : ConsumptionSavingsUnbounded) {x : ℝ} (hx : x ∈ Set.Icc 0 P.assetCap) {a₀ a₁ : ℝ} (h₀ : a₀ ∈ P.toExtended.feasible x) (h₁ : a₁ ∈ P.toExtended.feasible x) (hm₀ : P.toExtended.objectiveE P.toExtended.valueFunction x a₀ = ↑(P.toExtended.bellmanFn P.toExtended.valueFunction x)) (hm₁ : P.toExtended.objectiveE P.toExtended.valueFunction x a₁ = ↑(P.toExtended.bellmanFn P.toExtended.valueFunction x)) : a₀ = a₁

The optimal action is unique. Two distinct optimal actions would be beaten by their midpoint, since utility is strictly concave and the continuation value concave.

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.policy (P : ConsumptionSavingsUnbounded) (x : ℝ) : ℝ

The optimal saving choice. By optimal_action_unique this is the optimal choice on the region, not merely an optimal choice.

Equations

• P.policy x = Classical.choose ⋯

theorem LeanEconomics.ConsumptionSavingsUnbounded.policy_mem (P : ConsumptionSavingsUnbounded) (x : ℝ) : P.policy x ∈ P.toExtended.feasible x

theorem LeanEconomics.ConsumptionSavingsUnbounded.policy_optimal (P : ConsumptionSavingsUnbounded) (x : ℝ) : P.toExtended.objectiveE P.toExtended.valueFunction x (P.policy x) = ↑(P.toExtended.bellmanFn P.toExtended.valueFunction x)

theorem LeanEconomics.ConsumptionSavingsUnbounded.policy_mem_region (P : ConsumptionSavingsUnbounded) (x : ℝ) : P.policy x ∈ Set.Icc 0 P.assetCap

theorem LeanEconomics.ConsumptionSavingsUnbounded.consumption_policy_pos (P : ConsumptionSavingsUnbounded) {x : ℝ} (hx : x ∈ Set.Icc 0 P.assetCap) : 0 < P.consumption x (P.policy x)

Consumption under the optimal policy is strictly positive: the household never starves itself. With a floor this had to be proved; here it follows from the value being real.

theorem LeanEconomics.ConsumptionSavingsUnbounded.eq_policy_of_optimal (P : ConsumptionSavingsUnbounded) {x : ℝ} (hx : x ∈ Set.Icc 0 P.assetCap) {a : ℝ} (ha : a ∈ P.toExtended.feasible x) (hopt : P.toExtended.objectiveE P.toExtended.valueFunction x a = ↑(P.toExtended.bellmanFn P.toExtended.valueFunction x)) : a = P.policy x

Any optimal action is the policy.

theorem LeanEconomics.ConsumptionSavingsUnbounded.valueFunction_eq_policy (P : ConsumptionSavingsUnbounded) {x : ℝ} (hx : x ∈ Set.Icc 0 P.assetCap) : P.toExtended.valueFunction x = P.u (P.consumption x (P.policy x)) + ↑P.discount * P.toExtended.valueFunction (P.policy x)

The Bellman equation at the policy, with honest utility and positive consumption.

theorem LeanEconomics.ConsumptionSavingsUnbounded.argmax_eq_singleton (P : ConsumptionSavingsUnbounded) {x : ℝ} (hx : x ∈ Set.Icc 0 P.assetCap) : argmax (P.toExtended.objectiveE P.toExtended.valueFunction) P.toExtended.feasible x = {P.policy x}

The maximiser set is exactly the policy.

theorem LeanEconomics.ConsumptionSavingsUnbounded.continuousOn_policy (P : ConsumptionSavingsUnbounded) : ContinuousOn P.policy (Set.Icc 0 P.assetCap)

The optimal policy is continuous on the region, for utility unbounded below.

Utilities that qualify

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.crra (σ c : ℝ) : ℝ

CES period utility.

Equations

• LeanEconomics.ConsumptionSavingsUnbounded.crra σ c = c ^ (1 - σ) / (1 - σ)

theorem LeanEconomics.ConsumptionSavingsUnbounded.continuousOn_crra {σ : ℝ} : ContinuousOn (crra σ) (Set.Ioi 0)

theorem LeanEconomics.ConsumptionSavingsUnbounded.monotoneOn_crra {σ : ℝ} (hσ : 1 < σ) : MonotoneOn (crra σ) (Set.Ioi 0)

theorem LeanEconomics.ConsumptionSavingsUnbounded.continuousOn_log : ContinuousOn Real.log (Set.Ioi 0)

theorem LeanEconomics.ConsumptionSavingsUnbounded.monotoneOn_log : MonotoneOn Real.log (Set.Ioi 0)

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.calibrated : ConsumptionSavingsUnbounded

A calibration with σ = 2, where CES utility is -1 / c.

Equations

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

noncomputable def LeanEconomics.ConsumptionSavingsUnbounded.calibratedLog : ConsumptionSavingsUnbounded

A log calibration (σ = 1).

Equations

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