From e81cff3104cd52f5a8d511b2802c42f7e1aa4d91 Mon Sep 17 00:00:00 2001
From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Sat, 27 Apr 2013 15:00:47 +0000
Subject: [PATCH] commit by user andrea

---
 weblib/arithmetics/bigO.ma | 56 ++++++++++++++++++++------------------
 1 file changed, 29 insertions(+), 27 deletions(-)

diff --git a/weblib/arithmetics/bigO.ma b/weblib/arithmetics/bigO.ma
index 95ccd1f43..39e3702f6 100644
--- a/weblib/arithmetics/bigO.ma
+++ b/weblib/arithmetics/bigO.ma
@@ -2,46 +2,46 @@ include "arithmetics/nat.ma".
 include "basics/sets.ma".
 
 (*  O f g means g ∈ O(f) *)
-definition O: relation (nat→nat) ≝
-  λf,g. ∃c.∃n0.∀n. n0 ≤ n → g n ≤ c* (f n).
+definition O: a href="cic:/matita/basics/relations/relation.def(1)"relation/a (a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) ≝
+  λf,g. a title="exists" href="cic:/fakeuri.def(1)"∃/ac.a title="exists" href="cic:/fakeuri.def(1)"∃/an0.∀n. n0 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → g n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a ca title="natural times" href="cic:/fakeuri.def(1)"*/a (f n).
   
-lemma O_refl: ∀s. O s s.
-#s %{1} %{0} #n #_ >commutative_times <times_n_1 @le_n qed.
-
-lemma O_trans: ∀s1,s2,s3. O s2 s1 → O s3 s2 → O s3 s1. 
-#s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1*c2)}
-%{(max n1 n2)} #n #Hmax 
-@(transitive_le … (H1 ??)) [@(le_maxl … Hmax)]
->associative_times @le_times [//|@H2 @(le_maxr … Hmax)]
+lemma O_refl: ∀s. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s s.
+#s %{a title="natural number" href="cic:/fakeuri.def(1)"1/a} %{a title="natural number" href="cic:/fakeuri.def(1)"0/a} #n #_ >a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"commutative_times/a <a href="cic:/matita/arithmetics/nat/times_n_1.def(8)"times_n_1/a @a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a qed.
+
+lemma O_trans: ∀s1,s2,s3. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s2 s1 → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s3 s2 → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s3 s1. 
+#s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1a title="natural times" href="cic:/fakeuri.def(1)"*/ac2)}
+%{(a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n1 n2)} #n #Hmax 
+@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (H1 ??)) [@(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … Hmax)]
+>a href="cic:/matita/arithmetics/nat/associative_times.def(10)"associative_times/a @a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a [//|@H2 @(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … Hmax)]
 qed.
 
-lemma sub_O_to_O: ∀s1,s2. O s1 ⊆ O s2 → O s2 s1.
+lemma sub_O_to_O: ∀s1,s2. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s1 a title="subset" href="cic:/fakeuri.def(1)"⊆/a a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s2 → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s2 s1.
 #s1 #s2 #H @H // qed.
 
-lemma O_to_sub_O: ∀s1,s2. O s2 s1 → O s1 ⊆ O s2.
-#s1 #s2 #H #g #Hg @(O_trans … H) // qed. 
+lemma O_to_sub_O: ∀s1,s2. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s2 s1 → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s1 a title="subset" href="cic:/fakeuri.def(1)"⊆/a a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s2.
+#s1 #s2 #H #g #Hg @(a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"O_trans/a … H) // qed. 
 
-definition sum_f ≝ λf,g:nat→nat.λn.f n + g n.
+definition sum_f ≝ λf,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.λn.f n a title="natural plus" href="cic:/fakeuri.def(1)"+/a g n.
 interpretation "function sum" 'plus f g = (sum_f f g).
 
-lemma O_plus: ∀f,g,s. O s f → O s g → O s (f+g).
+lemma O_plus: ∀f,g,s. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s f → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s g → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s (fa title="function sum" href="cic:/fakeuri.def(1)"+/ag).
 #f #g #s * #cf * #nf #Hf * #cg * #ng #Hg
-%{(cf+cg)} %{(max nf ng)} #n #Hmax normalize 
->distributive_times_plus_r @le_plus 
-  [@Hf @(le_maxl … Hmax) |@Hg @(le_maxr … Hmax) ]
+%{(cfa title="natural plus" href="cic:/fakeuri.def(1)"+/acg)} %{(a href="cic:/matita/arithmetics/nat/max.def(2)"max/a nf ng)} #n #Hmax normalize 
+>a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"distributive_times_plus_r/a @a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a 
+  [@Hf @(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … Hmax) |@Hg @(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … Hmax) ]
 qed.
  
-lemma O_plus_l: ∀f,s1,s2. O s1 f → O (s1+s2) f.
+lemma O_plus_l: ∀f,s1,s2. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s1 f → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a (s1a title="function sum" href="cic:/fakeuri.def(1)"+/as2) f.
 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean 
-@(transitive_le … (Os1f n lean)) @le_times //
+@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (Os1f n lean)) @a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a //
 qed.
 
-lemma O_absorbl: ∀f,g,s. O s f → O f g → O s (g+f).
-#f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
+lemma O_absorbl: ∀f,g,s. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s f → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a f g → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s (ga title="function sum" href="cic:/fakeuri.def(1)"+/af).
+#f #g #s #Osf #Ofg @(a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"O_plus/a … Osf) @(a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"O_trans/a … Osf) //
 qed.
 
-lemma O_absorbr: ∀f,g,s. O s f → O f g → O s (f+g).
-#f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
+lemma O_absorbr: ∀f,g,s. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s f → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a f g → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s (fa title="function sum" href="cic:/fakeuri.def(1)"+/ag).
+#f #g #s #Osf #Ofg @(a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"O_plus/a … Osf) @(a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"O_trans/a … Osf) //
 qed.
 
 (* 
@@ -49,12 +49,14 @@ lemma O_ff: ∀f,s. O s f → O s (f+f).
 #f #s #Osf /2/ 
 qed. *)
 
-lemma O_ext2: ∀f,g,s. O s f → (∀x.f x = g x) → O s g.
+lemma O_ext2: ∀f,g,s. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s f → (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s g.
 #f #g #s * #c * #a #Osf #eqfg %{c} %{a} #n #lean <eqfg @Osf //
 qed.    
 
 
-definition not_O ≝ λf,g.∀c,n0.∃n. n0 ≤ n ∧ c* (f n) < g n .
+definition not_O ≝ λf,g.∀c,n0.a title="exists" href="cic:/fakeuri.def(1)"∃/an. n0 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a ca title="natural times" href="cic:/fakeuri.def(1)"*/a (f n) a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a g n .
 
 (* this is the only classical result *)
-axiom not_O_def: ∀f,g. ¬ O f g → not_O f g.
\ No newline at end of file
+axiom not_O_def: ∀f,g. a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a f g → a href="cic:/matita/arithmetics/bigO/not_O.def(3)"not_O/a f g.
+
+
-- 
2.39.2