CES with γ < 1: utility bounded below

crra_pinch showed that CRRA was confined to log: tendsto_atBot_u forced γ ≥ 1, and Light's uniqueness condition forced γ ≤ 1. This file removes the first half of the pincer.

What had to change, and where

The obstruction was never the axiom by itself. tendsto_atBot_u is what makes extendBot u CONTINUOUS into EReal, and continuity of the reward is what Berge's maximum theorem runs on. With u (0⁺) finite, extendBot u drops from a finite limit to ⊥ at zero consumption: not even upper semicontinuous, so the maximum need not be attained. Deleting the axiom would have broken exists_optimal_action, not weakened it.

IncomeFluctuation was therefore refactored over a utility DOMAIN, with continuousOn_extendDom in place of tendsto_atBot_u. All that remains here is to take dom = Ici 0 and check that CES with γ < 1 fits.

Two things it costs

continuousOn_extendDom is discharged differently — continuousOn_extendDom_Ici below, where the ⊥ branch is simply unreachable — and that part is free.

Positive consumption at the optimum is not. In the unbounded model it is a corollary of the reward being ⊥ there. Here the reward at c = 0 is u 0, a perfectly ordinary number, and the household has to be shown not to want it. That is MarginalInadaOn: marginal utility explodes at zero even though utility itself does not, and positiveConsumption_of_marginalInada turns it into the PositiveConsumption the rest of the development asks for. Note that the condition has to reach c = 0 itself, which is why MarginalInada was generalised to a domain.

What comes for free

Everything stated for IncomeFluctuation: the Bellman equation, uniqueness of the optimal action, concavity and monotonicity of the value function, policy_mono, the Feller property, stationary distributions, the Aiyagari equilibrium machinery. There is no second structure to carry them to.

The domain Ici 0

theorem LeanEconomics.continuousOn_extendDom_Ici {u : ℝ → ℝ} (hc : ContinuousOn u (Set.Ici 0)) : ContinuousOn (extendDom (Set.Ici 0) u) (Set.Ici 0)

The bounded case discharges the continuity requirement trivially. On Ici 0 the ⊥ branch of extendDom is never taken, so what is left is continuity of u itself.

CES with 0 < γ < 1

theorem LeanEconomics.continuousOn_crraUtility_Ici {γ : ℝ} (hγ1 : γ < 1) : ContinuousOn (crraUtility γ) (Set.Ici 0)

theorem LeanEconomics.monotoneOn_crraUtility_Ici {γ : ℝ} (hγ1 : γ < 1) : MonotoneOn (crraUtility γ) (Set.Ici 0)

theorem LeanEconomics.strictConcaveOn_crraUtility_Ici {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) : StrictConcaveOn ℝ (Set.Ici 0) (crraUtility γ)

theorem LeanEconomics.crraUtility_zero {γ : ℝ} (hγ1 : γ < 1) : crraUtility γ 0 = 0

theorem LeanEconomics.marginalInadaOn_Ici_crraUtility {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) : MarginalInadaOn (Set.Ici 0) (crraUtility γ)

CES with γ < 1 has unbounded marginal value AT zero, not merely near it. The level condition tendsto_atBot_u fails here, and this is what replaces it: the household still refuses to consume nothing, because the first unit of consumption is worth more than any bounded gain from the saving it displaces.

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

Utility is bounded below: the domain is the closed half-line.

Equations

• P.Bounded = (P.dom = Set.Ici 0)

theorem LeanEconomics.IncomeFluctuation.positiveConsumption_of_bounded_crra {Z : Type u_1} [Fintype Z] [Nonempty Z] [TopologicalSpace Z] [DiscreteTopology Z] {assetFloor assetCap : ℝ} (P : IncomeFluctuation Z assetFloor assetCap) {γ : ℝ} (hγ0 : 0 < γ) (hγ1 : γ < 1) (hb : P.Bounded) (hu : P.u = crraUtility γ) : P.PositiveConsumption

Positive consumption in the bounded case. The ⊥ at zero consumption is gone, so the argument that used to be free is replaced by a marginal Inada condition.

A CES economy with γ = 1/2

crraUtility (1/2) c = 2 √c, which is finite at c = 0 and therefore inadmissible under the old structure. The parameters are those of dispersed, so the two economies differ only in the curvature of u.

noncomputable def LeanEconomics.sqrtCES : IncomeFluctuation (Fin 2) 0 1

A household with CES utility at γ = 1/2: square-root utility, bounded below.

Equations

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

@[simp]

theorem LeanEconomics.sqrtCES_u : sqrtCES.u = crraUtility (1 / 2)

theorem LeanEconomics.sqrtCES_bounded : sqrtCES.Bounded

theorem LeanEconomics.sqrtCES_u_zero : sqrtCES.u 0 = 0

Utility at zero consumption is finite. This is the fact the old structure forbade.

theorem LeanEconomics.sqrtCES_not_tendsto_atBot : ¬Filter.Tendsto (crraUtility (1 / 2)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atBot

And it is not admissible under the level condition: crra_pinch rejected exactly this.

theorem LeanEconomics.sqrtCES_not_unbounded : ¬sqrtCES.Unbounded

The reward is nonetheless real at zero consumption, so the household could in principle choose it -- and sqrtCES_positiveConsumption is the proof that it does not.

theorem LeanEconomics.sqrtCES_positiveConsumption : sqrtCES.PositiveConsumption

Positive consumption, earned from the margin.

The whole development applies, unchanged

theorem LeanEconomics.sqrtCES_bellman {s : ℝ × Fin 2} (hs : s.1 ∈ Set.Icc 0 1) : ∃ a' ∈ Set.Icc 0 (sqrtCES.maxSaving s), sqrtCES.consumption s a' ∈ sqrtCES.dom ∧ sqrtCES.toExtended.valueFunction s = sqrtCES.u (sqrtCES.consumption s a') + ↑sqrtCES.discount * ∑ z' : Fin 2, sqrtCES.transitionMatrix s.2 z' * sqrtCES.toExtended.valueFunction (a', z')

The Bellman equation, with honest utility.

theorem LeanEconomics.sqrtCES_optimal_action_unique {s : ℝ × Fin 2} (hs : s.1 ∈ Set.Icc 0 1) {a₀ a₁ : ℝ} (h₀ : a₀ ∈ sqrtCES.toExtended.feasible s) (h₁ : a₁ ∈ sqrtCES.toExtended.feasible s) (hm₀ : sqrtCES.toExtended.objectiveE sqrtCES.toExtended.valueFunction s a₀ = ↑(sqrtCES.toExtended.bellmanFn sqrtCES.toExtended.valueFunction s)) (hm₁ : sqrtCES.toExtended.objectiveE sqrtCES.toExtended.valueFunction s a₁ = ↑(sqrtCES.toExtended.bellmanFn sqrtCES.toExtended.valueFunction s)) : a₀ = a₁

The optimal action is unique, from strict concavity on Ici 0.

theorem LeanEconomics.sqrtCES_policy_mono {a a' : ℝ} {z : Fin 2} (ha : a ∈ Set.Icc 0 1) (ha' : a' ∈ Set.Icc 0 1) (hle : a ≤ a') : sqrtCES.policy (a, z) ≤ sqrtCES.policy (a', z)

The policy is increasing in assets at a fixed interest rate. This specializes the asset-monotonicity theorem for IncomeFluctuation.

theorem LeanEconomics.sqrtCES_consumptionFn_pos {a : ℝ} (ha : a ∈ Set.Icc 0 1) (z : Fin 2) : 0 < sqrtCES.consumptionFn z a

Consumption is positive, and increasing in assets.

theorem LeanEconomics.sqrtCES_monotoneOn_consumptionFn (z : Fin 2) : MonotoneOn (sqrtCES.consumptionFn z) (Set.Icc 0 1)

theorem LeanEconomics.sqrtCES_exists_isStationary (μ₀ : MeasureTheory.ProbabilityMeasure sqrtCES.State) : ∃ (μ : MeasureTheory.ProbabilityMeasure sqrtCES.State), sqrtCES.IsStationary μ

A stationary agent distribution exists, by Krylov-Bogolyubov, with aggregate capital equal to mean saving. The distribution half of the development needs no porting either.

theorem LeanEconomics.sqrtCES_aggregateCapital_eq_integral_policy {μ : MeasureTheory.ProbabilityMeasure sqrtCES.State} (hμ : sqrtCES.IsStationary μ) : sqrtCES.aggregateCapital μ = ∫ (s : sqrtCES.State), sqrtCES.policy (sqrtCES.incl s) ∂↑μ