Entry Value
Package Name natural-exp-log-thm
Count 13
Theorems
  • exp_log_le : !k n. 1 < k /\ ~(n = 0) ==> k EXP log k n <= n
  • log_eq : !k n m. 1 < k /\ ~(n = 0) ==> (log k n = m <=> k EXP m <= n /\ n < k EXP (m + 1))
  • log_eq_zero : !k n. 1 < k /\ ~(n = 0) ==> (log k n = 0 <=> n < k)
  • log_eq_zero_imp : !k n. 1 < k /\ ~(n = 0) /\ n < k ==> log k n = 0
  • log_lower_bound : !k m n. 1 < k /\ k EXP m <= n ==> m <= log k n
  • log_max : !k m. 1 < k ==> log k (k EXP (m + 1) - 1) = m
  • log_min : !k m. 1 < k ==> log k (k EXP m) = m
  • log_mono : !k n1 n2. 1 < k /\ ~(n1 = 0) /\ n1 <= n2 ==> log k n1 <= log k n2
  • log_mult_upper_bound : !k n1 n2. 1 < k /\ ~(n1 = 0) /\ ~(n2 = 0) ==> log k (n1 * n2) <= log k n1 + log k n2 + 1
  • log_one : !k. 1 < k ==> log k 1 = 0
  • log_recursion : !k n. 1 < k /\ ~(n = 0) ==> log k n = (if n < k then 0 else log k (n DIV k) + 1)
  • log_upper_bound : !k m n. 1 < k /\ ~(n = 0) /\ n < k EXP m ==> log k n < m
  • lt_exp_log : !k n. 1 < k /\ ~(n = 0) ==> n < k EXP (log k n + 1)
  • Back to main package page