Documentation

Lean 4 Proof

theorem minimum_information_sources (S_min sig_new T : ℝ)
    (hS : 0 < S_min) (hsig : 0 < sig_new) (hT : 0 < T)
    (M : ℝ) (hM_ge : S_min / sig_new ≤ M) :
    S_min / T ≤ steadyStateSusceptibility M sig_new T := by
  simp only [steadyStateSusceptibility]
  apply div_le_div_of_nonneg_right _ (le_of_lt hT)
  calc S_min = S_min / sig_new * sig_new := by field_simp
    _ ≤ M * sig_new := by apply mul_le_mul_of_nonneg_right hM_ge (le_of_lt hsig)

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:186

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file