Light (2018) Theorem 2: aggregate savings rise with the interest rate

Equilibrium.Uniqueness proves single crossing — Light's Theorem 3 — but carries MONOTONE CAPITAL SUPPLY as a hypothesis, with nothing in the development connecting that hypothesis to the household side. This file supplies the connection. Given that every household saves more at the higher rate, aggregate capital is larger there, so the hypothesis of equilibriumRate_unique follows from the conclusion of Light's Theorem 1.

That leaves the whole uniqueness argument resting on one thing: Theorem 1, itself reduced to the Carroll and Kimball step in IncomeFluctuationCarrollKimball.

The argument

Aggregate capital is mean assets under the stationary distribution, so what has to be compared is two distributions, not two numbers. The comparison is first-order stochastic dominance in the asset coordinate, Dominates, tested against bounded continuous functions that rise with assets at each income state.

Three facts do the work, and they are the three things a dominance argument always needs.

• The Markov operator PRESERVES the test class: markovOp of a function rising in assets rises in assets, because the policy does (policy_mono). Note where the income chain enters — it does not. The probabilities depend on today's income state alone, so comparing two asset levels at a FIXED income state leaves them untouched.
• A uniformly larger policy gives a larger operator, on the test class.
• Dominance survives weak limits, since the test functions are bounded and continuous.

Then run both economies forward from the SAME initial distribution. They stay ordered at every date by the first two facts, and each converges to its own stationary distribution by tendsto_pushProb_iterate — the Doeblin convergence proved for step 4 of the roadmap, which has had no consumer until now. The third fact passes the order to the limit.

The Doeblin data appears as hypotheses at both rates. It is the same minorisation the uniqueness theorem runs on: an atom at the borrowing constraint.

Stochastic dominance in the asset coordinate

def LeanEconomics.IncomeFluctuation.MonoAsset {Z : Type u_1} [TopologicalSpace Z] {assetFloor assetCap : ℝ} (h : BoundedContinuousFunction (↑(Set.Icc assetFloor assetCap) × Z) ℝ) : Prop

Bounded continuous functions that rise with assets, at each income state separately. These are the test functions of first-order stochastic dominance in the asset coordinate.

Equations

• LeanEconomics.IncomeFluctuation.MonoAsset h = ∀ (z : Z) (a b : ↑(Set.Icc assetFloor assetCap)), a ≤ b → h (a, z) ≤ h (b, z)

def LeanEconomics.IncomeFluctuation.Dominates {Z : Type u_1} [TopologicalSpace Z] [MeasurableSpace Z] {assetFloor assetCap : ℝ} (μ ν : MeasureTheory.ProbabilityMeasure (↑(Set.Icc assetFloor assetCap) × Z)) : Prop

First-order stochastic dominance in assets.

Equations

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

theorem LeanEconomics.IncomeFluctuation.Dominates.refl {Z : Type u_1} [TopologicalSpace Z] [MeasurableSpace Z] {assetFloor assetCap : ℝ} (μ : MeasureTheory.ProbabilityMeasure (↑(Set.Icc assetFloor assetCap) × Z)) : Dominates μ μ

theorem LeanEconomics.IncomeFluctuation.Dominates.of_tendsto {Z : Type u_1} [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} [Finite Z] {μs νs : ℕ → MeasureTheory.ProbabilityMeasure (↑(Set.Icc assetFloor assetCap) × Z)} {μ ν : MeasureTheory.ProbabilityMeasure (↑(Set.Icc assetFloor assetCap) × Z)} (hμ : Filter.Tendsto μs Filter.atTop (nhds μ)) (hν : Filter.Tendsto νs Filter.atTop (nhds ν)) (hd : ∀ (n : ℕ), Dominates (μs n) (νs n)) : Dominates μ ν

Dominance survives weak limits, because the test functions are bounded and continuous.

The operator preserves the test class, and respects a larger policy

theorem LeanEconomics.IncomeFluctuation.monoAsset_markovOp {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {h : BoundedContinuousFunction P.State ℝ} (hh : MonoAsset h) : MonoAsset (P.markovOp h)

The Markov operator preserves the test class. The expected value tomorrow of a payoff that rises with assets itself rises with assets, because the policy does.

theorem LeanEconomics.IncomeFluctuation.markovOp_le_of_policy_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P Q : IncomeFluctuation Z assetFloor assetCap) (hprob : ∀ (z z' : Z), P.transitionMatrix z z' = Q.transitionMatrix z z') (hpol : ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → P.policy s ≤ Q.policy s) {h : BoundedContinuousFunction P.State ℝ} (hh : MonoAsset h) (s : P.State) : (P.markovOp h) s ≤ (Q.markovOp h) s

A uniformly larger policy gives a larger operator, on the test class.

theorem LeanEconomics.IncomeFluctuation.Dominates.pushProb {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P Q : IncomeFluctuation Z assetFloor assetCap) (hprob : ∀ (z z' : Z), P.transitionMatrix z z' = Q.transitionMatrix z z') (hpol : ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → P.policy s ≤ Q.policy s) {μ ν : MeasureTheory.ProbabilityMeasure P.State} (hd : Dominates μ ν) : Dominates (P.pushProb μ) (Q.pushProb ν)

One period preserves dominance.

Theorem 2

theorem LeanEconomics.IncomeFluctuation.dominates_of_policy_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P Q : IncomeFluctuation Z assetFloor assetCap) (hprob : ∀ (z z' : Z), P.transitionMatrix z z' = Q.transitionMatrix z z') (hpol : ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → P.policy s ≤ Q.policy s) {μ₀ μ ν : MeasureTheory.ProbabilityMeasure P.State} (hP : Filter.Tendsto (fun (m : ℕ) => P.pushProb^[m] μ₀) Filter.atTop (nhds μ)) (hQ : Filter.Tendsto (fun (m : ℕ) => Q.pushProb^[m] μ₀) Filter.atTop (nhds ν)) : Dominates μ ν

Stationary distributions are ordered when policies are. Both economies are run forward from the same starting distribution and stay ordered at every date, so their limits are ordered.

Convergence is the hypothesis rather than the Doeblin data, because that is all the argument uses; dominates_stationary_of_policy_le supplies it from the minorisation.

theorem LeanEconomics.IncomeFluctuation.dominates_stationary_of_policy_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P Q : IncomeFluctuation Z assetFloor assetCap) (hprob : ∀ (z z' : Z), P.transitionMatrix z z' = Q.transitionMatrix z z') (hpol : ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → P.policy s ≤ Q.policy s) {zP : Z} {sP : P.State} {pP : ℝ} {NP : ℕ} (hpP0 : 0 < pP) (hpP : ∀ (s : P.State), pP ≤ P.prob s zP) (hbadP : ∀ (s : P.State), (P.badStep zP)^[NP] s = sP) {zQ : Z} {sQ : Q.State} {pQ : ℝ} {NQ : ℕ} (hpQ0 : 0 < pQ) (hpQ : ∀ (s : Q.State), pQ ≤ Q.prob s zQ) (hbadQ : ∀ (s : Q.State), (Q.badStep zQ)^[NQ] s = sQ) {μ ν : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) (hν : Q.IsStationary ν) : Dominates μ ν

The same, with convergence supplied by the Doeblin minorisation at each rate — the atom at the borrowing constraint that Distribution.Uniqueness runs on.

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

theorem LeanEconomics.IncomeFluctuation.aggregateCapital_le_of_policy_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P Q : IncomeFluctuation Z assetFloor assetCap) (hprob : ∀ (z z' : Z), P.transitionMatrix z z' = Q.transitionMatrix z z') (hpol : ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → P.policy s ≤ Q.policy s) {zP : Z} {sP : P.State} {pP : ℝ} {NP : ℕ} (hpP0 : 0 < pP) (hpP : ∀ (s : P.State), pP ≤ P.prob s zP) (hbadP : ∀ (s : P.State), (P.badStep zP)^[NP] s = sP) {zQ : Z} {sQ : Q.State} {pQ : ℝ} {NQ : ℕ} (hpQ0 : 0 < pQ) (hpQ : ∀ (s : Q.State), pQ ≤ Q.prob s zQ) (hbadQ : ∀ (s : Q.State), (Q.badStep zQ)^[NQ] s = sQ) {μ ν : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) (hν : Q.IsStationary ν) : P.aggregateCapital μ ≤ Q.aggregateCapital ν

Light (2018) Theorem 2. If every household saves at least as much in the second economy as in the first, aggregate capital is at least as large.

theorem LeanEconomics.IncomeFluctuation.monotoneOn_capitalSupply_of_policy_mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {rlo rhi : ℝ} (Pf : ℝ → IncomeFluctuation Z assetFloor assetCap) (hprob : ∀ (r r' : ℝ) (z z' : Z), (Pf r).transitionMatrix z z' = (Pf r').transitionMatrix z z') (hpol : ∀ r ∈ Set.Icc rlo rhi, ∀ r' ∈ Set.Icc rlo rhi, r ≤ r' → ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → (Pf r).policy s ≤ (Pf r').policy s) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hconv : ∀ r ∈ Set.Icc rlo rhi, Filter.Tendsto (fun (m : ℕ) => (Pf r).pushProb^[m] μ₀) Filter.atTop (nhds (ν r))) : MonotoneOn (fun (r : ℝ) => P.aggregateCapital (ν r)) (Set.Icc rlo rhi)

Capital supply is monotone in the interest rate whenever the household policy is.

This is exactly the hypothesis hS of equilibriumRate_unique, so with Light's Theorem 1 in hand — the policy rising in the rate — the equilibrium rate is unique. Theorem 1 is the only thing still missing, and IncomeFluctuationCarrollKimball has reduced it to one step.

theorem LeanEconomics.IncomeFluctuation.capitalSupply_le_of_policy_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {rlo rhi : ℝ} (Pf Qf : ℝ → IncomeFluctuation Z assetFloor assetCap) (hprob : ∀ (r : ℝ) (z z' : Z), (Pf r).transitionMatrix z z' = (Qf r).transitionMatrix z z') (hpol : ∀ r ∈ Set.Icc rlo rhi, ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → (Pf r).policy s ≤ (Qf r).policy s) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) (ν ρ : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hconvP : ∀ r ∈ Set.Icc rlo rhi, Filter.Tendsto (fun (m : ℕ) => (Pf r).pushProb^[m] μ₀) Filter.atTop (nhds (ν r))) (hconvQ : ∀ r ∈ Set.Icc rlo rhi, Filter.Tendsto (fun (m : ℕ) => (Qf r).pushProb^[m] μ₀) Filter.atTop (nhds (ρ r))) {r : ℝ} (hr : r ∈ Set.Icc rlo rhi) : P.aggregateCapital (ν r) ≤ P.aggregateCapital (ρ r)

Capital supply is ordered when the policies are, across two FAMILIES of economies rather than across two rates of one. The patience comparative static consumes this: a more patient population saves more at every rate, so its supply schedule lies above.