The income fluctuation problem

The canonical incomplete-markets household: income follows a finite Markov chain, assets earn interest, borrowing is ruled out, and the household chooses savings. The state is the pair (a, z) of assets and income state, and

V (a, z) = max { u c + β * ∑ z', P z z' * V (a', z') }.

Period utility may fall to -∞ at zero consumption, so this covers log and CRRA with σ ≥ 1 -- and, since the utility DOMAIN is a field, CES with γ < 1 as well.

The domain field

u is required to behave on a set dom with Ioi 0 ⊆ dom ⊆ Ici 0, so there are exactly two choices: Ioi 0, where utility is unbounded below, and Ici 0, where it is bounded there. The old tendsto_atBot_u is replaced by continuousOn_extendDom, which says that u extended by ⊥ off dom is continuous where consumption lives. That is what Berge actually consumes, and it is exactly tendsto_atBot_u when dom = Ioi 0 (see continuousOn_extendDom_Ioi) and merely continuity of u on Ici 0 in the other case, where the ⊥ branch is unreachable.

Nothing is lost by the swap: tendsto_atBot_u comes BACK as a theorem from Unbounded.

The one real consequence is that positive consumption at the optimum is no longer free. With dom = Ioi 0 the reward is ⊥ there and the value being real settles it; with dom = Ici 0 it has to be earned from a MARGINAL Inada condition instead — see ConsumptionFloor. Results that need it take PositiveConsumption as a hypothesis, which both routes supply. Results that only need u to behave take membership in dom, and carry over untouched.

Retrofitted onto extended-real rewards

This file used a floor, with the same apparatus as the deterministic models: floor, cFloor, and a chain of results establishing that the floor never binds. All of it is gone. The reward is -∞ where consumption vanishes, and positive consumption at the optimum follows from the value function being real rather than from an argument.

The stochastic case needed LeanEconomics.DynamicProgramming.ExtendedStochastic, since the continuation here is an expectation over shocks rather than v at a single point. That turned out to be routine: the expectation is a sum of reals, so the objective is again an extended real plus a finite coercion, and the reward's -∞ never meets the expectation's arithmetic.

Unchanged

Discreteness of the income state is still what makes every function of z continuous, so the budget correspondence is continuous in the pair. Consumption is still clamped above and assets still capped -- the ordinary boundedness requirement, unrelated to the floor. Cash on hand is computed from max 0 a, as in the deterministic retrofits, so that the value stays finite at every state.

noncomputable def LeanEconomics.extendDom (D : Set ℝ) (u : ℝ → ℝ) (c : ℝ) : EReal

Utility extended by ⊥ outside the domain on which it is required to behave. With D = Ioi 0 this is extendBot; with D = Ici 0 the ⊥ branch is unreachable on Ici 0.

Equations

• LeanEconomics.extendDom D u c = if c ∈ D then ↑(u c) else ⊥

theorem LeanEconomics.extendDom_of_mem {D : Set ℝ} {u : ℝ → ℝ} {c : ℝ} (h : c ∈ D) : extendDom D u c = ↑(u c)

theorem LeanEconomics.extendDom_of_not_mem {D : Set ℝ} {u : ℝ → ℝ} {c : ℝ} (h : c ∉ D) : extendDom D u c = ⊥

theorem LeanEconomics.extendDom_ne_bot_iff {D : Set ℝ} {u : ℝ → ℝ} {c : ℝ} : extendDom D u c ≠ ⊥ ↔ c ∈ D

theorem LeanEconomics.extendDom_Ioi (u : ℝ → ℝ) : extendDom (Set.Ioi 0) u = extendBot u

With D = Ioi 0 the extension is extendBot, so the divergence condition supplies the continuity requirement.

theorem LeanEconomics.continuousOn_extendDom_Ioi {u : ℝ → ℝ} (hc : ContinuousOn u (Set.Ioi 0)) (ht : Filter.Tendsto u (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot) : ContinuousOn (extendDom (Set.Ioi 0) u) (Set.Ici 0)

The unbounded case: divergence at zero supplies the continuity requirement.

structure LeanEconomics.IncomeFluctuation (Z : Type u_1) [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] (assetFloor assetCap : ℝ) : Type u_1

The income fluctuation problem, with a utility domain supporting bounded and unbounded below period utility.

• income : Z → ℝ

  Income in each state.

• transitionMatrix : Z → Z → ℝ

  The Markov transition matrix on income states.

• interest : ℝ

  The interest rate on assets.

• discount : NNReal

  The discount factor.

• u : ℝ → ℝ

  Period utility, required to behave only on positive consumption.

• minIncome : ℝ

  A lower bound on income.

• maxIncome : ℝ

  An upper bound on income.

• minIncome_pos : 0 < self.minIncome
• minIncome_le (z : Z) : self.minIncome ≤ self.income z
• le_maxIncome (z : Z) : self.income z ≤ self.maxIncome
• transitionMatrix_nonneg (z z' : Z) : 0 ≤ self.transitionMatrix z z'
• transitionMatrix_sum (z : Z) : ∑ z' : Z, self.transitionMatrix z z' = 1
• interest_gt_neg_one : 0 < 1 + self.interest
• assetFloor_le_assetCap : assetFloor ≤ assetCap

  The borrowing limit is below the asset cap, so the household always has somewhere to be.

• assetCap_nonneg : 0 ≤ assetCap

  The asset cap is a large positive number; nothing in the development needs it to be small, but several bounds need it to have a sign.

• minConsumption : ℝ

  A declared floor on consumption, at most what a household pinned at the borrowing limit can afford. Carrying it as data rather than computing it from the rate is what lets the same household problem be re-run at a different interest rate without moving the reward's lower bound: minConsumption is the rate-free part of the natural-borrowing-limit condition.

• minConsumption_pos : 0 < self.minConsumption

  The borrowing limit is sustainable: at the limit, income covers the interest on the debt with something left to eat. With assetFloor = 0 this is 0 < minIncome; with a negative limit it is Aiyagari's natural-borrowing-limit condition, and it is what replaces positivity of cash on hand -- resources can be negative when the household is in debt, while consumption cannot.

• minConsumption_le_floor : self.minConsumption ≤ self.minIncome + self.interest * assetFloor
• discount_lt_one : self.discount < 1
• dom : Set ℝ

  The consumption levels at which utility is required to behave. Ioi 0 when utility is unbounded below, Ici 0 when it is bounded there.

• Ioi_subset_dom : Set.Ioi 0 ⊆ self.dom
• dom_subset_Ici : self.dom ⊆ Set.Ici 0
• continuousOn_u_dom : ContinuousOn self.u self.dom
• monotoneOn_u_dom : MonotoneOn self.u self.dom
• strictConcaveOn_u_dom : StrictConcaveOn ℝ self.dom self.u

  Diminishing marginal utility, which makes the optimal policy unique.

• continuousOn_extendDom : ContinuousOn (extendDom self.dom self.u) (Set.Ici 0)

  What replaces the Inada condition. Utility, extended by ⊥ off its domain, must be continuous where consumption lives. For dom = Ioi 0 this is exactly Tendsto u (𝓝[>] 0) atBot via continuous_extendBot; for dom = Ici 0 the ⊥ branch is never taken and it is just continuity of u on Ici 0.

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

Cash on hand, with assets read as nonnegative.

Equations

• P.resources s = P.income s.2 + (1 + P.interest) * max assetFloor s.1

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

The largest consumption the capped problem allows.

Equations

• P.maxConsumption = P.maxIncome + (1 + P.interest) * assetCap - assetFloor

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

The largest asset holding that can be carried forward.

Equations

• P.maxSaving s = max assetFloor (min assetCap (P.resources s))

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

Consumption on the budget line.

Equations

• P.consumption s a' = P.resources s - a'

noncomputable def LeanEconomics.IncomeFluctuation.clampedConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (p : (ℝ × Z) × ℝ) : ℝ

Consumption clamped into [0, maxConsumption]. On the feasible set the lower clamp is inactive, so this is consumption itself; off it, it keeps the reward's argument in Ici 0, which is where continuousOn_extendDom applies.

Equations

• P.clampedConsumption p = min P.maxConsumption (max 0 (P.consumption p.1 p.2))

noncomputable def LeanEconomics.IncomeFluctuation.rewardFn {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (p : (ℝ × Z) × ℝ) : EReal

The reward: utility of consumption clamped above, and ⊥ where consumption falls outside the domain on which utility behaves. No floor.

Equations

• P.rewardFn p = LeanEconomics.extendDom P.dom P.u (P.clampedConsumption p)

def LeanEconomics.IncomeFluctuation.RateOK {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (r : ℝ) : Prop

The rates at which the borrowing limit is sustainable. Raising the interest rate raises the debt service on a negative floor, so a floor that supports positive consumption at one rate need not support it at another: sustainability is part of what it means for a rate to be admissible, not a consequence of -1 < r. With assetFloor = 0 the second conjunct is free.

Equations

• P.RateOK r = (0 < 1 + r ∧ P.minConsumption ≤ P.minIncome + r * assetFloor)

theorem LeanEconomics.IncomeFluctuation.RateOK.one_add_pos {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P : IncomeFluctuation Z assetFloor assetCap} {r : ℝ} (h : P.RateOK r) : 0 < 1 + r

theorem LeanEconomics.IncomeFluctuation.RateOK.sustainable {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} {P : IncomeFluctuation Z assetFloor assetCap} {r : ℝ} (h : P.RateOK r) : P.minConsumption ≤ P.minIncome + r * assetFloor

theorem LeanEconomics.IncomeFluctuation.rateOK_of_floor_zero {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetCap : ℝ} {P : IncomeFluctuation Z 0 assetCap} {r : ℝ} (hr : 0 < 1 + r) : P.RateOK r

At a zero borrowing limit every admissible rate is sustainable.

theorem LeanEconomics.IncomeFluctuation.rateOK_of_mem_Icc {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {rlo rhi r : ℝ} (hlo : P.RateOK rlo) (hhi : P.RateOK rhi) (hr : r ∈ Set.Icc rlo rhi) : P.RateOK r

Sustainability is linear in the rate, so it is inherited from the endpoints of an interval.

theorem LeanEconomics.IncomeFluctuation.rateOK_self {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : P.RateOK P.interest

theorem LeanEconomics.IncomeFluctuation.minConsumption_le_consumption_floor {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.minConsumption ≤ P.resources s - assetFloor

theorem LeanEconomics.IncomeFluctuation.assetFloor_lt_resources {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : assetFloor < P.resources s

Cash on hand always exceeds the borrowing limit, so something can always be eaten. This replaces positivity of cash on hand: in debt, resources can be negative while consumption cannot.

theorem LeanEconomics.IncomeFluctuation.minIncome_le_maxIncome {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : P.minIncome ≤ P.maxIncome

theorem LeanEconomics.IncomeFluctuation.minConsumption_le_maxConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : P.minConsumption ≤ P.maxConsumption

theorem LeanEconomics.IncomeFluctuation.maxConsumption_pos {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : 0 < P.maxConsumption

theorem LeanEconomics.IncomeFluctuation.mem_dom_of_pos {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {c : ℝ} (hc : 0 < c) : c ∈ P.dom

theorem LeanEconomics.IncomeFluctuation.nonneg_of_mem_dom {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {c : ℝ} (hc : c ∈ P.dom) : 0 ≤ c

theorem LeanEconomics.IncomeFluctuation.maxConsumption_mem_dom {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : P.maxConsumption ∈ P.dom

theorem LeanEconomics.IncomeFluctuation.convex_dom {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : Convex ℝ P.dom

theorem LeanEconomics.IncomeFluctuation.dom_upward {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {c c' : ℝ} (hc : c ∈ P.dom) (h : c ≤ c') : c' ∈ P.dom

The domain is an up-set: if utility behaves at c it behaves at anything larger. Both Ioi 0 and Ici 0 are, and it follows from the two bracketing inclusions alone.

theorem LeanEconomics.IncomeFluctuation.continuousOn_u {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : ContinuousOn P.u (Set.Ioi 0)

Utility behaves on the positives whatever the domain is, so every existing argument that supplies 0 < c keeps working.

theorem LeanEconomics.IncomeFluctuation.monotoneOn_u {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : MonotoneOn P.u (Set.Ioi 0)

theorem LeanEconomics.IncomeFluctuation.strictConcaveOn_u {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : StrictConcaveOn ℝ (Set.Ioi 0) P.u

theorem LeanEconomics.IncomeFluctuation.clampedConsumption_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (p : (ℝ × Z) × ℝ) : 0 ≤ P.clampedConsumption p

theorem LeanEconomics.IncomeFluctuation.clampedConsumption_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (p : (ℝ × Z) × ℝ) : P.clampedConsumption p ≤ P.maxConsumption

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

Discreteness of Z is what makes this continuous.

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

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

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

noncomputable def LeanEconomics.IncomeFluctuation.toExtended {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : ExtendedStochasticProgram (ℝ × Z) ℝ Z

The problem as a stochastic dynamic program with an extended-real reward.

Equations

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

@[simp]

theorem LeanEconomics.IncomeFluctuation.feasible_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.toExtended.feasible s = Set.Icc assetFloor (P.maxSaving s)

theorem LeanEconomics.IncomeFluctuation.maxSaving_le_resources {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.maxSaving s ≤ P.resources s

theorem LeanEconomics.IncomeFluctuation.consumption_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {a : ℝ} (ha : a ∈ P.toExtended.feasible s) : 0 ≤ P.consumption s a

theorem LeanEconomics.IncomeFluctuation.consumption_le_maxConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {a' : ℝ} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (ha' : assetFloor ≤ a') : P.consumption s a' ≤ P.maxConsumption

def LeanEconomics.IncomeFluctuation.Unbounded {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : Prop

Utility is unbounded below: the domain is the open half-line, so the reward is ⊥ at zero consumption. This is the hypothesis under which positive consumption comes free.

Equations

• P.Unbounded = (P.dom = Set.Ioi 0)

theorem LeanEconomics.IncomeFluctuation.clampedConsumption_mem_dom_of_ne_bot {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {a : ℝ} (h : P.toExtended.reward (s, a) ≠ ⊥) : P.clampedConsumption (s, a) ∈ P.dom

theorem LeanEconomics.IncomeFluctuation.consumption_pos_of_ne_bot {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hd : P.Unbounded) {s : ℝ × Z} {a : ℝ} (h : P.toExtended.reward (s, a) ≠ ⊥) : 0 < P.consumption s a

theorem LeanEconomics.IncomeFluctuation.clampedConsumption_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {a : ℝ} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (ha : a ∈ P.toExtended.feasible s) : P.clampedConsumption (s, a) = P.consumption s a

On the feasible set the clamps are both inactive, so the reward's argument is consumption itself.

theorem LeanEconomics.IncomeFluctuation.consumption_mem_dom_of_ne_bot {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {a : ℝ} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (ha : a ∈ P.toExtended.feasible s) (h : P.toExtended.reward (s, a) ≠ ⊥) : P.consumption s a ∈ P.dom

theorem LeanEconomics.IncomeFluctuation.reward_eq_coe_dom {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {a : ℝ} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (ha : a ∈ P.toExtended.feasible s) (hc : P.consumption s a ∈ P.dom) : P.toExtended.reward (s, a) = ↑(P.u (P.consumption s a))

The reward is the utility of consumption, wherever consumption lies in the domain on which utility is required to behave.

theorem LeanEconomics.IncomeFluctuation.reward_eq_coe {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {a : ℝ} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (ha : a ∈ P.toExtended.feasible s) (hc : 0 < P.consumption s a) : P.toExtended.reward (s, a) = ↑(P.u (P.consumption s a))

theorem LeanEconomics.IncomeFluctuation.exists_optimal_saving {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) : ∃ a' ∈ Set.Icc assetFloor (P.maxSaving s), P.consumption s a' ∈ P.dom ∧ P.toExtended.valueFunction s = P.u (P.consumption s a') + ↑P.discount * ∑ z' : Z, P.transitionMatrix s.2 z' * P.toExtended.valueFunction (a', z')

The stochastic Bellman equation, with honest utility and positive consumption. That consumption is positive at the optimum is a consequence of the value being real, not a separate development.

Concavity and the optimal policy

The state is a pair (assets, income state), which is not a module over ℝ, so concavity is stated along the asset slice for each income state -- see LeanEconomics.Blackwell.forall_concaveOn_valueFunction. Everything else follows the deterministic argument, with the continuation value now an expectation: it is concave in next period's assets because each V (·, z') is, and the transition probabilities are nonnegative.

theorem LeanEconomics.IncomeFluctuation.le_convex_comb {c x y θ φ : ℝ} (hx : c ≤ x) (hy : c ≤ y) (hθ : 0 ≤ θ) (hφ : 0 ≤ φ) (hθφ : θ + φ = 1) : c ≤ θ * x + φ * y

A convex combination stays above a common lower bound. Used wherever the borrowing limit has to survive an averaging argument, which with a floor of zero was add_nonneg.

theorem LeanEconomics.IncomeFluctuation.convex_comb_le {c x y θ φ : ℝ} (hx : x ≤ c) (hy : y ≤ c) (hθ : 0 ≤ θ) (hφ : 0 ≤ φ) (hθφ : θ + φ = 1) : θ * x + φ * y ≤ c

theorem LeanEconomics.IncomeFluctuation.resources_eq_affine {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : assetFloor ≤ s.1) : P.resources s = P.income s.2 + (1 + P.interest) * s.1

theorem LeanEconomics.IncomeFluctuation.resources_affine_comb {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {x y θ φ : ℝ} {z : Z} (hx : assetFloor ≤ x) (hy : assetFloor ≤ y) (hθ : 0 ≤ θ) (hφ : 0 ≤ φ) (hθφ : θ + φ = 1) : P.resources (θ * x + φ * y, z) = θ * P.resources (x, z) + φ * P.resources (y, z)

theorem LeanEconomics.IncomeFluctuation.maxSaving_le_assetCap {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.maxSaving s ≤ assetCap

theorem LeanEconomics.IncomeFluctuation.feasible_subset_region {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} {a : ℝ} (ha : a ∈ P.toExtended.feasible s) : a ∈ Set.Icc assetFloor assetCap

theorem LeanEconomics.IncomeFluctuation.maxSaving_eq {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.maxSaving s = min assetCap (P.resources s)

theorem LeanEconomics.IncomeFluctuation.feasible_convex {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {x y : ℝ} {z : Z} (hx : x ∈ Set.Icc assetFloor assetCap) (hy : y ∈ Set.Icc assetFloor assetCap) {ax ay θ φ : ℝ} (hax : ax ∈ P.toExtended.feasible (x, z)) (hay : ay ∈ P.toExtended.feasible (y, z)) (hθ : 0 ≤ θ) (hφ : 0 ≤ φ) (hθφ : θ + φ = 1) : θ * ax + φ * ay ∈ P.toExtended.feasible (θ * x + φ * y, z)

theorem LeanEconomics.IncomeFluctuation.bellmanFn_eq_of_optimal {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {s : ℝ × Z} {a : ℝ} (hs : s.1 ∈ Set.Icc assetFloor assetCap) (ha : a ∈ P.toExtended.feasible s) (heq : P.toExtended.objectiveE v s a = ↑(P.toExtended.bellmanFn v s)) : P.consumption s a ∈ P.dom ∧ P.toExtended.bellmanFn v s = P.u (P.consumption s a) + ↑P.discount * ∑ z' : Z, P.transitionMatrix s.2 z' * v (a, z')

theorem LeanEconomics.IncomeFluctuation.concaveOn_bellman {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (hv : ∀ (z : Z), ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => v (a, z)) (z : Z) : ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => (P.toExtended.bellman v) (a, z)

The Bellman operator preserves concavity along each asset slice.

theorem LeanEconomics.IncomeFluctuation.concaveOn_valueFunction {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z : Z) : ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => P.toExtended.valueFunction (a, z)

The value function is concave in assets, for each income state.

theorem LeanEconomics.IncomeFluctuation.optimal_action_unique_of_concave {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} (hv : ∀ (z : Z), ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => v (a, z)) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) {a₀ a₁ : ℝ} (h₀ : a₀ ∈ P.toExtended.feasible s) (h₁ : a₁ ∈ P.toExtended.feasible s) (hm₀ : P.toExtended.objectiveE v s a₀ = ↑(P.toExtended.bellmanFn v s)) (hm₁ : P.toExtended.objectiveE v s a₁ = ↑(P.toExtended.bellmanFn v s)) : a₀ = a₁

The optimal action is unique for any continuation with concave slices.

theorem LeanEconomics.IncomeFluctuation.optimal_action_unique {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) {a₀ a₁ : ℝ} (h₀ : a₀ ∈ P.toExtended.feasible s) (h₁ : a₁ ∈ P.toExtended.feasible s) (hm₀ : P.toExtended.objectiveE P.toExtended.valueFunction s a₀ = ↑(P.toExtended.bellmanFn P.toExtended.valueFunction s)) (hm₁ : P.toExtended.objectiveE P.toExtended.valueFunction s a₁ = ↑(P.toExtended.bellmanFn P.toExtended.valueFunction s)) : a₀ = a₁

The optimal action is unique.

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

The optimal saving choice.

Equations

• P.policy s = Classical.choose ⋯

theorem LeanEconomics.IncomeFluctuation.policy_mem {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.policy s ∈ P.toExtended.feasible s

theorem LeanEconomics.IncomeFluctuation.policy_optimal {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.toExtended.objectiveE P.toExtended.valueFunction s (P.policy s) = ↑(P.toExtended.bellmanFn P.toExtended.valueFunction s)

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

The optimal saving choice under an arbitrary continuation. At the value function this is definitionally policy.

Equations

• P.policyOf v s = Classical.choose ⋯

theorem LeanEconomics.IncomeFluctuation.policyOf_mem {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (s : ℝ × Z) : P.policyOf v s ∈ P.toExtended.feasible s

theorem LeanEconomics.IncomeFluctuation.policyOf_optimal {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) (s : ℝ × Z) : P.toExtended.objectiveE v s (P.policyOf v s) = ↑(P.toExtended.bellmanFn v s)

theorem LeanEconomics.IncomeFluctuation.policyOf_valueFunction {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : P.policyOf P.toExtended.valueFunction = P.policy

theorem LeanEconomics.IncomeFluctuation.policy_mem_region {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (s : ℝ × Z) : P.policy s ∈ Set.Icc assetFloor assetCap

theorem LeanEconomics.IncomeFluctuation.consumption_policy_mem_dom {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) : P.consumption s (P.policy s) ∈ P.dom

def LeanEconomics.IncomeFluctuation.PositiveConsumption {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : Prop

Consumption never vanishes at the optimum. Automatic when utility is unbounded below (positiveConsumption_of_unbounded); when it is bounded, it has to be earned from a marginal Inada condition, which is what ConsumptionFloor does.

Equations

• P.PositiveConsumption = ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → 0 < P.consumption s (P.policy s)

theorem LeanEconomics.IncomeFluctuation.tendsto_atBot_u {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hd : P.Unbounded) : Filter.Tendsto P.u (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

Utility really does diverge when the domain is the open half-line. The structure no longer carries tendsto_atBot_u, but it has not lost it: continuousOn_extendDom says the extension is continuous at zero consumption, and with dom = Ioi 0 the value there is ⊥.

theorem LeanEconomics.IncomeFluctuation.positiveConsumption_of_unbounded {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hd : P.Unbounded) : P.PositiveConsumption

theorem LeanEconomics.IncomeFluctuation.consumption_policy_pos {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hpc : P.PositiveConsumption) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) : 0 < P.consumption s (P.policy s)

theorem LeanEconomics.IncomeFluctuation.eq_policy_of_optimal {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) {a : ℝ} (ha : a ∈ P.toExtended.feasible s) (hopt : P.toExtended.objectiveE P.toExtended.valueFunction s a = ↑(P.toExtended.bellmanFn P.toExtended.valueFunction s)) : a = P.policy s

theorem LeanEconomics.IncomeFluctuation.argmax_eq_singleton {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) : argmax (P.toExtended.objectiveE P.toExtended.valueFunction) P.toExtended.feasible s = {P.policy s}

theorem LeanEconomics.IncomeFluctuation.continuousOn_policy {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) : ContinuousOn P.policy {s : ℝ × Z | s.1 ∈ Set.Icc assetFloor assetCap}

The optimal policy is continuous on the region of states with assets in [0, assetCap].

theorem LeanEconomics.IncomeFluctuation.valueFunction_eq_policy {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {s : ℝ × Z} (hs : s.1 ∈ Set.Icc assetFloor assetCap) : P.toExtended.valueFunction s = P.u (P.consumption s (P.policy s)) + ↑P.discount * ∑ z' : Z, P.transitionMatrix s.2 z' * P.toExtended.valueFunction (P.policy s, z')

The Bellman equation at the policy.

noncomputable def LeanEconomics.IncomeFluctuation.calibrated : IncomeFluctuation (Fin 2) 0 10

A two-state calibration with σ = 2, where CES utility is -1 / c.

Equations

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