Documentation

Lean 4 Proof

theorem modeRate_lt_one {k : ℕ} (hk : 2 ≤ k) {m : ℕ} (hm : 3 ≤ m) :
    modeRate k m < 1 := by
  simp only [modeRate, if_neg (show ¬(m ≤ 2) by omega)]
  apply Real.rpow_lt_one_of_one_lt_of_neg
  · exact_mod_cast (show 1 < k by omega)
  · apply div_neg_of_neg_of_pos
    · rw [neg_lt_zero]
      exact_mod_cast (show 0 < m - 2 by omega)
    · norm_num

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:157

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file