Import normalized clearing for capped log households

LeanPool/AiyagariEquilibrium.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2026 Robert Kirkby. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Kirkby
+-/
+
+module
+
+public import LeanPool.AiyagariEquilibrium.Models.AiyagariTauchenWitness
+public import LeanPool.AiyagariEquilibrium.Equilibrium.Bisection
+
+/-!
+# Normalized capped log-household clearing and dynamic programming
+
+Source: url:https://github.com/LeanEconomics/LeanEconomics
+Authors: Robert Kirkby
+Status: verified
+Main declarations: `LeanEconomics.aiyagariTauchen_equilibriumRate_unique_Ioo`
+Tags: mathematical-economics, dynamic-programming, stationary-equilibrium, markov-processes
+MSC: 91B50, 90C39, 60J05
+-/

LeanPool/AiyagariEquilibrium/Analysis/DecreasingIncrements.lean

@@ -0,0 +1,161 @@
+/-
+Copyright (c) 2026 Robert Kirkby. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Kirkby
+-/
+
+module
+public import Mathlib.Analysis.Convex.SpecificFunctions.Basic
+
+/-!
+# Decreasing increments of a concave function
+
+Numbered Light references use the October 31, 2018 author draft, printed page 13:
+https://www.researchgate.net/publication/314238962
+
+A concave function's increment over an interval of fixed length shrinks as the interval
+slides right. In economics this is the increasing-differences (supermodularity) condition
+that monotone-comparative-statics arguments run on, usually stated as a cross partial
+`-u'' > 0`. Stated this way it needs no derivatives and no smoothness at all.
+
+The proof is two applications of concavity. Writing `L = (c₂ + Δ) - c₁`, the two interior
+points `c₁ + Δ` and `c₂` are *complementary* convex combinations of the endpoints `c₁` and
+`c₂ + Δ`: the weights on `c₂ + Δ` are `Δ / L` and `(c₂ - c₁) / L`, which sum to one. Adding
+the two concavity inequalities makes the weights cancel.
+-/
+
+@[expose] public section
+
+open Set
+
+/-- **Decreasing increments.** For a concave `u`, sliding an interval to the right by `Δ`
+cannot increase the increment of `u` across it. -/
+theorem ConcaveOn.sub_le_sub_of_shift {s : Set ℝ} {u : ℝ → ℝ} (hu : ConcaveOn ℝ s u)
+    {c₁ c₂ Δ : ℝ} (h₁ : c₁ ∈ s) (h₂ : c₂ + Δ ∈ s) (hc : c₁ ≤ c₂) (hΔ : 0 ≤ Δ) :
+    u (c₂ + Δ) - u (c₁ + Δ) ≤ u c₂ - u c₁ := by
+  rcases eq_or_lt_of_le (show c₁ ≤ c₂ + Δ by linarith) with hdeg | hpos
+  · -- `c₁ = c₂ + Δ` forces `Δ = 0` and `c₁ = c₂`, and the claim is an equality
+    have hΔ0 : Δ = 0 := by linarith
+    have hcc : c₁ = c₂ := by linarith
+    subst hΔ0
+    simp [hcc]
+  · have hL : 0 < c₂ + Δ - c₁ := by linarith
+    set θ : ℝ := Δ / (c₂ + Δ - c₁) with hθdef
+    have hθ0 : 0 ≤ θ := div_nonneg hΔ hL.le
+    have hθ1 : 0 ≤ 1 - θ := by
+      rw [hθdef, sub_nonneg, div_le_one hL]
+      linarith
+    -- `c₁ + Δ` and `c₂` are complementary convex combinations of `c₁` and `c₂ + Δ`
+    have e1 : (1 - θ) * c₁ + θ * (c₂ + Δ) = c₁ + Δ := by
+      rw [hθdef]; field_simp; ring
+    have e2 : θ * c₁ + (1 - θ) * (c₂ + Δ) = c₂ := by
+      rw [hθdef]; field_simp; ring
+    have i1 := hu.2 h₁ h₂ hθ1 hθ0 (by ring)
+    have i2 := hu.2 h₁ h₂ hθ0 hθ1 (by ring)
+    rw [smul_eq_mul, smul_eq_mul, smul_eq_mul, smul_eq_mul, e1] at i1
+    rw [smul_eq_mul, smul_eq_mul, smul_eq_mul, smul_eq_mul, e2] at i2
+    nlinarith [i1, i2]
+
+/-! ### Lipschitz away from the left endpoint
+
+A concave function on `Ioi 0` need not be Lipschitz there -- utility functions used in
+economics are exactly the ones that are not, diverging at zero -- but it IS Lipschitz on
+`[δ, ∞)` for any `δ > 0`, with a constant read off a single secant. No differentiability is
+needed: the bound comes from antitonicity of secant slopes.
+
+This is what lets a marginal argument be run without a derivative. Where the textbook
+argument bounds the marginal utility of consumption by `u'(δ)`, this bounds it by the slope
+of `u` across `[δ/2, δ]`, which is available from concavity alone. -/
+
+/-- The secant slope of `u` across `[δ/2, δ]`, which bounds every slope further right. -/
+noncomputable def slopeBound (u : ℝ → ℝ) (δ : ℝ) : ℝ := (u δ - u (δ / 2)) / (δ / 2)
+
+theorem slopeBound_nonneg {u : ℝ → ℝ} (hmono : MonotoneOn u (Ioi 0)) {δ : ℝ} (hδ : 0 < δ) :
+    0 ≤ slopeBound u δ := by
+  refine div_nonneg (sub_nonneg.mpr (hmono ?_ ?_ (by linarith))) (by linarith)
+  · exact mem_Ioi.mpr (by linarith)
+  · exact mem_Ioi.mpr hδ
+
+/-- The one-sided bound: moving right from `a ≥ δ` raises `u` by at most the slope bound
+times the distance. -/
+theorem ConcaveOn.sub_le_slopeBound_mul {u : ℝ → ℝ} (hu : ConcaveOn ℝ (Ioi 0) u) {δ : ℝ}
+    (hδ : 0 < δ) {a b : ℝ} (ha : δ ≤ a) (hab : a ≤ b) :
+    u b - u a ≤ slopeBound u δ * (b - a) := by
+  rcases eq_or_lt_of_le hab with rfl | hlt
+  · simp
+  have hhalf : (0 : ℝ) < δ / 2 := by linarith
+  have hmemh : δ / 2 ∈ Ioi (0 : ℝ) := mem_Ioi.mpr hhalf
+  have hmemd : δ ∈ Ioi (0 : ℝ) := mem_Ioi.mpr hδ
+  have hmema : a ∈ Ioi (0 : ℝ) := mem_Ioi.mpr (by linarith)
+  have hmemb : b ∈ Ioi (0 : ℝ) := mem_Ioi.mpr (by linarith)
+  -- the slope across `[a, b]` is at most the slope bound
+  have hkey : (u b - u a) / (b - a) ≤ slopeBound u δ := by
+    rcases eq_or_lt_of_le ha with rfl | hgt
+    · -- `a = δ`: one step
+      have h := hu.slope_anti_adjacent hmemh hmemb (by linarith) hlt
+      simpa only [slopeBound, show δ - δ / 2 = δ / 2 by ring] using h
+    · -- `a > δ`: chain two steps through `δ`
+      have h1 := hu.slope_anti_adjacent hmemd hmemb hgt hlt
+      have h2 := hu.slope_anti_adjacent hmemh hmema (by linarith) hgt
+      simp only [slopeBound, show δ - δ / 2 = δ / 2 by ring] at h2 ⊢
+      linarith
+  rw [div_le_iff₀ (by linarith)] at hkey
+  linarith
+
+/-- **A concave function is Lipschitz away from the left endpoint**, with an explicit
+constant and no appeal to differentiability. -/
+theorem ConcaveOn.abs_sub_le_slopeBound_mul {u : ℝ → ℝ} (hu : ConcaveOn ℝ (Ioi 0) u)
+    (hmono : MonotoneOn u (Ioi 0)) {δ : ℝ} (hδ : 0 < δ) {x y : ℝ}
+    (hx : δ ≤ x) (hy : δ ≤ y) :
+    |u x - u y| ≤ slopeBound u δ * |x - y| := by
+  rcases le_total y x with h | h
+  · rw [abs_of_nonneg (sub_nonneg.mpr (hmono (mem_Ioi.mpr (by linarith))
+      (mem_Ioi.mpr (by linarith)) h)), abs_of_nonneg (by linarith)]
+    exact hu.sub_le_slopeBound_mul hδ hy h
+  · rw [abs_sub_comm, abs_sub_comm x y,
+      abs_of_nonneg (sub_nonneg.mpr (hmono (mem_Ioi.mpr (by linarith))
+        (mem_Ioi.mpr (by linarith)) h)), abs_of_nonneg (by linarith)]
+    exact hu.sub_le_slopeBound_mul hδ hx h
+
+/-! ### Scaling a concave function
+
+For a concave, strictly positive `z`, the ratio `α / z (α x)` rises with `α`. This is Lemma 4
+of Light (2018), one of the three ingredients of his Theorem 1 (savings rise with the interest
+rate when relative risk aversion is at most one).
+
+Like the increments lemma above, it needs no derivative: `α₁ x` is a convex combination of `0`
+and `α₂ x` with weight `α₁ / α₂`, so concavity gives the inequality directly, and strict
+positivity at the origin is what turns it from weak into the stated form.
+-/
+
+/-- **Light (2018), Lemma 4**, on any convex set containing the origin. In the application `z`
+is the consumption function, which is concave on the asset region and nowhere else, so the
+original statement over `[0, ∞)` would not reach it. Positivity is needed only at the origin
+and at the far point: concavity carries it to everything in between. -/
+theorem ConcaveOn.div_le_div_of_scale {z : ℝ → ℝ} {s : Set ℝ} (hz : ConcaveOn ℝ s z)
+    (h0 : (0 : ℝ) ∈ s) (hz0 : 0 < z 0) {α₁ α₂ x : ℝ} (h1 : 0 < α₁) (h12 : α₁ ≤ α₂)
+    (hm2 : α₂ * x ∈ s) (hp2 : 0 < z (α₂ * x)) :
+    α₁ / z (α₁ * x) ≤ α₂ / z (α₂ * x) := by
+  have h2 : 0 < α₂ := lt_of_lt_of_le h1 h12
+  -- `α₁ x` is a convex combination of `0` and `α₂ x`
+  have hcomb : (1 - α₁ / α₂) • (0 : ℝ) + (α₁ / α₂) • (α₂ * x) = α₁ * x := by
+    simp only [smul_eq_mul, mul_zero, zero_add]
+    field_simp
+  have hw1 : (0 : ℝ) ≤ 1 - α₁ / α₂ := by
+    rw [sub_nonneg, div_le_one h2]; exact h12
+  have hw2 : (0 : ℝ) < α₁ / α₂ := div_pos h1 h2
+  have hcc := hz.2 h0 hm2 hw1 hw2.le (by ring)
+  rw [hcomb] at hcc
+  simp only [smul_eq_mul] at hcc
+  -- concavity carries positivity from the endpoints to `α₁ x`
+  have hp1 : 0 < z (α₁ * x) := by
+    nlinarith [mul_nonneg hw1 hz0.le, mul_pos hw2 hp2]
+  rw [div_le_div_iff₀ hp1 hp2]
+  have hkey : α₁ * z (α₂ * x) ≤ α₂ * z (α₁ * x) := by
+    have hmul := mul_le_mul_of_nonneg_left hcc h2.le
+    have hexp : α₂ * ((1 - α₁ / α₂) * z 0 + α₁ / α₂ * z (α₂ * x))
+        = (α₂ - α₁) * z 0 + α₁ * z (α₂ * x) := by field_simp
+    rw [hexp] at hmul
+    have hz0' : 0 ≤ (α₂ - α₁) * z 0 := mul_nonneg (by linarith) hz0.le
+    linarith
+  linarith

LeanPool/AiyagariEquilibrium/Analysis/DifferentiableSandwich.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Robert Kirkby. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Kirkby
+-/
+
+module
+public import Mathlib.Analysis.Convex.Deriv
+
+/-!
+# The Differentiable Sandwich Lemma
+
+A function squeezed between two functions that are differentiable at a point, and agreeing
+with both at that point, is itself differentiable there, with the same derivative.
+
+This is Lemma 1 of Clausen and Strub (2020), "Reverse Calculus and Nested Optimization",
+*Journal of Economic Theory* 187, 105019, and it is the foundation of their approach to
+envelope theorems. Their point is that it needs neither concavity nor interiority, so it
+applies where Benveniste–Scheinkman does not — in particular where a constraint binds, which
+in a Bewley economy is exactly the states that matter, since the borrowing constraint is where
+the whole ergodic argument lives.
+
+The proof is two moves. The gap `U - L` is nonnegative near the point and vanishes at it, so
+it has a local minimum there and its derivative is zero, which forces the two derivatives to
+agree. Then the difference quotients of `F` are squeezed between those of `L` and `U`.
+
+Mathlib has the local-minimum step (`IsLocalMin.hasDerivAt_eq_zero`) but not this lemma.
+-/
+
+@[expose] public section
+
+open Filter Topology Asymptotics
+
+/-- **Differentiable Sandwich Lemma** (Clausen–Strub 2020, Lemma 1). If `F` is squeezed
+between `L` and `U` near `c`, all three agree at `c`, and `L` and `U` are differentiable at
+`c`, then the two derivatives coincide and `F` is differentiable at `c` with that derivative. -/
+theorem hasDerivAt_of_sandwich {F L U : ℝ → ℝ} {c l u : ℝ} {N : Set ℝ} (hN : N ∈ 𝓝 c)
+    (hLF : ∀ x ∈ N, L x ≤ F x) (hFU : ∀ x ∈ N, F x ≤ U x)
+    (hLc : L c = F c) (hUc : U c = F c)
+    (hL : HasDerivAt L l c) (hU : HasDerivAt U u c) :
+    l = u ∧ HasDerivAt F l c := by
+  -- the gap has a local minimum at `c`, so the derivatives agree
+  have hd : HasDerivAt (fun x => U x - L x) (u - l) c := hU.sub hL
+  have hmin : IsLocalMin (fun x => U x - L x) c := by
+    filter_upwards [hN] with x hx
+    have h1 := hLF x hx
+    have h2 := hFU x hx
+    simp only [hLc, hUc]
+    linarith
+  have hul : u - l = 0 := hmin.hasDerivAt_eq_zero hd
+  have hlu : l = u := by linarith
+  refine ⟨hlu, ?_⟩
+  -- and the difference quotients of `F` are squeezed
+  have hU' : HasDerivAt U l c := by rwa [hlu]
+  rw [hasDerivAt_iff_isLittleO, isLittleO_iff]
+  intro ε hε
+  have hA := isLittleO_iff.mp (hasDerivAt_iff_isLittleO.mp hL) hε
+  have hB := isLittleO_iff.mp (hasDerivAt_iff_isLittleO.mp hU') hε
+  filter_upwards [hA, hB, hN] with y hya hyb hyn
+  rw [Real.norm_eq_abs] at hya hyb ⊢
+  have h1 := hLF y hyn
+  have h2 := hFU y hyn
+  rw [abs_le] at hya hyb ⊢
+  simp only [smul_eq_mul] at hya hyb ⊢
+  rw [hLc] at hya
+  rw [hUc] at hyb
+  constructor <;> linarith [hya.1, hya.2, hyb.1, hyb.2]
+
+/-! ### The supporting line
+
+The upper half of the sandwich, for a concave function of one real variable. Mathlib has no
+subgradient or supporting-hyperplane theory for convex or concave FUNCTIONS, but in one
+dimension the slope API suffices: `ConcaveOn.slope_anti` says secant slopes through a point
+are antitone, so every slope to the left is at least every slope to the right, and the
+infimum of the left slopes separates them.
+
+Clausen and Strub note that concavity is needed only for this half — the lower bound in the
+sandwich need not be concave, which is where they improve on Rockafellar's antecedent. For a
+value function that matters: concavity is available here, and the lazy agent's lower bound
+would not have to be concave in the state.
+-/
+
+/-- **A concave function has a supporting line at any point with neighbours on both sides.**
+The slope is the infimum of the secant slopes to the left. -/
+theorem ConcaveOn.exists_supportingLine {f : ℝ → ℝ} {s : Set ℝ} (hf : ConcaveOn ℝ s f)
+    {x : ℝ} (hx : x ∈ s) (hlt : ∃ y ∈ s, y < x) (hgt : ∃ y ∈ s, x < y) :
+    ∃ m : ℝ, ∀ y ∈ s, f y ≤ f x + m * (y - x) := by
+  classical
+  have hanti := hf.slope_anti hx
+  obtain ⟨y₁, hy₁s, hy₁⟩ := hlt
+  obtain ⟨y₂, hy₂s, hy₂⟩ := hgt
+  -- every slope to the left dominates every slope to the right
+  have hcross : ∀ z ∈ s, z < x → ∀ y ∈ s, x < y → slope f x y ≤ slope f x z := by
+    intro z hzs hz y hys hy
+    exact hanti ⟨hzs, by simp [ne_of_lt hz]⟩ ⟨hys, by simp [ne_of_gt hy]⟩ (le_of_lt (hz.trans hy))
+  set Lset : Set ℝ := slope f x '' {y ∈ s | y < x} with hLdef
+  have hne : Lset.Nonempty := ⟨slope f x y₁, ⟨y₁, ⟨hy₁s, hy₁⟩, rfl⟩⟩
+  have hbdd : BddBelow Lset := by
+    refine ⟨slope f x y₂, ?_⟩
+    rintro _ ⟨z, ⟨hzs, hz⟩, rfl⟩
+    exact hcross z hzs hz y₂ hy₂s hy₂
+  refine ⟨sInf Lset, fun y hy => ?_⟩
+  rcases lt_trichotomy y x with h | h | h
+  · -- to the left: the slope is at least the infimum
+    have hmem : slope f x y ∈ Lset := ⟨y, ⟨hy, h⟩, rfl⟩
+    have hle : sInf Lset ≤ slope f x y := csInf_le hbdd hmem
+    rw [slope_def_field, le_div_iff_of_neg (by linarith)] at hle
+    linarith
+  · subst h; simp
+  · -- to the right: the slope is a lower bound for the left slopes, hence below the infimum
+    have hle : slope f x y ≤ sInf Lset := by
+      refine le_csInf hne ?_
+      rintro _ ⟨z, ⟨hzs, hz⟩, rfl⟩
+      exact hcross z hzs hz y hy h
+    rw [slope_def_field, div_le_iff₀ (by linarith)] at hle
+    linarith
+
+/-- **A concave function with a differentiable lower bound touching at a point is
+differentiable there**, with the lower bound's derivative.
+
+This is the form the envelope theorem uses: concavity supplies the upper half of the sandwich
+automatically, so only the lower bound has to be produced, and Clausen and Strub produce it
+with the lazy agent — freeze the optimal choice and vary the state, which is differentiable
+because the state then enters only through the reward. -/
+theorem ConcaveOn.hasDerivAt_of_lowerBound {f L : ℝ → ℝ} {s : Set ℝ} {x l : ℝ}
+    (hf : ConcaveOn ℝ s f) (hx : x ∈ s) (hs : s ∈ 𝓝 x)
+    (hlt : ∃ y ∈ s, y < x) (hgt : ∃ y ∈ s, x < y)
+    (hLf : ∀ y ∈ s, L y ≤ f y) (hLx : L x = f x) (hL : HasDerivAt L l x) :
+    HasDerivAt f l x := by
+  obtain ⟨m, hm⟩ := hf.exists_supportingLine hx hlt hgt
+  have hU : HasDerivAt (fun y => f x + m * (y - x)) m x := by
+    simpa using (((hasDerivAt_id x).sub_const x).const_mul m).const_add (f x)
+  exact (hasDerivAt_of_sandwich hs hLf hm hLx (by simp) hL hU).2