src/HOL/Library/BigO.thy
 changeset 60500 903bb1495239 parent 60142 3275dddf356f child 61585 a9599d3d7610
```--- a/src/HOL/Library/BigO.thy	Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/BigO.thy	Wed Jun 17 11:03:05 2015 +0200
@@ -2,13 +2,13 @@
Authors:    Jeremy Avigad and Kevin Donnelly
*)

-section {* Big O notation *}
+section \<open>Big O notation\<close>

theory BigO
imports Complex_Main Function_Algebras Set_Algebras
begin

-text {*
+text \<open>
This library is designed to support asymptotic ``big O'' calculations,
i.e.~reasoning with expressions of the form \$f = O(g)\$ and \$f = g +
O(h)\$.  An earlier version of this library is described in detail in
@@ -30,9 +30,9 @@
one should redeclare the theorem @{text "subsetI"} as an intro rule,
rather than as an @{text "intro!"} rule, for example, using
\isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}.
-*}
+\<close>

-subsection {* Definitions *}
+subsection \<open>Definitions\<close>

definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")
where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}"
@@ -558,7 +558,7 @@
done

-subsection {* Setsum *}
+subsection \<open>Setsum\<close>

lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
\<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>
@@ -659,7 +659,7 @@
done

-subsection {* Misc useful stuff *}
+subsection \<open>Misc useful stuff\<close>

lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
apply (subst bigo_plus_idemp [symmetric])
@@ -712,7 +712,7 @@
done

-subsection {* Less than or equal to *}
+subsection \<open>Less than or equal to\<close>

definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)
where "f <o g = (\<lambda>x. max (f x - g x) 0)"```