add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
authorhoelzl
Mon Dec 03 18:19:02 2012 +0100 (2012-12-03)
changeset 503240a1242d5e7d4
parent 50323 3764d4620fb3
child 50325 5e40ad9f212a
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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.51      by (simp add: open_Int)
    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.129 +lemma filterlim_tendsto_add_at_top: 
   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.144 +lemma filterlim_at_top_add_at_top: 
   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 +
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 03 18:19:01 2012 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 03 18:19:02 2012 +0100
     2.3 @@ -1102,28 +1102,10 @@
     2.4  subsection {* Filters and the ``eventually true'' quantifier *}
     2.5  
     2.6  definition
     2.7 -  at_infinity :: "'a::real_normed_vector filter" where
     2.8 -  "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
     2.9 -
    2.10 -definition
    2.11    indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
    2.12      (infixr "indirection" 70) where
    2.13    "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
    2.14  
    2.15 -text{* Prove That They are all filters. *}
    2.16 -
    2.17 -lemma eventually_at_infinity:
    2.18 -  "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
    2.19 -unfolding at_infinity_def
    2.20 -proof (rule eventually_Abs_filter, rule is_filter.intro)
    2.21 -  fix P Q :: "'a \<Rightarrow> bool"
    2.22 -  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
    2.23 -  then obtain r s where
    2.24 -    "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
    2.25 -  then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
    2.26 -  then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
    2.27 -qed auto
    2.28 -
    2.29  text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
    2.30  
    2.31  lemma trivial_limit_within: