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  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)"
```