From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 7 Dec 2007 11:38:57 +0000 (+0000)
Subject: A few more theorems.
X-Git-Tag: make_still_working~5720
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=947ee89dec9e60561dfac3ce7e1842f35f178cb8;p=helm.git

A few more theorems.
---

diff --git a/helm/software/matita/library/nat/div_and_mod_diseq.ma b/helm/software/matita/library/nat/div_and_mod_diseq.ma
index 53c59de35..4977df660 100644
--- a/helm/software/matita/library/nat/div_and_mod_diseq.ma
+++ b/helm/software/matita/library/nat/div_and_mod_diseq.ma
@@ -306,3 +306,41 @@ apply (trans_le ? ((a*m/i)/m))
   ]
 qed.
        
+theorem le_div_times_Sm: \forall a,i,m. O < i \to O < m \to
+a / i \le (a * S (m / i))/m.
+intros.
+apply (trans_le ? ((a * S (m / i))/((S (m/i))*i)))
+  [rewrite < (eq_div_div_div_times ? i)
+    [rewrite > lt_O_to_div_times
+      [apply le_n
+      |apply lt_O_S
+      ]
+    |apply lt_O_S
+    |assumption
+    ]
+  |apply le_times_to_le_div
+    [assumption
+    |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
+      [apply le_times_div_div_times.
+       rewrite > (times_n_O O).
+       apply lt_times
+        [apply lt_O_S
+        |assumption
+        ]
+      |rewrite > sym_times.
+       apply le_times_to_le_div2
+        [rewrite > (times_n_O O).
+         apply lt_times
+          [apply lt_O_S
+          |assumption
+          ]
+        |apply le_times_r.
+         apply lt_to_le.
+         apply lt_div_S.
+         assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+
diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma
index d96fb28c2..d4e1b2bd9 100644
--- a/helm/software/matita/library/nat/log.ma
+++ b/helm/software/matita/library/nat/log.ma
@@ -18,6 +18,8 @@ include "datatypes/constructors.ma".
 include "nat/minimization.ma".
 include "nat/relevant_equations.ma".
 include "nat/primes.ma".
+include "nat/iteration2.ma".
+include "nat/div_and_mod_diseq.ma".
 
 definition log \def \lambda p,n.
 max n (\lambda x.leb (exp p x) n).
@@ -246,6 +248,29 @@ intros.elim m
   ]
 qed.
     
+theorem log_exp2: \forall p,n,m.S O < p \to O < n \to
+m*(log p n) \le log p (exp n m).
+intros.
+apply le_S_S_to_le.
+apply (lt_exp_to_lt p)
+  [assumption
+  |rewrite > sym_times.
+   rewrite < exp_exp_times.
+   apply (le_to_lt_to_lt ? (exp n m))
+    [elim m
+      [simplify.apply le_n
+      |simplify.apply le_times
+        [apply le_exp_log.
+         assumption
+        |assumption
+        ]
+      ]
+    |apply lt_exp_log.
+     assumption
+    ]
+  ]
+qed.
+
 theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to 
 log p n \le log p m.
 intros.
@@ -319,3 +344,68 @@ apply antisymmetric_le
     ]
   ]
 qed.
+
+theorem exp_n_O: \forall n. O < n \to exp O n = O.
+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.
+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
+      [assumption
+      |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.
+*)
+(* 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.
+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))))
+      [
diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma
index ec7118980..0186d4324 100644
--- a/helm/software/matita/library/nat/primes.ma
+++ b/helm/software/matita/library/nat/primes.ma
@@ -286,6 +286,28 @@ cut(O \lt c)
 ]
 qed.
 
+theorem eq_div_plus: \forall n,m,d. O < d \to
+divides d n \to divides d m \to
+(n + m ) / d = n/d + m/d.
+intros.
+elim H1.
+elim H2.
+rewrite > H3.rewrite > H4.
+rewrite < distr_times_plus.
+rewrite > sym_times.
+rewrite > sym_times in ⊢ (? ? ? (? (? % ?) ?)).
+rewrite > sym_times in ⊢ (? ? ? (? ? (? % ?))).
+rewrite > lt_O_to_div_times
+  [rewrite > lt_O_to_div_times
+    [rewrite > lt_O_to_div_times
+      [reflexivity
+      |assumption
+      ]
+    |assumption
+    ]
+  |assumption
+  ]
+qed.
 
 (* boolean divides *)
 definition divides_b : nat \to nat \to bool \def