equal
deleted
inserted
replaced
1097 apply (simp add: fun_diff_def) |
1097 apply (simp add: fun_diff_def) |
1098 done |
1098 done |
1099 |
1099 |
1100 subsection {* Less than or equal to *} |
1100 subsection {* Less than or equal to *} |
1101 |
1101 |
1102 constdefs |
1102 definition lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" (infixl "<o" 70) where |
1103 lesso :: "('a => 'b::linordered_idom) => ('a => 'b) => ('a => 'b)" |
|
1104 (infixl "<o" 70) |
|
1105 "f <o g == (%x. max (f x - g x) 0)" |
1103 "f <o g == (%x. max (f x - g x) 0)" |
1106 |
1104 |
1107 lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==> |
1105 lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==> |
1108 g =o O(h)" |
1106 g =o O(h)" |
1109 apply (unfold bigo_def) |
1107 apply (unfold bigo_def) |