Documentation

Lean 4 Proof

theorem decay_factor_in_unit (M : ℝ) (hM : 1 < M) :
    0 < 1 - 1 / M ∧ 1 - 1 / M < 1 := by
  constructor
  · rw [sub_pos, div_lt_one (by linarith)]; linarith
  · linarith [div_pos one_pos (by linarith : (0 : ℝ) < M)]

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:50

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file