Comparing two interest rates

Estimates relating two household problems that share an income process and an asset cap but differ in the interest rate. These are the cross-rate ingredients of the sup-norm estimate on the Bellman operator; they are stated for two programs rather than for a family, which is more flexible and needs no indexing.

They are only expressible at all because assetCap is a structure PARAMETER: P and Q below have the same type, so their state spaces and feasible sets are directly comparable.

The trap

The obvious estimate is false as stated. Resources differ by

resources_P s - resources_Q s = (P.interest - Q.interest) * max 0 s.1

which is UNBOUNDED in the state: a household with enormous assets sees an enormous change in income from a small change in the rate. A sup-norm estimate over all states cannot come from this quantity directly.

What rescues it is that the difference is only visible through a clamp. Maximum feasible saving is min assetCap resources, so once resources exceed the cap at BOTH rates the difference is exactly zero. The difference can be nonzero only where some rate leaves resources below the cap, and that confines the state: (1 + r) * max 0 s.1 < assetCap. So wherever the estimate is not trivially zero, the offending factor is bounded — by assetCap / (1 + rlo), with rlo any lower bound on the rates considered.

That is the shape every cross-rate estimate here takes: a case split on whether the clamp binds, trivial on one side, and bounded on the other precisely because the clamp failing to bind confines the state.

theorem LeanEconomics.IncomeFluctuation.abs_min_sub_min_le (c x y : ℝ) : |min c x - min c y| ≤ |x - y|

min c · is 1-Lipschitz. A direct corollary of Mathlib's lipschitzWith_min.

theorem LeanEconomics.IncomeFluctuation.resources_sub {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P Q : IncomeFluctuation Z assetFloor assetCap} (hinc : P.income = Q.income) (s : ℝ × Z) : P.resources s - Q.resources s = (P.interest - Q.interest) * max assetFloor s.1

Resources differ by the rate gap times assets — a quantity unbounded in the state.

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

The uniform bound on the state coordinate that the confinement lemmas deliver. With a borrowing limit the coordinate can be negative, so what is bounded is its ABSOLUTE value, and the limit contributes its own modulus to the constant.

Equations

• P.stateBoundCross rlo = |assetFloor| + |assetCap| + (P.maxIncome + |assetFloor| + |assetCap|) / (1 + rlo)

theorem LeanEconomics.IncomeFluctuation.maxIncome_pos {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : 0 < P.maxIncome

theorem LeanEconomics.IncomeFluctuation.stateBoundCross_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {rlo : ℝ} (hr : 0 < 1 + rlo) : 0 ≤ P.stateBoundCross rlo

theorem LeanEconomics.IncomeFluctuation.abs_assetCap_le_stateBoundCross {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {rlo : ℝ} (hr : 0 < 1 + rlo) : |assetCap| ≤ P.stateBoundCross rlo

theorem LeanEconomics.IncomeFluctuation.abs_max_le_of_resources_lt {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P : IncomeFluctuation Z assetFloor assetCap} {rlo : ℝ} (hr : 0 < 1 + rlo) (hP : rlo ≤ P.interest) {s : ℝ × Z} (hlt : P.resources s < assetCap) : |max assetFloor s.1| ≤ P.stateBoundCross rlo

Where the cap fails to bind, the state is confined. This is what tames the unbounded factor above.

theorem LeanEconomics.IncomeFluctuation.abs_maxSaving_sub_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P Q : IncomeFluctuation Z assetFloor assetCap} (hinc : P.income = Q.income) (hmi : P.maxIncome = Q.maxIncome) {rlo : ℝ} (hr : 0 < 1 + rlo) (hP : rlo ≤ P.interest) (hQ : rlo ≤ Q.interest) (s : ℝ × Z) : |P.maxSaving s - Q.maxSaving s| ≤ |P.interest - Q.interest| * P.stateBoundCross rlo

The maximum feasible saving moves little when the interest rate does.

The bound is uniform over the whole state space, which the raw resources gap is not.

The clamped consumption gap

Harder than the saving bound in two ways. The clamp LEVEL maxConsumption now moves with the rate too, since it is maxIncome + (1 + r) * assetCap - assetFloor; and the chosen saving has to be carried along, which is where the θ reparametrisation earns its place — with the choice written as the borrowing limit plus a fraction of the saving room, the same θ can be fed to both programs.

theorem LeanEconomics.IncomeFluctuation.abs_min_sub_min_le_max (A B x y : ℝ) : |min A x - min B y| ≤ max |A - B| |x - y|

min is 1-Lipschitz in both arguments at once: lipschitzWith_min read through the product's supremum metric.

theorem LeanEconomics.IncomeFluctuation.abs_maxConsumption_sub {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P Q : IncomeFluctuation Z assetFloor assetCap} (hmax : P.maxIncome = Q.maxIncome) : |P.maxConsumption - Q.maxConsumption| = |P.interest - Q.interest| * |assetCap|

The clamp level itself moves with the rate, but only by a bounded amount.

theorem LeanEconomics.IncomeFluctuation.abs_max_le_of_consumption_lt {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P : IncomeFluctuation Z assetFloor assetCap} {rlo : ℝ} (hr : 0 < 1 + rlo) (hP : rlo ≤ P.interest) {θ : ℝ} (hθ : θ ∈ Set.Icc 0 1) {s : ℝ × Z} (hlt : P.consumption s (assetFloor + θ * P.savingRoom s) < P.maxConsumption) : |max assetFloor s.1| ≤ P.stateBoundCross rlo

Where the consumption clamp fails to bind, the state is confined. The same move as abs_max_le_of_resources_lt, one clamp further along.

theorem LeanEconomics.IncomeFluctuation.abs_clamped_consumption_sub_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P Q : IncomeFluctuation Z assetFloor assetCap} (hinc : P.income = Q.income) (hmax : P.maxIncome = Q.maxIncome) {rlo : ℝ} (hr : 0 < 1 + rlo) (hP : rlo ≤ P.interest) (hQ : rlo ≤ Q.interest) {θ : ℝ} (hθ : θ ∈ Set.Icc 0 1) (s : ℝ × Z) : |min P.maxConsumption (P.consumption s (assetFloor + θ * P.savingRoom s)) - min Q.maxConsumption (Q.consumption s (assetFloor + θ * Q.savingRoom s))| ≤ |P.interest - Q.interest| * (2 * P.stateBoundCross rlo)

The clamped consumption gap. Uniform over the state space and over the choice θ.

Assembling: from pointwise bounds to a bound on the supremum

The sup-norm estimate compares two suprema, and the reparametrisation has already made them suprema over the SAME set [0,1]. What remains is to get from a bound on the objectives to a bound on their suprema.

A naive pointwise bound would not do, and the reason is worth stating. Where consumption is tiny but positive, u of the two consumptions can differ by an arbitrary amount however close the rates are, because u falls to -∞; so

∀ θ, objective_P θ ≤ objective_Q θ + ε

is FALSE. Those actions are dominated -- consuming almost nothing is far worse than the always-available choice θ = 0 -- so they cannot affect either supremum, but a pointwise statement cannot see that.

The cutoff L is what encodes it. The hypothesis is only required at actions worth at least L, and L is separately known to sit below the other program's supremum. Actions below L are then bounded by L itself and need no comparison at all. In use, L will be the value of θ = 0, which both programs have available.

theorem LeanEconomics.IncomeFluctuation.maxE_le_of_pointwise {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P Q : IncomeFluctuation Z assetFloor assetCap} (v : BoundedContinuousFunction (ℝ × Z) ℝ) (s : ℝ × Z) (L ε : EReal) (hL : L ≤ Q.toExtended.maxE v s + ε) (h : ∀ θ ∈ Set.Icc 0 1, L ≤ P.toExtended.objectiveE v s (assetFloor + θ * P.savingRoom s) → P.toExtended.objectiveE v s (assetFloor + θ * P.savingRoom s) ≤ Q.toExtended.objectiveE v s (assetFloor + θ * Q.savingRoom s) + ε) : P.toExtended.maxE v s ≤ Q.toExtended.maxE v s + ε