pith. machine review for the scientific record. sign in
lemma proved tactic proof

log2_succ_le

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  96private lemma log2_succ_le (n : Nat) : Nat.log2 n.succ ≤ n := by

proof body

Tactic-mode proof.

  97  rw [Nat.log2_eq_log_two]
  98  have h1 : 1 < 2 := by norm_num
  99  have h3 : n.succ ≠ 0 := by omega
 100  have hlt : Nat.log 2 n.succ < n.succ := by
 101    rw [Nat.log_lt_iff_lt_pow h1 h3]
 102    have h4 : n.succ.succ ≤ 2^n.succ := succ_le_two_pow n.succ
 103    calc n.succ < n.succ.succ := by omega
 104      _ ≤ 2 ^ n.succ := h4
 105  omega
 106
 107/-- maxOctantLevel n ≤ n (since log2(n+1)/3 ≤ log2(n+1) ≤ n). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.