Documentation

Lean 4 Proof

theorem double_jeopardy (M sig_new T : ℝ)
    (hM : 0 < M) (hsig : 0 < sig_new) (hT : 0 < T) :
    steadyStateSusceptibility (M / 2) sig_new T <
    steadyStateSusceptibility M sig_new T := by
  simp only [steadyStateSusceptibility]
  apply div_lt_div_of_pos_right _ hT
  exact mul_lt_mul_of_pos_right (by linarith) hsig

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:209

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file