commit by user andrea

diff --git a/weblib/arithmetics/bigO.ma b/weblib/arithmetics/bigO.ma
index 95ccd1f43c7bb2bf5fc9f1eb8912a89a3b0772be..39e3702f6e4d9675ec2978e7483f22ac3ab2d2d9 100644 (file)
--- 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: \ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) ≝
+  λf,g. \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6n0.∀n. n0 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → g n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 (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. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s s.
+#s %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6} %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6} #n #_ >\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/times_n_1.def(8)"\ 6times_n_1\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 qed.
+
+lemma O_trans: ∀s1,s2,s3. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 s1 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s3 s2 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s3 s1. 
+#s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c2)}
+%{(\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n1 n2)} #n #Hmax 
+@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … (H1 ??)) [@(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … Hmax)]
+>\ 5a href="cic:/matita/arithmetics/nat/associative_times.def(10)"\ 6associative_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 [//|@H2 @(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … Hmax)]
 qed.
 
-lemma sub_O_to_O: ∀s1,s2. O s1 ⊆ O s2 → O s2 s1.
+lemma sub_O_to_O: ∀s1,s2. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s1 \ 5a title="subset" href="cic:/fakeuri.def(1)"\ 6⊆\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 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. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 s1 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s1 \ 5a title="subset" href="cic:/fakeuri.def(1)"\ 6⊆\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2.
+#s1 #s2 #H #g #Hg @(\ 5a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"\ 6O_trans\ 5/a\ 6 … H) // qed. 
 
-definition sum_f ≝ λf,g:nat→nat.λn.f n + g n.
+definition sum_f ≝ λf,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.λn.f n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 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. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s f → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s g → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s (f\ 5a title="function sum" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6g).
 #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) ]
+%{(cf\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6cg)} %{(\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 nf ng)} #n #Hmax normalize 
+>\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"\ 6le_plus\ 5/a\ 6 
+  [@Hf @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … Hmax) |@Hg @(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … Hmax) ]
 qed.
  
-lemma O_plus_l: ∀f,s1,s2. O s1 f → O (s1+s2) f.
+lemma O_plus_l: ∀f,s1,s2. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s1 f → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 (s1\ 5a title="function sum" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6s2) f.
 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean 
-@(transitive_le … (Os1f n lean)) @le_times //
+@(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … (Os1f n lean)) @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 //
 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. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s f → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 f g → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s (g\ 5a title="function sum" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6f).
+#f #g #s #Osf #Ofg @(\ 5a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"\ 6O_plus\ 5/a\ 6 … Osf) @(\ 5a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"\ 6O_trans\ 5/a\ 6 … 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. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s f → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 f g → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s (f\ 5a title="function sum" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6g).
+#f #g #s #Osf #Ofg @(\ 5a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"\ 6O_plus\ 5/a\ 6 … Osf) @(\ 5a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"\ 6O_trans\ 5/a\ 6 … 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. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s f → (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 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.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6n. n0 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 (f n) \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 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. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 f g → \ 5a href="cic:/matita/arithmetics/bigO/not_O.def(3)"\ 6not_O\ 5/a\ 6 f g.
+
+