-(*
-theorem tech1: \forall n,i.O < n \to
-(exp (S n) (S(S i)))/(exp n (S i)) \le ((exp n i) + (exp (S n) (S i)))/(exp n i).
-intros.
-simplify in ⊢ (? (? ? %) ?).
-rewrite < eq_div_div_div_times
- [apply monotonic_div
- [apply lt_O_exp.assumption
- |apply le_S_S_to_le.
- apply lt_times_to_lt_div.
- change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))).
-
-
- |apply (trans_le ? ((n)\sup(i)*(S n)\sup(S i)/(n)\sup(S i)))
- [apply le_times_div_div_times.
- apply lt_O_exp.assumption
- |apply le_times_to_le_div2
- [apply lt_O_exp.assumption
- |simplify.
-
-theorem tech1: \forall a,b,n,m.O < m \to
-n/m \le b \to (a*n)/m \le a*b.
-intros.
-apply le_times_to_le_div2
- [assumption
- |
-
-theorem tech2: \forall n,m. O < n \to
-(exp (S n) m) / (exp n m) \le (n + m)/n.
-intros.
-elim m
- [rewrite < plus_n_O.simplify.
- rewrite > div_n_n.apply le_n
- |apply le_times_to_le_div
- [assumption
- |apply (trans_le ? (n*(S n)\sup(S n1)/(n)\sup(S n1)))
- [apply le_times_div_div_times.
- apply lt_O_exp
- |simplify in ⊢ (? (? ? %) ?).
- rewrite > sym_times in ⊢ (? (? ? %) ?).
- rewrite < eq_div_div_div_times
- [apply le_times_to_le_div2
- [assumption
- |
-
-
-theorem le_log_sigma_p:\forall n,m,p. O < m \to S O < p \to
-log p (exp n m) \le sigma_p n (\lambda i.true) (\lambda i. (m / i)).
-intros.
-elim n
- [rewrite > exp_n_O
- [simplify.apply le_n
- |assumption
- ]
- |rewrite > true_to_sigma_p_Sn
- [apply (trans_le ? (m/n1+(log p (exp n1 m))))
- [
-*)
-*)