1 include "arithmetics/nat.ma".
2 include "basics/sets.ma".
4 (* O f g means g ∈ O(f) *)
5 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) ≝
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).
8 lemma O_refl: ∀s.
\ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"
\ 6O
\ 5/a
\ 6 s s.
9 #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.
11 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.
12 #s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6c2)}
13 %{(
\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"
\ 6max
\ 5/a
\ 6 n1 n2)} #n #Hmax
14 @(
\ 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)]
15 >
\ 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)]
18 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.
21 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.
22 #s1 #s2 #H #g #Hg @(
\ 5a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"
\ 6O_trans
\ 5/a
\ 6 … H) // qed.
24 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.
25 interpretation "function sum" 'plus f g = (sum_f f g).
27 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).
28 #f #g #s * #cf * #nf #Hf * #cg * #ng #Hg
29 %{(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
30 >
\ 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
31 [@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) ]
34 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.
35 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean
36 @(
\ 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 //
39 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).
40 #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) //
43 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).
44 #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) //
48 lemma O_ff: ∀f,s. O s f → O s (f+f).
52 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.
53 #f #g #s * #c * #a #Osf #eqfg %{c} %{a} #n #lean <eqfg @Osf //
57 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 .
59 (* this is the only classical result *)
60 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.