The sign change, both ends

Equilibrium.Firm proved the LOW end of the sign change — capital demand diverges as the rate approaches -δ, while capital supply can never exceed the asset cap — and recorded that the HIGH end was open, needing capitalDemand δ rhi ≤ S rhi and hence S rhi > 0, which it called "obvious economically and unproved here".

That is now proved. PositiveCapital gives strictly positive capital supply, and what remains is to make the bound QUANTITATIVE: the sign change needs a number, not merely positivity, because rhi has to be chosen from it. le_aggregateCapital supplies the number from a uniform lower bound on saving, and exists_capitalDemand_le is the mirror of exists_capitalDemand_ge — Cobb–Douglas demand vanishes at high rates, so any positive supply floor is eventually met.

exists_sign_change then brackets the equilibrium from two-sided bounds on capital supply, and exists_equilibrium_of_bounds hands the bracket to exists_aiyagari_equilibrium.

What is still assumed, and it is no longer the demand side

The bounds m ≤ S r ≤ M are required at every rate. The upper one is free, from aggregateCapital_le. The lower one is the live hypothesis: PositiveCapital proves it at a rate, and making it uniform over an interval wide enough for the curves to cross is what the crude constants make hard — the decline condition alone needs ε > r/(1+r), and with ε ≈ 0.27 that caps the interval near r = 0.37. So the remaining obstruction is a QUANTITATIVE one about the household side, not a structural gap in the equilibrium argument.

theorem LeanEconomics.exists_capitalDemand_le (A δ : ℝ) {m : ℝ} (hm : 0 < m) (r₀ : ℝ) : ∃ (rhi : ℝ), r₀ ≤ rhi ∧ 0 < rhi + δ ∧ capitalDemand A δ rhi ≤ m

Capital demand vanishes at high rates. The mirror of exists_capitalDemand_ge, and what makes the high end of the sign change a theorem.

theorem LeanEconomics.exists_sign_change (δ : ℝ) {S : ℝ → ℝ} {m M : ℝ} (hm : 0 < m) (hlb : ∀ (r : ℝ), m ≤ S r) (hub : ∀ (r : ℝ), S r ≤ M) : ∃ (rlo : ℝ) (rhi : ℝ), 0 < rlo + δ ∧ rlo ≤ rhi ∧ S rlo ≤ capitalDemand 1 δ rlo ∧ capitalDemand 1 δ rhi ≤ S rhi

The sign change, from two-sided bounds on capital supply.

theorem LeanEconomics.exists_firm_of_bounds {rlo rhi m M : ℝ} (hlt : rlo < rhi) (hm : 0 < m) (hmM : m ≤ M) : ∃ (A : ℝ) (δ : ℝ), 0 < A ∧ 0 < rlo + δ ∧ M ≤ capitalDemand A δ rlo ∧ capitalDemand A δ rhi ≤ m

The firm can be calibrated to the households, rather than the other way round. Given any rate interval and any two-sided bound on capital supply, some productivity and depreciation put capital demand above supply at the low end and below it at the high end.

This is what the productivity parameter buys. With A fixed at one the demand schedule carries a scale of its own, and the household economy has to be stretched — in practice to absurd depreciation rates — for the curves to meet. Here A sets the scale and δ the curvature, and the construction is explicit: η = d √m / (√M + √m) with d = rhi - rlo, then δ = η - rlo and A = 2 η √M, at which the low end holds with EQUALITY.

theorem LeanEconomics.IncomeFluctuation.le_aggregateCapital {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) {z₁ : Z} {p₀ ε : ℝ} (hε : 0 ≤ ε) (hp : ∀ (z : Z), p₀ ≤ P.transitionMatrix z z₁) (hpol : ∀ a ∈ Set.Icc 0 assetCap, ε ≤ P.policy (a, z₁)) : ε * p₀ ≤ P.aggregateCapital μ

A quantitative lower bound on capital supply. Households in income state z₁ save at least ε, the stationary distribution puts at least p₀ of its mass there, and capital is mean saving — so capital is at least ε p₀. Positivity alone would not do: the sign change needs a number from which to choose rhi.

theorem LeanEconomics.IncomeFluctuation.le_aggregateCapital_of_gain {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (hpc : P.PositiveConsumption) (hu : P.u = Real.log) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) {z₁ z₀ : Z} {p₀ h : ℝ} (hh0 : 0 < h) (hhcap : h ≤ assetCap) (hhinc : h < P.income z₁) (hp : ∀ (z : Z), p₀ ≤ P.transitionMatrix z z₁) (hgain : Real.log (P.income z₁ / (P.income z₁ - h)) < ↑P.discount * (P.transitionMatrix z₁ z₀ * Real.log (1 + (1 + P.interest) * (h / 2) / (P.income z₀ + (1 + P.interest) * (h / 2))))) : h / 2 * p₀ ≤ P.aggregateCapital μ

The supply floor, in primitives. Combining the quantitative saving bound with the primitive bound on the continuation's gain: every stationary distribution carries at least h/2 · p₀ of capital.

The equilibrium, from uniqueness and a floor

Everything the equilibrium theorem wants is now available on the household side: uniqueness of the stationary distribution at each rate (from the uniform corner and decline conditions) and a positive floor under capital supply (from the gain condition, checked at the low end). This assembles them.

The selection ν is built by choosing the unique stationary distribution at the CLAMPED rate, so it is defined at every real number while agreeing with the intended one on the interval — the same device rateFamily uses, and for the same reason. Uniqueness then gives both halves of what exists_equilibrium_of_selection asks: that ν r is stationary, and that nothing else is.

exists_equilibrium_of_technology is the primitive statement: the technology (A, δ) is GIVEN, and two inequalities on it — enough demand at rlo to clear the asset cap, little enough at rhi to fall under the supply floor — deliver the equilibrium. exists_equilibrium_of_uniqueness_and_floor is then the corollary in which the firm is chosen last, by exists_firm_of_bounds, from the supply floor m and the asset cap.

theorem LeanEconomics.IncomeFluctuation.withRate_congr {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {a b : ℝ} (hab : a = b) (h₁ : P.RateOK a) (h₂ : P.RateOK b) : P.withRate a h₁ = P.withRate b h₂

theorem LeanEconomics.IncomeFluctuation.exists_equilibrium_of_ceiling_and_floor_of_demand {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hlt : rlo < rhi) (huniq : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), ∃! μ : MeasureTheory.ProbabilityMeasure P.State, (P.withRate r hrr).IsStationary μ) {m M : ℝ} (hceil : ∀ (hrlo' : P.RateOK rlo) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate rlo hrlo').IsStationary μ → P.aggregateCapital μ ≤ M) (hfloor : ∀ (hrhi : P.RateOK rhi) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate rhi hrhi).IsStationary μ → m ≤ P.aggregateCapital μ) (D : ℝ → ℝ) (hD : ContinuousOn D (Set.Icc rlo rhi)) (hDlo : M ≤ D rlo) (hDhi : D rhi ≤ m) : ∃ r ∈ Set.Icc rlo rhi, IsAiyagariEquilibrium (P.rateFamily hrlo ⋯) D r

The same for any continuous demand schedule. The ceiling at rlo and the floor at rhi are compared with D there; the selection of stationary distributions supplies the continuity of supply in between.

theorem LeanEconomics.IncomeFluctuation.exists_equilibrium_of_ceiling_and_floor {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hlt : rlo < rhi) (huniq : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), ∃! μ : MeasureTheory.ProbabilityMeasure P.State, (P.withRate r hrr).IsStationary μ) {m M : ℝ} (hceil : ∀ (hrlo' : P.RateOK rlo) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate rlo hrlo').IsStationary μ → P.aggregateCapital μ ≤ M) (hfloor : ∀ (hrhi : P.RateOK rhi) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate rhi hrhi).IsStationary μ → m ≤ P.aggregateCapital μ) (A δ : ℝ) (hδ : 0 < rlo + δ) (hDlo : M ≤ capitalDemand A δ rlo) (hDhi : capitalDemand A δ rhi ≤ m) : ∃ r ∈ Set.Icc rlo rhi, IsAiyagariEquilibrium (P.rateFamily hrlo ⋯) (capitalDemand A δ) r

An Aiyagari equilibrium with the technology GIVEN. The firm is no longer chosen to fit the household: any (A, δ) whose demand clears the asset cap at the bottom of the interval and falls below the supply floor at the top produces an equilibrium inside it.

The two hypotheses are inequalities on the technology and nothing else — le_capitalDemand_of_sq and capitalDemand_le_of_sq turn them into 4(rlo+δ)²·assetCap ≤ A² and A² ≤ 4(rhi+δ)²·m, which is the band 2(rlo+δ)√assetCap ≤ A ≤ 2(rhi+δ)√m. Such an A exists exactly when (rlo+δ)√assetCap ≤ (rhi+δ)√m, so the band is non-empty for small δ whenever the household has a positive supply floor: that is the content of exists_equilibrium_of_uniqueness_and_floor, which is now a corollary.

Note which bound is used where. The ceiling is the free one, aggregateCapital_le; only the floor m is household work.

theorem LeanEconomics.IncomeFluctuation.exists_equilibrium_of_technology {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hlt : rlo < rhi) (huniq : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), ∃! μ : MeasureTheory.ProbabilityMeasure P.State, (P.withRate r hrr).IsStationary μ) {m : ℝ} (hfloor : ∀ (hrhi : P.RateOK rhi) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate rhi hrhi).IsStationary μ → m ≤ P.aggregateCapital μ) (A δ : ℝ) (hδ : 0 < rlo + δ) (hDlo : assetCap ≤ capitalDemand A δ rlo) (hDhi : capitalDemand A δ rhi ≤ m) : ∃ r ∈ Set.Icc rlo rhi, IsAiyagariEquilibrium (P.rateFamily hrlo ⋯) (capitalDemand A δ) r

The same with the free ceiling. Capital supply can never exceed the asset cap, so a technology that clears the cap at rlo needs no household-side ceiling at all. This is the form every witness used before crra_aggregateCapital_le_of_minMPC gave a sharper one.

theorem LeanEconomics.IncomeFluctuation.exists_equilibrium_of_uniqueness_and_floor {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hrlo : 0 < 1 + rlo) (hlt : rlo < rhi) (huniq : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), ∃! μ : MeasureTheory.ProbabilityMeasure P.State, (P.withRate r hrr).IsStationary μ) {m : ℝ} (hm : 0 < m) (hfloor : ∀ (hrhi : P.RateOK rhi) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate rhi hrhi).IsStationary μ → m ≤ P.aggregateCapital μ) : ∃ (A : ℝ) (δ : ℝ), 0 < A ∧ 0 < rlo + δ ∧ ∃ r ∈ Set.Icc rlo rhi, IsAiyagariEquilibrium (P.rateFamily hrlo ⋯) (capitalDemand A δ) r

An Aiyagari equilibrium from household-side hypotheses alone. Uniqueness of the stationary distribution at each rate, and a positive floor under capital supply AT THE TOP OF THE INTERVAL, suffice: the firm is then calibrated to meet them.

The floor is needed only at rhi, which matters: gain_term_mono says the gain condition is easier at higher rates, so the floor may be taken at the best rate rather than the worst.

theorem LeanEconomics.IncomeFluctuation.aggregateCapital_le_of_consumption_bound {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) {ε : ℝ} (hε1 : ε ≤ 1) (hlt : (1 - ε) * (1 + P.interest) < 1) (hlb : ∀ (z : Z), ∀ a ∈ Set.Icc 0 assetCap, ε * P.resources (a, z) ≤ P.consumptionFn z a) : P.aggregateCapital μ ≤ (1 - ε) * P.maxIncome / (1 - (1 - ε) * (1 + P.interest))

Capital supply is bounded above by the impatience of the household. Every household saves at most 1 - ε of its resources, capital is mean saving, and resources are income plus the return on capital — so the bound closes on itself.

This is the quantitative form of "assets are small when the household is impatient", and it blows up exactly as (1-ε)(1+r) → 1, which is where the household stops running its assets down.

theorem LeanEconomics.IncomeFluctuation.crra_aggregateCapital_le_of_minMPC {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hu : P.u = crraUtility γ) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hβR : ↑P.discount * (1 + P.interest) < 1) (hpos : ∀ (n : ℕ) (z : Z), ∀ a ∈ Set.Icc 0 assetCap, 0 < P.consumptionFnOf (P.toExtended.bellman^[n] 0) z a) (hcapit : ∀ (n : ℕ), ∀ a ∈ Set.Icc 0 assetCap, ∀ (z : Z), P.policyOf (P.toExtended.bellman^[n] 0) (a, z) < assetCap) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) : P.aggregateCapital μ ≤ (1 - P.minMPC γ) * P.maxIncome / (1 - (1 - P.minMPC γ) * (1 + P.interest))

A quantitative ceiling on capital supply, from primitives. The minimal-MPC bound says the household consumes at least the share κ of cash on hand; feeding that to aggregateCapital_le_of_consumption_bound replaces the asset cap, which is bookkeeping, by a number the calibration determines. The denominator is 1 - Þ, so the ceiling blows up exactly as the household stops being impatient.

theorem LeanEconomics.IncomeFluctuation.hara_aggregateCapital_le_of_minMPC {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {γ η : ℝ} (hγ0 : 0 < γ) (hη : 0 ≤ η) (hu : P.u = haraUtility γ η) (hκ : 0 < P.minMPC γ) (hβ : 0 < ↑P.discount) (hshare : (1 - minMPCShare γ η) * (1 + P.interest) < 1) (hpos : ∀ (n : ℕ) (z : Z), ∀ a ∈ Set.Icc 0 assetCap, 0 < P.consumptionFnOf (P.toExtended.bellman^[n] 0) z a) (hcapit : ∀ (n : ℕ), ∀ a ∈ Set.Icc 0 assetCap, ∀ (z : Z), P.policyOf (P.toExtended.bellman^[n] 0) (a, z) < assetCap) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : P.IsStationary μ) : P.aggregateCapital μ ≤ (1 - minMPCShare γ η) * P.maxIncome / (1 - (1 - minMPCShare γ η) * (1 + P.interest))

The ceiling for shifted CRRA. The subsistence level enters through minMPCShare, which charges the constant in κ(η+m) ≤ η+c against the smallest cash on hand there can be. At η = 0 it is the CRRA statement.

Uniformity in the interest rate

The supply floor has to hold at every rate in the interval, and the gain condition is MONOTONE in the rate: raising r raises (1+r) t / (y₀ + (1+r) t) towards one, so the right-hand side grows while the left does not move. Checking the condition at the LOW end of the interval therefore covers all of it.

theorem LeanEconomics.gain_term_mono {y₀ t : ℝ} (hy₀ : 0 < y₀) (ht : 0 < t) {s₀ s₁ : ℝ} (hs₀ : 0 < s₀) (hs : s₀ ≤ s₁) : Real.log (1 + s₀ * t / (y₀ + s₀ * t)) ≤ Real.log (1 + s₁ * t / (y₀ + s₁ * t))

theorem LeanEconomics.exists_equilibrium_of_bounds {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} {Pf : ℝ → IncomeFluctuation Z assetFloor assetCap} {S : ℝ → ℝ} (δ : ℝ) {m M : ℝ} (hm : 0 < m) (hlb : ∀ (r : ℝ), m ≤ S r) (hub : ∀ (r : ℝ), S r ≤ M) (hS : ∀ (r : ℝ), ∃ (μ : MeasureTheory.ProbabilityMeasure (Pf r).State), (Pf r).IsStationary μ ∧ (Pf r).aggregateCapital μ = S r) (hScont : ∀ (rlo rhi : ℝ), ContinuousOn S (Set.Icc rlo rhi)) : ∃ (rlo : ℝ) (rhi : ℝ), rlo ≤ rhi ∧ ∃ r ∈ Set.Icc rlo rhi, IsAiyagariEquilibrium Pf (capitalDemand 1 δ) r

An Aiyagari equilibrium with the Cobb–Douglas firm, from two-sided bounds on capital supply. Both ends of the sign change are now theorems; what is assumed is a positive floor under capital supply, uniform in the rate.