Documentation

Lean 4 Proof

theorem variance_decay_monotone (S₀ : ℝ) (hS : 0 < S₀) (r : ℝ)
    (hr0 : 0 < r) (hr1 : r < 1) (n : ℕ) :
    S₀ * r ^ (n + 1) < S₀ * r ^ n := by
  have : r ^ (n + 1) < r ^ n := by
    rw [pow_succ']
    exact mul_lt_of_lt_one_left (pow_pos hr0 n) hr1
  exact mul_lt_mul_of_pos_left this hS

Dependency Graph

Location

thesis/CESProofs/Dynamics/VarianceCollapse.lean:58

Module Section

Results 86-92: Endogenous Variance Dynamics

In the same file