Documentation

Lean 4 Proof

theorem modeRate_in_unit_interval {k : ℕ} (hk : 2 ≤ k) {m : ℕ} (hm : 3 ≤ m) :
    0 < modeRate k m ∧ modeRate k m < 1 :=
  ⟨modeRate_pos (by omega) m, modeRate_lt_one hk hm⟩

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/Emergence.lean:168

Module Section

Emergence results from Paper 1, Sections 3-5:

In the same file