src/HOL/Library/BigO.thy
changeset 60500 903bb1495239
parent 60142 3275dddf356f
child 61585 a9599d3d7610
     1.1 --- a/src/HOL/Library/BigO.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,13 +2,13 @@
     1.4      Authors:    Jeremy Avigad and Kevin Donnelly
     1.5  *)
     1.6  
     1.7 -section {* Big O notation *}
     1.8 +section \<open>Big O notation\<close>
     1.9  
    1.10  theory BigO
    1.11  imports Complex_Main Function_Algebras Set_Algebras
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16  This library is designed to support asymptotic ``big O'' calculations,
    1.17  i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g +
    1.18  O(h)$.  An earlier version of this library is described in detail in
    1.19 @@ -30,9 +30,9 @@
    1.20  one should redeclare the theorem @{text "subsetI"} as an intro rule,
    1.21  rather than as an @{text "intro!"} rule, for example, using
    1.22  \isa{\isakeyword{declare}}~@{text "subsetI [del, intro]"}.
    1.23 -*}
    1.24 +\<close>
    1.25  
    1.26 -subsection {* Definitions *}
    1.27 +subsection \<open>Definitions\<close>
    1.28  
    1.29  definition bigo :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(1O'(_'))")
    1.30    where "O(f:: 'a \<Rightarrow> 'b) = {h. \<exists>c. \<forall>x. abs (h x) \<le> c * abs (f x)}"
    1.31 @@ -558,7 +558,7 @@
    1.32    done
    1.33  
    1.34  
    1.35 -subsection {* Setsum *}
    1.36 +subsection \<open>Setsum\<close>
    1.37  
    1.38  lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 \<le> h x y \<Longrightarrow>
    1.39      \<exists>c. \<forall>x. \<forall>y \<in> A x. abs (f x y) \<le> c * (h x y) \<Longrightarrow>
    1.40 @@ -659,7 +659,7 @@
    1.41    done
    1.42  
    1.43  
    1.44 -subsection {* Misc useful stuff *}
    1.45 +subsection \<open>Misc useful stuff\<close>
    1.46  
    1.47  lemma bigo_useful_intro: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
    1.48    apply (subst bigo_plus_idemp [symmetric])
    1.49 @@ -712,7 +712,7 @@
    1.50    done
    1.51  
    1.52  
    1.53 -subsection {* Less than or equal to *}
    1.54 +subsection \<open>Less than or equal to\<close>
    1.55  
    1.56  definition lesso :: "('a \<Rightarrow> 'b::linordered_idom) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"  (infixl "<o" 70)
    1.57    where "f <o g = (\<lambda>x. max (f x - g x) 0)"