]
qed.
-theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to
+lemma le_log_plus: \forall p,n.S O < p \to log p n \leq log p (S n).
+intros;apply (bool_elim ? (leb (p*(exp p n)) (S n)))
+ [simplify;intro;rewrite > H1;simplify;apply (trans_le ? n)
+ [apply le_log_n_n;assumption
+ |apply le_n_Sn]
+ |intro;unfold log;simplify;rewrite > H1;simplify;apply le_max_f_max_g;
+ intros;apply le_to_leb_true;constructor 2;apply leb_true_to_le;assumption]
+qed.
+
+theorem le_log: \forall p,n,m. S O < p \to n \le m \to
log p n \le log p m.
-intros.
-apply le_S_S_to_le.
-apply (lt_exp_to_lt p)
- [assumption
- |apply (le_to_lt_to_lt ? n)
- [apply le_exp_log.
- assumption
- |apply (le_to_lt_to_lt ? m)
- [assumption
- |apply lt_exp_log.
- assumption
- ]
- ]
- ]
+intros.elim H1
+ [constructor 1
+ |apply (trans_le ? ? ? H3);apply le_log_plus;assumption]
qed.
theorem log_n_n: \forall n. S O < n \to log n n = S O.
[rewrite < (log_n_n i) in ⊢ (? % ?)
[apply le_log
[apply (trans_lt ? n);assumption
- |apply (ltn_to_ltO ? ? H1)
|apply le_n
]
|apply (trans_lt ? n);assumption
]
|apply le_log
[apply (trans_lt ? n);assumption
- |apply (ltn_to_ltO ? ? H1)
|assumption
]
]
apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
[apply le_log
[assumption
- |apply lt_O_exp.
- apply lt_O_S
|apply lt_to_le.
apply lt_exp_Sn_m_SSSO;assumption
]
]
qed.
-theorem le_log_exp_Sn_log_exp_n: \forall a,b,n,p. S O < p \to
-a \le b \to b \le n \to
+theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to
+O < a \to a \le b \to b \le n \to
log p (exp b n!) - log p (exp a n!) \le
sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))).
-intros 6.
+intros 7.
elim b
[simplify.
apply (lt_O_n_elim ? (lt_O_fact n)).intro.
apply le_log_exp_Sn_log_exp_n
[apply lt_O_fact
|assumption
- |
+ |apply divides_fact;
+ [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
+ |apply lt_to_le;assumption]]
+ |apply le_log
+ [assumption
+ |cut (O = exp O n!)
+ [rewrite > Hcut;apply monotonic_exp1;constructor 2;
+ apply leb_true_to_le;assumption
+ |elim n
+ [reflexivity
+ |simplify;rewrite > exp_plus_times;rewrite < H6;
+ rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
+ |apply le_log
+ [assumption
+ |apply monotonic_exp1;apply leb_true_to_le;assumption]]
+ |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
+ rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
+ |assumption]
+ |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
+ rewrite > eq_minus_n_m_O
+ [apply le_O_n
+ |apply le_log
+ [assumption
+ |apply monotonic_exp1;assumption]]]]
+qed.
-theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
+(* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
divides n m \to
log p (exp n m) - log p (exp a m) \le
sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))).
apply le_log_exp_Sn_log_exp_n.
-(* a generalization
+* a generalization
theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le
sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
intros.