include "nat/iteration2.ma".
include "nat/div_and_mod_diseq.ma".
include "nat/binomial.ma".
+include "nat/log.ma".
theorem sigma_p_div_exp: \forall n,m.
sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
]
qed.
-theorem le_exp_Sn_n_SSSO: \forall n. (exp (S n) n) \le (S(S(S O)))*(exp n n).
-intro.
-apply (trans_le ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
- [apply le_exp_sigma_p_exp
+theorem lt_SO_to_lt_exp_Sn_n_SSSO: \forall n. S O < n \to
+(exp (S n) n) < (S(S(S O)))*(exp n n).
+intros.
+apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
+ [apply lt_exp_sigma_p_exp.assumption
|apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
[apply le_sigma_p.intros.
apply le_times_to_le_div
]
]
]
-qed.
-
-
+qed.
+theorem lt_exp_Sn_n_SSSO: \forall n.
+(exp (S n) n) < (S(S(S O)))*(exp n n).
+intro.cases n;intros
+ [simplify.apply le_S.apply le_n
+ |cases n1;intros
+ [simplify.apply le_n
+ |apply lt_SO_to_lt_exp_Sn_n_SSSO.
+ apply le_S_S.apply le_S_S.apply le_O_n
+ ]
+ ]
+qed.
+
+theorem lt_exp_Sn_m_SSSO: \forall n,m. O < m \to
+divides n m \to
+(exp (S n) m) < (exp (S(S(S O))) (m/n)) *(exp n m).
+intros.
+elim H1.rewrite > H2.
+rewrite < exp_exp_times.
+rewrite < exp_exp_times.
+rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?)).
+rewrite > lt_O_to_div_times
+ [rewrite > times_exp.
+ apply lt_exp1
+ [apply (O_lt_times_to_O_lt ? n).
+ rewrite > sym_times.
+ rewrite < H2.
+ assumption
+ |apply lt_exp_Sn_n_SSSO
+ ]
+ |apply (O_lt_times_to_O_lt ? n2).
+ rewrite < H2.
+ assumption
+ ]
+qed.
+
+theorem le_log_exp_Sn_log_exp_n: \forall n,m,p. O < m \to S O < p \to
+divides n m \to
+log p (exp (S n) m) \le S((m/n)*S(log p (S(S(S O))))) + log p (exp n m).
+intros.
+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
+ ]
+ |apply (trans_le ? (S(log p (exp (S(S(S O))) (m/n)) + log p (exp n m))))
+ [apply log_times.
+ assumption
+ |change in ⊢ (? ? %) with (S (m/n*S (log p (S(S(S O))))+log p ((n)\sup(m)))).
+ apply le_S_S.
+ apply le_plus_l.
+ apply log_exp1.
+ 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
+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.
+elim b
+ [simplify.
+ apply (lt_O_n_elim ? (lt_O_fact n)).intro.
+ apply le_n.
+ |apply (bool_elim ? (leb a n1));intro
+ [rewrite > true_to_sigma_p_Sn
+ [apply (trans_le ? (S (n!/n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(n!))-log p ((a)\sup(n!)))))
+ [rewrite > sym_plus.
+ rewrite > plus_minus
+ [apply le_plus_to_minus_r.
+ rewrite < plus_minus_m_m
+ [rewrite > sym_plus.
+ apply le_log_exp_Sn_log_exp_n
+ [apply lt_O_fact
+ |assumption
+ |
+
+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)))))).
+intros.
+elim n
+ [rewrite > false_to_sigma_p_Sn.
+ simplify.
+ apply (lt_O_n_elim ? H).intro.
+ simplify.apply le_O_n
+ |apply (bool_elim ? (leb a n1));intro
+ [rewrite > true_to_sigma_p_Sn
+ [apply (trans_le ? (S (m/S n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(m))-log p ((a)\sup(m)))))
+ [rewrite > sym_plus.
+ rewrite > plus_minus
+ [apply le_plus_to_minus_r.
+ rewrite < plus_minus_m_m
+ [rewrite > sym_plus.
+ apply le_log_exp_Sn_log_exp_n.
+
+
+(* 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.
+rewrite > exp_S_sigma_p.
+apply le_sigma_p.
+intros.unfold bc.
+apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
+ [rewrite > sym_times.
+ apply le_times_r.
+ rewrite > sym_times.
+ rewrite < eq_div_div_div_times
+ [apply monotonic_div
+ [apply lt_O_fact
+ |apply le_times_to_le_div2
+ [apply lt_O_fact
+ |apply le_fact_exp.
+ apply le_S_S_to_le.
+ assumption
+ ]
+ ]
+ |apply lt_O_fact
+ |apply lt_O_fact
+ ]
+ |apply le_times_div_div_times.
+ apply lt_O_fact
+ ]
+qed.
+theorem lt_exp_sigma_p_exp_m: \forall m,n. S O < n \to
+(exp (S m) n) <
+sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
+intros.
+rewrite > exp_S_sigma_p.
+apply lt_sigma_p
+ [intros.unfold bc.
+ apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
+ [rewrite > sym_times.
+ apply le_times_r.
+ rewrite > sym_times.
+ rewrite < eq_div_div_div_times
+ [apply monotonic_div
+ [apply lt_O_fact
+ |apply le_times_to_le_div2
+ [apply lt_O_fact
+ |apply le_fact_exp.
+ apply le_S_S_to_le.
+ assumption
+ ]
+ ]
+ |apply lt_O_fact
+ |apply lt_O_fact
+ ]
+ |apply le_times_div_div_times.
+ apply lt_O_fact
+ ]
+ |apply (ex_intro ? ? n).
+ split
+ [split
+ [apply le_n
+ |reflexivity
+ ]
+ |rewrite < minus_n_n.
+ rewrite > bc_n_n.
+ simplify.unfold lt.
+ apply le_times_to_le_div
+ [apply lt_O_fact
+ |rewrite > sym_times.
+ rewrite < plus_n_O.
+ apply le_fact_exp1.
+ assumption
+ ]
+ ]
+ ]
+qed.
+theorem lt_SO_to_lt_exp_Sn_n_SSSO_bof: \forall m,n. S O < n \to
+(exp (S m) n) < (S(S(S O)))*(exp m n).
+intros.
+apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!))))
+ [apply lt_exp_sigma_p_exp_m.assumption
+ |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
+ [apply le_sigma_p.intros.
+ apply le_times_to_le_div
+ [apply lt_O_exp.
+ apply lt_O_S
+ |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
+ [apply le_times_div_div_times.
+ apply lt_O_fact
+ |apply le_times_to_le_div2
+ [apply lt_O_fact
+ |rewrite < sym_times.
+ apply le_times_r.
+ apply le_exp_SSO_fact
+ ]
+ ]
+ ]
+ |rewrite > eq_sigma_p_pred
+ [rewrite > div_SO.
+ rewrite > sym_plus.
+ change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
+ apply le_plus_r.
+ apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n)))
+ [apply sigma_p_div_exp
+ |apply le_times_to_le_div2
+ [apply lt_O_exp.
+ apply lt_O_S.
+ |apply le_minus_m
+ ]
+ ]
+ |reflexivity
+ ]
+ ]
+ ]
+qed.
+*)
\ No newline at end of file
projects / helm.git / blobdiff