Documentation

Lean 4 Proof

theorem susceptibility_proportional_to_M (M₁ M₂ sig_new T : ℝ)
    (hT : 0 < T) (hsig : 0 < sig_new) (hM : M₁ < M₂) :
    steadyStateSusceptibility M₁ sig_new T <
    steadyStateSusceptibility M₂ sig_new T := by
  simp only [steadyStateSusceptibility]
  exact div_lt_div_of_pos_right (mul_lt_mul_of_pos_right hM hsig) hT

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:121

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file