Tauchen (1986) chains have monotone transitions

Tauchen's discretisation of z' = ρ z + σ ε, ε ~ N(0,1), on the grid lo, lo + w, …, lo + n w puts on state j the normal mass of the interval of half-width w/2 about lo + j w, with the end states taking the tails. Written through the row's cumulative mass on states below k,

F_i(k) = Φ((lo + k w - w/2 - ρ(lo + i w)) / σ) for 0 < k ≤ n, F_i(0) = 0, F_i(n+1) = 1,

the entry is F_i(j+1) - F_i(j). Everything about the chain is then one fact about Φ: it is monotone. Entries are non-negative and rows sum to one because F_i rises from 0 to 1 in k; the rows are ordered by first-order stochastic dominance because F_i(k) FALLS in i when ρ ≥ 0; and the lowest state is reachable from everywhere because Φ > 0.

There is nothing special about seven states. Aiyagari (1994) used seven; the results here are for n + 1 states, any n.

First-order stochastic dominance on a finite chain

sum_mul_le_of_cum_le is the finite FOSD lemma: if q puts no more mass than p on every initial segment, then q gives the smaller expectation to every antitone f. Summation by parts (Finset.sum_range_by_parts) does it in one line.

The standard normal cdf

noncomputable def LeanEconomics.normalCdf : ℝ → ℝ

The standard normal distribution function Φ.

Equations

• LeanEconomics.normalCdf = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))

theorem LeanEconomics.normalCdf_mono : Monotone normalCdf

theorem LeanEconomics.normalCdf_nonneg (x : ℝ) : 0 ≤ normalCdf x

theorem LeanEconomics.normalCdf_le_one (x : ℝ) : normalCdf x ≤ 1

theorem LeanEconomics.normalCdf_pos (x : ℝ) : 0 < normalCdf x

Φ > 0 everywhere: the normal density is positive and Iic x has positive Lebesgue measure.

The finite FOSD lemma

theorem LeanEconomics.sum_mul_le_of_cum_le {n : ℕ} {p q : Fin (n + 1) → ℝ} {F G : ℕ → ℝ} (hp : ∀ (j : Fin (n + 1)), p j = F (↑j + 1) - F ↑j) (hq : ∀ (j : Fin (n + 1)), q j = G (↑j + 1) - G ↑j) (hF0 : F 0 = 0) (hG0 : G 0 = 0) (hFn : F (n + 1) = 1) (hGn : G (n + 1) = 1) (hle : ∀ (k : ℕ), G k ≤ F k) {f : Fin (n + 1) → ℝ} (hf : ∀ (j j' : Fin (n + 1)), j ≤ j' → f j' ≤ f j) : ∑ j : Fin (n + 1), q j * f j ≤ ∑ j : Fin (n + 1), p j * f j

First-order stochastic dominance on {0, …, n}. Two probability vectors given through cumulative functions F and G (p j = F (j+1) - F j, F 0 = 0, F (n+1) = 1, likewise G), with G ≤ F pointwise — q puts no more mass on any initial segment — give, for every antitone f, the inequality ∑ q f ≤ ∑ p f.

The chain

noncomputable def LeanEconomics.tauchenCum (ρ σ lo w : ℝ) (n : ℕ) (i : Fin (n + 1)) (k : ℕ) : ℝ

Tauchen's cumulative row: the mass row i puts on states below k.

Equations

• LeanEconomics.tauchenCum ρ σ lo w n i k = if k = 0 then 0 else if n + 1 ≤ k then 1 else LeanEconomics.normalCdf ((lo + ↑k * w - w / 2 - ρ * (lo + ↑↑i * w)) / σ)

noncomputable def LeanEconomics.tauchen (ρ σ lo w : ℝ) (n : ℕ) (i j : Fin (n + 1)) : ℝ

Tauchen's transition matrix on n + 1 states.

Equations

• LeanEconomics.tauchen ρ σ lo w n i j = LeanEconomics.tauchenCum ρ σ lo w n i (↑j + 1) - LeanEconomics.tauchenCum ρ σ lo w n i ↑j

theorem LeanEconomics.tauchenCum_zero {ρ σ lo w : ℝ} {n : ℕ} (i : Fin (n + 1)) : tauchenCum ρ σ lo w n i 0 = 0

theorem LeanEconomics.tauchenCum_top {ρ σ lo w : ℝ} {n : ℕ} (i : Fin (n + 1)) : tauchenCum ρ σ lo w n i (n + 1) = 1

theorem LeanEconomics.tauchenCum_mono {ρ σ lo w : ℝ} {n : ℕ} (hσ : 0 < σ) (hw : 0 < w) (i : Fin (n + 1)) : Monotone (tauchenCum ρ σ lo w n i)

The cumulative row rises in k.

theorem LeanEconomics.tauchenCum_anti {ρ σ lo w : ℝ} {n : ℕ} (hρ : 0 ≤ ρ) (hσ : 0 < σ) (hw : 0 < w) {i i' : Fin (n + 1)} (hii' : i ≤ i') (k : ℕ) : tauchenCum ρ σ lo w n i' k ≤ tauchenCum ρ σ lo w n i k

The cumulative row falls in the state when ρ ≥ 0: first-order stochastic dominance.

theorem LeanEconomics.tauchen_nonneg {ρ σ lo w : ℝ} {n : ℕ} (hσ : 0 < σ) (hw : 0 < w) (i j : Fin (n + 1)) : 0 ≤ tauchen ρ σ lo w n i j

theorem LeanEconomics.tauchen_sum {ρ σ lo w : ℝ} {n : ℕ} (i : Fin (n + 1)) : ∑ j : Fin (n + 1), tauchen ρ σ lo w n i j = 1

theorem LeanEconomics.tauchen_pos_zero {ρ σ lo w : ℝ} {n : ℕ} (i : Fin (n + 1)) : 0 < tauchen ρ σ lo w n i 0

The lowest state is reached from everywhere in one step.

theorem LeanEconomics.monotoneTransitions_of_tauchen {ρ σ lo w : ℝ} {n : ℕ} {assetFloor assetCap : ℝ} (P : IncomeFluctuation (Fin (n + 1)) assetFloor assetCap) (hπ : P.transitionMatrix = tauchen ρ σ lo w n) (hinc : StrictMono P.income) (hρ : 0 ≤ ρ) (hσ : 0 < σ) (hw : 0 < w) : P.MonotoneTransitions

A Tauchen chain with ρ ≥ 0 has monotone transitions, for any economy whose income is strictly increasing in the state.