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