The contraction, run on the compact region alone

The value function is a bounded continuous function on all of ℝ × Z, but the model only ever lives on [0, assetCap] × Z, which is forward invariant: every feasible choice lands back in it (feasible_subset_region). So the Bellman operator evaluated at a state of the region never consults the continuation value anywhere else.

That has a consequence worth exploiting. The whole contraction estimate can be run with suprema taken over the REGION rather than globally:

sup_region |V_P - V_Q| ≤ (1 - β)⁻¹ * sup_region |bellman_P V_Q - V_Q|

so comparative statics in the interest rate never needs a global sup-norm estimate. Since the agent distribution also lives on the region, this is all the equilibrium argument requires. It needs no second programme on the subtype, and no transport: it is a direct estimate on the objects already built.

The mechanism is that the reward cancels. Two continuation values fed to the same programme give objectives differing only in the discounted expectation, and the expectation samples the next asset level, which feasibility confines to the region.

def LeanEconomics.IncomeFluctuation.region {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (_P : IncomeFluctuation Z assetFloor assetCap) : Set (ℝ × Z)

The region the model lives on.

Equations

• _P.region = {s : ℝ × Z | s.1 ∈ Set.Icc assetFloor assetCap}

theorem LeanEconomics.IncomeFluctuation.isCompact_region {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : IsCompact P.region

theorem LeanEconomics.IncomeFluctuation.region_nonempty {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : P.region.Nonempty

theorem LeanEconomics.IncomeFluctuation.abs_expect_sub_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v w : BoundedContinuousFunction (ℝ × Z) ℝ} {c : ℝ} (hvw : ∀ t ∈ P.region, |v t - w t| ≤ c) {s : ℝ × Z} {a : ℝ} (ha : a ∈ P.toExtended.feasible s) : |P.toExtended.expect v (s, a) - P.toExtended.expect w (s, a)| ≤ c

The expectation only samples the region. This is forward invariance in the form the estimate needs.

theorem LeanEconomics.IncomeFluctuation.abs_bellmanFn_sub_le_region {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v w : BoundedContinuousFunction (ℝ × Z) ℝ} {c : ℝ} (hvw : ∀ t ∈ P.region, |v t - w t| ≤ c) (s : ℝ × Z) : |P.toExtended.bellmanFn v s - P.toExtended.bellmanFn w s| ≤ ↑P.discount * c

The operator contracts, measured on the region alone. The reward cancels, so the two objectives differ only in the discounted expectation, and the expectation samples the next asset level, which feasibility confines to the region.

theorem LeanEconomics.IncomeFluctuation.abs_valueFunction_sub_le_region {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P Q : IncomeFluctuation Z assetFloor assetCap} {D : ℝ} (hD : ∀ t ∈ P.region, |P.toExtended.bellmanFn Q.toExtended.valueFunction t - Q.toExtended.valueFunction t| ≤ D) {s : ℝ × Z} (hs : s ∈ P.region) : |P.toExtended.valueFunction s - Q.toExtended.valueFunction s| ≤ D / (1 - ↑P.discount)

The bridge. Two value functions differ on the region by at most the operator gap on the region, amplified by (1 - β)⁻¹. Every norm here is taken over the COMPACT REGION, so comparative statics in the interest rate never needs a global sup-norm estimate.

Since the agent distribution also lives on the region, this is all the equilibrium argument requires. Note it needs no second programme on the compact state space and no transport -- it is a direct estimate on the objects already built.

The cutoff: actions worth keeping consume a bounded amount

The pointwise comparison the sup-norm estimate needs is false at actions that consume almost nothing, because u falls to -∞ there and two nearby rates can give utilities an arbitrary distance apart. Such actions are dominated: saving nothing is always feasible and is worth at least loBound v = u minIncome - β‖v‖, which the framework already places below the supremum (le_maxE).

So it is enough to compare actions worth at least loBound v, and this section shows those actions consume at least a fixed δ > 0. The δ depends on u and on ‖v‖ only — not on the state and not on the interest rate, which is what the parametric argument needs.

theorem LeanEconomics.IncomeFluctuation.abs_expect_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (p : (ℝ × Z) × ℝ) : |P.toExtended.expect v p| ≤ ‖v‖

theorem LeanEconomics.IncomeFluctuation.le_consumption_of_cutoff {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) {δ : ℝ} (hspec : ∀ c ∈ P.dom, c < δ → P.u c < P.toExtended.loBound v - ↑P.discount * ‖v‖) {s : ℝ × Z} (hs : s ∈ P.region) {a : ℝ} (ha : a ∈ P.toExtended.feasible s) (hL : ↑(P.toExtended.loBound v) ≤ P.toExtended.objectiveE v s a) : δ ≤ P.consumption s a

Actions worth keeping consume a bounded amount, for a cutoff δ given in advance.

Separating the choice of δ from its use is what makes the bound uniform across interest rates: the hypothesis on δ mentions only u, loBound v and the discount factor, none of which move with the rate, so a single δ serves every rate.

theorem LeanEconomics.IncomeFluctuation.exists_cutoff {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hd : P.Unbounded) (v : BoundedContinuousFunction (ℝ × Z) ℝ) : ∃ δ > 0, ∀ c ∈ P.dom, c < δ → P.u c < P.toExtended.loBound v - ↑P.discount * ‖v‖

A cutoff exists, and its defining property mentions only data that does not move with the interest rate.

theorem LeanEconomics.IncomeFluctuation.exists_cutoff_consumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hd : P.Unbounded) (v : BoundedContinuousFunction (ℝ × Z) ℝ) : ∃ δ > 0, ∀ s ∈ P.region, ∀ a ∈ P.toExtended.feasible s, ↑(P.toExtended.loBound v) ≤ P.toExtended.objectiveE v s a → δ ≤ P.consumption s a

Actions worth keeping consume a bounded amount.

Uniform continuity

The two moduli the sup-norm estimate consumes. Both are uniform in the state, which is what matters; neither is uniform in the interest rate, and neither needs to be, since the rate enters only through the ARGUMENTS fed to u and to the continuation value, and those gaps are already controlled by the cross-rate lemmas.

Note Z carries only a discrete topology, with no metric, so ℝ × Z is not a metric space and uniform continuity of the continuation value cannot be taken there directly. It is taken in the asset coordinate for each income state separately and the finitely many moduli combined, which is legitimate exactly because Z is a Fintype.

theorem LeanEconomics.IncomeFluctuation.exists_modulus_u {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {lo hi ε : ℝ} (hlo : 0 < lo) (hε : 0 < ε) : ∃ η > 0, ∀ c₁ ∈ Set.Icc lo hi, ∀ c₂ ∈ Set.Icc lo hi, |c₁ - c₂| < η → |P.u c₁ - P.u c₂| < ε

Uniform continuity of utility, away from zero consumption. The interval is compact and sits inside Ioi 0, where u is assumed continuous; the cutoff is what puts consumption there.

theorem LeanEconomics.IncomeFluctuation.exists_modulus_v {Z : Type u_1} [Nonempty Z] [TopologicalSpace Z] {assetFloor assetCap : ℝ} [Finite Z] (v : BoundedContinuousFunction (ℝ × Z) ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ (z' : Z), ∀ a₁ ∈ Set.Icc assetFloor assetCap, ∀ a₂ ∈ Set.Icc assetFloor assetCap, |a₁ - a₂| < η → |v (a₁, z') - v (a₂, z')| < ε

Uniform continuity of the continuation value in the asset coordinate, uniformly over income states. The finiteness of Z is used in the PROOF, to combine the per-state moduli, though it does not appear in the statement.