-theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
-reflexivity.
-qed.
-
-lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
-reflexivity.
-qed.
-(*
-theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
-reflexivity.
-qed.
-*)
-theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
-reflexivity.
-qed.
-
-theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to
-n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
-intros.
-elim H
- [rewrite > factS in ⊢ (? (? %) ?).
- rewrite > factS in ⊢ (? (? (? ? %)) ?).
- rewrite < assoc_times in ⊢ (? (? %) ?).
- rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
- rewrite > assoc_times in ⊢ (? (? %) ?).
- change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
-
-theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
-intro.apply (nat_elim1 n).
-intros.
-elim (lt_O_to_or_eq_S m)
- [elim H2.clear H2.
- elim H4.clear H4.
- rewrite > H2.
- apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
- [apply monotonic_log.
- apply fact1
- |rewrite > assoc_times in ⊢ (? (? %) ?).
- rewrite > log_exp.
- apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
- [apply le_plus_r.
- apply log_times
- |rewrite > plus_n_Sm.
- rewrite > log_SSO.
- rewrite < times_n_Sm.
- apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
- [apply le_plus_r.
- apply le_plus_r.
- apply H.assumption
- |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
- [apply lt_plus_r.
- apply lt_plus_l.
- apply H.
- assumption.
- |rewrite > times_SSO_n.
- rewrite > distr_times_minus.
- rewrite > sym_plus.
- rewrite > plus_minus
- [rewrite > sym_plus.
- rewrite < assoc_times.
- apply le_n
- |rewrite < assoc_times.
- rewrite > times_n_SO in ⊢ (? % ?).
- apply le_times
- [apply le_n
- |apply lt_O_log.
- apply (lt_times_n_to_lt_r (S(S O)))
- [apply lt_O_S
- |rewrite < times_n_SO.
- rewrite < H2.
- assumption
- ]
- ]
- ]
- ]
-
- .
- ]
- |
- rewrite < eq_plus_minus_minus_plus.
-
- rewrite > assoc_plus.
- apply lt_plus_r.
- rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
- change with
- (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
- apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
- [apply le_S_S.
- apply lt_plus_r.
- apply lt_times_r.
- apply H.
- assumption
- |
-
-theorem stirling: \forall n,k.k \le n \to
-log (fact n) < n*log n - n + k*log n.
-intro.
-apply (nat_elim1 n).
-intros.
-elim (lt_O_to_or_eq_S m)
- [elim H2.clear H2.
- elim H4.clear H4.
- rewrite > H2.
- apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
- [apply monotonic_log.
- apply fact1
- |rewrite > assoc_times in ⊢ (? (? %) ?).
- rewrite > log_exp.
- apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
- [apply le_plus_r.
- apply log_times
- |rewrite < plus_n_Sm.
- rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
- change with
- (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
- apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
- [apply le_S_S.
- apply lt_plus_r.
- apply lt_times_r.
- apply H.
- assumption
- |
-
- [
-
- a*log a-a+k*log a
-