src/HOL/Limits.thy
 changeset 50324 0a1242d5e7d4 parent 50323 3764d4620fb3 child 50325 5e40ad9f212a
```     1.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:19:01 2012 +0100
1.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:02 2012 +0100
1.3 @@ -285,8 +285,7 @@
1.4  definition at_top :: "('a::order) filter"
1.5    where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
1.6
1.7 -lemma eventually_at_top_linorder:
1.8 -  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_top \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
1.9 +lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"
1.10    unfolding at_top_def
1.11  proof (rule eventually_Abs_filter, rule is_filter.intro)
1.12    fix P Q :: "'a \<Rightarrow> bool"
1.13 @@ -296,13 +295,12 @@
1.14    then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
1.15  qed auto
1.16
1.17 -lemma eventually_at_top_dense:
1.18 -  fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_top \<longleftrightarrow> (\<exists>N. \<forall>n>N. P n)"
1.19 +lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::dense_linorder. \<forall>n>N. P n)"
1.20    unfolding eventually_at_top_linorder
1.21  proof safe
1.22    fix N assume "\<forall>n\<ge>N. P n" then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])
1.23  next
1.24 -  fix N assume "\<forall>n>N. P n"
1.25 +  fix N assume "\<forall>n>N. P n"
1.26    moreover from gt_ex[of N] guess y ..
1.27    ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
1.28  qed
1.29 @@ -375,6 +373,9 @@
1.30  definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
1.31    where "at a = nhds a within - {a}"
1.32
1.33 +definition at_infinity :: "'a::real_normed_vector filter" where
1.34 +  "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
1.35 +
1.36  lemma eventually_within:
1.37    "eventually P (F within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F"
1.38    unfolding within_def
1.39 @@ -401,7 +402,7 @@
1.40  unfolding nhds_def
1.41  proof (rule eventually_Abs_filter, rule is_filter.intro)
1.42    have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
1.43 -  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" by - rule
1.44 +  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" ..
1.45  next
1.46    fix P Q
1.47    assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"
1.48 @@ -411,7 +412,7 @@
1.49      "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto
1.50    hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)"
1.52 -  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" by - rule
1.53 +  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" ..
1.54  qed auto
1.55
1.56  lemma eventually_nhds_metric:
1.57 @@ -445,6 +446,17 @@
1.58  lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
1.59    by (simp add: at_eq_bot_iff not_open_singleton)
1.60
1.61 +lemma eventually_at_infinity:
1.62 +  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
1.63 +unfolding at_infinity_def
1.64 +proof (rule eventually_Abs_filter, rule is_filter.intro)
1.65 +  fix P Q :: "'a \<Rightarrow> bool"
1.66 +  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
1.67 +  then obtain r s where
1.68 +    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
1.69 +  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
1.70 +  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
1.71 +qed auto
1.72
1.73  subsection {* Boundedness *}
1.74
1.75 @@ -1164,4 +1176,85 @@
1.76  lemma filterlim_uminus_at_bot: "LIM x F. f x :> at_top \<Longrightarrow> LIM x F. - (f x) :: real :> at_bot"
1.77    by (rule filterlim_compose[OF filterlim_uminus_at_bot_at_top])
1.78
1.79 +text {*
1.80 +
1.81 +We only show rules for multiplication and addition when the functions are either against a real
1.82 +value or against infinity. Further rules are easy to derive by using @{thm filterlim_uminus_at_top}.
1.83 +
1.84 +*}
1.85 +
1.86 +lemma filterlim_tendsto_pos_mult_at_top:
1.87 +  assumes f: "(f ---> c) F" and c: "0 < c"
1.88 +  assumes g: "LIM x F. g x :> at_top"
1.89 +  shows "LIM x F. (f x * g x :: real) :> at_top"
1.90 +  unfolding filterlim_at_top_gt[where c=0]
1.91 +proof safe
1.92 +  fix Z :: real assume "0 < Z"
1.93 +  from f `0 < c` have "eventually (\<lambda>x. c / 2 < f x) F"
1.94 +    by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1
1.95 +             simp: dist_real_def abs_real_def split: split_if_asm)
1.96 +  moreover from g have "eventually (\<lambda>x. (Z / c * 2) < g x) F"
1.97 +    unfolding filterlim_at_top by auto
1.98 +  ultimately show "eventually (\<lambda>x. Z < f x * g x) F"
1.99 +  proof eventually_elim
1.100 +    fix x assume "c / 2 < f x" "Z / c * 2 < g x"
1.101 +    with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) < f x * g x"
1.102 +      by (intro mult_strict_mono) (auto simp: zero_le_divide_iff)
1.103 +    with `0 < c` show "Z < f x * g x"
1.104 +       by simp
1.105 +  qed
1.106 +qed
1.107 +
1.108 +lemma filterlim_at_top_mult_at_top:
1.109 +  assumes f: "LIM x F. f x :> at_top"
1.110 +  assumes g: "LIM x F. g x :> at_top"
1.111 +  shows "LIM x F. (f x * g x :: real) :> at_top"
1.112 +  unfolding filterlim_at_top_gt[where c=0]
1.113 +proof safe
1.114 +  fix Z :: real assume "0 < Z"
1.115 +  from f have "eventually (\<lambda>x. 1 < f x) F"
1.116 +    unfolding filterlim_at_top by auto
1.117 +  moreover from g have "eventually (\<lambda>x. Z < g x) F"
1.118 +    unfolding filterlim_at_top by auto
1.119 +  ultimately show "eventually (\<lambda>x. Z < f x * g x) F"
1.120 +  proof eventually_elim
1.121 +    fix x assume "1 < f x" "Z < g x"
1.122 +    with `0 < Z` have "1 * Z < f x * g x"
1.123 +      by (intro mult_strict_mono) (auto simp: zero_le_divide_iff)
1.124 +    then show "Z < f x * g x"
1.125 +       by simp
1.126 +  qed
1.127 +qed
1.128 +
1.130 +  assumes f: "(f ---> c) F"
1.131 +  assumes g: "LIM x F. g x :> at_top"
1.132 +  shows "LIM x F. (f x + g x :: real) :> at_top"
1.133 +  unfolding filterlim_at_top_gt[where c=0]
1.134 +proof safe
1.135 +  fix Z :: real assume "0 < Z"
1.136 +  from f have "eventually (\<lambda>x. c - 1 < f x) F"
1.137 +    by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def)
1.138 +  moreover from g have "eventually (\<lambda>x. Z - (c - 1) < g x) F"
1.139 +    unfolding filterlim_at_top by auto
1.140 +  ultimately show "eventually (\<lambda>x. Z < f x + g x) F"
1.141 +    by eventually_elim simp
1.142 +qed
1.143 +
1.145 +  assumes f: "LIM x F. f x :> at_top"
1.146 +  assumes g: "LIM x F. g x :> at_top"
1.147 +  shows "LIM x F. (f x + g x :: real) :> at_top"
1.148 +  unfolding filterlim_at_top_gt[where c=0]
1.149 +proof safe
1.150 +  fix Z :: real assume "0 < Z"
1.151 +  from f have "eventually (\<lambda>x. 0 < f x) F"
1.152 +    unfolding filterlim_at_top by auto
1.153 +  moreover from g have "eventually (\<lambda>x. Z < g x) F"
1.154 +    unfolding filterlim_at_top by auto
1.155 +  ultimately show "eventually (\<lambda>x. Z < f x + g x) F"
1.156 +    by eventually_elim simp
1.157 +qed
1.158 +
1.159  end
1.160 +
```