Documentation

Lean 4 Proof

theorem steady_state_variance (M sig_new : ℝ) (hM : 1 < M) :
    varianceRecurrence (M * sig_new) M sig_new = M * sig_new := by
  simp only [varianceRecurrence]
  have hMne : M ≠ 0 := ne_of_gt (by linarith)
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:85

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file