The agent distribution: state space and Markov operator

Step one towards a stationary agent distribution for the income fluctuation problem.

The compact state space

The model is posed with state space ℝ × Z, but a distribution has to live somewhere compact -- Prokhorov's theorem, which supplies the compactness of the space of probability measures, needs a compact underlying space. The household never leaves [0, assetCap] × Z, so that is where the distribution lives, and State is that region as a space in its own right rather than as a subset of a larger one.

Taking it as a subtype is forced. A subset of ℝ × Z would not be a compact space, and the earlier concavity work could not use a subtype because it is not a module over ℝ. Both choices are right in their own place: concavity needs the linear structure of the ambient space, the distribution needs compactness of the region.

The Markov operator

markovOp h s is the expected value of h at next period's state, given that the household is at s today and follows its optimal policy. The content of the definition is that it lands in the bounded continuous functions again:

• continuity is the Feller property, and comes from continuity of the optimal policy, which is what the whole concavity and uniqueness development was for;
• boundedness is immediate from ∑ prob = 1.

Feller is what will make the induced map on probability measures continuous, and continuity of that map is what a fixed point argument needs.

The operator on measures

push μ is where the distribution μ is a period later. It is assembled from Measure.withDensity and Measure.map rather than from Measure.bind: Mathlib has lintegral_bind but no Bochner integral_bind, whereas both of the former have their Bochner lemmas, and it is the Bochner integral that the weak topology is stated with.

integral_push is the duality ∫ h d(push μ) = ∫ (markovOp h) dμ, and it is what makes the whole thing work: weak convergence is tested against bounded continuous functions, so weak continuity of push reduces immediately to markovOp h being one.

@[reducible, inline]

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

The compact region the agent distribution lives on: assets in [0, assetCap] paired with an income state.

Equations

• _P.State = (↑(Set.Icc assetFloor assetCap) × Z)

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

def LeanEconomics.IncomeFluctuation.incl {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) : ℝ × Z

The region, read back as a state of the original model.

Equations

• P.incl s = (↑s.1, s.2)

theorem LeanEconomics.IncomeFluctuation.continuous_incl {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : Continuous P.incl

theorem LeanEconomics.IncomeFluctuation.incl_mem {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) : (P.incl s).1 ∈ Set.Icc assetFloor assetCap

noncomputable def LeanEconomics.IncomeFluctuation.nextAssets {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) : ↑(Set.Icc assetFloor assetCap)

Next period's assets under the optimal policy, as a point of the region.

Equations

• P.nextAssets s = ⟨P.policy (P.incl s), ⋯⟩

noncomputable def LeanEconomics.IncomeFluctuation.nextState {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) (z' : Z) : P.State

Next period's state if the income shock z' occurs.

Equations

• P.nextState s z' = (P.nextAssets s, z')

theorem LeanEconomics.IncomeFluctuation.continuous_nextAssets {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : Continuous P.nextAssets

The policy moves the household continuously within the region. This is the Feller input, and it is exactly what the concavity and uniqueness development bought.

theorem LeanEconomics.IncomeFluctuation.continuous_nextState {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z' : Z) : Continuous fun (s : P.State) => P.nextState s z'

noncomputable def LeanEconomics.IncomeFluctuation.prob {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) (z' : Z) : ℝ

The probability of moving to income state z', as a function of today's state.

Equations

• P.prob s z' = P.transitionMatrix s.2 z'

theorem LeanEconomics.IncomeFluctuation.prob_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) (z' : Z) : 0 ≤ P.prob s z'

theorem LeanEconomics.IncomeFluctuation.prob_sum {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) : ∑ z' : Z, P.prob s z' = 1

theorem LeanEconomics.IncomeFluctuation.continuous_prob {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z' : Z) : Continuous fun (s : P.State) => P.prob s z'

noncomputable def LeanEconomics.IncomeFluctuation.markovFn {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (s : P.State) : ℝ

The expected value of h next period, as a bare function.

Equations

• P.markovFn h s = ∑ z' : Z, P.prob s z' * h (P.nextState s z')

theorem LeanEconomics.IncomeFluctuation.continuous_markovFn {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) : Continuous (P.markovFn h)

theorem LeanEconomics.IncomeFluctuation.abs_markovFn_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (s : P.State) : |P.markovFn h s| ≤ ‖h‖

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

The Markov operator. markovOp h is the expected value of h next period. That it is again bounded and continuous is the Feller property.

Equations

• P.markovOp h = BoundedContinuousFunction.ofNormedAddCommGroup (P.markovFn h) ⋯ ‖h‖ ⋯

@[simp]

theorem LeanEconomics.IncomeFluctuation.markovOp_apply {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (h : BoundedContinuousFunction P.State ℝ) (s : P.State) : (P.markovOp h) s = ∑ z' : Z, P.prob s z' * h (P.nextState s z')

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

theorem LeanEconomics.IncomeFluctuation.markovOp_mono {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {h k : BoundedContinuousFunction P.State ℝ} (hk : ⇑h ≤ ⇑k) : ⇑(P.markovOp h) ≤ ⇑(P.markovOp k)

The operator is monotone: a larger payoff tomorrow is worth more today.

theorem LeanEconomics.IncomeFluctuation.markovOp_const {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (c : ℝ) : P.markovOp (BoundedContinuousFunction.const P.State c) = BoundedContinuousFunction.const P.State c

The operator is unital: a constant payoff is worth its own value. This is ∑ prob = 1, and it is what will make the induced map send probability measures to probability measures.

The operator on measures

noncomputable def LeanEconomics.IncomeFluctuation.dens {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z' : Z) (s : P.State) : NNReal

The reweighting density for shock z', as an ℝ≥0-valued function.

Equations

• P.dens z' s = (P.prob s z').toNNReal

theorem LeanEconomics.IncomeFluctuation.measurable_dens {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (z' : Z) : Measurable (P.dens z')

@[simp]

theorem LeanEconomics.IncomeFluctuation.coe_dens {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z' : Z) (s : P.State) : ↑(P.dens z' s) = P.prob s z'

theorem LeanEconomics.IncomeFluctuation.sum_dens {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) : ∑ z' : Z, ↑(P.dens z' s) = 1

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

One period of the agent distribution's motion. Each income state z' reweights the distribution by the probability of moving there and pushes it along the policy.

Equations

• P.push μ = MeasureTheory.Measure.sum fun (z' : Z) => MeasureTheory.Measure.map (fun (s : P.State) => P.nextState s z') (μ.withDensity fun (s : P.State) => ↑(P.dens z' s))

theorem LeanEconomics.IncomeFluctuation.measurable_nextState {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (z' : Z) : Measurable fun (s : P.State) => P.nextState s z'

instance LeanEconomics.IncomeFluctuation.isProbabilityMeasure_push {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (μ : MeasureTheory.Measure P.State) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (P.push μ)

push preserves total mass, because the transition probabilities sum to one.

theorem LeanEconomics.IncomeFluctuation.prob_le_one {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : P.State) (z' : Z) : P.prob s z' ≤ 1

Each transition probability is at most one.

theorem LeanEconomics.IncomeFluctuation.integrable_term {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (μ : MeasureTheory.Measure P.State) [MeasureTheory.IsProbabilityMeasure μ] (h : BoundedContinuousFunction P.State ℝ) (z' : Z) : MeasureTheory.Integrable (fun (s : P.State) => P.prob s z' * h (P.nextState s z')) μ

theorem LeanEconomics.IncomeFluctuation.integral_push {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (μ : MeasureTheory.Measure P.State) [MeasureTheory.IsProbabilityMeasure μ] (h : BoundedContinuousFunction P.State ℝ) : ∫ (s : P.State), h s ∂P.push μ = ∫ (s : P.State), (P.markovOp h) s ∂μ

Duality. The integral of h against tomorrow's distribution is the integral of the expected value of h against today's. This is the bridge between the two operators, and it is what turns the Feller property into weak continuity.

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

The agent distribution operator, on probability measures.

Equations

• P.pushProb μ = ⟨P.push ↑μ, ⋯⟩

@[simp]

theorem LeanEconomics.IncomeFluctuation.coe_pushProb {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] (μ : MeasureTheory.ProbabilityMeasure P.State) : ↑(P.pushProb μ) = P.push ↑μ

theorem LeanEconomics.IncomeFluctuation.continuous_pushProb {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) [MeasurableSpace Z] [BorelSpace Z] : Continuous P.pushProb

The distribution operator is weakly continuous. This is the Feller property in the form a fixed point argument needs, and it falls straight out of the duality: weak convergence is tested against bounded continuous functions, and markovOp h is one.

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

A stationary agent distribution is a fixed point of the operator.

Equations

• P.IsStationary μ = (P.pushProb μ = μ)