Varying the interest rate

The cross-rate estimates so far take two programmes plus a hypothesis for each field they must share -- income, maximum income, minimum income, the transition matrix, the discount factor, the utility function. Six hypotheses is a signal that the wrong object is being quantified over: in the comparative statics only the INTEREST RATE varies.

withRate makes that structural. Every field except interest is inherited, so every sharing hypothesis becomes rfl and disappears from the statements, and fun r => P.withRate r _ is the family the equilibrium theorem wants.

The other content here is the step that turns the two argument gaps -- in consumption and in the continuation value -- into a comparison of objectives. It is stated with the gaps as hypotheses, so the analytic work (uniform continuity) and the arithmetic (extended reals) stay separate.

def LeanEconomics.IncomeFluctuation.withRate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : IncomeFluctuation Z assetFloor assetCap

The same household problem at a different interest rate.

Equations

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

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_interest {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).interest = r

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_income {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).income = P.income

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_maxIncome {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).maxIncome = P.maxIncome

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_minIncome {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).minIncome = P.minIncome

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_minConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).minConsumption = P.minConsumption

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_u {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).u = P.u

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_discount {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).discount = P.discount

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_transitionMatrix {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).transitionMatrix = P.transitionMatrix

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_region {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) : (P.withRate r hr).region = P.region

@[simp]

theorem LeanEconomics.IncomeFluctuation.withRate_loBound {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) (hr : P.RateOK r) (v : BoundedContinuousFunction (ℝ × Z) ℝ) : (P.withRate r hr).toExtended.loBound v = P.toExtended.loBound v

theorem LeanEconomics.IncomeFluctuation.objectiveE_le_of_gaps {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) {r r' : ℝ} (hr : P.RateOK r) (hr' : P.RateOK r') {s : ℝ × Z} (hs : s ∈ P.region) {a a' : ℝ} (ha : a ∈ (P.withRate r hr).toExtended.feasible s) (ha' : a' ∈ (P.withRate r' hr').toExtended.feasible s) (hcA : 0 < (P.withRate r hr).consumption s a) (hcB : 0 < (P.withRate r' hr').consumption s a') {e₁ e₂ : ℝ} (hu : P.u ((P.withRate r hr).consumption s a) - P.u ((P.withRate r' hr').consumption s a') ≤ e₁) (hv : (P.withRate r hr).toExtended.expect v (s, a) - (P.withRate r' hr').toExtended.expect v (s, a') ≤ e₂) : (P.withRate r hr).toExtended.objectiveE v s a ≤ (P.withRate r' hr').toExtended.objectiveE v s a' + ↑(e₁ + ↑P.discount * e₂)

From argument gaps to an objective comparison.

The reward is real at both actions because consumption is positive at both -- which is what the cutoff delivers -- so the extended-real objective collapses to a real one and the comparison is ordinary arithmetic. Keeping the two gaps as hypotheses separates the analytic work from the arithmetic.

The sup-norm estimate

Everything assembled. Choosing the rate gap small enough makes the Bellman operator move by less than any prescribed amount, uniformly over the region.

Three separate smallness requirements are imposed on the rate gap, and the + 1 in each constant is only to keep the divisions safe when the asset cap is zero:

• the saving gap must fall under the continuation value's modulus,
• the consumption gap must fall under utility's modulus,
• the consumption gap must be at most δ/2, so that consumption at the SECOND rate stays positive given that the cutoff bounds it at the first. Without this the reward at the second rate could be ⊥ and the comparison would be vacuous.

Actions below the cutoff need no comparison at all: they are already worth less than loBound v, which is itself below the other operator's value.

theorem LeanEconomics.IncomeFluctuation.exists_rate_modulus {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) ℝ) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ (r r' : ℝ) (hr : P.RateOK r) (hr' : P.RateOK r'), rlo ≤ r → r ≤ rhi → rlo ≤ r' → r' ≤ rhi → |r - r'| < η → ∀ s ∈ P.region, (P.withRate r hr).toExtended.bellmanFn v s ≤ (P.withRate r' hr').toExtended.bellmanFn v s + ε

theorem LeanEconomics.IncomeFluctuation.exists_valueFunction_modulus {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hd : P.Unbounded) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) {r₀ : ℝ} (hr₀ : P.RateOK r₀) (hlo₀ : rlo ≤ r₀) (hhi₀ : r₀ ≤ rhi) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ (r : ℝ) (hr : P.RateOK r), rlo ≤ r → r ≤ rhi → |r - r₀| < η → ∀ s ∈ P.region, |(P.withRate r hr).toExtended.valueFunction s - (P.withRate r₀ hr₀).toExtended.valueFunction s| ≤ ε

The value function moves continuously with the interest rate, on the region.

Stated AT a reference rate rather than between two arbitrary rates, and that is not a weakening -- it is what makes the argument work. The modulus produced by exists_rate_modulus depends on the continuation value fed to the operator, so comparing two moving rates would need the family of value functions to be equicontinuous. Fixing the reference rate makes the continuation value a single fixed function, and continuity at every point is continuity.

What policy continuity is for

The distribution side consumes the policy only through the Markov operator, and only through its SUP norm: the closed-graph argument for r ↦ μ r needs

‖markovOp_r h - markovOp_r₀ h‖ → 0

because ∫ markovOp_r h dμ_r splits into ∫ (markovOp_r h - markovOp_r₀ h) dμ_r, bounded by that norm, plus a term weak convergence handles. Pointwise convergence of the policy would not do.

The lemma below is the interface: it reduces the operator gap to the gap in the SUCCESSOR STATES, which is where the policy enters. Combined with uniform continuity of h on the compact state space, uniform convergence of the policy is exactly what is needed, and nothing more.

theorem LeanEconomics.IncomeFluctuation.abs_markovFn_sub_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {A B : IncomeFluctuation Z assetFloor assetCap} (hAB : A.transitionMatrix = B.transitionMatrix) (h : BoundedContinuousFunction A.State ℝ) {ε : ℝ} (hclose : ∀ (s : A.State) (z' : Z), |h (A.nextState s z') - h (B.nextState s z')| ≤ ε) (s : A.State) : |A.markovFn h s - B.markovFn h s| ≤ ε