src/HOL/Limits.thy
changeset 60758 d8d85a8172b5
parent 60721 c1b7793c23a3
child 60974 6a6f15d8fbc4
     1.1 --- a/src/HOL/Limits.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Limits.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -5,13 +5,13 @@
     1.4      Author:     Jeremy Avigad
     1.5  *)
     1.6  
     1.7 -section {* Limits on Real Vector Spaces *}
     1.8 +section \<open>Limits on Real Vector Spaces\<close>
     1.9  
    1.10  theory Limits
    1.11  imports Real_Vector_Spaces
    1.12  begin
    1.13  
    1.14 -subsection {* Filter going to infinity norm *}
    1.15 +subsection \<open>Filter going to infinity norm\<close>
    1.16  
    1.17  definition at_infinity :: "'a::real_normed_vector filter" where
    1.18    "at_infinity = (INF r. principal {x. r \<le> norm x})"
    1.19 @@ -47,7 +47,7 @@
    1.20  by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
    1.21  
    1.22  
    1.23 -subsubsection {* Boundedness *}
    1.24 +subsubsection \<open>Boundedness\<close>
    1.25  
    1.26  definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    1.27    Bfun_metric_def: "Bfun f F = (\<exists>y. \<exists>K>0. eventually (\<lambda>x. dist (f x) y \<le> K) F)"
    1.28 @@ -72,7 +72,7 @@
    1.29      by (intro always_eventually) (metis dist_commute dist_triangle)
    1.30    with * have "eventually (\<lambda>x. dist (f x) 0 \<le> K + dist 0 y) F"
    1.31      by eventually_elim auto
    1.32 -  with `0 < K` show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F"
    1.33 +  with \<open>0 < K\<close> show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F"
    1.34      by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto
    1.35  qed auto
    1.36  
    1.37 @@ -105,7 +105,7 @@
    1.38    done
    1.39  
    1.40  
    1.41 -subsubsection {* Bounded Sequences *}
    1.42 +subsubsection \<open>Bounded Sequences\<close>
    1.43  
    1.44  lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
    1.45    by (intro BfunI) (auto simp: eventually_sequentially)
    1.46 @@ -155,7 +155,7 @@
    1.47    then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
    1.48  qed (force simp add: real_of_nat_Suc)
    1.49  
    1.50 -text{* alternative definition for Bseq *}
    1.51 +text\<open>alternative definition for Bseq\<close>
    1.52  lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    1.53  apply (simp add: Bseq_def)
    1.54  apply (simp (no_asm) add: lemma_NBseq_def)
    1.55 @@ -175,9 +175,9 @@
    1.56  lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
    1.57  by (simp add: Bseq_def lemma_NBseq_def2)
    1.58  
    1.59 -subsubsection{*A Few More Equivalence Theorems for Boundedness*}
    1.60 +subsubsection\<open>A Few More Equivalence Theorems for Boundedness\<close>
    1.61  
    1.62 -text{*alternative formulation for boundedness*}
    1.63 +text\<open>alternative formulation for boundedness\<close>
    1.64  lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
    1.65  apply (unfold Bseq_def, safe)
    1.66  apply (rule_tac [2] x = "k + norm x" in exI)
    1.67 @@ -189,7 +189,7 @@
    1.68  apply simp
    1.69  done
    1.70  
    1.71 -text{*alternative formulation for boundedness*}
    1.72 +text\<open>alternative formulation for boundedness\<close>
    1.73  lemma Bseq_iff3:
    1.74    "Bseq X \<longleftrightarrow> (\<exists>k>0. \<exists>N. \<forall>n. norm (X n + - X N) \<le> k)" (is "?P \<longleftrightarrow> ?Q")
    1.75  proof
    1.76 @@ -201,7 +201,7 @@
    1.77      by (auto intro: order_trans norm_triangle_ineq4)
    1.78    then have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)"
    1.79      by simp
    1.80 -  with `0 < K + norm (X 0)` show ?Q by blast
    1.81 +  with \<open>0 < K + norm (X 0)\<close> show ?Q by blast
    1.82  next
    1.83    assume ?Q then show ?P by (auto simp add: Bseq_iff2)
    1.84  qed
    1.85 @@ -213,7 +213,7 @@
    1.86  done
    1.87  
    1.88  
    1.89 -subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
    1.90 +subsubsection\<open>Upper Bounds and Lubs of Bounded Sequences\<close>
    1.91  
    1.92  lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
    1.93    by (simp add: Bseq_def)
    1.94 @@ -231,9 +231,9 @@
    1.95  lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
    1.96    by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
    1.97  
    1.98 -subsection {* Bounded Monotonic Sequences *}
    1.99 +subsection \<open>Bounded Monotonic Sequences\<close>
   1.100  
   1.101 -subsubsection{*A Bounded and Monotonic Sequence Converges*}
   1.102 +subsubsection\<open>A Bounded and Monotonic Sequence Converges\<close>
   1.103  
   1.104  (* TODO: delete *)
   1.105  (* FIXME: one use in NSA/HSEQ.thy *)
   1.106 @@ -244,7 +244,7 @@
   1.107    apply blast
   1.108    done
   1.109  
   1.110 -subsection {* Convergence to Zero *}
   1.111 +subsection \<open>Convergence to Zero\<close>
   1.112  
   1.113  definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
   1.114    where "Zfun f F = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) F)"
   1.115 @@ -301,7 +301,7 @@
   1.116        also have "norm (f x) * K \<le> norm (f x) * 0"
   1.117          using K norm_ge_zero by (rule mult_left_mono)
   1.118        finally show ?case
   1.119 -        using `0 < r` by simp
   1.120 +        using \<open>0 < r\<close> by simp
   1.121      qed
   1.122    qed
   1.123  qed
   1.124 @@ -400,7 +400,7 @@
   1.125                       \<Longrightarrow> (g ---> 0) F"
   1.126    by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)
   1.127  
   1.128 -subsubsection {* Distance and norms *}
   1.129 +subsubsection \<open>Distance and norms\<close>
   1.130  
   1.131  lemma tendsto_dist [tendsto_intros]:
   1.132    fixes l m :: "'a :: metric_space"
   1.133 @@ -481,7 +481,7 @@
   1.134    "((\<lambda>x. \<bar>f x\<bar>) ---> (0::real)) F \<longleftrightarrow> (f ---> 0) F"
   1.135    by (fold real_norm_def, rule tendsto_norm_zero_iff)
   1.136  
   1.137 -subsubsection {* Addition and subtraction *}
   1.138 +subsubsection \<open>Addition and subtraction\<close>
   1.139  
   1.140  lemma tendsto_add [tendsto_intros]:
   1.141    fixes a b :: "'a::real_normed_vector"
   1.142 @@ -564,7 +564,7 @@
   1.143  
   1.144  lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real]
   1.145  
   1.146 -subsubsection {* Linear operators and multiplication *}
   1.147 +subsubsection \<open>Linear operators and multiplication\<close>
   1.148  
   1.149  lemma (in bounded_linear) tendsto:
   1.150    "(g ---> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) F"
   1.151 @@ -679,7 +679,7 @@
   1.152    shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)"
   1.153    unfolding continuous_on_def by (auto intro: tendsto_setprod)
   1.154  
   1.155 -subsubsection {* Inverse and division *}
   1.156 +subsubsection \<open>Inverse and division\<close>
   1.157  
   1.158  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   1.159    assumes f: "Zfun f F"
   1.160 @@ -890,14 +890,14 @@
   1.161    qed
   1.162  qed force
   1.163  
   1.164 -subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
   1.165 +subsection \<open>Relate @{const at}, @{const at_left} and @{const at_right}\<close>
   1.166  
   1.167 -text {*
   1.168 +text \<open>
   1.169  
   1.170  This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and
   1.171  @{term "at_right x"} and also @{term "at_right 0"}.
   1.172  
   1.173 -*}
   1.174 +\<close>
   1.175  
   1.176  lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
   1.177  
   1.178 @@ -991,10 +991,10 @@
   1.179    show "\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> norm (inverse x :: 'a) < r"
   1.180    proof (intro exI[of _ "inverse (r / 2)"] allI impI)
   1.181      fix x :: 'a
   1.182 -    from `0 < r` have "0 < inverse (r / 2)" by simp
   1.183 +    from \<open>0 < r\<close> have "0 < inverse (r / 2)" by simp
   1.184      also assume *: "inverse (r / 2) \<le> norm x"
   1.185      finally show "norm (inverse x) < r"
   1.186 -      using * `0 < r` by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps)
   1.187 +      using * \<open>0 < r\<close> by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps)
   1.188    qed
   1.189  qed
   1.190  
   1.191 @@ -1106,12 +1106,12 @@
   1.192  by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)
   1.193  
   1.194  
   1.195 -text {*
   1.196 +text \<open>
   1.197  
   1.198  We only show rules for multiplication and addition when the functions are either against a real
   1.199  value or against infinity. Further rules are easy to derive by using @{thm filterlim_uminus_at_top}.
   1.200  
   1.201 -*}
   1.202 +\<close>
   1.203  
   1.204  lemma filterlim_tendsto_pos_mult_at_top:
   1.205    assumes f: "(f ---> c) F" and c: "0 < c"
   1.206 @@ -1120,7 +1120,7 @@
   1.207    unfolding filterlim_at_top_gt[where c=0]
   1.208  proof safe
   1.209    fix Z :: real assume "0 < Z"
   1.210 -  from f `0 < c` have "eventually (\<lambda>x. c / 2 < f x) F"
   1.211 +  from f \<open>0 < c\<close> have "eventually (\<lambda>x. c / 2 < f x) F"
   1.212      by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1
   1.213               simp: dist_real_def abs_real_def split: split_if_asm)
   1.214    moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F"
   1.215 @@ -1128,9 +1128,9 @@
   1.216    ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F"
   1.217    proof eventually_elim
   1.218      fix x assume "c / 2 < f x" "Z / c * 2 \<le> g x"
   1.219 -    with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) \<le> f x * g x"
   1.220 +    with \<open>0 < Z\<close> \<open>0 < c\<close> have "c / 2 * (Z / c * 2) \<le> f x * g x"
   1.221        by (intro mult_mono) (auto simp: zero_le_divide_iff)
   1.222 -    with `0 < c` show "Z \<le> f x * g x"
   1.223 +    with \<open>0 < c\<close> show "Z \<le> f x * g x"
   1.224         by simp
   1.225    qed
   1.226  qed
   1.227 @@ -1149,7 +1149,7 @@
   1.228    ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F"
   1.229    proof eventually_elim
   1.230      fix x assume "1 \<le> f x" "Z \<le> g x"
   1.231 -    with `0 < Z` have "1 * Z \<le> f x * g x"
   1.232 +    with \<open>0 < Z\<close> have "1 * Z \<le> f x * g x"
   1.233        by (intro mult_mono) (auto simp: zero_le_divide_iff)
   1.234      then show "Z \<le> f x * g x"
   1.235         by simp
   1.236 @@ -1172,7 +1172,7 @@
   1.237    fixes f :: "real \<Rightarrow> real"
   1.238    assumes "0 < n" and f: "LIM x F. f x :> at_top"
   1.239    shows "LIM x F. (f x)^n :: real :> at_top"
   1.240 -using `0 < n` proof (induct n)
   1.241 +using \<open>0 < n\<close> proof (induct n)
   1.242    case (Suc n) with f show ?case
   1.243      by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top)
   1.244  qed simp
   1.245 @@ -1264,7 +1264,7 @@
   1.246  qed simp
   1.247  
   1.248  
   1.249 -subsection {* Limits of Sequences *}
   1.250 +subsection \<open>Limits of Sequences\<close>
   1.251  
   1.252  lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
   1.253    by simp
   1.254 @@ -1300,7 +1300,7 @@
   1.255    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
   1.256    by (rule Bfun_inverse)
   1.257  
   1.258 -text{* Transformation of limit. *}
   1.259 +text\<open>Transformation of limit.\<close>
   1.260  
   1.261  lemma eventually_at2:
   1.262    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
   1.263 @@ -1346,7 +1346,7 @@
   1.264      using assms(1,2) by auto
   1.265  qed
   1.266  
   1.267 -text{* Common case assuming being away from some crucial point like 0. *}
   1.268 +text\<open>Common case assuming being away from some crucial point like 0.\<close>
   1.269  
   1.270  lemma Lim_transform_away_within:
   1.271    fixes a b :: "'a::t1_space"
   1.272 @@ -1369,7 +1369,7 @@
   1.273    shows "(g ---> l) (at a)"
   1.274    using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp
   1.275  
   1.276 -text{* Alternatively, within an open set. *}
   1.277 +text\<open>Alternatively, within an open set.\<close>
   1.278  
   1.279  lemma Lim_transform_within_open:
   1.280    assumes "open S" and "a \<in> S"
   1.281 @@ -1383,7 +1383,7 @@
   1.282    show "(f ---> l) (at a)" by fact
   1.283  qed
   1.284  
   1.285 -text{* A congruence rule allowing us to transform limits assuming not at point. *}
   1.286 +text\<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
   1.287  
   1.288  (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
   1.289  
   1.290 @@ -1402,7 +1402,7 @@
   1.291    shows "((\<lambda>x. f x) ---> x) (at a) \<longleftrightarrow> ((g ---> y) (at a))"
   1.292    unfolding tendsto_def eventually_at_topological
   1.293    using assms by simp
   1.294 -text{*An unbounded sequence's inverse tends to 0*}
   1.295 +text\<open>An unbounded sequence's inverse tends to 0\<close>
   1.296  
   1.297  lemma LIMSEQ_inverse_zero:
   1.298    "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
   1.299 @@ -1411,14 +1411,14 @@
   1.300    apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
   1.301    done
   1.302  
   1.303 -text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
   1.304 +text\<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity\<close>
   1.305  
   1.306  lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
   1.307    by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
   1.308              filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
   1.309  
   1.310 -text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
   1.311 -infinity is now easily proved*}
   1.312 +text\<open>The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
   1.313 +infinity is now easily proved\<close>
   1.314  
   1.315  lemma LIMSEQ_inverse_real_of_nat_add:
   1.316       "(%n. r + inverse(real(Suc n))) ----> r"
   1.317 @@ -1434,7 +1434,7 @@
   1.318    using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
   1.319    by auto
   1.320  
   1.321 -subsection {* Convergence on sequences *}
   1.322 +subsection \<open>Convergence on sequences\<close>
   1.323  
   1.324  lemma convergent_add:
   1.325    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
   1.326 @@ -1471,7 +1471,7 @@
   1.327  done
   1.328  
   1.329  
   1.330 -text {* A monotone sequence converges to its least upper bound. *}
   1.331 +text \<open>A monotone sequence converges to its least upper bound.\<close>
   1.332  
   1.333  lemma LIMSEQ_incseq_SUP:
   1.334    fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
   1.335 @@ -1489,7 +1489,7 @@
   1.336    by (rule order_tendstoI)
   1.337       (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])
   1.338  
   1.339 -text{*Main monotonicity theorem*}
   1.340 +text\<open>Main monotonicity theorem\<close>
   1.341  
   1.342  lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
   1.343    by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below)
   1.344 @@ -1517,10 +1517,10 @@
   1.345    assumes "incseq X" and "\<forall>i. X i \<le> B"
   1.346    obtains L where "X ----> L" "\<forall>i. X i \<le> L"
   1.347  proof atomize_elim
   1.348 -  from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X]
   1.349 +  from incseq_bounded[OF assms] \<open>incseq X\<close> Bseq_monoseq_convergent[of X]
   1.350    obtain L where "X ----> L"
   1.351      by (auto simp: convergent_def monoseq_def incseq_def)
   1.352 -  with `incseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
   1.353 +  with \<open>incseq X\<close> show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
   1.354      by (auto intro!: exI[of _ L] incseq_le)
   1.355  qed
   1.356  
   1.357 @@ -1529,17 +1529,17 @@
   1.358    assumes "decseq X" and "\<forall>i. B \<le> X i"
   1.359    obtains L where "X ----> L" "\<forall>i. L \<le> X i"
   1.360  proof atomize_elim
   1.361 -  from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X]
   1.362 +  from decseq_bounded[OF assms] \<open>decseq X\<close> Bseq_monoseq_convergent[of X]
   1.363    obtain L where "X ----> L"
   1.364      by (auto simp: convergent_def monoseq_def decseq_def)
   1.365 -  with `decseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
   1.366 +  with \<open>decseq X\<close> show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
   1.367      by (auto intro!: exI[of _ L] decseq_le)
   1.368  qed
   1.369  
   1.370 -subsubsection {* Cauchy Sequences are Bounded *}
   1.371 +subsubsection \<open>Cauchy Sequences are Bounded\<close>
   1.372  
   1.373 -text{*A Cauchy sequence is bounded -- this is the standard
   1.374 -  proof mechanization rather than the nonstandard proof*}
   1.375 +text\<open>A Cauchy sequence is bounded -- this is the standard
   1.376 +  proof mechanization rather than the nonstandard proof\<close>
   1.377  
   1.378  lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
   1.379            ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
   1.380 @@ -1549,11 +1549,11 @@
   1.381  apply simp
   1.382  done
   1.383  
   1.384 -subsection {* Power Sequences *}
   1.385 +subsection \<open>Power Sequences\<close>
   1.386  
   1.387 -text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   1.388 +text\<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   1.389  "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   1.390 -  also fact that bounded and monotonic sequence converges.*}
   1.391 +  also fact that bounded and monotonic sequence converges.\<close>
   1.392  
   1.393  lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
   1.394  apply (simp add: Bseq_def)
   1.395 @@ -1598,7 +1598,7 @@
   1.396  lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
   1.397    by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
   1.398  
   1.399 -text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
   1.400 +text\<open>Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}\<close>
   1.401  
   1.402  lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
   1.403    by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
   1.404 @@ -1607,7 +1607,7 @@
   1.405    by (rule LIMSEQ_power_zero) simp
   1.406  
   1.407  
   1.408 -subsection {* Limits of Functions *}
   1.409 +subsection \<open>Limits of Functions\<close>
   1.410  
   1.411  lemma LIM_eq:
   1.412    fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
   1.413 @@ -1702,7 +1702,7 @@
   1.414  qed
   1.415  
   1.416  
   1.417 -subsection {* Continuity *}
   1.418 +subsection \<open>Continuity\<close>
   1.419  
   1.420  lemma LIM_isCont_iff:
   1.421    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   1.422 @@ -1777,7 +1777,7 @@
   1.423    shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   1.424    by (auto intro: continuous_setsum)
   1.425  
   1.426 -subsection {* Uniform Continuity *}
   1.427 +subsection \<open>Uniform Continuity\<close>
   1.428  
   1.429  definition
   1.430    isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
   1.431 @@ -1823,13 +1823,13 @@
   1.432    shows "0 \<le> f x"
   1.433  proof (rule tendsto_le_const)
   1.434    show "(f ---> f x) (at_left x)"
   1.435 -    using `isCont f x` by (simp add: filterlim_at_split isCont_def)
   1.436 +    using \<open>isCont f x\<close> by (simp add: filterlim_at_split isCont_def)
   1.437    show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
   1.438      using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"])
   1.439  qed simp
   1.440  
   1.441  
   1.442 -subsection {* Nested Intervals and Bisection -- Needed for Compactness *}
   1.443 +subsection \<open>Nested Intervals and Bisection -- Needed for Compactness\<close>
   1.444  
   1.445  lemma nested_sequence_unique:
   1.446    assumes "\<forall>n. f n \<le> f (Suc n)" "\<forall>n. g (Suc n) \<le> g n" "\<forall>n. f n \<le> g n" "(\<lambda>n. f n - g n) ----> 0"
   1.447 @@ -1839,17 +1839,17 @@
   1.448    have "decseq g" unfolding decseq_Suc_iff by fact
   1.449  
   1.450    { fix n
   1.451 -    from `decseq g` have "g n \<le> g 0" by (rule decseqD) simp
   1.452 -    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f n \<le> g 0" by auto }
   1.453 +    from \<open>decseq g\<close> have "g n \<le> g 0" by (rule decseqD) simp
   1.454 +    with \<open>\<forall>n. f n \<le> g n\<close>[THEN spec, of n] have "f n \<le> g 0" by auto }
   1.455    then obtain u where "f ----> u" "\<forall>i. f i \<le> u"
   1.456 -    using incseq_convergent[OF `incseq f`] by auto
   1.457 +    using incseq_convergent[OF \<open>incseq f\<close>] by auto
   1.458    moreover
   1.459    { fix n
   1.460 -    from `incseq f` have "f 0 \<le> f n" by (rule incseqD) simp
   1.461 -    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f 0 \<le> g n" by simp }
   1.462 +    from \<open>incseq f\<close> have "f 0 \<le> f n" by (rule incseqD) simp
   1.463 +    with \<open>\<forall>n. f n \<le> g n\<close>[THEN spec, of n] have "f 0 \<le> g n" by simp }
   1.464    then obtain l where "g ----> l" "\<forall>i. l \<le> g i"
   1.465 -    using decseq_convergent[OF `decseq g`] by auto
   1.466 -  moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF `f ----> u` `g ----> l`]]
   1.467 +    using decseq_convergent[OF \<open>decseq g\<close>] by auto
   1.468 +  moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF \<open>f ----> u\<close> \<open>g ----> l\<close>]]
   1.469    ultimately show ?thesis by auto
   1.470  qed
   1.471  
   1.472 @@ -1877,7 +1877,7 @@
   1.473    qed fact
   1.474    then obtain x where x: "\<And>n. l n \<le> x" "\<And>n. x \<le> u n" and "l ----> x" "u ----> x" by auto
   1.475    obtain d where "0 < d" and d: "\<And>a b. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> b - a < d \<Longrightarrow> P a b"
   1.476 -    using `l 0 \<le> x` `x \<le> u 0` local[of x] by auto
   1.477 +    using \<open>l 0 \<le> x\<close> \<open>x \<le> u 0\<close> local[of x] by auto
   1.478  
   1.479    show "P a b"
   1.480    proof (rule ccontr)
   1.481 @@ -1885,12 +1885,12 @@
   1.482      { fix n have "\<not> P (l n) (u n)"
   1.483        proof (induct n)
   1.484          case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto
   1.485 -      qed (simp add: `\<not> P a b`) }
   1.486 +      qed (simp add: \<open>\<not> P a b\<close>) }
   1.487      moreover
   1.488      { have "eventually (\<lambda>n. x - d / 2 < l n) sequentially"
   1.489 -        using `0 < d` `l ----> x` by (intro order_tendstoD[of _ x]) auto
   1.490 +        using \<open>0 < d\<close> \<open>l ----> x\<close> by (intro order_tendstoD[of _ x]) auto
   1.491        moreover have "eventually (\<lambda>n. u n < x + d / 2) sequentially"
   1.492 -        using `0 < d` `u ----> x` by (intro order_tendstoD[of _ x]) auto
   1.493 +        using \<open>0 < d\<close> \<open>u ----> x\<close> by (intro order_tendstoD[of _ x]) auto
   1.494        ultimately have "eventually (\<lambda>n. P (l n) (u n)) sequentially"
   1.495        proof eventually_elim
   1.496          fix n assume "x - d / 2 < l n" "u n < x + d / 2"
   1.497 @@ -1919,7 +1919,7 @@
   1.498      with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" by auto
   1.499      then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c"
   1.500        by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff)
   1.501 -    with `c \<in> C` show ?case
   1.502 +    with \<open>c \<in> C\<close> show ?case
   1.503        by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
   1.504    qed
   1.505  qed simp
   1.506 @@ -1932,7 +1932,7 @@
   1.507    shows "\<exists>c d. f`S = {c..d} \<and> c \<le> d"
   1.508  proof -
   1.509    have S: "compact S" "S \<noteq> {}"
   1.510 -    using `a \<le> b` by (auto simp: S_def)
   1.511 +    using \<open>a \<le> b\<close> by (auto simp: S_def)
   1.512    obtain c where "c \<in> S" "\<forall>d\<in>S. f d \<le> f c"
   1.513      using continuous_attains_sup[OF S f] by auto
   1.514    moreover obtain d where "d \<in> S" "\<forall>c\<in>S. f d \<le> f c"
   1.515 @@ -1945,9 +1945,9 @@
   1.516      by auto
   1.517  qed
   1.518  
   1.519 -subsection {* Boundedness of continuous functions *}
   1.520 +subsection \<open>Boundedness of continuous functions\<close>
   1.521  
   1.522 -text{*By bisection, function continuous on closed interval is bounded above*}
   1.523 +text\<open>By bisection, function continuous on closed interval is bounded above\<close>
   1.524  
   1.525  lemma isCont_eq_Ub:
   1.526    fixes f :: "real \<Rightarrow> 'a::linorder_topology"
   1.527 @@ -2006,7 +2006,7 @@
   1.528  qed
   1.529  
   1.530  
   1.531 -text{*Continuity of inverse function*}
   1.532 +text\<open>Continuity of inverse function\<close>
   1.533  
   1.534  lemma isCont_inverse_function:
   1.535    fixes f g :: "real \<Rightarrow> real"
   1.536 @@ -2056,7 +2056,7 @@
   1.537        ==> isCont g (f x)"
   1.538  by (rule isCont_inverse_function)
   1.539  
   1.540 -text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
   1.541 +text\<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110\<close>
   1.542  lemma LIM_fun_gt_zero:
   1.543    fixes f :: "real \<Rightarrow> real"
   1.544    shows "f -- c --> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)"