The interest rate as a state variable

Comparative statics in the interest rate can be done by a parametric argument -- prove the value function continuous in the parameter, then the policy, then the distribution -- or by putting the rate INTO the state and letting the existing machinery do the work. This file takes the second route.

The rate never changes, so the operator is block diagonal in it: the transition carries the rate forward untouched. The r-slice of the augmented value function is therefore a fixed point of the r-programme's own Bellman operator, hence equal to its value function; and Berge, already proved in this library, gives continuity of the augmented policy in the whole state, which includes the rate.

Two design points.

The rate coordinate is CLAMPED to [rlo, rhi]. Without it the reward has no bound above, since maximum consumption grows with the rate. This is the same clamp-and-prove-inactive device the model already uses for consumption, and clampRate_eq is the "inactive" half.

The clamp inside the reward is STATE-DEPENDENT rather than a constant, even though a constant would also bound it. That is what makes the slice at a rate in range equal to the r-programme rather than merely close to it: every piece of data matches on the nose, so the two Bellman operators are literally the same and uniqueness of the fixed point finishes. With a constant clamp the two would differ off the region and the slice lemma would need the region bridge instead of an equality.

noncomputable def LeanEconomics.clampRate (rlo rhi r : ℝ) : ℝ

The rate, clamped to the interval under consideration.

Equations

• LeanEconomics.clampRate rlo rhi r = min rhi (max rlo r)

theorem LeanEconomics.continuous_clampRate (rlo rhi : ℝ) : Continuous (clampRate rlo rhi)

theorem LeanEconomics.clampRate_mem {rlo rhi : ℝ} (hle : rlo ≤ rhi) (r : ℝ) : clampRate rlo rhi r ∈ Set.Icc rlo rhi

theorem LeanEconomics.clampRate_eq {rlo rhi r : ℝ} (hr : r ∈ Set.Icc rlo rhi) : clampRate rlo rhi r = r

On the interval, the clamp is inactive.

@[reducible, inline]

abbrev LeanEconomics.IncomeFluctuation.AugState {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (_P : IncomeFluctuation Z 0 assetCap) : Type u_1

The augmented state: assets, the interest rate, and the income state.

Equations

• _P.AugState = ((ℝ × ℝ) × Z)

noncomputable def LeanEconomics.IncomeFluctuation.augResources {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) (s : P.AugState) : ℝ

Cash on hand when the interest rate is carried in the state and clamped to the interval.

Equations

• P.augResources rlo rhi s = P.income s.2 + (1 + LeanEconomics.clampRate rlo rhi s.1.2) * max 0 s.1.1

noncomputable def LeanEconomics.IncomeFluctuation.augMaxConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) (s : P.AugState) : ℝ

The consumption ceiling for the rate carried by an augmented state.

Equations

• P.augMaxConsumption rlo rhi s = P.maxIncome + (1 + LeanEconomics.clampRate rlo rhi s.1.2) * assetCap

noncomputable def LeanEconomics.IncomeFluctuation.augMaxSaving {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) (s : P.AugState) : ℝ

The largest feasible saving, respecting the zero borrowing limit and asset cap.

Equations

• P.augMaxSaving rlo rhi s = max 0 (min assetCap (P.augResources rlo rhi s))

noncomputable def LeanEconomics.IncomeFluctuation.augClampedConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) (p : P.AugState × ℝ) : ℝ

Consumption restricted to the domain on which the extended reward is defined.

Equations

• P.augClampedConsumption rlo rhi p = min (P.augMaxConsumption rlo rhi p.1) (max 0 (P.augResources rlo rhi p.1 - p.2))

noncomputable def LeanEconomics.IncomeFluctuation.augRewardFn {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) (p : P.AugState × ℝ) : EReal

The extended period utility used by the augmented Bellman operator.

Equations

• P.augRewardFn rlo rhi p = LeanEconomics.extendDom P.dom P.u (P.augClampedConsumption rlo rhi p)

theorem LeanEconomics.IncomeFluctuation.one_add_clampRate_pos {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (r : ℝ) : 0 < 1 + clampRate rlo rhi r

theorem LeanEconomics.IncomeFluctuation.minIncome_le_augResources {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (s : P.AugState) : P.minIncome ≤ P.augResources rlo rhi s

theorem LeanEconomics.IncomeFluctuation.augResources_pos {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (s : P.AugState) : 0 < P.augResources rlo rhi s

theorem LeanEconomics.IncomeFluctuation.minIncome_le_augMaxConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (s : P.AugState) : P.minIncome ≤ P.augMaxConsumption rlo rhi s

theorem LeanEconomics.IncomeFluctuation.augMaxConsumption_pos {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (s : P.AugState) : 0 < P.augMaxConsumption rlo rhi s

theorem LeanEconomics.IncomeFluctuation.augMaxConsumption_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hle : rlo ≤ rhi) (s : P.AugState) : P.augMaxConsumption rlo rhi s ≤ P.maxIncome + (1 + rhi) * assetCap

The rate clamp is what bounds the reward above.

theorem LeanEconomics.IncomeFluctuation.continuous_augResources {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) : Continuous (P.augResources rlo rhi)

theorem LeanEconomics.IncomeFluctuation.continuous_augMaxConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) : Continuous (P.augMaxConsumption rlo rhi)

theorem LeanEconomics.IncomeFluctuation.continuous_augMaxSaving {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) : Continuous (P.augMaxSaving rlo rhi)

theorem LeanEconomics.IncomeFluctuation.augClampedConsumption_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (p : P.AugState × ℝ) : 0 ≤ P.augClampedConsumption rlo rhi p

theorem LeanEconomics.IncomeFluctuation.augClampedConsumption_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) (p : P.AugState × ℝ) : P.augClampedConsumption rlo rhi p ≤ P.augMaxConsumption rlo rhi p.1

theorem LeanEconomics.IncomeFluctuation.continuous_augClampedConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) : Continuous (P.augClampedConsumption rlo rhi)

theorem LeanEconomics.IncomeFluctuation.continuous_augRewardFn {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (rlo rhi : ℝ) (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) : Continuous (P.augRewardFn rlo rhi)

noncomputable def LeanEconomics.IncomeFluctuation.toAugmented {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) : ExtendedStochasticProgram P.AugState ℝ Z

The augmented programme: the interest rate carried along as a state that never changes.

Equations

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

The slice

At a rate inside the interval the clamp is inactive, so every piece of the augmented programme's data agrees on the nose with the r-programme's. The two Bellman operators are then literally equal on the slice, and uniqueness of the fixed point does the rest.

theorem LeanEconomics.IncomeFluctuation.augResources_slice {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) (t : ℝ × Z) : P.augResources rlo rhi ((t.1, r), t.2) = (P.withRate r hrr).resources t

theorem LeanEconomics.IncomeFluctuation.augMaxConsumption_slice {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) (t : ℝ × Z) : P.augMaxConsumption rlo rhi ((t.1, r), t.2) = (P.withRate r hrr).maxConsumption

theorem LeanEconomics.IncomeFluctuation.augMaxSaving_slice {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) (t : ℝ × Z) : P.augMaxSaving rlo rhi ((t.1, r), t.2) = (P.withRate r hrr).maxSaving t

noncomputable def LeanEconomics.IncomeFluctuation.sliceAt {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (w : BoundedContinuousFunction P.AugState ℝ) (r : ℝ) : BoundedContinuousFunction (ℝ × Z) ℝ

The slice of a bounded continuous function on the augmented state.

Equations

• P.sliceAt w r = w.compContinuous { toFun := fun (t : ℝ × Z) => ((t.1, r), t.2), continuous_toFun := ⋯ }

@[simp]

theorem LeanEconomics.IncomeFluctuation.sliceAt_apply {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (w : BoundedContinuousFunction P.AugState ℝ) (r : ℝ) (t : ℝ × Z) : (P.sliceAt w r) t = w ((t.1, r), t.2)

theorem LeanEconomics.IncomeFluctuation.feasible_aug_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi r : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) (t : ℝ × Z) : (P.withRate r hrr).toExtended.feasible t = (P.toAugmented hrlo hle).feasible ((t.1, r), t.2)

The feasible sets agree on the slice.

theorem LeanEconomics.IncomeFluctuation.objectiveE_aug_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi r : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) (W : BoundedContinuousFunction P.AugState ℝ) (t : ℝ × Z) (a : ℝ) : (P.withRate r hrr).toExtended.objectiveE (P.sliceAt W r) t a = (P.toAugmented hrlo hle).objectiveE W ((t.1, r), t.2) a

The objectives agree on the slice, for ANY continuation value.

theorem LeanEconomics.IncomeFluctuation.sliceAt_valueFunction {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi r : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) : P.sliceAt (P.toAugmented hrlo hle).valueFunction r = (P.withRate r hrr).toExtended.valueFunction

The slice of the augmented value function is the value function at that rate.

The transfer

Uniqueness of the maximiser is IMPORTED from the slice rather than reproved: since the two objectives and the two feasible sets coincide, the augmented argmax at ((a, r), z) is the r-programme's argmax at (a, z), which is already known to be a singleton. So the whole concavity and strict-concavity chain is reused rather than redone for the augmented state, which is the reason this route was worth taking.

noncomputable def LeanEconomics.IncomeFluctuation.augPolicy {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (x : P.AugState) : ℝ

An optimal saving choice for the augmented value function.

Equations

• P.augPolicy hrlo hle x = Classical.choose ⋯

theorem LeanEconomics.IncomeFluctuation.augPolicy_mem {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (x : P.AugState) : P.augPolicy hrlo hle x ∈ (P.toAugmented hrlo hle).feasible x

theorem LeanEconomics.IncomeFluctuation.augPolicy_optimal {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (x : P.AugState) : (P.toAugmented hrlo hle).objectiveE (P.toAugmented hrlo hle).valueFunction x (P.augPolicy hrlo hle x) = ↑((P.toAugmented hrlo hle).bellmanFn (P.toAugmented hrlo hle).valueFunction x)

theorem LeanEconomics.IncomeFluctuation.augPolicy_mem_argmax {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (x : P.AugState) : P.augPolicy hrlo hle x ∈ argmax ((P.toAugmented hrlo hle).objectiveE (P.toAugmented hrlo hle).valueFunction) (P.toAugmented hrlo hle).feasible x

theorem LeanEconomics.IncomeFluctuation.argmax_aug_eq_singleton {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi r : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) {t : ℝ × Z} (ht : t.1 ∈ Set.Icc 0 assetCap) : argmax ((P.toAugmented hrlo hle).objectiveE (P.toAugmented hrlo hle).valueFunction) (P.toAugmented hrlo hle).feasible ((t.1, r), t.2) = {(P.withRate r hrr).policy t}

The augmented argmax is the sliced programme's policy.

theorem LeanEconomics.IncomeFluctuation.augPolicy_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi r : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) {t : ℝ × Z} (ht : t.1 ∈ Set.Icc 0 assetCap) : P.augPolicy hrlo hle ((t.1, r), t.2) = (P.withRate r hrr).policy t

theorem LeanEconomics.IncomeFluctuation.continuousOn_augPolicy {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) : ContinuousOn (P.augPolicy hrlo hle) {x : P.AugState | x.1.1 ∈ Set.Icc 0 assetCap ∧ x.1.2 ∈ Set.Icc rlo rhi}

The policy is continuous in the state AND the interest rate, jointly.

Uniform convergence of the policy

Joint continuity plus compactness gives uniform continuity, and that is what resolves the pointwise-versus-uniform difficulty recorded with abs_markovFn_sub_le: a parametric argument would have produced continuity in r for each fixed state and then owed an equicontinuity argument to make it uniform. Here uniformity is free, because a continuous function on a compact set is uniformly continuous.

As with the continuation value, Z carries no metric, so (ℝ × ℝ) × Z is not a metric space and the modulus is taken in (assets, rate) for each income state, then combined over the finitely many states.

theorem LeanEconomics.IncomeFluctuation.exists_policy_modulus {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ (z : Z), ∀ a ∈ Set.Icc 0 assetCap, ∀ r ∈ Set.Icc rlo rhi, ∀ r' ∈ Set.Icc rlo rhi, |r - r'| < η → |P.augPolicy hrlo hle ((a, r), z) - P.augPolicy hrlo hle ((a, r'), z)| < ε

The policy converges uniformly as the interest rate moves.

theorem LeanEconomics.IncomeFluctuation.exists_policy_modulus_withRate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ (z : Z), ∀ a ∈ Set.Icc 0 assetCap, ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), ∀ r' ∈ Set.Icc rlo rhi, ∀ (hrr' : P.RateOK r'), |r - r'| < η → |(P.withRate r hrr).policy (a, z) - (P.withRate r' hrr').policy (a, z)| < ε

The same, stated for the policies of the sliced programmes.

The Markov operator converges uniformly

Feeding the policy modulus through abs_markovFn_sub_le. The two successor states differ only in their asset coordinate -- the income state is the same draw -- so a modulus for the test function in that coordinate is all that is needed.

theorem LeanEconomics.IncomeFluctuation.exists_modulus_state {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (h : BoundedContinuousFunction P.State ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ (z' : Z) (x y : ↑(Set.Icc 0 assetCap)), |↑x - ↑y| < η → |h (x, z') - h (y, z')| ≤ ε

A modulus for a test function in the asset coordinate, uniform over income states.

theorem LeanEconomics.IncomeFluctuation.exists_markovFn_modulus {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) (h : BoundedContinuousFunction P.State ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), ∀ r' ∈ Set.Icc rlo rhi, ∀ (hrr' : P.RateOK r'), |r - r'| < η → ∀ (s : P.State), |(P.withRate r hrr).markovFn h s - (P.withRate r' hrr').markovFn h s| ≤ ε

The Markov operator converges uniformly as the interest rate moves. This is the statement the distribution's closed-graph argument consumes.

The closed-graph estimate

A distribution stationary for a NEARBY rate is almost stationary for the reference rate, with an error controlled uniformly. This is the estimate the closed-graph argument runs on: the error term below involves only the two fixed bounded continuous functions markovOp h and h, so it survives passage to a weak limit, and uniqueness of the stationary distribution then pins the limit down.

theorem LeanEconomics.IncomeFluctuation.exists_almost_stationary_modulus {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} [MeasurableSpace Z] [BorelSpace Z] (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) {r₀ : ℝ} (hr₀ : r₀ ∈ Set.Icc rlo rhi) (hrr₀ : P.RateOK r₀) (h : BoundedContinuousFunction P.State ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), |r - r₀| < η → ∀ (ν : MeasureTheory.ProbabilityMeasure P.State), (P.withRate r hrr).IsStationary ν → |∫ (s : P.State), ((P.withRate r₀ hrr₀).markovOp h) s ∂↑ν - ∫ (s : P.State), h s ∂↑ν| ≤ ε

The stationary distribution moves continuously with the rate

The cluster point step. Compactness of the space of probability measures supplies cluster points; the estimate above makes any cluster point exactly stationary at the reference rate; uniqueness there collapses it to a single point, and a filter with a unique cluster point in a compact space converges.

Uniqueness is needed only AT the reference rate. Existence at nearby rates is all that is asked of them, and it is supplied by the selection ν rather than assumed of the model, so the Doeblin hypotheses need not be carried across the whole interval.

theorem LeanEconomics.IncomeFluctuation.tendsto_stationary {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} [MeasurableSpace Z] [BorelSpace Z] (hrlo : 0 < 1 + rlo) (hle : rlo ≤ rhi) {r₀ : ℝ} (hr₀ : r₀ ∈ Set.Icc rlo rhi) (hrr₀ : P.RateOK r₀) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hν : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), (P.withRate r hrr).IsStationary (ν r)) (huniq : ∀ (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate r₀ hrr₀).IsStationary μ → μ = ν r₀) : Filter.Tendsto ν (nhdsWithin r₀ (Set.Icc rlo rhi)) (nhds (ν r₀))