Documentation

Lean 4 Proof

theorem steady_state_unique (S_star M sig_new : ℝ) (hM : 1 < M)
    (hfix : varianceRecurrence S_star M sig_new = S_star) :
    S_star = M * sig_new := by
  simp only [varianceRecurrence] at hfix
  -- hfix : S_star * (1 - 1/M) + sig_new = S_star
  -- => sig_new = S_star - S_star * (1 - 1/M) = S_star * (1/M)
  -- => S_star = M * sig_new
  have hMne : M ≠ 0 := ne_of_gt (by linarith)
  have hsig_eq : sig_new = S_star * (1 / M) := by linarith
  field_simp at hsig_eq
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:93

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file