Bisection for a monotone zero and normalized clearing

Bisection evaluates excess supply at the midpoint of a bracket and keeps the half containing the zero. Hajek and Livesay (2019) discuss stability of best-response fixed points in mean field games. Here, a decreasing inverse-demand map composed with an increasing supply map can reverse order, so raw iteration r ↦ r_d(K_s(r)) may oscillate. This file certifies bisection.

The abstract statement

bisect f a b n is the bracket after n steps. If f is STRICTLY MONOTONE on [a, b] and vanishes at r ∈ [a, b], then every bracket contains r (bisect_mem_of_strictMonoOn), the width halves each step (bisect_width), and the endpoints converge to r (tendsto_bisect_fst). No continuity and no sign condition at the ends are used: strict monotonicity alone decides which half the zero is in. The midpoint after n steps is within (b - a)/2^(n+1) of r (abs_bisect_mid_sub_le).

The instance

For the capped log-household calibration, stationary mean assets are monotone in the rate under the stated hypotheses, and the prescribed normalized demand is strictly decreasing. Thus normalized excess supply is strictly increasing. Given a stationary distribution and a rate solving that explicit normalized clearing equation, aiyagari1994_log_bisection proves that bisection brackets the rate and converges to it. Existence of such a solution is an input.

Normalized clearing scope

The economic endpoints use the prescribed equation aggregateCapital μ = normalisedDemand (9/25) (2/25) r, where the right side is (9/25) / ((1 - 9/25) * (r + 2/25)). This is a unit-wage normalized clearing problem. The household earnings scale is arbitrary; no mean-one endowment condition or bridge from these units and the fixed asset cap to full competitive market clearing is established here. The uniqueness and bisection claims concern this explicit normalized equation.

Bisection on the line

noncomputable def LeanEconomics.bisectStep (f : ℝ → ℝ) (p : ℝ × ℝ) : ℝ × ℝ

One bisection step on a bracket (a, b): if f ≤ 0 at the midpoint the zero of an increasing f is to the right, so keep (mid, b); otherwise keep (a, mid).

Equations

• LeanEconomics.bisectStep f p = if f ((p.1 + p.2) / 2) ≤ 0 then ((p.1 + p.2) / 2, p.2) else (p.1, (p.1 + p.2) / 2)

noncomputable def LeanEconomics.bisect (f : ℝ → ℝ) (a b : ℝ) (n : ℕ) : ℝ × ℝ

The bracket after n bisection steps from (a, b).

Equations

• LeanEconomics.bisect f a b n = (LeanEconomics.bisectStep f)^[n] (a, b)

theorem LeanEconomics.bisect_succ (f : ℝ → ℝ) (a b : ℝ) (n : ℕ) : bisect f a b (n + 1) = bisectStep f (bisect f a b n)

theorem LeanEconomics.bisectStep_width (f : ℝ → ℝ) (p : ℝ × ℝ) : (bisectStep f p).2 - (bisectStep f p).1 = (p.2 - p.1) / 2

theorem LeanEconomics.bisect_width (f : ℝ → ℝ) (a b : ℝ) (n : ℕ) : (bisect f a b n).2 - (bisect f a b n).1 = (b - a) / 2 ^ n

The bracket halves at every step.

theorem LeanEconomics.bisect_mem_of_strictMonoOn {f : ℝ → ℝ} {a b r : ℝ} (hf : StrictMonoOn f (Set.Icc a b)) (hr : r ∈ Set.Icc a b) (hfr : f r = 0) (n : ℕ) : a ≤ (bisect f a b n).1 ∧ (bisect f a b n).2 ≤ b ∧ r ∈ Set.Icc (bisect f a b n).1 (bisect f a b n).2

Every bracket contains the zero of a strictly increasing function, and stays inside the initial bracket.

theorem LeanEconomics.abs_bisect_mid_sub_le {f : ℝ → ℝ} {a b r : ℝ} (hf : StrictMonoOn f (Set.Icc a b)) (hr : r ∈ Set.Icc a b) (hfr : f r = 0) (n : ℕ) : |((bisect f a b n).1 + (bisect f a b n).2) / 2 - r| ≤ (b - a) / 2 ^ (n + 1)

The midpoint after n steps is within (b - a)/2^(n+1) of the zero.

theorem LeanEconomics.tendsto_bisect_width (a b : ℝ) : Filter.Tendsto (fun (n : ℕ) => (b - a) / 2 ^ n) Filter.atTop (nhds 0)

The bracket width tends to zero.

theorem LeanEconomics.tendsto_bisect_fst {f : ℝ → ℝ} {a b r : ℝ} (hf : StrictMonoOn f (Set.Icc a b)) (hr : r ∈ Set.Icc a b) (hfr : f r = 0) : Filter.Tendsto (fun (n : ℕ) => (bisect f a b n).1) Filter.atTop (nhds r)

The left endpoints converge to the zero.

theorem LeanEconomics.tendsto_bisect_snd {f : ℝ → ℝ} {a b r : ℝ} (hf : StrictMonoOn f (Set.Icc a b)) (hr : r ∈ Set.Icc a b) (hfr : f r = 0) : Filter.Tendsto (fun (n : ℕ) => (bisect f a b n).2) Filter.atTop (nhds r)

The right endpoints converge to the zero.

theorem LeanEconomics.strictMonoOn_sub_of_monotoneOn_of_strictAntiOn {S D : ℝ → ℝ} {s : Set ℝ} (hS : MonotoneOn S s) (hD : StrictAntiOn D s) : StrictMonoOn (fun (r : ℝ) => S r - D r) s

Monotone supply minus strictly decreasing demand is strictly increasing.

The log Aiyagari instance

noncomputable def LeanEconomics.IncomeFluctuation.excessSupply {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (D : ℝ → ℝ) (r : ℝ) : ℝ

Excess supply along a selection of stationary distributions: capital supplied under ν r minus capital demanded at r.

Equations

• P.excessSupply ν D r = P.aggregateCapital (ν r) - D r

theorem LeanEconomics.IncomeFluctuation.log_selection_of_cap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hrlo : 0 < 1 + rlo) (hlohi : rlo ≤ rhi) (hβR : ↑P.discount * (1 + rhi) < 1) (hcap : 2 * ↑P.discount * P.maxIncome < (1 - ↑P.discount * (1 + rhi)) * assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hmin : P.income z₀ = P.minIncome) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hν : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), (P.withRate r hrr).IsStationary (ν r)) : MonotoneOn (fun (r : ℝ) => P.aggregateCapital (ν r)) (Set.Icc rlo rhi) ∧ ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r) (μ : MeasureTheory.ProbabilityMeasure P.State), (P.withRate r hrr).IsStationary μ → μ = ν r

The two facts about a selection that the bisection needs, from one inequality on the cap: supply along it is monotone, and it is the ONLY stationary distribution at each rate. The constants are chosen as in log_equilibriumRate_unique_of_cap.

theorem LeanEconomics.IncomeFluctuation.log_bisection_of_cap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi α δ : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (hδ : 0 < rlo + δ) (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : 0 < ↑P.discount) (hrlo : 0 < 1 + rlo) (hlohi : rlo ≤ rhi) (hβR : ↑P.discount * (1 + rhi) < 1) (hcap : 2 * ↑P.discount * P.maxIncome < (1 - ↑P.discount * (1 + rhi)) * assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hmin : P.income z₀ = P.minIncome) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hν : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), (P.withRate r hrr).IsStationary (ν r)) {r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : (P.withRate r hrr).IsStationary μ) (he : P.aggregateCapital μ = normalisedDemand α δ r) : (∀ (n : ℕ), r ∈ Set.Icc (bisect (P.excessSupply ν (normalisedDemand α δ)) rlo rhi n).1 (bisect (P.excessSupply ν (normalisedDemand α δ)) rlo rhi n).2) ∧ (∀ (n : ℕ), |((bisect (P.excessSupply ν (normalisedDemand α δ)) rlo rhi n).1 + (bisect (P.excessSupply ν (normalisedDemand α δ)) rlo rhi n).2) / 2 - r| ≤ (rhi - rlo) / 2 ^ (n + 1)) ∧ Filter.Tendsto (fun (n : ℕ) => (bisect (P.excessSupply ν (normalisedDemand α δ)) rlo rhi n).1) Filter.atTop (nhds r)

Bisection on excess supply brackets and converges to the equilibrium rate of the log economy, along any selection of stationary distributions.

theorem LeanEconomics.IncomeFluctuation.aiyagari1994_log_bisection {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetCap : ℝ} (P : IncomeFluctuation Z 0 assetCap) {rlo rhi : ℝ} (hu : P.u = crraUtility 1) (hunb : P.Unbounded) (hβ : ↑P.discount = 24 / 25) (hrlo : -2 / 25 < rlo) (hlohi : rlo ≤ rhi) (hlam : rhi < 1 / 24) (hcap : 2 * (24 / 25) * P.maxIncome < (1 - 24 / 25 * (1 + rhi)) * assetCap) (hmono : P.MonotoneTransitions) {z₀ : Z} (hz₀ : ∀ (z : Z), P.income z₀ ≤ P.income z) (hmin : P.income z₀ = P.minIncome) (hreach : ∀ (z : Z), 0 < P.transitionMatrix z z₀) (ν : ℝ → MeasureTheory.ProbabilityMeasure P.State) (hν : ∀ r ∈ Set.Icc rlo rhi, ∀ (hrr : P.RateOK r), (P.withRate r hrr).IsStationary (ν r)) {r : ℝ} (hr : r ∈ Set.Icc rlo rhi) (hrr : P.RateOK r) {μ : MeasureTheory.ProbabilityMeasure P.State} (hμ : (P.withRate r hrr).IsStationary μ) (he : P.aggregateCapital μ = normalisedDemand (9 / 25) (2 / 25) r) : (∀ (n : ℕ), r ∈ Set.Icc (bisect (P.excessSupply ν (normalisedDemand (9 / 25) (2 / 25))) rlo rhi n).1 (bisect (P.excessSupply ν (normalisedDemand (9 / 25) (2 / 25))) rlo rhi n).2) ∧ (∀ (n : ℕ), |((bisect (P.excessSupply ν (normalisedDemand (9 / 25) (2 / 25))) rlo rhi n).1 + (bisect (P.excessSupply ν (normalisedDemand (9 / 25) (2 / 25))) rlo rhi n).2) / 2 - r| ≤ (rhi - rlo) / 2 ^ (n + 1)) ∧ Filter.Tendsto (fun (n : ℕ) => (bisect (P.excessSupply ν (normalisedDemand (9 / 25) (2 / 25))) rlo rhi n).1) Filter.atTop (nhds r)

Bisection for normalized clearing with the Aiyagari log calibration. On any [rlo, rhi] ⊂ (-δ, λ) with the cap clearing (48/25)·maxIncome/(1 - (24/25)(1+rhi)), and along any selection of stationary distributions, the bisection on excess supply brackets the equilibrium rate at every step, its midpoint is within (rhi - rlo)/2^(n+1) after n steps, and its endpoints converge to the rate.