src/HOL/Lim.thy
 changeset 36661 0a5b7b818d65 parent 32650 34bfa2492298 child 36662 621122eeb138
equal inserted replaced
36660:1cc4ab4b7ff7 36661:0a5b7b818d65
`    10 imports SEQ`
`    10 imports SEQ`
`    11 begin`
`    11 begin`
`    12 `
`    12 `
`    13 text{*Standard Definitions*}`
`    13 text{*Standard Definitions*}`
`    14 `
`    14 `
`    15 definition`
`    15 abbreviation`
`    16   LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"`
`    16   LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"`
`    17         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where`
`    17         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where`
`    18   [code del]: "f -- a --> L =`
`    18   "f -- a --> L \<equiv> (f ---> L) (at a)"`
`    19      (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s`
`       `
`    20         --> dist (f x) L < r)"`
`       `
`    21 `
`    19 `
`    22 definition`
`    20 definition`
`    23   isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where`
`    21   isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where`
`    24   "isCont f a = (f -- a --> (f a))"`
`    22   "isCont f a = (f -- a --> (f a))"`
`    25 `
`    23 `
`    27   isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where`
`    25   isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where`
`    28   [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"`
`    26   [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"`
`    29 `
`    27 `
`    30 subsection {* Limits of Functions *}`
`    28 subsection {* Limits of Functions *}`
`    31 `
`    29 `
`    32 lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"`
`    30 lemma LIM_def: "f -- a --> L =`
`    33 unfolding LIM_def tendsto_iff eventually_at ..`
`    31      (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s`
`       `
`    32         --> dist (f x) L < r)"`
`       `
`    33 unfolding tendsto_iff eventually_at ..`
`    34 `
`    34 `
`    35 lemma metric_LIM_I:`
`    35 lemma metric_LIM_I:`
`    36   "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)`
`    36   "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)`
`    37     \<Longrightarrow> f -- a --> L"`
`    37     \<Longrightarrow> f -- a --> L"`
`    38 by (simp add: LIM_def)`
`    38 by (simp add: LIM_def)`
`    80   fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"`
`    80   fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"`
`    81   shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"`
`    81   shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"`
`    82 by (drule_tac k="- a" in LIM_offset, simp)`
`    82 by (drule_tac k="- a" in LIM_offset, simp)`
`    83 `
`    83 `
`    84 lemma LIM_const [simp]: "(%x. k) -- x --> k"`
`    84 lemma LIM_const [simp]: "(%x. k) -- x --> k"`
`    85 by (simp add: LIM_def)`
`    85 by (rule tendsto_const)`
`    86 `
`    86 `
`    87 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp`
`    87 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp`
`    88 `
`    88 `
`    89 lemma LIM_add:`
`    89 lemma LIM_add:`
`    90   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`    90   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`    91   assumes f: "f -- a --> L" and g: "g -- a --> M"`
`    91   assumes f: "f -- a --> L" and g: "g -- a --> M"`
`    92   shows "(\<lambda>x. f x + g x) -- a --> (L + M)"`
`    92   shows "(\<lambda>x. f x + g x) -- a --> (L + M)"`
`    93 using assms unfolding LIM_conv_tendsto by (rule tendsto_add)`
`    93 using assms by (rule tendsto_add)`
`    94 `
`    94 `
`    95 lemma LIM_add_zero:`
`    95 lemma LIM_add_zero:`
`    96   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`    96   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`    97   shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"`
`    97   shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"`
`    98 by (drule (1) LIM_add, simp)`
`    98 by (drule (1) LIM_add, simp)`
`    99 `
`    99 `
`   105 lemma LIM_minus:`
`   100 lemma LIM_minus:`
`   106   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   101   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   107   shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"`
`   102   shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"`
`   108 unfolding LIM_conv_tendsto by (rule tendsto_minus)`
`   103 by (rule tendsto_minus)`
`   109 `
`   104 `
`   110 (* TODO: delete *)`
`   105 (* TODO: delete *)`
`   111 lemma LIM_add_minus:`
`   106 lemma LIM_add_minus:`
`   112   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   107   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   113   shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"`
`   108   shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"`
`   114 by (intro LIM_add LIM_minus)`
`   109 by (intro LIM_add LIM_minus)`
`   115 `
`   110 `
`   116 lemma LIM_diff:`
`   111 lemma LIM_diff:`
`   117   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   112   fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   118   shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"`
`   113   shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"`
`   119 unfolding LIM_conv_tendsto by (rule tendsto_diff)`
`   114 by (rule tendsto_diff)`
`   120 `
`   115 `
`   121 lemma LIM_zero:`
`   116 lemma LIM_zero:`
`   122   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   117   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   123   shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"`
`   118   shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"`
`   124 by (simp add: LIM_def dist_norm)`
`   119 by (simp add: LIM_def dist_norm)`
`   154 done`
`   149 done`
`   155 `
`   150 `
`   156 lemma LIM_norm:`
`   151 lemma LIM_norm:`
`   157   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   152   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   158   shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"`
`   153   shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"`
`   159 unfolding LIM_conv_tendsto by (rule tendsto_norm)`
`   154 by (rule tendsto_norm)`
`   160 `
`   155 `
`   161 lemma LIM_norm_zero:`
`   156 lemma LIM_norm_zero:`
`   162   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   157   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"`
`   163   shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"`
`   158   shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"`
`   164 by (drule LIM_norm, simp)`
`   159 by (drule LIM_norm, simp)`
`   219 apply (subst dist_commute, rule dist_triangle)`
`   214 apply (subst dist_commute, rule dist_triangle)`
`   220 apply simp`
`   215 apply simp`
`   221 done`
`   216 done`
`   222 `
`   217 `
`   223 lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"`
`   218 lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"`
`   224 by (auto simp add: LIM_def)`
`   219 by (rule tendsto_ident_at)`
`   225 `
`   220 `
`   226 text{*Limits are equal for functions equal except at limit point*}`
`   221 text{*Limits are equal for functions equal except at limit point*}`
`   227 lemma LIM_equal:`
`   222 lemma LIM_equal:`
`   228      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"`
`   223      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"`
`   229 by (simp add: LIM_def)`
`   224 by (simp add: LIM_def)`
`   347 `
`   342 `
`   348 text {* Bounded Linear Operators *}`
`   343 text {* Bounded Linear Operators *}`
`   349 `
`   344 `
`   350 lemma (in bounded_linear) LIM:`
`   345 lemma (in bounded_linear) LIM:`
`   351   "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"`
`   346   "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"`
`   352 unfolding LIM_conv_tendsto by (rule tendsto)`
`   347 by (rule tendsto)`
`   353 `
`   348 `
`   354 lemma (in bounded_linear) cont: "f -- a --> f a"`
`   349 lemma (in bounded_linear) cont: "f -- a --> f a"`
`   355 by (rule LIM [OF LIM_ident])`
`   350 by (rule LIM [OF LIM_ident])`
`   356 `
`   351 `
`   357 lemma (in bounded_linear) LIM_zero:`
`   352 lemma (in bounded_linear) LIM_zero:`
`   360 `
`   355 `
`   361 text {* Bounded Bilinear Operators *}`
`   356 text {* Bounded Bilinear Operators *}`
`   362 `
`   357 `
`   363 lemma (in bounded_bilinear) LIM:`
`   358 lemma (in bounded_bilinear) LIM:`
`   364   "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"`
`   359   "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"`
`   365 unfolding LIM_conv_tendsto by (rule tendsto)`
`   360 by (rule tendsto)`
`   366 `
`   361 `
`   367 lemma (in bounded_bilinear) LIM_prod_zero:`
`   362 lemma (in bounded_bilinear) LIM_prod_zero:`
`   368   fixes a :: "'d::metric_space"`
`   363   fixes a :: "'d::metric_space"`
`   369   assumes f: "f -- a --> 0"`
`   364   assumes f: "f -- a --> 0"`
`   370   assumes g: "g -- a --> 0"`
`   365   assumes g: "g -- a --> 0"`
`   400 subsubsection {* Derived theorems about @{term LIM} *}`
`   395 subsubsection {* Derived theorems about @{term LIM} *}`
`   401 `
`   396 `
`   402 lemma LIM_inverse:`
`   397 lemma LIM_inverse:`
`   403   fixes L :: "'a::real_normed_div_algebra"`
`   398   fixes L :: "'a::real_normed_div_algebra"`
`   404   shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"`
`   399   shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"`
`   406 by (rule tendsto_inverse)`
`   400 by (rule tendsto_inverse)`
`   407 `
`   401 `
`   408 lemma LIM_inverse_fun:`
`   402 lemma LIM_inverse_fun:`
`   409   assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"`
`   403   assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"`
`   410   shows "inverse -- a --> inverse a"`
`   404   shows "inverse -- a --> inverse a"`