Documentation

Lean 4 Proof

theorem mode_geometric_decay (k m L : ℕ) (a₀ : ℝ) :
    modeAfterL k m (L + 1) a₀ = modeRate k m * modeAfterL k m L a₀ := by
  simp only [modeAfterL, pow_succ]; ring

Dependency Graph

Location

thesis/CESProofs/Foundations/Emergence.lean:140

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file