Existence of a stationary agent distribution

Krylov–Bogolyubov, for the income fluctuation problem: average the iterates of the distribution operator, and any cluster point of those averages is stationary.

The two ingredients are both already in place. The space of probability measures over the compact state space is compact, by Prokhorov; and the operator is weakly continuous, by the Feller property. What the averaging adds is that the difference between an average and its image telescopes, so it vanishes in the limit even though the individual iterates need not converge at all.

instance LeanEconomics.IncomeFluctuation.instNonemptyState {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : Nonempty P.State

The state space is nonempty: a household at the borrowing limit is in it. This has to be given by hand, since assetFloor ≤ assetCap is data carried by P rather than an instance.

noncomputable def LeanEconomics.IncomeFluctuation.cesaro {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) (n : ℕ) : MeasureTheory.Measure P.State

The average of the first n + 1 iterates of the distribution operator.

Equations

• P.cesaro μ₀ n = (↑n + 1)⁻¹ • ∑ k ∈ Finset.range (n + 1), ↑(P.pushProb^[k] μ₀)

instance LeanEconomics.IncomeFluctuation.isProbabilityMeasure_cesaro {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (P.cesaro μ₀ n)

theorem LeanEconomics.IncomeFluctuation.integral_cesaro {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) (n : ℕ) (h : BoundedContinuousFunction P.State ℝ) : ∫ (s : P.State), h s ∂P.cesaro μ₀ n = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), ∫ (s : P.State), h s ∂↑(P.pushProb^[k] μ₀)

The integral against a Cesàro average is the average of the integrals.

theorem LeanEconomics.IncomeFluctuation.continuous_integral_bcf {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) : Continuous fun (ν : MeasureTheory.ProbabilityMeasure P.State) => ∫ (s : P.State), h s ∂↑ν

Integration against a bounded continuous function is weakly continuous.

theorem LeanEconomics.IncomeFluctuation.abs_integral_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (ν : MeasureTheory.Measure P.State) [MeasureTheory.IsProbabilityMeasure ν] (h : BoundedContinuousFunction P.State ℝ) : |∫ (s : P.State), h s ∂ν| ≤ ‖h‖

theorem LeanEconomics.IncomeFluctuation.integral_markovOp_iterate {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) (k : ℕ) (h : BoundedContinuousFunction P.State ℝ) : ∫ (s : P.State), (P.markovOp h) s ∂↑(P.pushProb^[k] μ₀) = ∫ (s : P.State), h s ∂↑(P.pushProb^[k + 1] μ₀)

Applying the operator to the test function advances the measure by one period.

theorem LeanEconomics.IncomeFluctuation.integral_cesaro_sub {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) (n : ℕ) (h : BoundedContinuousFunction P.State ℝ) : ∫ (s : P.State), (P.markovOp h) s ∂P.cesaro μ₀ n - ∫ (s : P.State), h s ∂P.cesaro μ₀ n = (↑(n + 1))⁻¹ * (∫ (s : P.State), h s ∂↑(P.pushProb^[n + 1] μ₀) - ∫ (s : P.State), h s ∂↑μ₀)

The telescoping estimate. The average and its image differ by a single boundary term over n + 1, which is the whole point of averaging: the individual iterates need not converge, but this difference must vanish.

theorem LeanEconomics.IncomeFluctuation.tendsto_cesaro_sub {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) (h : BoundedContinuousFunction P.State ℝ) : Filter.Tendsto (fun (n : ℕ) => ∫ (s : P.State), (P.markovOp h) s ∂P.cesaro μ₀ n - ∫ (s : P.State), h s ∂P.cesaro μ₀ n) Filter.atTop (nhds 0)

theorem LeanEconomics.IncomeFluctuation.exists_isStationary {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] [MeasurableSpace Z] [BorelSpace Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (μ₀ : MeasureTheory.ProbabilityMeasure P.State) : ∃ (μ : MeasureTheory.ProbabilityMeasure P.State), P.IsStationary μ

Krylov–Bogolyubov: a stationary agent distribution exists. Average the iterates and take a cluster point, which exists because the space of probability measures over the compact state space is compact. The telescoping estimate makes that cluster point stationary.