Consumption at the optimum is bounded away from zero

Positivity of optimal consumption is already known pointwise: a zero would make the reward ⊥ and the value could not be real. What is needed for comparative statics is a UNIFORM bound, a single δ > 0 working at every state.

The bound proved here is explicit rather than compactness-based, and that is the whole point. A compactness argument would say that optimal consumption is continuous and positive on a compact state space, hence has a positive minimum — true, and recorded below as a sanity check, but useless for the parametric problem. There the bound has to be uniform over an interval of interest rates as well, and the corresponding compactness argument would need joint continuity in (r, s), which is precisely what the bound is wanted to prove. It would be circular.

The explicit route avoids that. At the optimum the Bellman equation reads

V s = u c* + β · E[V]

so u c* ≥ -(1 + β)‖V‖, a lower bound on the UTILITY of optimal consumption depending only on the sup norm of the value function. Since u falls to -∞ at zero, that pins consumption away from zero. Nothing in the argument refers to the state, so the bound is automatically uniform in the state; and when r varies, ‖V‖ is controlled by the reward bounds, which are themselves uniform over a compact interval of rates.

theorem LeanEconomics.IncomeFluctuation.abs_expectation_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (a : ℝ) (z : Z) : |∑ z' : Z, P.transitionMatrix z z' * P.toExtended.valueFunction (a, z')| ≤ ‖P.toExtended.valueFunction‖

The expected continuation value is bounded by the sup norm of the value function.

theorem LeanEconomics.IncomeFluctuation.le_utility_consumption_policy {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) : -(1 + ↑P.discount) * ‖P.toExtended.valueFunction‖ ≤ P.u (P.consumption s (P.policy s))

The utility of optimal consumption is bounded below, by a quantity depending only on the sup norm of the value function — not on the state.

theorem LeanEconomics.IncomeFluctuation.le_utility_consumption_policy_of_bounds {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) : -(1 + ↑P.discount) * (max |P.u P.minConsumption| |P.u P.maxConsumption| / (1 - ↑P.discount)) ≤ P.u (P.consumption s (P.policy s))

The utility bound in terms of the reward bounds alone — no fixed point on the right.

This is the form that survives into a parametric statement. A family of programs sharing a utility function and a common bound on max |u minConsumption| |u maxConsumption| / (1 - β) has a common L, and then exists_lower_bound_of_utility_ge hands it a single δ.

theorem LeanEconomics.IncomeFluctuation.exists_lower_bound_of_utility_ge {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hd : P.Unbounded) (L : ℝ) (hL : ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → L ≤ P.u (P.consumption s (P.policy s))) : ∃ δ > 0, ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → δ ≤ P.consumption s (P.policy s)

From a lower bound on utility to a lower bound on consumption. The resulting δ depends only on u and on L — NOT on the state, and not on anything that moves with the interest rate. That is the property the parametric argument needs.

theorem LeanEconomics.IncomeFluctuation.exists_consumption_policy_lower_bound {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hd : P.Unbounded) : ∃ δ > 0, ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → δ ≤ P.consumption s (P.policy s)

Consumption at the optimum is bounded away from zero, uniformly in the state.

No compactness and no continuity of the policy are used, which is exactly what lets the same argument run uniformly in the interest rate: a compactness proof would need joint continuity in (r, s), which is what such a bound is wanted to prove in the first place.

A choice set that does not move

The Bellman operator maximises over Icc 0 (maxSaving s), an interval whose RIGHT ENDPOINT moves with the interest rate. Comparing the operator at two rates therefore means comparing suprema over two different sets, which is the awkward part of any such estimate.

Writing the choice as a fraction θ ∈ [0,1] of the maximum feasible saving removes the problem: the choice set becomes [0,1] for every rate and every state, and all the rate dependence moves into the objective, where it can be estimated pointwise. |sSup f - sSup g| over a COMMON set is bounded by the pointwise gap; over two different sets it is not.

theorem LeanEconomics.IncomeFluctuation.assetFloor_le_maxSaving {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : assetFloor ≤ P.maxSaving s

noncomputable def LeanEconomics.IncomeFluctuation.savingRoom {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : ℝ

How much saving room the household has above the borrowing limit.

Equations

• P.savingRoom s = P.maxSaving s - assetFloor

theorem LeanEconomics.IncomeFluctuation.savingRoom_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : 0 ≤ P.savingRoom s

theorem LeanEconomics.IncomeFluctuation.feasible_eq_image {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.toExtended.feasible s = (fun (θ : ℝ) => assetFloor + θ * P.savingRoom s) '' Set.Icc 0 1

The feasible set is the image of the FIXED interval [0,1] under the affine map that takes θ to the borrowing limit plus a fraction θ of the saving room. With assetFloor = 0 this is just scaling by the maximum feasible saving.

theorem LeanEconomics.IncomeFluctuation.maxE_eq_sSup_unit {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (s : ℝ × Z) : P.toExtended.maxE v s = sSup ((fun (θ : ℝ) => P.toExtended.objectiveE v s (assetFloor + θ * P.savingRoom s)) '' Set.Icc 0 1)

The one-period value as a supremum over a fixed interval.

theorem LeanEconomics.IncomeFluctuation.minConsumption_mul_le_consumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {θ : ℝ} (hθ : θ ∈ Set.Icc 0 1) (s : ℝ × Z) : P.minConsumption * (1 - θ) ≤ P.consumption s (assetFloor + θ * P.savingRoom s)

Consumption is bounded below by a quantity free of the state and the interest rate.

Along the reparametrised choice, consumption is at least minConsumption * (1 - θ). The bound holds because the saving room never exceeds what is left after servicing the debt, so taking a fraction θ of it leaves at least a fraction 1 - θ.

This is the uniformity that makes the parametric estimate possible: it does not mention the state, and the only model data it mentions -- minConsumption -- does not move with the interest rate. Away from θ = 1 the reward is therefore real and bounded, so the -∞ cannot interfere.