src/HOL/Limits.thy
changeset 45892 8dcf6692433f
parent 45294 3c5d3d286055
child 46886 4cd29473c65d
     1.1 --- a/src/HOL/Limits.thy	Thu Dec 15 13:40:20 2011 +0100
     1.2 +++ b/src/HOL/Limits.thy	Thu Dec 15 15:55:39 2011 +0100
     1.3 @@ -101,6 +101,18 @@
     1.4    shows "eventually (\<lambda>i. R i) F"
     1.5    using assms by (auto elim!: eventually_rev_mp)
     1.6  
     1.7 +lemma eventually_subst:
     1.8 +  assumes "eventually (\<lambda>n. P n = Q n) F"
     1.9 +  shows "eventually P F = eventually Q F" (is "?L = ?R")
    1.10 +proof -
    1.11 +  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.12 +      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"
    1.13 +    by (auto elim: eventually_elim1)
    1.14 +  then show ?thesis by (auto elim: eventually_elim2)
    1.15 +qed
    1.16 +
    1.17 +
    1.18 +
    1.19  subsection {* Finer-than relation *}
    1.20  
    1.21  text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
    1.22 @@ -280,6 +292,11 @@
    1.23    unfolding le_filter_def eventually_sequentially
    1.24    by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
    1.25  
    1.26 +lemma eventually_sequentiallyI:
    1.27 +  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
    1.28 +  shows "eventually P sequentially"
    1.29 +using assms by (auto simp: eventually_sequentially)
    1.30 +
    1.31  
    1.32  subsection {* Standard filters *}
    1.33  
    1.34 @@ -537,6 +554,9 @@
    1.35    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
    1.36    "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
    1.37  
    1.38 +definition real_tendsto_inf :: "('a \<Rightarrow> real) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    1.39 +  "real_tendsto_inf f F \<equiv> \<forall>x. eventually (\<lambda>y. x < f y) F"
    1.40 +
    1.41  ML {*
    1.42  structure Tendsto_Intros = Named_Thms
    1.43  (
    1.44 @@ -673,6 +693,15 @@
    1.45      using le_less_trans by (rule eventually_elim2)
    1.46  qed
    1.47  
    1.48 +lemma real_tendsto_inf_real: "real_tendsto_inf real sequentially"
    1.49 +proof (unfold real_tendsto_inf_def, rule allI)
    1.50 +  fix x show "eventually (\<lambda>y. x < real y) sequentially"
    1.51 +    by (rule eventually_sequentiallyI[of "natceiling (x + 1)"])
    1.52 +        (simp add: natceiling_le_eq)
    1.53 +qed
    1.54 +
    1.55 +
    1.56 +
    1.57  subsubsection {* Distance and norms *}
    1.58  
    1.59  lemma tendsto_dist [tendsto_intros]:
    1.60 @@ -769,6 +798,22 @@
    1.61      by (simp add: tendsto_const)
    1.62  qed
    1.63  
    1.64 +lemma real_tendsto_sandwich:
    1.65 +  fixes f g h :: "'a \<Rightarrow> real"
    1.66 +  assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
    1.67 +  assumes lim: "(f ---> c) net" "(h ---> c) net"
    1.68 +  shows "(g ---> c) net"
    1.69 +proof -
    1.70 +  have "((\<lambda>n. g n - f n) ---> 0) net"
    1.71 +  proof (rule metric_tendsto_imp_tendsto)
    1.72 +    show "eventually (\<lambda>n. dist (g n - f n) 0 \<le> dist (h n - f n) 0) net"
    1.73 +      using ev by (rule eventually_elim2) (simp add: dist_real_def)
    1.74 +    show "((\<lambda>n. h n - f n) ---> 0) net"
    1.75 +      using tendsto_diff[OF lim(2,1)] by simp
    1.76 +  qed
    1.77 +  from tendsto_add[OF this lim(1)] show ?thesis by simp
    1.78 +qed
    1.79 +
    1.80  subsubsection {* Linear operators and multiplication *}
    1.81  
    1.82  lemma (in bounded_linear) tendsto: