A consumption floor from the margin, not from the level

crra_pinch traced the restriction γ = 1 to tendsto_atBot_u, the requirement that utility fall to -∞ at zero consumption. This file replaces the use of that condition in the one place where it does economic work — the uniform lower bound on consumption at the optimum — by a condition on the MARGIN, which CRRA satisfies for every γ > 0, γ < 1 included.

Minimum income is necessary and not sufficient

A positive lower bound on income does not by itself keep consumption away from zero. It bounds RESOURCES below, not consumption: maxSaving = min assetCap resources, so whenever the cap is slack the household may save everything and consume nothing. Nothing about the income process says it will not.

What minimum income does is make the CONTINUATION Lipschitz where the argument needs it. The deviation argument compares the optimum with saving h less:

u (c + h) - u c ≤ β * (cont a - cont (a - h)),

and the right-hand side has to be bounded by a multiple of h. The continuation is concave and bounded, so its slope from assetFloor to x is at most 2‖V‖ / (x - assetFloor). The positive sustainability bound minConsumption keeps the deviation away from that endpoint: small consumption forces saving at least assetFloor + 3 * minConsumption / 4. The resulting state-independent slope constant is 4‖V‖ / minConsumption, as used by cont_sub_le.

With a state-independent constant L, any consumption level whose marginal value beats β L cannot be optimal, and MarginalInada supplies one. The floor is explicit: min δ (minConsumption / 4).

How the current bounded-domain model uses this result

Divergence at zero has two distinct roles in the unbounded-domain model: it makes extendBot u continuous into EReal and excludes zero consumption at an optimum. The marginal argument here replaces the latter role.

The current IncomeFluctuation structure has a utility-domain field. BoundedIncomeFluctuation takes dom = Ici 0, where extendDom uses the finite value u 0 rather than ⊥, and proves the needed reward continuity. Its marginal Inada argument then establishes positive consumption separately. The floor results here fit that shared structure; they do not require a new household type or a divergence assumption.

def LeanEconomics.MarginalInadaOn (D : Set ℝ) (u : ℝ → ℝ) : Prop

Marginal Inada. Consumption near zero has unboundedly large marginal value, measured by secant slopes so that no derivative is needed. CRRA satisfies this for every γ > 0, including the γ < 1 range where utility itself stays bounded.

Equations

• LeanEconomics.MarginalInadaOn D u = ∀ (M : ℝ), ∃ δ > 0, ∀ (c c' : ℝ), c ∈ D → c < c' → c' ≤ δ → M * (c' - c) ≤ u c' - u c

@[reducible, inline]

abbrev LeanEconomics.MarginalInada (u : ℝ → ℝ) : Prop

The classical form, on the positives.

Equations

• LeanEconomics.MarginalInada u = LeanEconomics.MarginalInadaOn (Set.Ioi 0) u

def LeanEconomics.MarginalBoundOn (D : Set ℝ) (u : ℝ → ℝ) (M : ℝ) : Prop

A marginal lower bound near zero. MarginalInadaOn is this for every M; a utility with finite marginal value at zero -- CARA, or a shifted CRRA -- satisfies it for the M its slope near zero allows, and the consumption floor then has to be earned by an inequality.

Equations

• LeanEconomics.MarginalBoundOn D u M = ∃ δ > 0, ∀ (c c' : ℝ), c ∈ D → c < c' → c' ≤ δ → M * (c' - c) ≤ u c' - u c

theorem LeanEconomics.marginalBoundOn_of_inada {D : Set ℝ} {u : ℝ → ℝ} (h : MarginalInadaOn D u) (M : ℝ) : MarginalBoundOn D u M

theorem LeanEconomics.tendsto_rpow_neg_atTop {γ : ℝ} (hγ : 0 < γ) : Filter.Tendsto (fun (c : ℝ) => c ^ (-γ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

Marginal utility explodes at zero.

theorem LeanEconomics.rpow_neg_antitone {γ : ℝ} (hγ : 0 < γ) {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) : y ^ (-γ) ≤ x ^ (-γ)

theorem LeanEconomics.marginalInada_crraUtility {γ : ℝ} (hγ : 0 < γ) : MarginalInada (crraUtility γ)

CRRA has unbounded marginal value at zero for every γ > 0 — the γ < 1 case included, where the LEVEL condition tendsto_atBot_u fails. This is the whole point.

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

The slope constant an oscillation bound G gives.

Equations

• P.oscSlopeConst G = 2 * G / P.minConsumption

theorem LeanEconomics.IncomeFluctuation.oscSlopeConst_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {G : ℝ} (hG : 0 ≤ G) : 0 ≤ P.oscSlopeConst G

theorem LeanEconomics.IncomeFluctuation.contOf_sub_le_of_osc {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {G : ℝ} (hG : 0 ≤ G) (hv : ∀ (z : Z), ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => v (a, z)) (hosc : P.OscOn v G) (z : Z) {x y : ℝ} (hx : assetFloor + P.minConsumption / 2 ≤ x) (hxy : x < y) (hy : y ∈ Set.Icc assetFloor assetCap) : P.contOf v z y - P.contOf v z x ≤ P.oscSlopeConst G * (y - x)

The continuation's slope, priced by its oscillation, above assetFloor + minConsumption / 2.

theorem LeanEconomics.IncomeFluctuation.exists_consumptionFnOf_floor_of_marginal {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {M G : ℝ} (hM : MarginalBoundOn P.dom P.u M) (hG : 0 ≤ G) {v : BoundedContinuousFunction (ℝ × Z) ℝ} (hv : ∀ (z : Z), ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => v (a, z)) (hosc : P.OscOn v G) (hlt : ↑P.discount * P.oscSlopeConst G < M) : ∃ δ > 0, ∀ (z : Z), ∀ a ∈ Set.Icc assetFloor assetCap, δ ≤ P.consumptionFnOf v z a

The consumption floor, from a finite marginal bound.

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

The state-independent bound on the continuation's slope, read against v.

Equations

• P.contSlopeConstOf v = 4 * ‖v‖ / P.minConsumption

theorem LeanEconomics.IncomeFluctuation.contSlopeConstOf_nonneg {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (v : BoundedContinuousFunction (ℝ × Z) ℝ) : 0 ≤ P.contSlopeConstOf v

theorem LeanEconomics.IncomeFluctuation.contOf_sub_le {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) {x y : ℝ} (hx : assetFloor + P.minConsumption / 2 ≤ x) (hxy : x < y) (hy : y ∈ Set.Icc assetFloor assetCap) : P.contOf v z y - P.contOf v z x ≤ P.contSlopeConstOf v * (y - x)

The continuation's slope is bounded by a state-independent constant, above assetFloor + minConsumption / 2, whatever the continuation.

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

The state-independent bound on the continuation's slope, which is where the positive income floor does its work.

Equations

• P.contSlopeConst = 4 * ‖P.toExtended.valueFunction‖ / P.minConsumption

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

theorem LeanEconomics.IncomeFluctuation.abs_cont_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z : Z) (x : ℝ) : |P.cont z x| ≤ ‖P.toExtended.valueFunction‖

theorem LeanEconomics.IncomeFluctuation.cont_sub_le {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (z : Z) {x y : ℝ} (hx : assetFloor + P.minConsumption / 2 ≤ x) (hxy : x < y) (hy : y ∈ Set.Icc assetFloor assetCap) : P.cont z y - P.cont z x ≤ P.contSlopeConst * (y - x)

The continuation's slope is bounded by a state-independent constant, provided we stay above assetFloor + minConsumption / 2 in savings — which is exactly where the deviation argument lives.

theorem LeanEconomics.IncomeFluctuation.exists_consumptionFnOf_floor_of_marginalInada {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hu : MarginalInadaOn P.dom P.u) {v : BoundedContinuousFunction (ℝ × Z) ℝ} (hv : ∀ (z : Z), ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => v (a, z)) : ∃ δ > 0, ∀ (z : Z), ∀ a ∈ Set.Icc assetFloor assetCap, δ ≤ P.consumptionFnOf v z a

A consumption floor from the margin, against an arbitrary continuation.

theorem LeanEconomics.IncomeFluctuation.exists_consumption_floor_of_marginalInada {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hu : MarginalInadaOn P.dom P.u) : ∃ δ > 0, ∀ (s : ℝ × Z), s.1 ∈ Set.Icc assetFloor assetCap → δ ≤ P.consumption s (P.policy s)

A consumption floor from the margin. No use is made of tendsto_atBot_u: the argument runs on concavity and boundedness of the continuation, a positive income floor, and unbounded marginal value at zero consumption.

theorem LeanEconomics.IncomeFluctuation.policyOf_le_of_marginal_bound {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)) {m : ℝ} (hm : 0 < m) (hmarg : ∀ (c d : ℝ), d ∈ P.dom → d ≤ c → c ≤ P.maxConsumption → m * (c - d) ≤ P.u c - P.u d) {a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (z : Z) : P.policyOf v (a, z) ≤ assetFloor + 4 * ↑P.discount * ‖v‖ / m

A uniform bound on saving from a uniform marginal bound, against any continuation.

theorem LeanEconomics.IncomeFluctuation.positiveConsumption_of_marginalInada {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) (hu : MarginalInadaOn P.dom P.u) : P.PositiveConsumption

The second route to positive consumption. When utility is unbounded below the reward is ⊥ at zero consumption and positivity is free; when it is bounded — CES with γ < 1 — it has to be earned, and this is where. The condition is on MARGINS, which is why it survives the loss of the level condition.

theorem LeanEconomics.IncomeFluctuation.policyOf_le_mul_of_power_marginal {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {γ η θ G : ℝ} (hθ0 : 0 < θ) (hθ1 : θ < 1) {v : BoundedContinuousFunction (ℝ × Z) ℝ} (hv : ∀ (z : Z), ConcaveOn ℝ (Set.Icc assetFloor assetCap) fun (a : ℝ) => v (a, z)) (hG : 0 ≤ G) (hosc : P.OscOn v G) (hmarg : ∀ (c d : ℝ), c ∈ P.dom → c ≤ d → 0 < η + c → (η + d) ^ (-γ) * (d - c) ≤ P.u d - P.u c) {a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (z : Z) (hcpos : 0 < η + P.consumptionFnOf v z a) : P.policyOf v (a, z) - assetFloor ≤ ↑P.discount * G / θ * (η + P.consumptionFnOf v z a + (1 - θ) * (P.policyOf v (a, z) - assetFloor)) ^ γ

A power marginal bound prices the same proportional saving deviation for every utility.

theorem LeanEconomics.IncomeFluctuation.policyOf_lt_cap_of_power_bound {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {γ η θ K : ℝ} (hγ : 0 ≤ γ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) (hK : 0 ≤ K) {v : BoundedContinuousFunction (ℝ × Z) ℝ} {a : ℝ} (ha : a ∈ Set.Icc assetFloor assetCap) (z : Z) (hc : 0 ≤ η + P.consumptionFnOf v z a) (hbound : P.policyOf v (a, z) - assetFloor ≤ K * (η + P.consumptionFnOf v z a + (1 - θ) * (P.policyOf v (a, z) - assetFloor)) ^ γ) (hcap : K * (η + P.maxIncome + (1 + P.interest - θ) * assetCap - (1 - θ) * assetFloor) ^ γ < assetCap - assetFloor) : P.policyOf v (a, z) < assetCap

A proportional power bound keeps saving below the cap under one primitive inequality.