Documentation

Lean 4 Proof

theorem modeRate_pos {k : ℕ} (hk : 1 ≤ k) (m : ℕ) :
    0 < modeRate k m := by
  simp only [modeRate]
  split
  · exact one_pos
  · exact rpow_pos_of_pos (Nat.cast_pos.mpr (by omega)) _

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:145

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file