Partial progress.

diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma
index c94e713b1b0381684f8ec00528a7ae5f6ce04b77..cb64efee23ede4a7b329cfde8cd311178a91465a 100644 (file)
--- a/helm/software/matita/library/nat/exp.ma
+++ b/helm/software/matita/library/nat/exp.ma
@@ -153,6 +153,15 @@ apply nat_elim2
   ]
 qed.
 
+theorem lt_exp1: \forall n,m,p:nat. O < p \to n < m \to exp n p < exp m p.
+intros.
+elim H
+  [rewrite < exp_n_SO.rewrite < exp_n_SO.assumption
+  |simplify.
+   apply lt_times;assumption
+  ]
+qed.
+
 theorem le_exp_to_le: 
 \forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
 intro.

diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma
index d4e1b2bd991ce58ef77329a8e2bde2dfea7aad7a..3c4f0ad0552870fe83e6ff2cebd00bb666963c51 100644 (file)
--- a/helm/software/matita/library/nat/log.ma
+++ b/helm/software/matita/library/nat/log.ma
@@ -350,6 +350,7 @@ intros.apply (lt_O_n_elim ? H).intros.
 simplify.reflexivity.
 qed.
 
+(*
 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.
@@ -358,9 +359,8 @@ 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
-      [assumption
-      |change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))).
+     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)))
@@ -369,15 +369,13 @@ rewrite < eq_div_div_div_times
     |apply le_times_to_le_div2
       [apply lt_O_exp.assumption
       |simplify.
-*)
-(* falso 
+
 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.
@@ -409,3 +407,4 @@ elim n
   |rewrite > true_to_sigma_p_Sn
     [apply (trans_le ? (m/n1+(log p (exp n1 m))))
       [
+*)
\ No newline at end of file

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index fe9b7ac1a80b5a241e48d84a7ceae64f4fa7f5a4..644db0630e88b7d39ae36573a20a69f321e056c9 100644 (file)
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/neper".
 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 
@@ -211,10 +212,11 @@ intro.elim n
   ]
 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
@@ -248,9 +250,223 @@ apply (trans_le ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
       ]
     ]
   ]
-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