Documentation

Lean 4 Proof

theorem variance_decay_nonneg (S₀ : ℝ) (hS : 0 ≤ S₀) (M : ℝ) (hM : 1 < M) (n : ℕ) :
    0 ≤ S₀ * (1 - 1 / M) ^ n := by
  apply mul_nonneg hS
  apply pow_nonneg
  have : 0 < 1 - 1 / M := by rw [sub_pos, div_lt_one (by linarith)]; linarith
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:40

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file