src/HOL/Limits.thy
changeset 50331 4b6dc5077e98
parent 50330 d0b12171118e
child 50346 a75c6429c3c3
     1.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:19:11 2012 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:12 2012 +0100
     1.3 @@ -463,6 +463,22 @@
     1.4  lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
     1.5    by (simp add: at_eq_bot_iff not_open_singleton)
     1.6  
     1.7 +lemma trivial_limit_at_left_real [simp]: (* maybe generalize type *)
     1.8 +  "\<not> trivial_limit (at_left (x::real))"
     1.9 +  unfolding trivial_limit_def eventually_within_le
    1.10 +  apply clarsimp
    1.11 +  apply (rule_tac x="x - d/2" in bexI)
    1.12 +  apply (auto simp: dist_real_def)
    1.13 +  done
    1.14 +
    1.15 +lemma trivial_limit_at_right_real [simp]: (* maybe generalize type *)
    1.16 +  "\<not> trivial_limit (at_right (x::real))"
    1.17 +  unfolding trivial_limit_def eventually_within_le
    1.18 +  apply clarsimp
    1.19 +  apply (rule_tac x="x + d/2" in bexI)
    1.20 +  apply (auto simp: dist_real_def)
    1.21 +  done
    1.22 +
    1.23  lemma eventually_at_infinity:
    1.24    "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
    1.25  unfolding at_infinity_def
    1.26 @@ -713,6 +729,9 @@
    1.27    "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
    1.28    unfolding filterlim_def filtermap_sup by auto
    1.29  
    1.30 +lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
    1.31 +  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
    1.32 +
    1.33  abbreviation (in topological_space)
    1.34    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
    1.35    "(f ---> l) F \<equiv> filterlim f (nhds l) F"
    1.36 @@ -1027,6 +1046,30 @@
    1.37      by (simp add: tendsto_const)
    1.38  qed
    1.39  
    1.40 +lemma tendsto_le_const:
    1.41 +  fixes f :: "_ \<Rightarrow> real" 
    1.42 +  assumes F: "\<not> trivial_limit F"
    1.43 +  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
    1.44 +  shows "a \<le> x"
    1.45 +proof (rule ccontr)
    1.46 +  assume "\<not> a \<le> x"
    1.47 +  with x have "eventually (\<lambda>x. f x < a) F"
    1.48 +    by (auto simp add: tendsto_def elim!: allE[of _ "{..< a}"])
    1.49 +  with a have "eventually (\<lambda>x. False) F"
    1.50 +    by eventually_elim auto
    1.51 +  with F show False
    1.52 +    by (simp add: eventually_False)
    1.53 +qed
    1.54 +
    1.55 +lemma tendsto_le:
    1.56 +  fixes f g :: "_ \<Rightarrow> real" 
    1.57 +  assumes F: "\<not> trivial_limit F"
    1.58 +  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
    1.59 +  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
    1.60 +  shows "y \<le> x"
    1.61 +  using tendsto_le_const[OF F tendsto_diff[OF x y], of 0] ev
    1.62 +  by (simp add: sign_simps)
    1.63 +
    1.64  subsubsection {* Inverse and division *}
    1.65  
    1.66  lemma (in bounded_bilinear) Zfun_prod_Bfun:
    1.67 @@ -1382,6 +1425,44 @@
    1.68      by eventually_elim simp
    1.69  qed
    1.70  
    1.71 +lemma tendsto_divide_0:
    1.72 +  fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
    1.73 +  assumes f: "(f ---> c) F"
    1.74 +  assumes g: "LIM x F. g x :> at_infinity"
    1.75 +  shows "((\<lambda>x. f x / g x) ---> 0) F"
    1.76 +  using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse)
    1.77 +
    1.78 +lemma linear_plus_1_le_power:
    1.79 +  fixes x :: real
    1.80 +  assumes x: "0 \<le> x"
    1.81 +  shows "real n * x + 1 \<le> (x + 1) ^ n"
    1.82 +proof (induct n)
    1.83 +  case (Suc n)
    1.84 +  have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
    1.85 +    by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
    1.86 +  also have "\<dots> \<le> (x + 1)^Suc n"
    1.87 +    using Suc x by (simp add: mult_left_mono)
    1.88 +  finally show ?case .
    1.89 +qed simp
    1.90 +
    1.91 +lemma filterlim_realpow_sequentially_gt1:
    1.92 +  fixes x :: "'a :: real_normed_div_algebra"
    1.93 +  assumes x[arith]: "1 < norm x"
    1.94 +  shows "LIM n sequentially. x ^ n :> at_infinity"
    1.95 +proof (intro filterlim_at_infinity[THEN iffD2] allI impI)
    1.96 +  fix y :: real assume "0 < y"
    1.97 +  have "0 < norm x - 1" by simp
    1.98 +  then obtain N::nat where "y < real N * (norm x - 1)" by (blast dest: reals_Archimedean3)
    1.99 +  also have "\<dots> \<le> real N * (norm x - 1) + 1" by simp
   1.100 +  also have "\<dots> \<le> (norm x - 1 + 1) ^ N" by (rule linear_plus_1_le_power) simp
   1.101 +  also have "\<dots> = norm x ^ N" by simp
   1.102 +  finally have "\<forall>n\<ge>N. y \<le> norm x ^ n"
   1.103 +    by (metis order_less_le_trans power_increasing order_less_imp_le x)
   1.104 +  then show "eventually (\<lambda>n. y \<le> norm (x ^ n)) sequentially"
   1.105 +    unfolding eventually_sequentially
   1.106 +    by (auto simp: norm_power)
   1.107 +qed simp
   1.108 +
   1.109  subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
   1.110  
   1.111  text {*