1(* Title: HOL/Limits.thy 2 Author: Brian Huffman 3 Author: Jacques D. Fleuriot, University of Cambridge 4 Author: Lawrence C Paulson 5 Author: Jeremy Avigad 6*) 7 8section \<open>Limits on Real Vector Spaces\<close> 9 10theory Limits 11 imports Real_Vector_Spaces 12begin 13 14subsection \<open>Filter going to infinity norm\<close> 15 16definition at_infinity :: "'a::real_normed_vector filter" 17 where "at_infinity = (INF r. principal {x. r \<le> norm x})" 18 19lemma eventually_at_infinity: "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)" 20 unfolding at_infinity_def 21 by (subst eventually_INF_base) 22 (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b]) 23 24corollary eventually_at_infinity_pos: 25 "eventually p at_infinity \<longleftrightarrow> (\<exists>b. 0 < b \<and> (\<forall>x. norm x \<ge> b \<longrightarrow> p x))" 26 unfolding eventually_at_infinity 27 by (meson le_less_trans norm_ge_zero not_le zero_less_one) 28 29lemma at_infinity_eq_at_top_bot: "(at_infinity :: real filter) = sup at_top at_bot" 30proof - 31 have 1: "\<lbrakk>\<forall>n\<ge>u. A n; \<forall>n\<le>v. A n\<rbrakk> 32 \<Longrightarrow> \<exists>b. \<forall>x. b \<le> \<bar>x\<bar> \<longrightarrow> A x" for A and u v::real 33 by (rule_tac x="max (- v) u" in exI) (auto simp: abs_real_def) 34 have 2: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. A n" for A and u::real 35 by (meson abs_less_iff le_cases less_le_not_le) 36 have 3: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<le>N. A n" for A and u::real 37 by (metis (full_types) abs_ge_self abs_minus_cancel le_minus_iff order_trans) 38 show ?thesis 39 by (auto simp: filter_eq_iff eventually_sup eventually_at_infinity 40 eventually_at_top_linorder eventually_at_bot_linorder intro: 1 2 3) 41qed 42 43lemma at_top_le_at_infinity: "at_top \<le> (at_infinity :: real filter)" 44 unfolding at_infinity_eq_at_top_bot by simp 45 46lemma at_bot_le_at_infinity: "at_bot \<le> (at_infinity :: real filter)" 47 unfolding at_infinity_eq_at_top_bot by simp 48 49lemma filterlim_at_top_imp_at_infinity: "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F" 50 for f :: "_ \<Rightarrow> real" 51 by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl]) 52 53lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially" 54 by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially) 55 56lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially" 57 by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially) 58 59 60subsubsection \<open>Boundedness\<close> 61 62definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" 63 where Bfun_metric_def: "Bfun f F = (\<exists>y. \<exists>K>0. eventually (\<lambda>x. dist (f x) y \<le> K) F)" 64 65abbreviation Bseq :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" 66 where "Bseq X \<equiv> Bfun X sequentially" 67 68lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" .. 69 70lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" 71 unfolding Bfun_metric_def by (subst eventually_sequentially_seg) 72 73lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" 74 unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg) 75 76lemma Bfun_def: "Bfun f F \<longleftrightarrow> (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)" 77 unfolding Bfun_metric_def norm_conv_dist 78proof safe 79 fix y K 80 assume K: "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F" 81 moreover have "eventually (\<lambda>x. dist (f x) 0 \<le> dist (f x) y + dist 0 y) F" 82 by (intro always_eventually) (metis dist_commute dist_triangle) 83 with * have "eventually (\<lambda>x. dist (f x) 0 \<le> K + dist 0 y) F" 84 by eventually_elim auto 85 with \<open>0 < K\<close> show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F" 86 by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto 87qed (force simp del: norm_conv_dist [symmetric]) 88 89lemma BfunI: 90 assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" 91 shows "Bfun f F" 92 unfolding Bfun_def 93proof (intro exI conjI allI) 94 show "0 < max K 1" by simp 95 show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F" 96 using K by (rule eventually_mono) simp 97qed 98 99lemma BfunE: 100 assumes "Bfun f F" 101 obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F" 102 using assms unfolding Bfun_def by blast 103 104lemma Cauchy_Bseq: 105 assumes "Cauchy X" shows "Bseq X" 106proof - 107 have "\<exists>y K. 0 < K \<and> (\<exists>N. \<forall>n\<ge>N. dist (X n) y \<le> K)" 108 if "\<And>m n. \<lbrakk>m \<ge> M; n \<ge> M\<rbrakk> \<Longrightarrow> dist (X m) (X n) < 1" for M 109 by (meson order.order_iff_strict that zero_less_one) 110 with assms show ?thesis 111 by (force simp: Cauchy_def Bfun_metric_def eventually_sequentially) 112qed 113 114subsubsection \<open>Bounded Sequences\<close> 115 116lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X" 117 by (intro BfunI) (auto simp: eventually_sequentially) 118 119lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X" 120 by (intro BfunI) (auto simp: eventually_sequentially) 121 122lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)" 123 unfolding Bfun_def eventually_sequentially 124proof safe 125 fix N K 126 assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K" 127 then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" 128 by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2) 129 (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj) 130qed auto 131 132lemma BseqE: "Bseq X \<Longrightarrow> (\<And>K. 0 < K \<Longrightarrow> \<forall>n. norm (X n) \<le> K \<Longrightarrow> Q) \<Longrightarrow> Q" 133 unfolding Bseq_def by auto 134 135lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K. 0 < K \<and> (\<forall>n. norm (X n) \<le> K)" 136 by (simp add: Bseq_def) 137 138lemma BseqI: "0 < K \<Longrightarrow> \<forall>n. norm (X n) \<le> K \<Longrightarrow> Bseq X" 139 by (auto simp: Bseq_def) 140 141lemma Bseq_bdd_above: "Bseq X \<Longrightarrow> bdd_above (range X)" 142 for X :: "nat \<Rightarrow> real" 143proof (elim BseqE, intro bdd_aboveI2) 144 fix K n 145 assume "0 < K" "\<forall>n. norm (X n) \<le> K" 146 then show "X n \<le> K" 147 by (auto elim!: allE[of _ n]) 148qed 149 150lemma Bseq_bdd_above': "Bseq X \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))" 151 for X :: "nat \<Rightarrow> 'a :: real_normed_vector" 152proof (elim BseqE, intro bdd_aboveI2) 153 fix K n 154 assume "0 < K" "\<forall>n. norm (X n) \<le> K" 155 then show "norm (X n) \<le> K" 156 by (auto elim!: allE[of _ n]) 157qed 158 159lemma Bseq_bdd_below: "Bseq X \<Longrightarrow> bdd_below (range X)" 160 for X :: "nat \<Rightarrow> real" 161proof (elim BseqE, intro bdd_belowI2) 162 fix K n 163 assume "0 < K" "\<forall>n. norm (X n) \<le> K" 164 then show "- K \<le> X n" 165 by (auto elim!: allE[of _ n]) 166qed 167 168lemma Bseq_eventually_mono: 169 assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g" 170 shows "Bseq f" 171proof - 172 from assms(2) obtain K where "0 < K" and "eventually (\<lambda>n. norm (g n) \<le> K) sequentially" 173 unfolding Bfun_def by fast 174 with assms(1) have "eventually (\<lambda>n. norm (f n) \<le> K) sequentially" 175 by (fast elim: eventually_elim2 order_trans) 176 with `0 < K` show "Bseq f" 177 unfolding Bfun_def by fast 178qed 179 180lemma lemma_NBseq_def: "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" 181proof safe 182 fix K :: real 183 from reals_Archimedean2 obtain n :: nat where "K < real n" .. 184 then have "K \<le> real (Suc n)" by auto 185 moreover assume "\<forall>m. norm (X m) \<le> K" 186 ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)" 187 by (blast intro: order_trans) 188 then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" .. 189next 190 show "\<And>N. \<forall>n. norm (X n) \<le> real (Suc N) \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K" 191 using of_nat_0_less_iff by blast 192qed 193 194text \<open>Alternative definition for \<open>Bseq\<close>.\<close> 195lemma Bseq_iff: "Bseq X \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" 196 by (simp add: Bseq_def) (simp add: lemma_NBseq_def) 197 198lemma lemma_NBseq_def2: "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" 199proof - 200 have *: "\<And>N. \<forall>n. norm (X n) \<le> 1 + real N \<Longrightarrow> 201 \<exists>N. \<forall>n. norm (X n) < 1 + real N" 202 by (metis add.commute le_less_trans less_add_one of_nat_Suc) 203 then show ?thesis 204 unfolding lemma_NBseq_def 205 by (metis less_le_not_le not_less_iff_gr_or_eq of_nat_Suc) 206qed 207 208text \<open>Yet another definition for Bseq.\<close> 209lemma Bseq_iff1a: "Bseq X \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) < real (Suc N))" 210 by (simp add: Bseq_def lemma_NBseq_def2) 211 212subsubsection \<open>A Few More Equivalence Theorems for Boundedness\<close> 213 214text \<open>Alternative formulation for boundedness.\<close> 215lemma Bseq_iff2: "Bseq X \<longleftrightarrow> (\<exists>k > 0. \<exists>x. \<forall>n. norm (X n + - x) \<le> k)" 216 by (metis BseqE BseqI' add.commute add_cancel_right_left add_uminus_conv_diff norm_add_leD 217 norm_minus_cancel norm_minus_commute) 218 219text \<open>Alternative formulation for boundedness.\<close> 220lemma Bseq_iff3: "Bseq X \<longleftrightarrow> (\<exists>k>0. \<exists>N. \<forall>n. norm (X n + - X N) \<le> k)" 221 (is "?P \<longleftrightarrow> ?Q") 222proof 223 assume ?P 224 then obtain K where *: "0 < K" and **: "\<And>n. norm (X n) \<le> K" 225 by (auto simp: Bseq_def) 226 from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp 227 from ** have "\<forall>n. norm (X n - X 0) \<le> K + norm (X 0)" 228 by (auto intro: order_trans norm_triangle_ineq4) 229 then have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)" 230 by simp 231 with \<open>0 < K + norm (X 0)\<close> show ?Q by blast 232next 233 assume ?Q 234 then show ?P by (auto simp: Bseq_iff2) 235qed 236 237 238subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close> 239 240lemma Bseq_minus_iff: "Bseq (\<lambda>n. - (X n) :: 'a::real_normed_vector) \<longleftrightarrow> Bseq X" 241 by (simp add: Bseq_def) 242 243lemma Bseq_add: 244 fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" 245 assumes "Bseq f" 246 shows "Bseq (\<lambda>x. f x + c)" 247proof - 248 from assms obtain K where K: "\<And>x. norm (f x) \<le> K" 249 unfolding Bseq_def by blast 250 { 251 fix x :: nat 252 have "norm (f x + c) \<le> norm (f x) + norm c" by (rule norm_triangle_ineq) 253 also have "norm (f x) \<le> K" by (rule K) 254 finally have "norm (f x + c) \<le> K + norm c" by simp 255 } 256 then show ?thesis by (rule BseqI') 257qed 258 259lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq f" 260 for f :: "nat \<Rightarrow> 'a::real_normed_vector" 261 using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto 262 263lemma Bseq_mult: 264 fixes f g :: "nat \<Rightarrow> 'a::real_normed_field" 265 assumes "Bseq f" and "Bseq g" 266 shows "Bseq (\<lambda>x. f x * g x)" 267proof - 268 from assms obtain K1 K2 where K: "norm (f x) \<le> K1" "K1 > 0" "norm (g x) \<le> K2" "K2 > 0" 269 for x 270 unfolding Bseq_def by blast 271 then have "norm (f x * g x) \<le> K1 * K2" for x 272 by (auto simp: norm_mult intro!: mult_mono) 273 then show ?thesis by (rule BseqI') 274qed 275 276lemma Bfun_const [simp]: "Bfun (\<lambda>_. c) F" 277 unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"]) 278 279lemma Bseq_cmult_iff: 280 fixes c :: "'a::real_normed_field" 281 assumes "c \<noteq> 0" 282 shows "Bseq (\<lambda>x. c * f x) \<longleftrightarrow> Bseq f" 283proof 284 assume "Bseq (\<lambda>x. c * f x)" 285 with Bfun_const have "Bseq (\<lambda>x. inverse c * (c * f x))" 286 by (rule Bseq_mult) 287 with \<open>c \<noteq> 0\<close> show "Bseq f" 288 by (simp add: divide_simps) 289qed (intro Bseq_mult Bfun_const) 290 291lemma Bseq_subseq: "Bseq f \<Longrightarrow> Bseq (\<lambda>x. f (g x))" 292 for f :: "nat \<Rightarrow> 'a::real_normed_vector" 293 unfolding Bseq_def by auto 294 295lemma Bseq_Suc_iff: "Bseq (\<lambda>n. f (Suc n)) \<longleftrightarrow> Bseq f" 296 for f :: "nat \<Rightarrow> 'a::real_normed_vector" 297 using Bseq_offset[of f 1] by (auto intro: Bseq_subseq) 298 299lemma increasing_Bseq_subseq_iff: 300 assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "strict_mono g" 301 shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f" 302proof 303 assume "Bseq (\<lambda>x. f (g x))" 304 then obtain K where K: "\<And>x. norm (f (g x)) \<le> K" 305 unfolding Bseq_def by auto 306 { 307 fix x :: nat 308 from filterlim_subseq[OF assms(2)] obtain y where "g y \<ge> x" 309 by (auto simp: filterlim_at_top eventually_at_top_linorder) 310 then have "norm (f x) \<le> norm (f (g y))" 311 using assms(1) by blast 312 also have "norm (f (g y)) \<le> K" by (rule K) 313 finally have "norm (f x) \<le> K" . 314 } 315 then show "Bseq f" by (rule BseqI') 316qed (use Bseq_subseq[of f g] in simp_all) 317 318lemma nonneg_incseq_Bseq_subseq_iff: 319 fixes f :: "nat \<Rightarrow> real" 320 and g :: "nat \<Rightarrow> nat" 321 assumes "\<And>x. f x \<ge> 0" "incseq f" "strict_mono g" 322 shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f" 323 using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def) 324 325lemma Bseq_eq_bounded: "range f \<subseteq> {a..b} \<Longrightarrow> Bseq f" 326 for a b :: real 327proof (rule BseqI'[where K="max (norm a) (norm b)"]) 328 fix n assume "range f \<subseteq> {a..b}" 329 then have "f n \<in> {a..b}" 330 by blast 331 then show "norm (f n) \<le> max (norm a) (norm b)" 332 by auto 333qed 334 335lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> B \<Longrightarrow> Bseq X" 336 for B :: real 337 by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def) 338 339lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. B \<le> X i \<Longrightarrow> Bseq X" 340 for B :: real 341 by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) 342 343 344subsection \<open>Convergence to Zero\<close> 345 346definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" 347 where "Zfun f F = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) F)" 348 349lemma ZfunI: "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F) \<Longrightarrow> Zfun f F" 350 by (simp add: Zfun_def) 351 352lemma ZfunD: "Zfun f F \<Longrightarrow> 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F" 353 by (simp add: Zfun_def) 354 355lemma Zfun_ssubst: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> Zfun g F \<Longrightarrow> Zfun f F" 356 unfolding Zfun_def by (auto elim!: eventually_rev_mp) 357 358lemma Zfun_zero: "Zfun (\<lambda>x. 0) F" 359 unfolding Zfun_def by simp 360 361lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) F = Zfun (\<lambda>x. f x) F" 362 unfolding Zfun_def by simp 363 364lemma Zfun_imp_Zfun: 365 assumes f: "Zfun f F" 366 and g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F" 367 shows "Zfun (\<lambda>x. g x) F" 368proof (cases "0 < K") 369 case K: True 370 show ?thesis 371 proof (rule ZfunI) 372 fix r :: real 373 assume "0 < r" 374 then have "0 < r / K" using K by simp 375 then have "eventually (\<lambda>x. norm (f x) < r / K) F" 376 using ZfunD [OF f] by blast 377 with g show "eventually (\<lambda>x. norm (g x) < r) F" 378 proof eventually_elim 379 case (elim x) 380 then have "norm (f x) * K < r" 381 by (simp add: pos_less_divide_eq K) 382 then show ?case 383 by (simp add: order_le_less_trans [OF elim(1)]) 384 qed 385 qed 386next 387 case False 388 then have K: "K \<le> 0" by (simp only: not_less) 389 show ?thesis 390 proof (rule ZfunI) 391 fix r :: real 392 assume "0 < r" 393 from g show "eventually (\<lambda>x. norm (g x) < r) F" 394 proof eventually_elim 395 case (elim x) 396 also have "norm (f x) * K \<le> norm (f x) * 0" 397 using K norm_ge_zero by (rule mult_left_mono) 398 finally show ?case 399 using \<open>0 < r\<close> by simp 400 qed 401 qed 402qed 403 404lemma Zfun_le: "Zfun g F \<Longrightarrow> \<forall>x. norm (f x) \<le> norm (g x) \<Longrightarrow> Zfun f F" 405 by (erule Zfun_imp_Zfun [where K = 1]) simp 406 407lemma Zfun_add: 408 assumes f: "Zfun f F" 409 and g: "Zfun g F" 410 shows "Zfun (\<lambda>x. f x + g x) F" 411proof (rule ZfunI) 412 fix r :: real 413 assume "0 < r" 414 then have r: "0 < r / 2" by simp 415 have "eventually (\<lambda>x. norm (f x) < r/2) F" 416 using f r by (rule ZfunD) 417 moreover 418 have "eventually (\<lambda>x. norm (g x) < r/2) F" 419 using g r by (rule ZfunD) 420 ultimately 421 show "eventually (\<lambda>x. norm (f x + g x) < r) F" 422 proof eventually_elim 423 case (elim x) 424 have "norm (f x + g x) \<le> norm (f x) + norm (g x)" 425 by (rule norm_triangle_ineq) 426 also have "\<dots> < r/2 + r/2" 427 using elim by (rule add_strict_mono) 428 finally show ?case 429 by simp 430 qed 431qed 432 433lemma Zfun_minus: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. - f x) F" 434 unfolding Zfun_def by simp 435 436lemma Zfun_diff: "Zfun f F \<Longrightarrow> Zfun g F \<Longrightarrow> Zfun (\<lambda>x. f x - g x) F" 437 using Zfun_add [of f F "\<lambda>x. - g x"] by (simp add: Zfun_minus) 438 439lemma (in bounded_linear) Zfun: 440 assumes g: "Zfun g F" 441 shows "Zfun (\<lambda>x. f (g x)) F" 442proof - 443 obtain K where "norm (f x) \<le> norm x * K" for x 444 using bounded by blast 445 then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) F" 446 by simp 447 with g show ?thesis 448 by (rule Zfun_imp_Zfun) 449qed 450 451lemma (in bounded_bilinear) Zfun: 452 assumes f: "Zfun f F" 453 and g: "Zfun g F" 454 shows "Zfun (\<lambda>x. f x ** g x) F" 455proof (rule ZfunI) 456 fix r :: real 457 assume r: "0 < r" 458 obtain K where K: "0 < K" 459 and norm_le: "norm (x ** y) \<le> norm x * norm y * K" for x y 460 using pos_bounded by blast 461 from K have K': "0 < inverse K" 462 by (rule positive_imp_inverse_positive) 463 have "eventually (\<lambda>x. norm (f x) < r) F" 464 using f r by (rule ZfunD) 465 moreover 466 have "eventually (\<lambda>x. norm (g x) < inverse K) F" 467 using g K' by (rule ZfunD) 468 ultimately 469 show "eventually (\<lambda>x. norm (f x ** g x) < r) F" 470 proof eventually_elim 471 case (elim x) 472 have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" 473 by (rule norm_le) 474 also have "norm (f x) * norm (g x) * K < r * inverse K * K" 475 by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K) 476 also from K have "r * inverse K * K = r" 477 by simp 478 finally show ?case . 479 qed 480qed 481 482lemma (in bounded_bilinear) Zfun_left: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. f x ** a) F" 483 by (rule bounded_linear_left [THEN bounded_linear.Zfun]) 484 485lemma (in bounded_bilinear) Zfun_right: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F" 486 by (rule bounded_linear_right [THEN bounded_linear.Zfun]) 487 488lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] 489lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] 490lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] 491 492lemma tendsto_Zfun_iff: "(f \<longlongrightarrow> a) F = Zfun (\<lambda>x. f x - a) F" 493 by (simp only: tendsto_iff Zfun_def dist_norm) 494 495lemma tendsto_0_le: 496 "(f \<longlongrightarrow> 0) F \<Longrightarrow> eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F \<Longrightarrow> (g \<longlongrightarrow> 0) F" 497 by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) 498 499 500subsubsection \<open>Distance and norms\<close> 501 502lemma tendsto_dist [tendsto_intros]: 503 fixes l m :: "'a::metric_space" 504 assumes f: "(f \<longlongrightarrow> l) F" 505 and g: "(g \<longlongrightarrow> m) F" 506 shows "((\<lambda>x. dist (f x) (g x)) \<longlongrightarrow> dist l m) F" 507proof (rule tendstoI) 508 fix e :: real 509 assume "0 < e" 510 then have e2: "0 < e/2" by simp 511 from tendstoD [OF f e2] tendstoD [OF g e2] 512 show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F" 513 proof (eventually_elim) 514 case (elim x) 515 then show "dist (dist (f x) (g x)) (dist l m) < e" 516 unfolding dist_real_def 517 using dist_triangle2 [of "f x" "g x" "l"] 518 and dist_triangle2 [of "g x" "l" "m"] 519 and dist_triangle3 [of "l" "m" "f x"] 520 and dist_triangle [of "f x" "m" "g x"] 521 by arith 522 qed 523qed 524 525lemma continuous_dist[continuous_intros]: 526 fixes f g :: "_ \<Rightarrow> 'a :: metric_space" 527 shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))" 528 unfolding continuous_def by (rule tendsto_dist) 529 530lemma continuous_on_dist[continuous_intros]: 531 fixes f g :: "_ \<Rightarrow> 'a :: metric_space" 532 shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))" 533 unfolding continuous_on_def by (auto intro: tendsto_dist) 534 535lemma tendsto_norm [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> norm a) F" 536 unfolding norm_conv_dist by (intro tendsto_intros) 537 538lemma continuous_norm [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))" 539 unfolding continuous_def by (rule tendsto_norm) 540 541lemma continuous_on_norm [continuous_intros]: 542 "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))" 543 unfolding continuous_on_def by (auto intro: tendsto_norm) 544 545lemma tendsto_norm_zero: "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F" 546 by (drule tendsto_norm) simp 547 548lemma tendsto_norm_zero_cancel: "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> 0) F" 549 unfolding tendsto_iff dist_norm by simp 550 551lemma tendsto_norm_zero_iff: "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F" 552 unfolding tendsto_iff dist_norm by simp 553 554lemma tendsto_rabs [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> \<bar>l\<bar>) F" 555 for l :: real 556 by (fold real_norm_def) (rule tendsto_norm) 557 558lemma continuous_rabs [continuous_intros]: 559 "continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)" 560 unfolding real_norm_def[symmetric] by (rule continuous_norm) 561 562lemma continuous_on_rabs [continuous_intros]: 563 "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)" 564 unfolding real_norm_def[symmetric] by (rule continuous_on_norm) 565 566lemma tendsto_rabs_zero: "(f \<longlongrightarrow> (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> 0) F" 567 by (fold real_norm_def) (rule tendsto_norm_zero) 568 569lemma tendsto_rabs_zero_cancel: "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<Longrightarrow> (f \<longlongrightarrow> 0) F" 570 by (fold real_norm_def) (rule tendsto_norm_zero_cancel) 571 572lemma tendsto_rabs_zero_iff: "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F" 573 by (fold real_norm_def) (rule tendsto_norm_zero_iff) 574 575 576subsection \<open>Topological Monoid\<close> 577 578class topological_monoid_add = topological_space + monoid_add + 579 assumes tendsto_add_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x + snd x :> nhds (a + b)" 580 581class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add 582 583lemma tendsto_add [tendsto_intros]: 584 fixes a b :: "'a::topological_monoid_add" 585 shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F" 586 using filterlim_compose[OF tendsto_add_Pair, of "\<lambda>x. (f x, g x)" a b F] 587 by (simp add: nhds_prod[symmetric] tendsto_Pair) 588 589lemma continuous_add [continuous_intros]: 590 fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" 591 shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)" 592 unfolding continuous_def by (rule tendsto_add) 593 594lemma continuous_on_add [continuous_intros]: 595 fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" 596 shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)" 597 unfolding continuous_on_def by (auto intro: tendsto_add) 598 599lemma tendsto_add_zero: 600 fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" 601 shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> (g \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> 0) F" 602 by (drule (1) tendsto_add) simp 603 604lemma tendsto_sum [tendsto_intros]: 605 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add" 606 shows "(\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F) \<Longrightarrow> ((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F" 607 by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add) 608 609lemma tendsto_null_sum: 610 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add" 611 assumes "\<And>i. i \<in> I \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> 0) F" 612 shows "((\<lambda>i. sum (f i) I) \<longlongrightarrow> 0) F" 613 using tendsto_sum [of I "\<lambda>x y. f y x" "\<lambda>x. 0"] assms by simp 614 615lemma continuous_sum [continuous_intros]: 616 fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add" 617 shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)" 618 unfolding continuous_def by (rule tendsto_sum) 619 620lemma continuous_on_sum [continuous_intros]: 621 fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_add" 622 shows "(\<And>i. i \<in> I \<Longrightarrow> continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<Sum>i\<in>I. f i x)" 623 unfolding continuous_on_def by (auto intro: tendsto_sum) 624 625instance nat :: topological_comm_monoid_add 626 by standard 627 (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) 628 629instance int :: topological_comm_monoid_add 630 by standard 631 (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) 632 633 634subsubsection \<open>Topological group\<close> 635 636class topological_group_add = topological_monoid_add + group_add + 637 assumes tendsto_uminus_nhds: "(uminus \<longlongrightarrow> - a) (nhds a)" 638begin 639 640lemma tendsto_minus [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. - f x) \<longlongrightarrow> - a) F" 641 by (rule filterlim_compose[OF tendsto_uminus_nhds]) 642 643end 644 645class topological_ab_group_add = topological_group_add + ab_group_add 646 647instance topological_ab_group_add < topological_comm_monoid_add .. 648 649lemma continuous_minus [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)" 650 for f :: "'a::t2_space \<Rightarrow> 'b::topological_group_add" 651 unfolding continuous_def by (rule tendsto_minus) 652 653lemma continuous_on_minus [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)" 654 for f :: "_ \<Rightarrow> 'b::topological_group_add" 655 unfolding continuous_on_def by (auto intro: tendsto_minus) 656 657lemma tendsto_minus_cancel: "((\<lambda>x. - f x) \<longlongrightarrow> - a) F \<Longrightarrow> (f \<longlongrightarrow> a) F" 658 for a :: "'a::topological_group_add" 659 by (drule tendsto_minus) simp 660 661lemma tendsto_minus_cancel_left: 662 "(f \<longlongrightarrow> - (y::_::topological_group_add)) F \<longleftrightarrow> ((\<lambda>x. - f x) \<longlongrightarrow> y) F" 663 using tendsto_minus_cancel[of f "- y" F] tendsto_minus[of f "- y" F] 664 by auto 665 666lemma tendsto_diff [tendsto_intros]: 667 fixes a b :: "'a::topological_group_add" 668 shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x - g x) \<longlongrightarrow> a - b) F" 669 using tendsto_add [of f a F "\<lambda>x. - g x" "- b"] by (simp add: tendsto_minus) 670 671lemma continuous_diff [continuous_intros]: 672 fixes f g :: "'a::t2_space \<Rightarrow> 'b::topological_group_add" 673 shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x - g x)" 674 unfolding continuous_def by (rule tendsto_diff) 675 676lemma continuous_on_diff [continuous_intros]: 677 fixes f g :: "_ \<Rightarrow> 'b::topological_group_add" 678 shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)" 679 unfolding continuous_on_def by (auto intro: tendsto_diff) 680 681lemma continuous_on_op_minus: "continuous_on (s::'a::topological_group_add set) ((-) x)" 682 by (rule continuous_intros | simp)+ 683 684instance real_normed_vector < topological_ab_group_add 685proof 686 fix a b :: 'a 687 show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)" 688 unfolding tendsto_Zfun_iff add_diff_add 689 using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"] 690 by (intro Zfun_add) 691 (auto simp: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst) 692 show "(uminus \<longlongrightarrow> - a) (nhds a)" 693 unfolding tendsto_Zfun_iff minus_diff_minus 694 using filterlim_ident[of "nhds a"] 695 by (intro Zfun_minus) (simp add: tendsto_Zfun_iff) 696qed 697 698lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real] 699 700 701subsubsection \<open>Linear operators and multiplication\<close> 702 703lemma linear_times: "linear (\<lambda>x. c * x)" 704 for c :: "'a::real_algebra" 705 by (auto simp: linearI distrib_left) 706 707lemma (in bounded_linear) tendsto: "(g \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f (g x)) \<longlongrightarrow> f a) F" 708 by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) 709 710lemma (in bounded_linear) continuous: "continuous F g \<Longrightarrow> continuous F (\<lambda>x. f (g x))" 711 using tendsto[of g _ F] by (auto simp: continuous_def) 712 713lemma (in bounded_linear) continuous_on: "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))" 714 using tendsto[of g] by (auto simp: continuous_on_def) 715 716lemma (in bounded_linear) tendsto_zero: "(g \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) \<longlongrightarrow> 0) F" 717 by (drule tendsto) (simp only: zero) 718 719lemma (in bounded_bilinear) tendsto: 720 "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x ** g x) \<longlongrightarrow> a ** b) F" 721 by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right) 722 723lemma (in bounded_bilinear) continuous: 724 "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x ** g x)" 725 using tendsto[of f _ F g] by (auto simp: continuous_def) 726 727lemma (in bounded_bilinear) continuous_on: 728 "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)" 729 using tendsto[of f _ _ g] by (auto simp: continuous_on_def) 730 731lemma (in bounded_bilinear) tendsto_zero: 732 assumes f: "(f \<longlongrightarrow> 0) F" 733 and g: "(g \<longlongrightarrow> 0) F" 734 shows "((\<lambda>x. f x ** g x) \<longlongrightarrow> 0) F" 735 using tendsto [OF f g] by (simp add: zero_left) 736 737lemma (in bounded_bilinear) tendsto_left_zero: 738 "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x ** c) \<longlongrightarrow> 0) F" 739 by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) 740 741lemma (in bounded_bilinear) tendsto_right_zero: 742 "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) \<longlongrightarrow> 0) F" 743 by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) 744 745lemmas tendsto_of_real [tendsto_intros] = 746 bounded_linear.tendsto [OF bounded_linear_of_real] 747 748lemmas tendsto_scaleR [tendsto_intros] = 749 bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] 750 751 752text\<open>Analogous type class for multiplication\<close> 753class topological_semigroup_mult = topological_space + semigroup_mult + 754 assumes tendsto_mult_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x * snd x :> nhds (a * b)" 755 756instance real_normed_algebra < topological_semigroup_mult 757proof 758 fix a b :: 'a 759 show "((\<lambda>x. fst x * snd x) \<longlongrightarrow> a * b) (nhds a \<times>\<^sub>F nhds b)" 760 unfolding nhds_prod[symmetric] 761 using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"] 762 by (simp add: bounded_bilinear.tendsto [OF bounded_bilinear_mult]) 763qed 764 765lemma tendsto_mult [tendsto_intros]: 766 fixes a b :: "'a::topological_semigroup_mult" 767 shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x * g x) \<longlongrightarrow> a * b) F" 768 using filterlim_compose[OF tendsto_mult_Pair, of "\<lambda>x. (f x, g x)" a b F] 769 by (simp add: nhds_prod[symmetric] tendsto_Pair) 770 771lemma tendsto_mult_left: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) \<longlongrightarrow> c * l) F" 772 for c :: "'a::topological_semigroup_mult" 773 by (rule tendsto_mult [OF tendsto_const]) 774 775lemma tendsto_mult_right: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) \<longlongrightarrow> l * c) F" 776 for c :: "'a::topological_semigroup_mult" 777 by (rule tendsto_mult [OF _ tendsto_const]) 778 779lemmas continuous_of_real [continuous_intros] = 780 bounded_linear.continuous [OF bounded_linear_of_real] 781 782lemmas continuous_scaleR [continuous_intros] = 783 bounded_bilinear.continuous [OF bounded_bilinear_scaleR] 784 785lemmas continuous_mult [continuous_intros] = 786 bounded_bilinear.continuous [OF bounded_bilinear_mult] 787 788lemmas continuous_on_of_real [continuous_intros] = 789 bounded_linear.continuous_on [OF bounded_linear_of_real] 790 791lemmas continuous_on_scaleR [continuous_intros] = 792 bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR] 793 794lemmas continuous_on_mult [continuous_intros] = 795 bounded_bilinear.continuous_on [OF bounded_bilinear_mult] 796 797lemmas tendsto_mult_zero = 798 bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] 799 800lemmas tendsto_mult_left_zero = 801 bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] 802 803lemmas tendsto_mult_right_zero = 804 bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] 805 806 807lemma continuous_mult_left: 808 fixes c::"'a::real_normed_algebra" 809 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)" 810by (rule continuous_mult [OF continuous_const]) 811 812lemma continuous_mult_right: 813 fixes c::"'a::real_normed_algebra" 814 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x * c)" 815by (rule continuous_mult [OF _ continuous_const]) 816 817lemma continuous_on_mult_left: 818 fixes c::"'a::real_normed_algebra" 819 shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c * f x)" 820by (rule continuous_on_mult [OF continuous_on_const]) 821 822lemma continuous_on_mult_right: 823 fixes c::"'a::real_normed_algebra" 824 shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)" 825by (rule continuous_on_mult [OF _ continuous_on_const]) 826 827lemma continuous_on_mult_const [simp]: 828 fixes c::"'a::real_normed_algebra" 829 shows "continuous_on s (( *) c)" 830 by (intro continuous_on_mult_left continuous_on_id) 831 832lemma tendsto_divide_zero: 833 fixes c :: "'a::real_normed_field" 834 shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x / c) \<longlongrightarrow> 0) F" 835 by (cases "c=0") (simp_all add: divide_inverse tendsto_mult_left_zero) 836 837lemma tendsto_power [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> a ^ n) F" 838 for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" 839 by (induct n) (simp_all add: tendsto_mult) 840 841lemma tendsto_null_power: "\<lbrakk>(f \<longlongrightarrow> 0) F; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F" 842 for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra_1}" 843 using tendsto_power [of f 0 F n] by (simp add: power_0_left) 844 845lemma continuous_power [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)" 846 for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}" 847 unfolding continuous_def by (rule tendsto_power) 848 849lemma continuous_on_power [continuous_intros]: 850 fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}" 851 shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)" 852 unfolding continuous_on_def by (auto intro: tendsto_power) 853 854lemma tendsto_prod [tendsto_intros]: 855 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 856 shows "(\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> L i) F) \<Longrightarrow> ((\<lambda>x. \<Prod>i\<in>S. f i x) \<longlongrightarrow> (\<Prod>i\<in>S. L i)) F" 857 by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult) 858 859lemma continuous_prod [continuous_intros]: 860 fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 861 shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)" 862 unfolding continuous_def by (rule tendsto_prod) 863 864lemma continuous_on_prod [continuous_intros]: 865 fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 866 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)" 867 unfolding continuous_on_def by (auto intro: tendsto_prod) 868 869lemma tendsto_of_real_iff: 870 "((\<lambda>x. of_real (f x) :: 'a::real_normed_div_algebra) \<longlongrightarrow> of_real c) F \<longleftrightarrow> (f \<longlongrightarrow> c) F" 871 unfolding tendsto_iff by simp 872 873lemma tendsto_add_const_iff: 874 "((\<lambda>x. c + f x :: 'a::real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F" 875 using tendsto_add[OF tendsto_const[of c], of f d] 876 and tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto 877 878 879subsubsection \<open>Inverse and division\<close> 880 881lemma (in bounded_bilinear) Zfun_prod_Bfun: 882 assumes f: "Zfun f F" 883 and g: "Bfun g F" 884 shows "Zfun (\<lambda>x. f x ** g x) F" 885proof - 886 obtain K where K: "0 \<le> K" 887 and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 888 using nonneg_bounded by blast 889 obtain B where B: "0 < B" 890 and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) F" 891 using g by (rule BfunE) 892 have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) F" 893 using norm_g proof eventually_elim 894 case (elim x) 895 have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" 896 by (rule norm_le) 897 also have "\<dots> \<le> norm (f x) * B * K" 898 by (intro mult_mono' order_refl norm_g norm_ge_zero mult_nonneg_nonneg K elim) 899 also have "\<dots> = norm (f x) * (B * K)" 900 by (rule mult.assoc) 901 finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" . 902 qed 903 with f show ?thesis 904 by (rule Zfun_imp_Zfun) 905qed 906 907lemma (in bounded_bilinear) Bfun_prod_Zfun: 908 assumes f: "Bfun f F" 909 and g: "Zfun g F" 910 shows "Zfun (\<lambda>x. f x ** g x) F" 911 using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) 912 913lemma Bfun_inverse: 914 fixes a :: "'a::real_normed_div_algebra" 915 assumes f: "(f \<longlongrightarrow> a) F" 916 assumes a: "a \<noteq> 0" 917 shows "Bfun (\<lambda>x. inverse (f x)) F" 918proof - 919 from a have "0 < norm a" by simp 920 then have "\<exists>r>0. r < norm a" by (rule dense) 921 then obtain r where r1: "0 < r" and r2: "r < norm a" 922 by blast 923 have "eventually (\<lambda>x. dist (f x) a < r) F" 924 using tendstoD [OF f r1] by blast 925 then have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) F" 926 proof eventually_elim 927 case (elim x) 928 then have 1: "norm (f x - a) < r" 929 by (simp add: dist_norm) 930 then have 2: "f x \<noteq> 0" using r2 by auto 931 then have "norm (inverse (f x)) = inverse (norm (f x))" 932 by (rule nonzero_norm_inverse) 933 also have "\<dots> \<le> inverse (norm a - r)" 934 proof (rule le_imp_inverse_le) 935 show "0 < norm a - r" 936 using r2 by simp 937 have "norm a - norm (f x) \<le> norm (a - f x)" 938 by (rule norm_triangle_ineq2) 939 also have "\<dots> = norm (f x - a)" 940 by (rule norm_minus_commute) 941 also have "\<dots> < r" using 1 . 942 finally show "norm a - r \<le> norm (f x)" 943 by simp 944 qed 945 finally show "norm (inverse (f x)) \<le> inverse (norm a - r)" . 946 qed 947 then show ?thesis by (rule BfunI) 948qed 949 950lemma tendsto_inverse [tendsto_intros]: 951 fixes a :: "'a::real_normed_div_algebra" 952 assumes f: "(f \<longlongrightarrow> a) F" 953 and a: "a \<noteq> 0" 954 shows "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse a) F" 955proof - 956 from a have "0 < norm a" by simp 957 with f have "eventually (\<lambda>x. dist (f x) a < norm a) F" 958 by (rule tendstoD) 959 then have "eventually (\<lambda>x. f x \<noteq> 0) F" 960 unfolding dist_norm by (auto elim!: eventually_mono) 961 with a have "eventually (\<lambda>x. inverse (f x) - inverse a = 962 - (inverse (f x) * (f x - a) * inverse a)) F" 963 by (auto elim!: eventually_mono simp: inverse_diff_inverse) 964 moreover have "Zfun (\<lambda>x. - (inverse (f x) * (f x - a) * inverse a)) F" 965 by (intro Zfun_minus Zfun_mult_left 966 bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] 967 Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff]) 968 ultimately show ?thesis 969 unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) 970qed 971 972lemma continuous_inverse: 973 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" 974 assumes "continuous F f" 975 and "f (Lim F (\<lambda>x. x)) \<noteq> 0" 976 shows "continuous F (\<lambda>x. inverse (f x))" 977 using assms unfolding continuous_def by (rule tendsto_inverse) 978 979lemma continuous_at_within_inverse[continuous_intros]: 980 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" 981 assumes "continuous (at a within s) f" 982 and "f a \<noteq> 0" 983 shows "continuous (at a within s) (\<lambda>x. inverse (f x))" 984 using assms unfolding continuous_within by (rule tendsto_inverse) 985 986lemma continuous_on_inverse[continuous_intros]: 987 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra" 988 assumes "continuous_on s f" 989 and "\<forall>x\<in>s. f x \<noteq> 0" 990 shows "continuous_on s (\<lambda>x. inverse (f x))" 991 using assms unfolding continuous_on_def by (blast intro: tendsto_inverse) 992 993lemma tendsto_divide [tendsto_intros]: 994 fixes a b :: "'a::real_normed_field" 995 shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> ((\<lambda>x. f x / g x) \<longlongrightarrow> a / b) F" 996 by (simp add: tendsto_mult tendsto_inverse divide_inverse) 997 998lemma continuous_divide: 999 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field" 1000 assumes "continuous F f" 1001 and "continuous F g" 1002 and "g (Lim F (\<lambda>x. x)) \<noteq> 0" 1003 shows "continuous F (\<lambda>x. (f x) / (g x))" 1004 using assms unfolding continuous_def by (rule tendsto_divide) 1005 1006lemma continuous_at_within_divide[continuous_intros]: 1007 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field" 1008 assumes "continuous (at a within s) f" "continuous (at a within s) g" 1009 and "g a \<noteq> 0" 1010 shows "continuous (at a within s) (\<lambda>x. (f x) / (g x))" 1011 using assms unfolding continuous_within by (rule tendsto_divide) 1012 1013lemma isCont_divide[continuous_intros, simp]: 1014 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field" 1015 assumes "isCont f a" "isCont g a" "g a \<noteq> 0" 1016 shows "isCont (\<lambda>x. (f x) / g x) a" 1017 using assms unfolding continuous_at by (rule tendsto_divide) 1018 1019lemma continuous_on_divide[continuous_intros]: 1020 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field" 1021 assumes "continuous_on s f" "continuous_on s g" 1022 and "\<forall>x\<in>s. g x \<noteq> 0" 1023 shows "continuous_on s (\<lambda>x. (f x) / (g x))" 1024 using assms unfolding continuous_on_def by (blast intro: tendsto_divide) 1025 1026lemma tendsto_sgn [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. sgn (f x)) \<longlongrightarrow> sgn l) F" 1027 for l :: "'a::real_normed_vector" 1028 unfolding sgn_div_norm by (simp add: tendsto_intros) 1029 1030lemma continuous_sgn: 1031 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 1032 assumes "continuous F f" 1033 and "f (Lim F (\<lambda>x. x)) \<noteq> 0" 1034 shows "continuous F (\<lambda>x. sgn (f x))" 1035 using assms unfolding continuous_def by (rule tendsto_sgn) 1036 1037lemma continuous_at_within_sgn[continuous_intros]: 1038 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 1039 assumes "continuous (at a within s) f" 1040 and "f a \<noteq> 0" 1041 shows "continuous (at a within s) (\<lambda>x. sgn (f x))" 1042 using assms unfolding continuous_within by (rule tendsto_sgn) 1043 1044lemma isCont_sgn[continuous_intros]: 1045 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 1046 assumes "isCont f a" 1047 and "f a \<noteq> 0" 1048 shows "isCont (\<lambda>x. sgn (f x)) a" 1049 using assms unfolding continuous_at by (rule tendsto_sgn) 1050 1051lemma continuous_on_sgn[continuous_intros]: 1052 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" 1053 assumes "continuous_on s f" 1054 and "\<forall>x\<in>s. f x \<noteq> 0" 1055 shows "continuous_on s (\<lambda>x. sgn (f x))" 1056 using assms unfolding continuous_on_def by (blast intro: tendsto_sgn) 1057 1058lemma filterlim_at_infinity: 1059 fixes f :: "_ \<Rightarrow> 'a::real_normed_vector" 1060 assumes "0 \<le> c" 1061 shows "(LIM x F. f x :> at_infinity) \<longleftrightarrow> (\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F)" 1062 unfolding filterlim_iff eventually_at_infinity 1063proof safe 1064 fix P :: "'a \<Rightarrow> bool" 1065 fix b 1066 assume *: "\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F" 1067 assume P: "\<forall>x. b \<le> norm x \<longrightarrow> P x" 1068 have "max b (c + 1) > c" by auto 1069 with * have "eventually (\<lambda>x. max b (c + 1) \<le> norm (f x)) F" 1070 by auto 1071 then show "eventually (\<lambda>x. P (f x)) F" 1072 proof eventually_elim 1073 case (elim x) 1074 with P show "P (f x)" by auto 1075 qed 1076qed force 1077 1078lemma filterlim_at_infinity_imp_norm_at_top: 1079 fixes F 1080 assumes "filterlim f at_infinity F" 1081 shows "filterlim (\<lambda>x. norm (f x)) at_top F" 1082proof - 1083 { 1084 fix r :: real 1085 have "\<forall>\<^sub>F x in F. r \<le> norm (f x)" using filterlim_at_infinity[of 0 f F] assms 1086 by (cases "r > 0") 1087 (auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero]) 1088 } 1089 thus ?thesis by (auto simp: filterlim_at_top) 1090qed 1091 1092lemma filterlim_norm_at_top_imp_at_infinity: 1093 fixes F 1094 assumes "filterlim (\<lambda>x. norm (f x)) at_top F" 1095 shows "filterlim f at_infinity F" 1096 using filterlim_at_infinity[of 0 f F] assms by (auto simp: filterlim_at_top) 1097 1098lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity" 1099 by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident) 1100 1101lemma filterlim_at_infinity_conv_norm_at_top: 1102 "filterlim f at_infinity G \<longleftrightarrow> filterlim (\<lambda>x. norm (f x)) at_top G" 1103 by (auto simp: filterlim_at_infinity[OF order.refl] filterlim_at_top_gt[of _ _ 0]) 1104 1105lemma eventually_not_equal_at_infinity: 1106 "eventually (\<lambda>x. x \<noteq> (a :: 'a :: {real_normed_vector})) at_infinity" 1107proof - 1108 from filterlim_norm_at_top[where 'a = 'a] 1109 have "\<forall>\<^sub>F x in at_infinity. norm a < norm (x::'a)" by (auto simp: filterlim_at_top_dense) 1110 thus ?thesis by eventually_elim auto 1111qed 1112 1113lemma filterlim_int_of_nat_at_topD: 1114 fixes F 1115 assumes "filterlim (\<lambda>x. f (int x)) F at_top" 1116 shows "filterlim f F at_top" 1117proof - 1118 have "filterlim (\<lambda>x. f (int (nat x))) F at_top" 1119 by (rule filterlim_compose[OF assms filterlim_nat_sequentially]) 1120 also have "?this \<longleftrightarrow> filterlim f F at_top" 1121 by (intro filterlim_cong refl eventually_mono [OF eventually_ge_at_top[of "0::int"]]) auto 1122 finally show ?thesis . 1123qed 1124 1125lemma filterlim_int_sequentially [tendsto_intros]: 1126 "filterlim int at_top sequentially" 1127 unfolding filterlim_at_top 1128proof 1129 fix C :: int 1130 show "eventually (\<lambda>n. int n \<ge> C) at_top" 1131 using eventually_ge_at_top[of "nat \<lceil>C\<rceil>"] by eventually_elim linarith 1132qed 1133 1134lemma filterlim_real_of_int_at_top [tendsto_intros]: 1135 "filterlim real_of_int at_top at_top" 1136 unfolding filterlim_at_top 1137proof 1138 fix C :: real 1139 show "eventually (\<lambda>n. real_of_int n \<ge> C) at_top" 1140 using eventually_ge_at_top[of "\<lceil>C\<rceil>"] by eventually_elim linarith 1141qed 1142 1143lemma filterlim_abs_real: "filterlim (abs::real \<Rightarrow> real) at_top at_top" 1144proof (subst filterlim_cong[OF refl refl]) 1145 from eventually_ge_at_top[of "0::real"] show "eventually (\<lambda>x::real. \<bar>x\<bar> = x) at_top" 1146 by eventually_elim simp 1147qed (simp_all add: filterlim_ident) 1148 1149lemma filterlim_of_real_at_infinity [tendsto_intros]: 1150 "filterlim (of_real :: real \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity at_top" 1151 by (intro filterlim_norm_at_top_imp_at_infinity) (auto simp: filterlim_abs_real) 1152 1153lemma not_tendsto_and_filterlim_at_infinity: 1154 fixes c :: "'a::real_normed_vector" 1155 assumes "F \<noteq> bot" 1156 and "(f \<longlongrightarrow> c) F" 1157 and "filterlim f at_infinity F" 1158 shows False 1159proof - 1160 from tendstoD[OF assms(2), of "1/2"] 1161 have "eventually (\<lambda>x. dist (f x) c < 1/2) F" 1162 by simp 1163 moreover 1164 from filterlim_at_infinity[of "norm c" f F] assms(3) 1165 have "eventually (\<lambda>x. norm (f x) \<ge> norm c + 1) F" by simp 1166 ultimately have "eventually (\<lambda>x. False) F" 1167 proof eventually_elim 1168 fix x 1169 assume A: "dist (f x) c < 1/2" 1170 assume "norm (f x) \<ge> norm c + 1" 1171 also have "norm (f x) = dist (f x) 0" by simp 1172 also have "\<dots> \<le> dist (f x) c + dist c 0" by (rule dist_triangle) 1173 finally show False using A by simp 1174 qed 1175 with assms show False by simp 1176qed 1177 1178lemma filterlim_at_infinity_imp_not_convergent: 1179 assumes "filterlim f at_infinity sequentially" 1180 shows "\<not> convergent f" 1181 by (rule notI, rule not_tendsto_and_filterlim_at_infinity[OF _ _ assms]) 1182 (simp_all add: convergent_LIMSEQ_iff) 1183 1184lemma filterlim_at_infinity_imp_eventually_ne: 1185 assumes "filterlim f at_infinity F" 1186 shows "eventually (\<lambda>z. f z \<noteq> c) F" 1187proof - 1188 have "norm c + 1 > 0" 1189 by (intro add_nonneg_pos) simp_all 1190 with filterlim_at_infinity[OF order.refl, of f F] assms 1191 have "eventually (\<lambda>z. norm (f z) \<ge> norm c + 1) F" 1192 by blast 1193 then show ?thesis 1194 by eventually_elim auto 1195qed 1196 1197lemma tendsto_of_nat [tendsto_intros]: 1198 "filterlim (of_nat :: nat \<Rightarrow> 'a::real_normed_algebra_1) at_infinity sequentially" 1199proof (subst filterlim_at_infinity[OF order.refl], intro allI impI) 1200 fix r :: real 1201 assume r: "r > 0" 1202 define n where "n = nat \<lceil>r\<rceil>" 1203 from r have n: "\<forall>m\<ge>n. of_nat m \<ge> r" 1204 unfolding n_def by linarith 1205 from eventually_ge_at_top[of n] show "eventually (\<lambda>m. norm (of_nat m :: 'a) \<ge> r) sequentially" 1206 by eventually_elim (use n in simp_all) 1207qed 1208 1209 1210subsection \<open>Relate @{const at}, @{const at_left} and @{const at_right}\<close> 1211 1212text \<open> 1213 This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and 1214 @{term "at_right x"} and also @{term "at_right 0"}. 1215\<close> 1216 1217lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real] 1218 1219lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d)" 1220 for a d :: "'a::real_normed_vector" 1221 by (rule filtermap_fun_inverse[where g="\<lambda>x. x + d"]) 1222 (auto intro!: tendsto_eq_intros filterlim_ident) 1223 1224lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a)" 1225 for a :: "'a::real_normed_vector" 1226 by (rule filtermap_fun_inverse[where g=uminus]) 1227 (auto intro!: tendsto_eq_intros filterlim_ident) 1228 1229lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d)" 1230 for a d :: "'a::real_normed_vector" 1231 by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) 1232 1233lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x - d) (at_right a) = at_right (a - d)" 1234 for a d :: "real" 1235 by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) 1236 1237lemma at_right_to_0: "at_right a = filtermap (\<lambda>x. x + a) (at_right 0)" 1238 for a :: real 1239 using filtermap_at_right_shift[of "-a" 0] by simp 1240 1241lemma filterlim_at_right_to_0: 1242 "filterlim f F (at_right a) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)" 1243 for a :: real 1244 unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] .. 1245 1246lemma eventually_at_right_to_0: 1247 "eventually P (at_right a) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)" 1248 for a :: real 1249 unfolding at_right_to_0[of a] by (simp add: eventually_filtermap) 1250 1251lemma at_to_0: "at a = filtermap (\<lambda>x. x + a) (at 0)" 1252 for a :: "'a::real_normed_vector" 1253 using filtermap_at_shift[of "-a" 0] by simp 1254 1255lemma filterlim_at_to_0: 1256 "filterlim f F (at a) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at 0)" 1257 for a :: "'a::real_normed_vector" 1258 unfolding filterlim_def filtermap_filtermap at_to_0[of a] .. 1259 1260lemma eventually_at_to_0: 1261 "eventually P (at a) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at 0)" 1262 for a :: "'a::real_normed_vector" 1263 unfolding at_to_0[of a] by (simp add: eventually_filtermap) 1264 1265lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a)" 1266 for a :: "'a::real_normed_vector" 1267 by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) 1268 1269lemma at_left_minus: "at_left a = filtermap (\<lambda>x. - x) (at_right (- a))" 1270 for a :: real 1271 by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) 1272 1273lemma at_right_minus: "at_right a = filtermap (\<lambda>x. - x) (at_left (- a))" 1274 for a :: real 1275 by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) 1276 1277 1278lemma filterlim_at_left_to_right: 1279 "filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))" 1280 for a :: real 1281 unfolding filterlim_def filtermap_filtermap at_left_minus[of a] .. 1282 1283lemma eventually_at_left_to_right: 1284 "eventually P (at_left a) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))" 1285 for a :: real 1286 unfolding at_left_minus[of a] by (simp add: eventually_filtermap) 1287 1288lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top" 1289 unfolding filterlim_at_top eventually_at_bot_dense 1290 by (metis leI minus_less_iff order_less_asym) 1291 1292lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot" 1293 unfolding filterlim_at_bot eventually_at_top_dense 1294 by (metis leI less_minus_iff order_less_asym) 1295 1296lemma at_bot_mirror : 1297 shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top" 1298 apply (rule filtermap_fun_inverse[of uminus, symmetric]) 1299 subgoal unfolding filterlim_at_top filterlim_at_bot eventually_at_bot_linorder using le_minus_iff by auto 1300 subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto 1301 by auto 1302 1303lemma at_top_mirror : 1304 shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot" 1305 apply (subst at_bot_mirror) 1306 by (auto simp: filtermap_filtermap) 1307 1308lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)" 1309 unfolding filterlim_def at_top_mirror filtermap_filtermap .. 1310 1311lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \<longleftrightarrow> (LIM x at_top. f (-x::real) :> F)" 1312 unfolding filterlim_def at_bot_mirror filtermap_filtermap .. 1313 1314lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_bot)" 1315 using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F] 1316 and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F] 1317 by auto 1318 1319lemma filterlim_at_infinity_imp_filterlim_at_top: 1320 assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F" 1321 assumes "eventually (\<lambda>x. f x > 0) F" 1322 shows "filterlim f at_top F" 1323proof - 1324 from assms(2) have *: "eventually (\<lambda>x. norm (f x) = f x) F" by eventually_elim simp 1325 from assms(1) show ?thesis unfolding filterlim_at_infinity_conv_norm_at_top 1326 by (subst (asm) filterlim_cong[OF refl refl *]) 1327qed 1328 1329lemma filterlim_at_infinity_imp_filterlim_at_bot: 1330 assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F" 1331 assumes "eventually (\<lambda>x. f x < 0) F" 1332 shows "filterlim f at_bot F" 1333proof - 1334 from assms(2) have *: "eventually (\<lambda>x. norm (f x) = -f x) F" by eventually_elim simp 1335 from assms(1) have "filterlim (\<lambda>x. - f x) at_top F" 1336 unfolding filterlim_at_infinity_conv_norm_at_top 1337 by (subst (asm) filterlim_cong[OF refl refl *]) 1338 thus ?thesis by (simp add: filterlim_uminus_at_top) 1339qed 1340 1341lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)" 1342 unfolding filterlim_uminus_at_top by simp 1343 1344lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top" 1345 unfolding filterlim_at_top_gt[where c=0] eventually_at_filter 1346proof safe 1347 fix Z :: real 1348 assume [arith]: "0 < Z" 1349 then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)" 1350 by (auto simp: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"]) 1351 then show "eventually (\<lambda>x. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)" 1352 by (auto elim!: eventually_mono simp: inverse_eq_divide field_simps) 1353qed 1354 1355lemma tendsto_inverse_0: 1356 fixes x :: "_ \<Rightarrow> 'a::real_normed_div_algebra" 1357 shows "(inverse \<longlongrightarrow> (0::'a)) at_infinity" 1358 unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity 1359proof safe 1360 fix r :: real 1361 assume "0 < r" 1362 show "\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> norm (inverse x :: 'a) < r" 1363 proof (intro exI[of _ "inverse (r / 2)"] allI impI) 1364 fix x :: 'a 1365 from \<open>0 < r\<close> have "0 < inverse (r / 2)" by simp 1366 also assume *: "inverse (r / 2) \<le> norm x" 1367 finally show "norm (inverse x) < r" 1368 using * \<open>0 < r\<close> 1369 by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps) 1370 qed 1371qed 1372 1373lemma tendsto_add_filterlim_at_infinity: 1374 fixes c :: "'b::real_normed_vector" 1375 and F :: "'a filter" 1376 assumes "(f \<longlongrightarrow> c) F" 1377 and "filterlim g at_infinity F" 1378 shows "filterlim (\<lambda>x. f x + g x) at_infinity F" 1379proof (subst filterlim_at_infinity[OF order_refl], safe) 1380 fix r :: real 1381 assume r: "r > 0" 1382 from assms(1) have "((\<lambda>x. norm (f x)) \<longlongrightarrow> norm c) F" 1383 by (rule tendsto_norm) 1384 then have "eventually (\<lambda>x. norm (f x) < norm c + 1) F" 1385 by (rule order_tendstoD) simp_all 1386 moreover from r have "r + norm c + 1 > 0" 1387 by (intro add_pos_nonneg) simp_all 1388 with assms(2) have "eventually (\<lambda>x. norm (g x) \<ge> r + norm c + 1) F" 1389 unfolding filterlim_at_infinity[OF order_refl] 1390 by (elim allE[of _ "r + norm c + 1"]) simp_all 1391 ultimately show "eventually (\<lambda>x. norm (f x + g x) \<ge> r) F" 1392 proof eventually_elim 1393 fix x :: 'a 1394 assume A: "norm (f x) < norm c + 1" and B: "r + norm c + 1 \<le> norm (g x)" 1395 from A B have "r \<le> norm (g x) - norm (f x)" 1396 by simp 1397 also have "norm (g x) - norm (f x) \<le> norm (g x + f x)" 1398 by (rule norm_diff_ineq) 1399 finally show "r \<le> norm (f x + g x)" 1400 by (simp add: add_ac) 1401 qed 1402qed 1403 1404lemma tendsto_add_filterlim_at_infinity': 1405 fixes c :: "'b::real_normed_vector" 1406 and F :: "'a filter" 1407 assumes "filterlim f at_infinity F" 1408 and "(g \<longlongrightarrow> c) F" 1409 shows "filterlim (\<lambda>x. f x + g x) at_infinity F" 1410 by (subst add.commute) (rule tendsto_add_filterlim_at_infinity assms)+ 1411 1412lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)" 1413 unfolding filterlim_at 1414 by (auto simp: eventually_at_top_dense) 1415 (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl) 1416 1417lemma filterlim_inverse_at_top: 1418 "(f \<longlongrightarrow> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top" 1419 by (intro filterlim_compose[OF filterlim_inverse_at_top_right]) 1420 (simp add: filterlim_def eventually_filtermap eventually_mono at_within_def le_principal) 1421 1422lemma filterlim_inverse_at_bot_neg: 1423 "LIM x (at_left (0::real)). inverse x :> at_bot" 1424 by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right) 1425 1426lemma filterlim_inverse_at_bot: 1427 "(f \<longlongrightarrow> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot" 1428 unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric] 1429 by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric]) 1430 1431lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top" 1432 by (intro filtermap_fun_inverse[symmetric, where g=inverse]) 1433 (auto intro: filterlim_inverse_at_top_right filterlim_inverse_at_right_top) 1434 1435lemma eventually_at_right_to_top: 1436 "eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top" 1437 unfolding at_right_to_top eventually_filtermap .. 1438 1439lemma filterlim_at_right_to_top: 1440 "filterlim f F (at_right (0::real)) \<longleftrightarrow> (LIM x at_top. f (inverse x) :> F)" 1441 unfolding filterlim_def at_right_to_top filtermap_filtermap .. 1442 1443lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))" 1444 unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident .. 1445 1446lemma eventually_at_top_to_right: 1447 "eventually P at_top \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) (at_right (0::real))" 1448 unfolding at_top_to_right eventually_filtermap .. 1449 1450lemma filterlim_at_top_to_right: 1451 "filterlim f F at_top \<longleftrightarrow> (LIM x (at_right (0::real)). f (inverse x) :> F)" 1452 unfolding filterlim_def at_top_to_right filtermap_filtermap .. 1453 1454lemma filterlim_inverse_at_infinity: 1455 fixes x :: "_ \<Rightarrow> 'a::{real_normed_div_algebra, division_ring}" 1456 shows "filterlim inverse at_infinity (at (0::'a))" 1457 unfolding filterlim_at_infinity[OF order_refl] 1458proof safe 1459 fix r :: real 1460 assume "0 < r" 1461 then show "eventually (\<lambda>x::'a. r \<le> norm (inverse x)) (at 0)" 1462 unfolding eventually_at norm_inverse 1463 by (intro exI[of _ "inverse r"]) 1464 (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide) 1465qed 1466 1467lemma filterlim_inverse_at_iff: 1468 fixes g :: "'a \<Rightarrow> 'b::{real_normed_div_algebra, division_ring}" 1469 shows "(LIM x F. inverse (g x) :> at 0) \<longleftrightarrow> (LIM x F. g x :> at_infinity)" 1470 unfolding filterlim_def filtermap_filtermap[symmetric] 1471proof 1472 assume "filtermap g F \<le> at_infinity" 1473 then have "filtermap inverse (filtermap g F) \<le> filtermap inverse at_infinity" 1474 by (rule filtermap_mono) 1475 also have "\<dots> \<le> at 0" 1476 using tendsto_inverse_0[where 'a='b] 1477 by (auto intro!: exI[of _ 1] 1478 simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity) 1479 finally show "filtermap inverse (filtermap g F) \<le> at 0" . 1480next 1481 assume "filtermap inverse (filtermap g F) \<le> at 0" 1482 then have "filtermap inverse (filtermap inverse (filtermap g F)) \<le> filtermap inverse (at 0)" 1483 by (rule filtermap_mono) 1484 with filterlim_inverse_at_infinity show "filtermap g F \<le> at_infinity" 1485 by (auto intro: order_trans simp: filterlim_def filtermap_filtermap) 1486qed 1487 1488lemma tendsto_mult_filterlim_at_infinity: 1489 fixes c :: "'a::real_normed_field" 1490 assumes "(f \<longlongrightarrow> c) F" "c \<noteq> 0" 1491 assumes "filterlim g at_infinity F" 1492 shows "filterlim (\<lambda>x. f x * g x) at_infinity F" 1493proof - 1494 have "((\<lambda>x. inverse (f x) * inverse (g x)) \<longlongrightarrow> inverse c * 0) F" 1495 by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0]) 1496 then have "filterlim (\<lambda>x. inverse (f x) * inverse (g x)) (at (inverse c * 0)) F" 1497 unfolding filterlim_at 1498 using assms 1499 by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj) 1500 then show ?thesis 1501 by (subst filterlim_inverse_at_iff[symmetric]) simp_all 1502qed 1503 1504lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F" 1505 by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) 1506 1507lemma real_tendsto_divide_at_top: 1508 fixes c::"real" 1509 assumes "(f \<longlongrightarrow> c) F" 1510 assumes "filterlim g at_top F" 1511 shows "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F" 1512 by (auto simp: divide_inverse_commute 1513 intro!: tendsto_mult[THEN tendsto_eq_rhs] tendsto_inverse_0_at_top assms) 1514 1515lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x) at_top sequentially" 1516 for c :: nat 1517 by (rule filterlim_subseq) (auto simp: strict_mono_def) 1518 1519lemma mult_nat_right_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. x * c) at_top sequentially" 1520 for c :: nat 1521 by (rule filterlim_subseq) (auto simp: strict_mono_def) 1522 1523lemma filterlim_times_pos: 1524 "LIM x F1. c * f x :> at_right l" 1525 if "filterlim f (at_right p) F1" "0 < c" "l = c * p" 1526 for c::"'a::{linordered_field, linorder_topology}" 1527 unfolding filterlim_iff 1528proof safe 1529 fix P 1530 assume "\<forall>\<^sub>F x in at_right l. P x" 1531 then obtain d where "c * p < d" "\<And>y. y > c * p \<Longrightarrow> y < d \<Longrightarrow> P y" 1532 unfolding \<open>l = _ \<close> eventually_at_right_field 1533 by auto 1534 then have "\<forall>\<^sub>F a in at_right p. P (c * a)" 1535 by (auto simp: eventually_at_right_field \<open>0 < c\<close> field_simps intro!: exI[where x="d/c"]) 1536 from that(1)[unfolded filterlim_iff, rule_format, OF this] 1537 show "\<forall>\<^sub>F x in F1. P (c * f x)" . 1538qed 1539 1540lemma filtermap_nhds_times: "c \<noteq> 0 \<Longrightarrow> filtermap (times c) (nhds a) = nhds (c * a)" 1541 for a c :: "'a::real_normed_field" 1542 by (rule filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"]) 1543 (auto intro!: tendsto_eq_intros filterlim_ident) 1544 1545lemma filtermap_times_pos_at_right: 1546 fixes c::"'a::{linordered_field, linorder_topology}" 1547 assumes "c > 0" 1548 shows "filtermap (times c) (at_right p) = at_right (c * p)" 1549 using assms 1550 by (intro filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"]) 1551 (auto intro!: filterlim_ident filterlim_times_pos) 1552 1553lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity" 1554proof (rule antisym) 1555 have "(inverse \<longlongrightarrow> (0::'a)) at_infinity" 1556 by (fact tendsto_inverse_0) 1557 then show "filtermap inverse at_infinity \<le> at (0::'a)" 1558 using filterlim_def filterlim_ident filterlim_inverse_at_iff by fastforce 1559next 1560 have "filtermap inverse (filtermap inverse (at (0::'a))) \<le> filtermap inverse at_infinity" 1561 using filterlim_inverse_at_infinity unfolding filterlim_def 1562 by (rule filtermap_mono) 1563 then show "at (0::'a) \<le> filtermap inverse at_infinity" 1564 by (simp add: filtermap_ident filtermap_filtermap) 1565qed 1566 1567lemma lim_at_infinity_0: 1568 fixes l :: "'a::{real_normed_field,field}" 1569 shows "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> ((f \<circ> inverse) \<longlongrightarrow> l) (at (0::'a))" 1570 by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap) 1571 1572lemma lim_zero_infinity: 1573 fixes l :: "'a::{real_normed_field,field}" 1574 shows "((\<lambda>x. f(1 / x)) \<longlongrightarrow> l) (at (0::'a)) \<Longrightarrow> (f \<longlongrightarrow> l) at_infinity" 1575 by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def) 1576 1577 1578text \<open> 1579 We only show rules for multiplication and addition when the functions are either against a real 1580 value or against infinity. Further rules are easy to derive by using @{thm 1581 filterlim_uminus_at_top}. 1582\<close> 1583 1584lemma filterlim_tendsto_pos_mult_at_top: 1585 assumes f: "(f \<longlongrightarrow> c) F" 1586 and c: "0 < c" 1587 and g: "LIM x F. g x :> at_top" 1588 shows "LIM x F. (f x * g x :: real) :> at_top" 1589 unfolding filterlim_at_top_gt[where c=0] 1590proof safe 1591 fix Z :: real 1592 assume "0 < Z" 1593 from f \<open>0 < c\<close> have "eventually (\<lambda>x. c / 2 < f x) F" 1594 by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_mono 1595 simp: dist_real_def abs_real_def split: if_split_asm) 1596 moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F" 1597 unfolding filterlim_at_top by auto 1598 ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F" 1599 proof eventually_elim 1600 case (elim x) 1601 with \<open>0 < Z\<close> \<open>0 < c\<close> have "c / 2 * (Z / c * 2) \<le> f x * g x" 1602 by (intro mult_mono) (auto simp: zero_le_divide_iff) 1603 with \<open>0 < c\<close> show "Z \<le> f x * g x" 1604 by simp 1605 qed 1606qed 1607 1608lemma filterlim_at_top_mult_at_top: 1609 assumes f: "LIM x F. f x :> at_top" 1610 and g: "LIM x F. g x :> at_top" 1611 shows "LIM x F. (f x * g x :: real) :> at_top" 1612 unfolding filterlim_at_top_gt[where c=0] 1613proof safe 1614 fix Z :: real 1615 assume "0 < Z" 1616 from f have "eventually (\<lambda>x. 1 \<le> f x) F" 1617 unfolding filterlim_at_top by auto 1618 moreover from g have "eventually (\<lambda>x. Z \<le> g x) F" 1619 unfolding filterlim_at_top by auto 1620 ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F" 1621 proof eventually_elim 1622 case (elim x) 1623 with \<open>0 < Z\<close> have "1 * Z \<le> f x * g x" 1624 by (intro mult_mono) (auto simp: zero_le_divide_iff) 1625 then show "Z \<le> f x * g x" 1626 by simp 1627 qed 1628qed 1629 1630lemma filterlim_at_top_mult_tendsto_pos: 1631 assumes f: "(f \<longlongrightarrow> c) F" 1632 and c: "0 < c" 1633 and g: "LIM x F. g x :> at_top" 1634 shows "LIM x F. (g x * f x:: real) :> at_top" 1635 by (auto simp: mult.commute intro!: filterlim_tendsto_pos_mult_at_top f c g) 1636 1637lemma filterlim_tendsto_pos_mult_at_bot: 1638 fixes c :: real 1639 assumes "(f \<longlongrightarrow> c) F" "0 < c" "filterlim g at_bot F" 1640 shows "LIM x F. f x * g x :> at_bot" 1641 using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x. - g x"] assms(3) 1642 unfolding filterlim_uminus_at_bot by simp 1643 1644lemma filterlim_tendsto_neg_mult_at_bot: 1645 fixes c :: real 1646 assumes c: "(f \<longlongrightarrow> c) F" "c < 0" and g: "filterlim g at_top F" 1647 shows "LIM x F. f x * g x :> at_bot" 1648 using c filterlim_tendsto_pos_mult_at_top[of "\<lambda>x. - f x" "- c" F, OF _ _ g] 1649 unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp 1650 1651lemma filterlim_pow_at_top: 1652 fixes f :: "'a \<Rightarrow> real" 1653 assumes "0 < n" 1654 and f: "LIM x F. f x :> at_top" 1655 shows "LIM x F. (f x)^n :: real :> at_top" 1656 using \<open>0 < n\<close> 1657proof (induct n) 1658 case 0 1659 then show ?case by simp 1660next 1661 case (Suc n) with f show ?case 1662 by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top) 1663qed 1664 1665lemma filterlim_pow_at_bot_even: 1666 fixes f :: "real \<Rightarrow> real" 1667 shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> even n \<Longrightarrow> LIM x F. (f x)^n :> at_top" 1668 using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_top) 1669 1670lemma filterlim_pow_at_bot_odd: 1671 fixes f :: "real \<Rightarrow> real" 1672 shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot" 1673 using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot) 1674 1675lemma filterlim_power_at_infinity [tendsto_intros]: 1676 fixes F and f :: "'a \<Rightarrow> 'b :: real_normed_div_algebra" 1677 assumes "filterlim f at_infinity F" "n > 0" 1678 shows "filterlim (\<lambda>x. f x ^ n) at_infinity F" 1679 by (rule filterlim_norm_at_top_imp_at_infinity) 1680 (auto simp: norm_power intro!: filterlim_pow_at_top assms 1681 intro: filterlim_at_infinity_imp_norm_at_top) 1682 1683lemma filterlim_tendsto_add_at_top: 1684 assumes f: "(f \<longlongrightarrow> c) F" 1685 and g: "LIM x F. g x :> at_top" 1686 shows "LIM x F. (f x + g x :: real) :> at_top" 1687 unfolding filterlim_at_top_gt[where c=0] 1688proof safe 1689 fix Z :: real 1690 assume "0 < Z" 1691 from f have "eventually (\<lambda>x. c - 1 < f x) F" 1692 by (auto dest!: tendstoD[where e=1] elim!: eventually_mono simp: dist_real_def) 1693 moreover from g have "eventually (\<lambda>x. Z - (c - 1) \<le> g x) F" 1694 unfolding filterlim_at_top by auto 1695 ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F" 1696 by eventually_elim simp 1697qed 1698 1699lemma LIM_at_top_divide: 1700 fixes f g :: "'a \<Rightarrow> real" 1701 assumes f: "(f \<longlongrightarrow> a) F" "0 < a" 1702 and g: "(g \<longlongrightarrow> 0) F" "eventually (\<lambda>x. 0 < g x) F" 1703 shows "LIM x F. f x / g x :> at_top" 1704 unfolding divide_inverse 1705 by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g]) 1706 1707lemma filterlim_at_top_add_at_top: 1708 assumes f: "LIM x F. f x :> at_top" 1709 and g: "LIM x F. g x :> at_top" 1710 shows "LIM x F. (f x + g x :: real) :> at_top" 1711 unfolding filterlim_at_top_gt[where c=0] 1712proof safe 1713 fix Z :: real 1714 assume "0 < Z" 1715 from f have "eventually (\<lambda>x. 0 \<le> f x) F" 1716 unfolding filterlim_at_top by auto 1717 moreover from g have "eventually (\<lambda>x. Z \<le> g x) F" 1718 unfolding filterlim_at_top by auto 1719 ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F" 1720 by eventually_elim simp 1721qed 1722 1723lemma tendsto_divide_0: 1724 fixes f :: "_ \<Rightarrow> 'a::{real_normed_div_algebra, division_ring}" 1725 assumes f: "(f \<longlongrightarrow> c) F" 1726 and g: "LIM x F. g x :> at_infinity" 1727 shows "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F" 1728 using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] 1729 by (simp add: divide_inverse) 1730 1731lemma linear_plus_1_le_power: 1732 fixes x :: real 1733 assumes x: "0 \<le> x" 1734 shows "real n * x + 1 \<le> (x + 1) ^ n" 1735proof (induct n) 1736 case 0 1737 then show ?case by simp 1738next 1739 case (Suc n) 1740 from x have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)" 1741 by (simp add: field_simps) 1742 also have "\<dots> \<le> (x + 1)^Suc n" 1743 using Suc x by (simp add: mult_left_mono) 1744 finally show ?case . 1745qed 1746 1747lemma filterlim_realpow_sequentially_gt1: 1748 fixes x :: "'a :: real_normed_div_algebra" 1749 assumes x[arith]: "1 < norm x" 1750 shows "LIM n sequentially. x ^ n :> at_infinity" 1751proof (intro filterlim_at_infinity[THEN iffD2] allI impI) 1752 fix y :: real 1753 assume "0 < y" 1754 have "0 < norm x - 1" by simp 1755 then obtain N :: nat where "y < real N * (norm x - 1)" 1756 by (blast dest: reals_Archimedean3) 1757 also have "\<dots> \<le> real N * (norm x - 1) + 1" 1758 by simp 1759 also have "\<dots> \<le> (norm x - 1 + 1) ^ N" 1760 by (rule linear_plus_1_le_power) simp 1761 also have "\<dots> = norm x ^ N" 1762 by simp 1763 finally have "\<forall>n\<ge>N. y \<le> norm x ^ n" 1764 by (metis order_less_le_trans power_increasing order_less_imp_le x) 1765 then show "eventually (\<lambda>n. y \<le> norm (x ^ n)) sequentially" 1766 unfolding eventually_sequentially 1767 by (auto simp: norm_power) 1768qed simp 1769 1770 1771lemma filterlim_divide_at_infinity: 1772 fixes f g :: "'a \<Rightarrow> 'a :: real_normed_field" 1773 assumes "filterlim f (nhds c) F" "filterlim g (at 0) F" "c \<noteq> 0" 1774 shows "filterlim (\<lambda>x. f x / g x) at_infinity F" 1775proof - 1776 have "filterlim (\<lambda>x. f x * inverse (g x)) at_infinity F" 1777 by (intro tendsto_mult_filterlim_at_infinity[OF assms(1,3)] 1778 filterlim_compose [OF filterlim_inverse_at_infinity assms(2)]) 1779 thus ?thesis by (simp add: field_simps) 1780qed 1781 1782subsection \<open>Floor and Ceiling\<close> 1783 1784lemma eventually_floor_less: 1785 fixes f :: "'a \<Rightarrow> 'b::{order_topology,floor_ceiling}" 1786 assumes f: "(f \<longlongrightarrow> l) F" 1787 and l: "l \<notin> \<int>" 1788 shows "\<forall>\<^sub>F x in F. of_int (floor l) < f x" 1789 by (intro order_tendstoD[OF f]) (metis Ints_of_int antisym_conv2 floor_correct l) 1790 1791lemma eventually_less_ceiling: 1792 fixes f :: "'a \<Rightarrow> 'b::{order_topology,floor_ceiling}" 1793 assumes f: "(f \<longlongrightarrow> l) F" 1794 and l: "l \<notin> \<int>" 1795 shows "\<forall>\<^sub>F x in F. f x < of_int (ceiling l)" 1796 by (intro order_tendstoD[OF f]) (metis Ints_of_int l le_of_int_ceiling less_le) 1797 1798lemma eventually_floor_eq: 1799 fixes f::"'a \<Rightarrow> 'b::{order_topology,floor_ceiling}" 1800 assumes f: "(f \<longlongrightarrow> l) F" 1801 and l: "l \<notin> \<int>" 1802 shows "\<forall>\<^sub>F x in F. floor (f x) = floor l" 1803 using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms] 1804 by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq) 1805 1806lemma eventually_ceiling_eq: 1807 fixes f::"'a \<Rightarrow> 'b::{order_topology,floor_ceiling}" 1808 assumes f: "(f \<longlongrightarrow> l) F" 1809 and l: "l \<notin> \<int>" 1810 shows "\<forall>\<^sub>F x in F. ceiling (f x) = ceiling l" 1811 using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms] 1812 by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq) 1813 1814lemma tendsto_of_int_floor: 1815 fixes f::"'a \<Rightarrow> 'b::{order_topology,floor_ceiling}" 1816 assumes "(f \<longlongrightarrow> l) F" 1817 and "l \<notin> \<int>" 1818 shows "((\<lambda>x. of_int (floor (f x)) :: 'c::{ring_1,topological_space}) \<longlongrightarrow> of_int (floor l)) F" 1819 using eventually_floor_eq[OF assms] 1820 by (simp add: eventually_mono topological_tendstoI) 1821 1822lemma tendsto_of_int_ceiling: 1823 fixes f::"'a \<Rightarrow> 'b::{order_topology,floor_ceiling}" 1824 assumes "(f \<longlongrightarrow> l) F" 1825 and "l \<notin> \<int>" 1826 shows "((\<lambda>x. of_int (ceiling (f x)):: 'c::{ring_1,topological_space}) \<longlongrightarrow> of_int (ceiling l)) F" 1827 using eventually_ceiling_eq[OF assms] 1828 by (simp add: eventually_mono topological_tendstoI) 1829 1830lemma continuous_on_of_int_floor: 1831 "continuous_on (UNIV - \<int>::'a::{order_topology, floor_ceiling} set) 1832 (\<lambda>x. of_int (floor x)::'b::{ring_1, topological_space})" 1833 unfolding continuous_on_def 1834 by (auto intro!: tendsto_of_int_floor) 1835 1836lemma continuous_on_of_int_ceiling: 1837 "continuous_on (UNIV - \<int>::'a::{order_topology, floor_ceiling} set) 1838 (\<lambda>x. of_int (ceiling x)::'b::{ring_1, topological_space})" 1839 unfolding continuous_on_def 1840 by (auto intro!: tendsto_of_int_ceiling) 1841 1842 1843subsection \<open>Limits of Sequences\<close> 1844 1845lemma [trans]: "X = Y \<Longrightarrow> Y \<longlonglongrightarrow> z \<Longrightarrow> X \<longlonglongrightarrow> z" 1846 by simp 1847 1848lemma LIMSEQ_iff: 1849 fixes L :: "'a::real_normed_vector" 1850 shows "(X \<longlonglongrightarrow> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)" 1851unfolding lim_sequentially dist_norm .. 1852 1853lemma LIMSEQ_I: "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X \<longlonglongrightarrow> L" 1854 for L :: "'a::real_normed_vector" 1855 by (simp add: LIMSEQ_iff) 1856 1857lemma LIMSEQ_D: "X \<longlonglongrightarrow> L \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r" 1858 for L :: "'a::real_normed_vector" 1859 by (simp add: LIMSEQ_iff) 1860 1861lemma LIMSEQ_linear: "X \<longlonglongrightarrow> x \<Longrightarrow> l > 0 \<Longrightarrow> (\<lambda> n. X (n * l)) \<longlonglongrightarrow> x" 1862 unfolding tendsto_def eventually_sequentially 1863 by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute) 1864 1865 1866text \<open>Transformation of limit.\<close> 1867 1868lemma Lim_transform: "(g \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x - g x) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> a) F" 1869 for a b :: "'a::real_normed_vector" 1870 using tendsto_add [of g a F "\<lambda>x. f x - g x" 0] by simp 1871 1872lemma Lim_transform2: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x - g x) \<longlongrightarrow> 0) F \<Longrightarrow> (g \<longlongrightarrow> a) F" 1873 for a b :: "'a::real_normed_vector" 1874 by (erule Lim_transform) (simp add: tendsto_minus_cancel) 1875 1876proposition Lim_transform_eq: "((\<lambda>x. f x - g x) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> a) F \<longleftrightarrow> (g \<longlongrightarrow> a) F" 1877 for a :: "'a::real_normed_vector" 1878 using Lim_transform Lim_transform2 by blast 1879 1880lemma Lim_transform_eventually: 1881 "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> (g \<longlongrightarrow> l) net" 1882 using eventually_elim2 by (fastforce simp add: tendsto_def) 1883 1884lemma Lim_transform_within: 1885 assumes "(f \<longlongrightarrow> l) (at x within S)" 1886 and "0 < d" 1887 and "\<And>x'. x'\<in>S \<Longrightarrow> 0 < dist x' x \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'" 1888 shows "(g \<longlongrightarrow> l) (at x within S)" 1889proof (rule Lim_transform_eventually) 1890 show "eventually (\<lambda>x. f x = g x) (at x within S)" 1891 using assms by (auto simp: eventually_at) 1892 show "(f \<longlongrightarrow> l) (at x within S)" 1893 by fact 1894qed 1895 1896lemma filterlim_transform_within: 1897 assumes "filterlim g G (at x within S)" 1898 assumes "G \<le> F" "0<d" "(\<And>x'. x' \<in> S \<Longrightarrow> 0 < dist x' x \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') " 1899 shows "filterlim f F (at x within S)" 1900 using assms 1901 apply (elim filterlim_mono_eventually) 1902 unfolding eventually_at by auto 1903 1904text \<open>Common case assuming being away from some crucial point like 0.\<close> 1905lemma Lim_transform_away_within: 1906 fixes a b :: "'a::t1_space" 1907 assumes "a \<noteq> b" 1908 and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x" 1909 and "(f \<longlongrightarrow> l) (at a within S)" 1910 shows "(g \<longlongrightarrow> l) (at a within S)" 1911proof (rule Lim_transform_eventually) 1912 show "(f \<longlongrightarrow> l) (at a within S)" 1913 by fact 1914 show "eventually (\<lambda>x. f x = g x) (at a within S)" 1915 unfolding eventually_at_topological 1916 by (rule exI [where x="- {b}"]) (simp add: open_Compl assms) 1917qed 1918 1919lemma Lim_transform_away_at: 1920 fixes a b :: "'a::t1_space" 1921 assumes ab: "a \<noteq> b" 1922 and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x" 1923 and fl: "(f \<longlongrightarrow> l) (at a)" 1924 shows "(g \<longlongrightarrow> l) (at a)" 1925 using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp 1926 1927text \<open>Alternatively, within an open set.\<close> 1928lemma Lim_transform_within_open: 1929 assumes "(f \<longlongrightarrow> l) (at a within T)" 1930 and "open s" and "a \<in> s" 1931 and "\<And>x. x\<in>s \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x = g x" 1932 shows "(g \<longlongrightarrow> l) (at a within T)" 1933proof (rule Lim_transform_eventually) 1934 show "eventually (\<lambda>x. f x = g x) (at a within T)" 1935 unfolding eventually_at_topological 1936 using assms by auto 1937 show "(f \<longlongrightarrow> l) (at a within T)" by fact 1938qed 1939 1940 1941text \<open>A congruence rule allowing us to transform limits assuming not at point.\<close> 1942 1943(* FIXME: Only one congruence rule for tendsto can be used at a time! *) 1944 1945lemma Lim_cong_within(*[cong add]*): 1946 assumes "a = b" 1947 and "x = y" 1948 and "S = T" 1949 and "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x" 1950 shows "(f \<longlongrightarrow> x) (at a within S) \<longleftrightarrow> (g \<longlongrightarrow> y) (at b within T)" 1951 unfolding tendsto_def eventually_at_topological 1952 using assms by simp 1953 1954lemma Lim_cong_at(*[cong add]*): 1955 assumes "a = b" "x = y" 1956 and "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x" 1957 shows "((\<lambda>x. f x) \<longlongrightarrow> x) (at a) \<longleftrightarrow> ((g \<longlongrightarrow> y) (at a))" 1958 unfolding tendsto_def eventually_at_topological 1959 using assms by simp 1960 1961text \<open>An unbounded sequence's inverse tends to 0.\<close> 1962lemma LIMSEQ_inverse_zero: 1963 assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n" 1964 shows "(\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0" 1965 apply (rule filterlim_compose[OF tendsto_inverse_0]) 1966 by (metis assms eventually_at_top_linorderI filterlim_at_top_dense filterlim_at_top_imp_at_infinity) 1967 1968text \<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\<close> 1969lemma LIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow> 0" 1970 by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc 1971 filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity) 1972 1973text \<open> 1974 The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to 1975 infinity is now easily proved. 1976\<close> 1977 1978lemma LIMSEQ_inverse_real_of_nat_add: "(\<lambda>n. r + inverse (real (Suc n))) \<longlonglongrightarrow> r" 1979 using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto 1980 1981lemma LIMSEQ_inverse_real_of_nat_add_minus: "(\<lambda>n. r + -inverse (real (Suc n))) \<longlonglongrightarrow> r" 1982 using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] 1983 by auto 1984 1985lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: "(\<lambda>n. r * (1 + - inverse (real (Suc n)))) \<longlonglongrightarrow> r" 1986 using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]] 1987 by auto 1988 1989lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially" 1990 using lim_1_over_n by (simp add: inverse_eq_divide) 1991 1992lemma lim_inverse_n': "((\<lambda>n. 1 / n) \<longlongrightarrow> 0) sequentially" 1993 using lim_inverse_n 1994 by (simp add: inverse_eq_divide) 1995 1996lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1" 1997proof (rule Lim_transform_eventually) 1998 show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially" 1999 using eventually_gt_at_top[of "0::nat"] 2000 by eventually_elim (simp add: field_simps) 2001 have "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) \<longlonglongrightarrow> 1 + 0" 2002 by (intro tendsto_add tendsto_const lim_inverse_n) 2003 then show "(\<lambda>n. 1 + inverse (of_nat n) :: 'a) \<longlonglongrightarrow> 1" 2004 by simp 2005qed 2006 2007lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \<longlonglongrightarrow> 1" 2008proof (rule Lim_transform_eventually) 2009 show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) = 2010 of_nat n / of_nat (Suc n)) sequentially" 2011 using eventually_gt_at_top[of "0::nat"] 2012 by eventually_elim (simp add: field_simps del: of_nat_Suc) 2013 have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \<longlonglongrightarrow> inverse 1" 2014 by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all 2015 then show "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \<longlonglongrightarrow> 1" 2016 by simp 2017qed 2018 2019 2020subsection \<open>Convergence on sequences\<close> 2021 2022lemma convergent_cong: 2023 assumes "eventually (\<lambda>x. f x = g x) sequentially" 2024 shows "convergent f \<longleftrightarrow> convergent g" 2025 unfolding convergent_def 2026 by (subst filterlim_cong[OF refl refl assms]) (rule refl) 2027 2028lemma convergent_Suc_iff: "convergent (\<lambda>n. f (Suc n)) \<longleftrightarrow> convergent f" 2029 by (auto simp: convergent_def LIMSEQ_Suc_iff) 2030 2031lemma convergent_ignore_initial_segment: "convergent (\<lambda>n. f (n + m)) = convergent f" 2032proof (induct m arbitrary: f) 2033 case 0 2034 then show ?case by simp 2035next 2036 case (Suc m) 2037 have "convergent (\<lambda>n. f (n + Suc m)) \<longleftrightarrow> convergent (\<lambda>n. f (Suc n + m))" 2038 by simp 2039 also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. f (n + m))" 2040 by (rule convergent_Suc_iff) 2041 also have "\<dots> \<longleftrightarrow> convergent f" 2042 by (rule Suc) 2043 finally show ?case . 2044qed 2045 2046lemma convergent_add: 2047 fixes X Y :: "nat \<Rightarrow> 'a::topological_monoid_add" 2048 assumes "convergent (\<lambda>n. X n)" 2049 and "convergent (\<lambda>n. Y n)" 2050 shows "convergent (\<lambda>n. X n + Y n)" 2051 using assms unfolding convergent_def by (blast intro: tendsto_add) 2052 2053lemma convergent_sum: 2054 fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::topological_comm_monoid_add" 2055 shows "(\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)) \<Longrightarrow> convergent (\<lambda>n. \<Sum>i\<in>A. X i n)" 2056 by (induct A rule: infinite_finite_induct) (simp_all add: convergent_const convergent_add) 2057 2058lemma (in bounded_linear) convergent: 2059 assumes "convergent (\<lambda>n. X n)" 2060 shows "convergent (\<lambda>n. f (X n))" 2061 using assms unfolding convergent_def by (blast intro: tendsto) 2062 2063lemma (in bounded_bilinear) convergent: 2064 assumes "convergent (\<lambda>n. X n)" 2065 and "convergent (\<lambda>n. Y n)" 2066 shows "convergent (\<lambda>n. X n ** Y n)" 2067 using assms unfolding convergent_def by (blast intro: tendsto) 2068 2069lemma convergent_minus_iff: 2070 fixes X :: "nat \<Rightarrow> 'a::topological_group_add" 2071 shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)" 2072 unfolding convergent_def by (force dest: tendsto_minus) 2073 2074lemma convergent_diff: 2075 fixes X Y :: "nat \<Rightarrow> 'a::topological_group_add" 2076 assumes "convergent (\<lambda>n. X n)" 2077 assumes "convergent (\<lambda>n. Y n)" 2078 shows "convergent (\<lambda>n. X n - Y n)" 2079 using assms unfolding convergent_def by (blast intro: tendsto_diff) 2080 2081lemma convergent_norm: 2082 assumes "convergent f" 2083 shows "convergent (\<lambda>n. norm (f n))" 2084proof - 2085 from assms have "f \<longlonglongrightarrow> lim f" 2086 by (simp add: convergent_LIMSEQ_iff) 2087 then have "(\<lambda>n. norm (f n)) \<longlonglongrightarrow> norm (lim f)" 2088 by (rule tendsto_norm) 2089 then show ?thesis 2090 by (auto simp: convergent_def) 2091qed 2092 2093lemma convergent_of_real: 2094 "convergent f \<Longrightarrow> convergent (\<lambda>n. of_real (f n) :: 'a::real_normed_algebra_1)" 2095 unfolding convergent_def by (blast intro!: tendsto_of_real) 2096 2097lemma convergent_add_const_iff: 2098 "convergent (\<lambda>n. c + f n :: 'a::topological_ab_group_add) \<longleftrightarrow> convergent f" 2099proof 2100 assume "convergent (\<lambda>n. c + f n)" 2101 from convergent_diff[OF this convergent_const[of c]] show "convergent f" 2102 by simp 2103next 2104 assume "convergent f" 2105 from convergent_add[OF convergent_const[of c] this] show "convergent (\<lambda>n. c + f n)" 2106 by simp 2107qed 2108 2109lemma convergent_add_const_right_iff: 2110 "convergent (\<lambda>n. f n + c :: 'a::topological_ab_group_add) \<longleftrightarrow> convergent f" 2111 using convergent_add_const_iff[of c f] by (simp add: add_ac) 2112 2113lemma convergent_diff_const_right_iff: 2114 "convergent (\<lambda>n. f n - c :: 'a::topological_ab_group_add) \<longleftrightarrow> convergent f" 2115 using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac) 2116 2117lemma convergent_mult: 2118 fixes X Y :: "nat \<Rightarrow> 'a::topological_semigroup_mult" 2119 assumes "convergent (\<lambda>n. X n)" 2120 and "convergent (\<lambda>n. Y n)" 2121 shows "convergent (\<lambda>n. X n * Y n)" 2122 using assms unfolding convergent_def by (blast intro: tendsto_mult) 2123 2124lemma convergent_mult_const_iff: 2125 assumes "c \<noteq> 0" 2126 shows "convergent (\<lambda>n. c * f n :: 'a::{field,topological_semigroup_mult}) \<longleftrightarrow> convergent f" 2127proof 2128 assume "convergent (\<lambda>n. c * f n)" 2129 from assms convergent_mult[OF this convergent_const[of "inverse c"]] 2130 show "convergent f" by (simp add: field_simps) 2131next 2132 assume "convergent f" 2133 from convergent_mult[OF convergent_const[of c] this] show "convergent (\<lambda>n. c * f n)" 2134 by simp 2135qed 2136 2137lemma convergent_mult_const_right_iff: 2138 fixes c :: "'a::{field,topological_semigroup_mult}" 2139 assumes "c \<noteq> 0" 2140 shows "convergent (\<lambda>n. f n * c) \<longleftrightarrow> convergent f" 2141 using convergent_mult_const_iff[OF assms, of f] by (simp add: mult_ac) 2142 2143lemma convergent_imp_Bseq: "convergent f \<Longrightarrow> Bseq f" 2144 by (simp add: Cauchy_Bseq convergent_Cauchy) 2145 2146 2147text \<open>A monotone sequence converges to its least upper bound.\<close> 2148 2149lemma LIMSEQ_incseq_SUP: 2150 fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder,linorder_topology}" 2151 assumes u: "bdd_above (range X)" 2152 and X: "incseq X" 2153 shows "X \<longlonglongrightarrow> (SUP i. X i)" 2154 by (rule order_tendstoI) 2155 (auto simp: eventually_sequentially u less_cSUP_iff 2156 intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u]) 2157 2158lemma LIMSEQ_decseq_INF: 2159 fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}" 2160 assumes u: "bdd_below (range X)" 2161 and X: "decseq X" 2162 shows "X \<longlonglongrightarrow> (INF i. X i)" 2163 by (rule order_tendstoI) 2164 (auto simp: eventually_sequentially u cINF_less_iff 2165 intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u]) 2166 2167text \<open>Main monotonicity theorem.\<close> 2168 2169lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent X" 2170 for X :: "nat \<Rightarrow> real" 2171 by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP 2172 dest: Bseq_bdd_above Bseq_bdd_below) 2173 2174lemma Bseq_mono_convergent: "Bseq X \<Longrightarrow> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n) \<Longrightarrow> convergent X" 2175 for X :: "nat \<Rightarrow> real" 2176 by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def) 2177 2178lemma monoseq_imp_convergent_iff_Bseq: "monoseq f \<Longrightarrow> convergent f \<longleftrightarrow> Bseq f" 2179 for f :: "nat \<Rightarrow> real" 2180 using Bseq_monoseq_convergent[of f] convergent_imp_Bseq[of f] by blast 2181 2182lemma Bseq_monoseq_convergent'_inc: 2183 fixes f :: "nat \<Rightarrow> real" 2184 shows "Bseq (\<lambda>n. f (n + M)) \<Longrightarrow> (\<And>m n. M \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m \<le> f n) \<Longrightarrow> convergent f" 2185 by (subst convergent_ignore_initial_segment [symmetric, of _ M]) 2186 (auto intro!: Bseq_monoseq_convergent simp: monoseq_def) 2187 2188lemma Bseq_monoseq_convergent'_dec: 2189 fixes f :: "nat \<Rightarrow> real" 2190 shows "Bseq (\<lambda>n. f (n + M)) \<Longrightarrow> (\<And>m n. M \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m \<ge> f n) \<Longrightarrow> convergent f" 2191 by (subst convergent_ignore_initial_segment [symmetric, of _ M]) 2192 (auto intro!: Bseq_monoseq_convergent simp: monoseq_def) 2193 2194lemma Cauchy_iff: "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)" 2195 for X :: "nat \<Rightarrow> 'a::real_normed_vector" 2196 unfolding Cauchy_def dist_norm .. 2197 2198lemma CauchyI: "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X" 2199 for X :: "nat \<Rightarrow> 'a::real_normed_vector" 2200 by (simp add: Cauchy_iff) 2201 2202lemma CauchyD: "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e" 2203 for X :: "nat \<Rightarrow> 'a::real_normed_vector" 2204 by (simp add: Cauchy_iff) 2205 2206lemma incseq_convergent: 2207 fixes X :: "nat \<Rightarrow> real" 2208 assumes "incseq X" 2209 and "\<forall>i. X i \<le> B" 2210 obtains L where "X \<longlonglongrightarrow> L" "\<forall>i. X i \<le> L" 2211proof atomize_elim 2212 from incseq_bounded[OF assms] \<open>incseq X\<close> Bseq_monoseq_convergent[of X] 2213 obtain L where "X \<longlonglongrightarrow> L" 2214 by (auto simp: convergent_def monoseq_def incseq_def) 2215 with \<open>incseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. X i \<le> L)" 2216 by (auto intro!: exI[of _ L] incseq_le) 2217qed 2218 2219lemma decseq_convergent: 2220 fixes X :: "nat \<Rightarrow> real" 2221 assumes "decseq X" 2222 and "\<forall>i. B \<le> X i" 2223 obtains L where "X \<longlonglongrightarrow> L" "\<forall>i. L \<le> X i" 2224proof atomize_elim 2225 from decseq_bounded[OF assms] \<open>decseq X\<close> Bseq_monoseq_convergent[of X] 2226 obtain L where "X \<longlonglongrightarrow> L" 2227 by (auto simp: convergent_def monoseq_def decseq_def) 2228 with \<open>decseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. L \<le> X i)" 2229 by (auto intro!: exI[of _ L] decseq_ge) 2230qed 2231 2232 2233subsection \<open>Power Sequences\<close> 2234 2235lemma Bseq_realpow: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> Bseq (\<lambda>n. x ^ n)" 2236 for x :: real 2237 by (metis decseq_bounded decseq_def power_decreasing zero_le_power) 2238 2239lemma monoseq_realpow: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> monoseq (\<lambda>n. x ^ n)" 2240 for x :: real 2241 using monoseq_def power_decreasing by blast 2242 2243lemma convergent_realpow: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> convergent (\<lambda>n. x ^ n)" 2244 for x :: real 2245 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) 2246 2247lemma LIMSEQ_inverse_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) \<longlonglongrightarrow> 0" 2248 for x :: real 2249 by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp 2250 2251lemma LIMSEQ_realpow_zero: 2252 fixes x :: real 2253 assumes "0 \<le> x" "x < 1" 2254 shows "(\<lambda>n. x ^ n) \<longlonglongrightarrow> 0" 2255proof (cases "x = 0") 2256 case False 2257 with \<open>0 \<le> x\<close> have x0: "0 < x" by simp 2258 then have "1 < inverse x" 2259 using \<open>x < 1\<close> by (rule one_less_inverse) 2260 then have "(\<lambda>n. inverse (inverse x ^ n)) \<longlonglongrightarrow> 0" 2261 by (rule LIMSEQ_inverse_realpow_zero) 2262 then show ?thesis by (simp add: power_inverse) 2263next 2264 case True 2265 show ?thesis 2266 by (rule LIMSEQ_imp_Suc) (simp add: True) 2267qed 2268 2269lemma LIMSEQ_power_zero: "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0" 2270 for x :: "'a::real_normed_algebra_1" 2271 apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) 2272 by (simp add: Zfun_le norm_power_ineq tendsto_Zfun_iff) 2273 2274lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) \<longlonglongrightarrow> 0" 2275 by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp 2276 2277lemma 2278 tendsto_power_zero: 2279 fixes x::"'a::real_normed_algebra_1" 2280 assumes "filterlim f at_top F" 2281 assumes "norm x < 1" 2282 shows "((\<lambda>y. x ^ (f y)) \<longlongrightarrow> 0) F" 2283proof (rule tendstoI) 2284 fix e::real assume "0 < e" 2285 from tendstoD[OF LIMSEQ_power_zero[OF \<open>norm x < 1\<close>] \<open>0 < e\<close>] 2286 have "\<forall>\<^sub>F xa in sequentially. norm (x ^ xa) < e" 2287 by simp 2288 then obtain N where N: "norm (x ^ n) < e" if "n \<ge> N" for n 2289 by (auto simp: eventually_sequentially) 2290 have "\<forall>\<^sub>F i in F. f i \<ge> N" 2291 using \<open>filterlim f sequentially F\<close> 2292 by (simp add: filterlim_at_top) 2293 then show "\<forall>\<^sub>F i in F. dist (x ^ f i) 0 < e" 2294 by eventually_elim (auto simp: N) 2295qed 2296 2297text \<open>Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}.\<close> 2298 2299lemma LIMSEQ_abs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) \<longlonglongrightarrow> 0" 2300 by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) 2301 2302lemma LIMSEQ_abs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) \<longlonglongrightarrow> 0" 2303 by (rule LIMSEQ_power_zero) simp 2304 2305 2306subsection \<open>Limits of Functions\<close> 2307 2308lemma LIM_eq: "f \<midarrow>a\<rightarrow> L = (\<forall>r>0. \<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r)" 2309 for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" 2310 by (simp add: LIM_def dist_norm) 2311 2312lemma LIM_I: 2313 "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r) \<Longrightarrow> f \<midarrow>a\<rightarrow> L" 2314 for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" 2315 by (simp add: LIM_eq) 2316 2317lemma LIM_D: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> 0 < r \<Longrightarrow> \<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r" 2318 for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" 2319 by (simp add: LIM_eq) 2320 2321lemma LIM_offset: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. f (x + k)) \<midarrow>(a - k)\<rightarrow> L" 2322 for a :: "'a::real_normed_vector" 2323 by (simp add: filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap) 2324 2325lemma LIM_offset_zero: "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L" 2326 for a :: "'a::real_normed_vector" 2327 by (drule LIM_offset [where k = a]) (simp add: add.commute) 2328 2329lemma LIM_offset_zero_cancel: "(\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L \<Longrightarrow> f \<midarrow>a\<rightarrow> L" 2330 for a :: "'a::real_normed_vector" 2331 by (drule LIM_offset [where k = "- a"]) simp 2332 2333lemma LIM_offset_zero_iff: "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L" 2334 for f :: "'a :: real_normed_vector \<Rightarrow> _" 2335 using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto 2336 2337lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F" 2338 for f :: "'a \<Rightarrow> 'b::real_normed_vector" 2339 unfolding tendsto_iff dist_norm by simp 2340 2341lemma LIM_zero_cancel: 2342 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" 2343 shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F" 2344unfolding tendsto_iff dist_norm by simp 2345 2346lemma LIM_zero_iff: "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F = (f \<longlongrightarrow> l) F" 2347 for f :: "'a \<Rightarrow> 'b::real_normed_vector" 2348 unfolding tendsto_iff dist_norm by simp 2349 2350lemma LIM_imp_LIM: 2351 fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" 2352 fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector" 2353 assumes f: "f \<midarrow>a\<rightarrow> l" 2354 and le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)" 2355 shows "g \<midarrow>a\<rightarrow> m" 2356 by (rule metric_LIM_imp_LIM [OF f]) (simp add: dist_norm le) 2357 2358lemma LIM_equal2: 2359 fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space" 2360 assumes "0 < R" 2361 and "\<And>x. x \<noteq> a \<Longrightarrow> norm (x - a) < R \<Longrightarrow> f x = g x" 2362 shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>a\<rightarrow> l" 2363 by (rule metric_LIM_equal2 [OF _ assms]) (simp_all add: dist_norm) 2364 2365lemma LIM_compose2: 2366 fixes a :: "'a::real_normed_vector" 2367 assumes f: "f \<midarrow>a\<rightarrow> b" 2368 and g: "g \<midarrow>b\<rightarrow> c" 2369 and inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b" 2370 shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c" 2371 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) 2372 2373lemma real_LIM_sandwich_zero: 2374 fixes f g :: "'a::topological_space \<Rightarrow> real" 2375 assumes f: "f \<midarrow>a\<rightarrow> 0" 2376 and 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x" 2377 and 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x" 2378 shows "g \<midarrow>a\<rightarrow> 0" 2379proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) 2380 fix x 2381 assume x: "x \<noteq> a" 2382 with 1 have "norm (g x - 0) = g x" by simp 2383 also have "g x \<le> f x" by (rule 2 [OF x]) 2384 also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self) 2385 also have "\<bar>f x\<bar> = norm (f x - 0)" by simp 2386 finally show "norm (g x - 0) \<le> norm (f x - 0)" . 2387qed 2388 2389 2390subsection \<open>Continuity\<close> 2391 2392lemma LIM_isCont_iff: "(f \<midarrow>a\<rightarrow> f a) = ((\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> f a)" 2393 for f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space" 2394 by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) 2395 2396lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h)) \<midarrow>0\<rightarrow> f x" 2397 for f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space" 2398 by (simp add: isCont_def LIM_isCont_iff) 2399 2400lemma isCont_LIM_compose2: 2401 fixes a :: "'a::real_normed_vector" 2402 assumes f [unfolded isCont_def]: "isCont f a" 2403 and g: "g \<midarrow>f a\<rightarrow> l" 2404 and inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a" 2405 shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> l" 2406 by (rule LIM_compose2 [OF f g inj]) 2407 2408lemma isCont_norm [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a" 2409 for f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 2410 by (fact continuous_norm) 2411 2412lemma isCont_rabs [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a" 2413 for f :: "'a::t2_space \<Rightarrow> real" 2414 by (fact continuous_rabs) 2415 2416lemma isCont_add [simp]: "isCont f a \<Longrightarrow> isCont g a \<Longrightarrow> isCont (\<lambda>x. f x + g x) a" 2417 for f :: "'a::t2_space \<Rightarrow> 'b::topological_monoid_add" 2418 by (fact continuous_add) 2419 2420lemma isCont_minus [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a" 2421 for f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 2422 by (fact continuous_minus) 2423 2424lemma isCont_diff [simp]: "isCont f a \<Longrightarrow> isCont g a \<Longrightarrow> isCont (\<lambda>x. f x - g x) a" 2425 for f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 2426 by (fact continuous_diff) 2427 2428lemma isCont_mult [simp]: "isCont f a \<Longrightarrow> isCont g a \<Longrightarrow> isCont (\<lambda>x. f x * g x) a" 2429 for f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra" 2430 by (fact continuous_mult) 2431 2432lemma (in bounded_linear) isCont: "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a" 2433 by (fact continuous) 2434 2435lemma (in bounded_bilinear) isCont: "isCont f a \<Longrightarrow> isCont g a \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a" 2436 by (fact continuous) 2437 2438lemmas isCont_scaleR [simp] = 2439 bounded_bilinear.isCont [OF bounded_bilinear_scaleR] 2440 2441lemmas isCont_of_real [simp] = 2442 bounded_linear.isCont [OF bounded_linear_of_real] 2443 2444lemma isCont_power [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a" 2445 for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}" 2446 by (fact continuous_power) 2447 2448lemma isCont_sum [simp]: "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a" 2449 for f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add" 2450 by (auto intro: continuous_sum) 2451 2452 2453subsection \<open>Uniform Continuity\<close> 2454 2455lemma uniformly_continuous_on_def: 2456 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" 2457 shows "uniformly_continuous_on s f \<longleftrightarrow> 2458 (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)" 2459 unfolding uniformly_continuous_on_uniformity 2460 uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal 2461 by (force simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric) 2462 2463abbreviation isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" 2464 where "isUCont f \<equiv> uniformly_continuous_on UNIV f" 2465 2466lemma isUCont_def: "isUCont f \<longleftrightarrow> (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)" 2467 by (auto simp: uniformly_continuous_on_def dist_commute) 2468 2469lemma isUCont_isCont: "isUCont f \<Longrightarrow> isCont f x" 2470 by (drule uniformly_continuous_imp_continuous) (simp add: continuous_on_eq_continuous_at) 2471 2472lemma uniformly_continuous_on_Cauchy: 2473 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" 2474 assumes "uniformly_continuous_on S f" "Cauchy X" "\<And>n. X n \<in> S" 2475 shows "Cauchy (\<lambda>n. f (X n))" 2476 using assms 2477 unfolding uniformly_continuous_on_def by (meson Cauchy_def) 2478 2479lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" 2480 by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all 2481 2482lemma uniformly_continuous_imp_Cauchy_continuous: 2483 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" 2484 shows "\<lbrakk>uniformly_continuous_on S f; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)" 2485 by (simp add: uniformly_continuous_on_def Cauchy_def) meson 2486 2487lemma (in bounded_linear) isUCont: "isUCont f" 2488 unfolding isUCont_def dist_norm 2489proof (intro allI impI) 2490 fix r :: real 2491 assume r: "0 < r" 2492 obtain K where K: "0 < K" and norm_le: "norm (f x) \<le> norm x * K" for x 2493 using pos_bounded by blast 2494 show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r" 2495 proof (rule exI, safe) 2496 from r K show "0 < r / K" by simp 2497 next 2498 fix x y :: 'a 2499 assume xy: "norm (x - y) < r / K" 2500 have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff) 2501 also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le) 2502 also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq) 2503 finally show "norm (f x - f y) < r" . 2504 qed 2505qed 2506 2507lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))" 2508 by (rule isUCont [THEN isUCont_Cauchy]) 2509 2510lemma LIM_less_bound: 2511 fixes f :: "real \<Rightarrow> real" 2512 assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x" 2513 shows "0 \<le> f x" 2514proof (rule tendsto_lowerbound) 2515 show "(f \<longlongrightarrow> f x) (at_left x)" 2516 using \<open>isCont f x\<close> by (simp add: filterlim_at_split isCont_def) 2517 show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)" 2518 using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"]) 2519qed simp 2520 2521 2522subsection \<open>Nested Intervals and Bisection -- Needed for Compactness\<close> 2523 2524lemma nested_sequence_unique: 2525 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) \<longlonglongrightarrow> 0" 2526 shows "\<exists>l::real. ((\<forall>n. f n \<le> l) \<and> f \<longlonglongrightarrow> l) \<and> ((\<forall>n. l \<le> g n) \<and> g \<longlonglongrightarrow> l)" 2527proof - 2528 have "incseq f" unfolding incseq_Suc_iff by fact 2529 have "decseq g" unfolding decseq_Suc_iff by fact 2530 have "f n \<le> g 0" for n 2531 proof - 2532 from \<open>decseq g\<close> have "g n \<le> g 0" 2533 by (rule decseqD) simp 2534 with \<open>\<forall>n. f n \<le> g n\<close>[THEN spec, of n] show ?thesis 2535 by auto 2536 qed 2537 then obtain u where "f \<longlonglongrightarrow> u" "\<forall>i. f i \<le> u" 2538 using incseq_convergent[OF \<open>incseq f\<close>] by auto 2539 moreover have "f 0 \<le> g n" for n 2540 proof - 2541 from \<open>incseq f\<close> have "f 0 \<le> f n" by (rule incseqD) simp 2542 with \<open>\<forall>n. f n \<le> g n\<close>[THEN spec, of n] show ?thesis 2543 by simp 2544 qed 2545 then obtain l where "g \<longlonglongrightarrow> l" "\<forall>i. l \<le> g i" 2546 using decseq_convergent[OF \<open>decseq g\<close>] by auto 2547 moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF \<open>f \<longlonglongrightarrow> u\<close> \<open>g \<longlonglongrightarrow> l\<close>]] 2548 ultimately show ?thesis by auto 2549qed 2550 2551lemma Bolzano[consumes 1, case_names trans local]: 2552 fixes P :: "real \<Rightarrow> real \<Rightarrow> bool" 2553 assumes [arith]: "a \<le> b" 2554 and trans: "\<And>a b c. P a b \<Longrightarrow> P b c \<Longrightarrow> a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> P a c" 2555 and local: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<exists>d>0. \<forall>a b. a \<le> x \<and> x \<le> b \<and> b - a < d \<longrightarrow> P a b" 2556 shows "P a b" 2557proof - 2558 define bisect where "bisect = 2559 rec_nat (a, b) (\<lambda>n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))" 2560 define l u where "l n = fst (bisect n)" and "u n = snd (bisect n)" for n 2561 have l[simp]: "l 0 = a" "\<And>n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)" 2562 and u[simp]: "u 0 = b" "\<And>n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)" 2563 by (simp_all add: l_def u_def bisect_def split: prod.split) 2564 2565 have [simp]: "l n \<le> u n" for n by (induct n) auto 2566 2567 have "\<exists>x. ((\<forall>n. l n \<le> x) \<and> l \<longlonglongrightarrow> x) \<and> ((\<forall>n. x \<le> u n) \<and> u \<longlonglongrightarrow> x)" 2568 proof (safe intro!: nested_sequence_unique) 2569 show "l n \<le> l (Suc n)" "u (Suc n) \<le> u n" for n 2570 by (induct n) auto 2571 next 2572 have "l n - u n = (a - b) / 2^n" for n 2573 by (induct n) (auto simp: field_simps) 2574 then show "(\<lambda>n. l n - u n) \<longlonglongrightarrow> 0" 2575 by (simp add: LIMSEQ_divide_realpow_zero) 2576 qed fact 2577 then obtain x where x: "\<And>n. l n \<le> x" "\<And>n. x \<le> u n" and "l \<longlonglongrightarrow> x" "u \<longlonglongrightarrow> x" 2578 by auto 2579 obtain d where "0 < d" and d: "a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> b - a < d \<Longrightarrow> P a b" for a b 2580 using \<open>l 0 \<le> x\<close> \<open>x \<le> u 0\<close> local[of x] by auto 2581 2582 show "P a b" 2583 proof (rule ccontr) 2584 assume "\<not> P a b" 2585 have "\<not> P (l n) (u n)" for n 2586 proof (induct n) 2587 case 0 2588 then show ?case 2589 by (simp add: \<open>\<not> P a b\<close>) 2590 next 2591 case (Suc n) 2592 with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case 2593 by auto 2594 qed 2595 moreover 2596 { 2597 have "eventually (\<lambda>n. x - d / 2 < l n) sequentially" 2598 using \<open>0 < d\<close> \<open>l \<longlonglongrightarrow> x\<close> by (intro order_tendstoD[of _ x]) auto 2599 moreover have "eventually (\<lambda>n. u n < x + d / 2) sequentially" 2600 using \<open>0 < d\<close> \<open>u \<longlonglongrightarrow> x\<close> by (intro order_tendstoD[of _ x]) auto 2601 ultimately have "eventually (\<lambda>n. P (l n) (u n)) sequentially" 2602 proof eventually_elim 2603 case (elim n) 2604 from add_strict_mono[OF this] have "u n - l n < d" by simp 2605 with x show "P (l n) (u n)" by (rule d) 2606 qed 2607 } 2608 ultimately show False by simp 2609 qed 2610qed 2611 2612lemma compact_Icc[simp, intro]: "compact {a .. b::real}" 2613proof (cases "a \<le> b", rule compactI) 2614 fix C 2615 assume C: "a \<le> b" "\<forall>t\<in>C. open t" "{a..b} \<subseteq> \<Union>C" 2616 define T where "T = {a .. b}" 2617 from C(1,3) show "\<exists>C'\<subseteq>C. finite C' \<and> {a..b} \<subseteq> \<Union>C'" 2618 proof (induct rule: Bolzano) 2619 case (trans a b c) 2620 then have *: "{a..c} = {a..b} \<union> {b..c}" 2621 by auto 2622 with trans obtain C1 C2 2623 where "C1\<subseteq>C" "finite C1" "{a..b} \<subseteq> \<Union>C1" "C2\<subseteq>C" "finite C2" "{b..c} \<subseteq> \<Union>C2" 2624 by auto 2625 with trans show ?case 2626 unfolding * by (intro exI[of _ "C1 \<union> C2"]) auto 2627 next 2628 case (local x) 2629 with C have "x \<in> \<Union>C" by auto 2630 with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" 2631 by auto 2632 then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c" 2633 by (auto simp: open_dist dist_real_def subset_eq Ball_def abs_less_iff) 2634 with \<open>c \<in> C\<close> show ?case 2635 by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto 2636 qed 2637qed simp 2638 2639 2640lemma continuous_image_closed_interval: 2641 fixes a b and f :: "real \<Rightarrow> real" 2642 defines "S \<equiv> {a..b}" 2643 assumes "a \<le> b" and f: "continuous_on S f" 2644 shows "\<exists>c d. f`S = {c..d} \<and> c \<le> d" 2645proof - 2646 have S: "compact S" "S \<noteq> {}" 2647 using \<open>a \<le> b\<close> by (auto simp: S_def) 2648 obtain c where "c \<in> S" "\<forall>d\<in>S. f d \<le> f c" 2649 using continuous_attains_sup[OF S f] by auto 2650 moreover obtain d where "d \<in> S" "\<forall>c\<in>S. f d \<le> f c" 2651 using continuous_attains_inf[OF S f] by auto 2652 moreover have "connected (f`S)" 2653 using connected_continuous_image[OF f] connected_Icc by (auto simp: S_def) 2654 ultimately have "f ` S = {f d .. f c} \<and> f d \<le> f c" 2655 by (auto simp: connected_iff_interval) 2656 then show ?thesis 2657 by auto 2658qed 2659 2660lemma open_Collect_positive: 2661 fixes f :: "'a::topological_space \<Rightarrow> real" 2662 assumes f: "continuous_on s f" 2663 shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. 0 < f x}" 2664 using continuous_on_open_invariant[THEN iffD1, OF f, rule_format, of "{0 <..}"] 2665 by (auto simp: Int_def field_simps) 2666 2667lemma open_Collect_less_Int: 2668 fixes f g :: "'a::topological_space \<Rightarrow> real" 2669 assumes f: "continuous_on s f" 2670 and g: "continuous_on s g" 2671 shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. f x < g x}" 2672 using open_Collect_positive[OF continuous_on_diff[OF g f]] by (simp add: field_simps) 2673 2674 2675subsection \<open>Boundedness of continuous functions\<close> 2676 2677text\<open>By bisection, function continuous on closed interval is bounded above\<close> 2678 2679lemma isCont_eq_Ub: 2680 fixes f :: "real \<Rightarrow> 'a::linorder_topology" 2681 shows "a \<le> b \<Longrightarrow> \<forall>x::real. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> 2682 \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)" 2683 using continuous_attains_sup[of "{a..b}" f] 2684 by (auto simp: continuous_at_imp_continuous_on Ball_def Bex_def) 2685 2686lemma isCont_eq_Lb: 2687 fixes f :: "real \<Rightarrow> 'a::linorder_topology" 2688 shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> 2689 \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> M \<le> f x) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)" 2690 using continuous_attains_inf[of "{a..b}" f] 2691 by (auto simp: continuous_at_imp_continuous_on Ball_def Bex_def) 2692 2693lemma isCont_bounded: 2694 fixes f :: "real \<Rightarrow> 'a::linorder_topology" 2695 shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> \<exists>M. \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" 2696 using isCont_eq_Ub[of a b f] by auto 2697 2698lemma isCont_has_Ub: 2699 fixes f :: "real \<Rightarrow> 'a::linorder_topology" 2700 shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> 2701 \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<forall>N. N < M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x))" 2702 using isCont_eq_Ub[of a b f] by auto 2703 2704(*HOL style here: object-level formulations*) 2705lemma IVT_objl: 2706 "(f a \<le> y \<and> y \<le> f b \<and> a \<le> b \<and> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x)) \<longrightarrow> 2707 (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y)" 2708 for a y :: real 2709 by (blast intro: IVT) 2710 2711lemma IVT2_objl: 2712 "(f b \<le> y \<and> y \<le> f a \<and> a \<le> b \<and> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x)) \<longrightarrow> 2713 (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y)" 2714 for b y :: real 2715 by (blast intro: IVT2) 2716 2717lemma isCont_Lb_Ub: 2718 fixes f :: "real \<Rightarrow> real" 2719 assumes "a \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x" 2720 shows "\<exists>L M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> L \<le> f x \<and> f x \<le> M) \<and> 2721 (\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> (f x = y)))" 2722proof - 2723 obtain M where M: "a \<le> M" "M \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> f M" 2724 using isCont_eq_Ub[OF assms] by auto 2725 obtain L where L: "a \<le> L" "L \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f L \<le> f x" 2726 using isCont_eq_Lb[OF assms] by auto 2727 have "(\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f L \<le> f x \<and> f x \<le> f M)" 2728 using M L by simp 2729 moreover 2730 have "(\<forall>y. f L \<le> y \<and> y \<le> f M \<longrightarrow> (\<exists>x\<ge>a. x \<le> b \<and> f x = y))" 2731 proof (cases "L \<le> M") 2732 case True then show ?thesis 2733 using IVT[of f L _ M] M L assms by (metis order.trans) 2734 next 2735 case False then show ?thesis 2736 using IVT2[of f L _ M] 2737 by (metis L(2) M(1) assms(2) le_cases order.trans) 2738qed 2739 ultimately show ?thesis 2740 by blast 2741qed 2742 2743 2744text \<open>Continuity of inverse function.\<close> 2745 2746lemma isCont_inverse_function: 2747 fixes f g :: "real \<Rightarrow> real" 2748 assumes d: "0 < d" 2749 and inj: "\<And>z. \<bar>z-x\<bar> \<le> d \<Longrightarrow> g (f z) = z" 2750 and cont: "\<And>z. \<bar>z-x\<bar> \<le> d \<Longrightarrow> isCont f z" 2751 shows "isCont g (f x)" 2752proof - 2753 let ?A = "f (x - d)" 2754 let ?B = "f (x + d)" 2755 let ?D = "{x - d..x + d}" 2756 2757 have f: "continuous_on ?D f" 2758 using cont by (intro continuous_at_imp_continuous_on ballI) auto 2759 then have g: "continuous_on (f`?D) g" 2760 using inj by (intro continuous_on_inv) auto 2761 2762 from d f have "{min ?A ?B <..< max ?A ?B} \<subseteq> f ` ?D" 2763 by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max) 2764 with g have "continuous_on {min ?A ?B <..< max ?A ?B} g" 2765 by (rule continuous_on_subset) 2766 moreover 2767 have "(?A < f x \<and> f x < ?B) \<or> (?B < f x \<and> f x < ?A)" 2768 using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto 2769 then have "f x \<in> {min ?A ?B <..< max ?A ?B}" 2770 by auto 2771 ultimately show ?thesis 2772 by (simp add: continuous_on_eq_continuous_at) 2773qed 2774 2775lemma isCont_inverse_function2: 2776 fixes f g :: "real \<Rightarrow> real" 2777 shows 2778 "\<lbrakk>a < x; x < b; 2779 \<And>z. \<lbrakk>a \<le> z; z \<le> b\<rbrakk> \<Longrightarrow> g (f z) = z; 2780 \<And>z. \<lbrakk>a \<le> z; z \<le> b\<rbrakk> \<Longrightarrow> isCont f z\<rbrakk> \<Longrightarrow> isCont g (f x)" 2781 apply (rule isCont_inverse_function [where f=f and d="min (x - a) (b - x)"]) 2782 apply (simp_all add: abs_le_iff) 2783 done 2784 2785text \<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110.\<close> 2786lemma LIM_fun_gt_zero: "f \<midarrow>c\<rightarrow> 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)" 2787 for f :: "real \<Rightarrow> real" 2788 by (force simp: dest: LIM_D) 2789 2790lemma LIM_fun_less_zero: "f \<midarrow>c\<rightarrow> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x < 0)" 2791 for f :: "real \<Rightarrow> real" 2792 by (drule LIM_D [where r="-l"]) force+ 2793 2794lemma LIM_fun_not_zero: "f \<midarrow>c\<rightarrow> l \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x \<noteq> 0)" 2795 for f :: "real \<Rightarrow> real" 2796 using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp: neq_iff) 2797 2798end 2799