generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
authorhoelzl
Tue Jul 14 13:48:03 2015 +0200 (2015-07-14)
changeset 60721c1b7793c23a3
parent 60720 8c99fa3b7c44
child 60725 daf200e2d79a
generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
src/HOL/Filter.thy
src/HOL/Limits.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Filter.thy	Tue Jul 14 13:37:44 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Tue Jul 14 13:48:03 2015 +0200
     1.3 @@ -602,8 +602,10 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 -lemma eventually_gt_at_top:
     1.8 -  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
     1.9 +lemma eventually_at_top_not_equal: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
    1.10 +  unfolding eventually_at_top_dense by auto
    1.11 +
    1.12 +lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
    1.13    unfolding eventually_at_top_dense by auto
    1.14  
    1.15  definition at_bot :: "('a::order) filter"
    1.16 @@ -631,6 +633,9 @@
    1.17    finally show ?thesis .
    1.18  qed
    1.19  
    1.20 +lemma eventually_at_bot_not_equal: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
    1.21 +  unfolding eventually_at_bot_dense by auto
    1.22 +
    1.23  lemma eventually_gt_at_bot:
    1.24    "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
    1.25    unfolding eventually_at_bot_dense by auto
    1.26 @@ -778,6 +783,21 @@
    1.27  lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
    1.28    by (simp add: filtermap_mono_strong eq_iff)
    1.29  
    1.30 +lemma filtermap_fun_inverse:
    1.31 +  assumes g: "filterlim g F G"
    1.32 +  assumes f: "filterlim f G F"
    1.33 +  assumes ev: "eventually (\<lambda>x. f (g x) = x) G"
    1.34 +  shows "filtermap f F = G"
    1.35 +proof (rule antisym)
    1.36 +  show "filtermap f F \<le> G"
    1.37 +    using f unfolding filterlim_def .
    1.38 +  have "G = filtermap f (filtermap g G)"
    1.39 +    using ev by (auto elim: eventually_elim2 simp: filter_eq_iff eventually_filtermap)
    1.40 +  also have "\<dots> \<le> filtermap f F"
    1.41 +    using g by (intro filtermap_mono) (simp add: filterlim_def)
    1.42 +  finally show "G \<le> filtermap f F" .
    1.43 +qed
    1.44 +
    1.45  lemma filterlim_principal:
    1.46    "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
    1.47    unfolding filterlim_def eventually_filtermap le_principal ..
     2.1 --- a/src/HOL/Limits.thy	Tue Jul 14 13:37:44 2015 +0200
     2.2 +++ b/src/HOL/Limits.thy	Tue Jul 14 13:48:03 2015 +0200
     2.3 @@ -901,30 +901,13 @@
     2.4  
     2.5  lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real]
     2.6  
     2.7 -lemma filtermap_homeomorph:
     2.8 -  assumes f: "continuous (at a) f"
     2.9 -  assumes g: "continuous (at (f a)) g"
    2.10 -  assumes bij1: "\<forall>x. f (g x) = x" and bij2: "\<forall>x. g (f x) = x"
    2.11 -  shows "filtermap f (nhds a) = nhds (f a)"
    2.12 -  unfolding filter_eq_iff eventually_filtermap eventually_nhds
    2.13 -proof safe
    2.14 -  fix P S assume S: "open S" "f a \<in> S" and P: "\<forall>x\<in>S. P x"
    2.15 -  from continuous_within_topological[THEN iffD1, rule_format, OF f S] P
    2.16 -  show "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P (f x))" by auto
    2.17 -next
    2.18 -  fix P S assume S: "open S" "a \<in> S" and P: "\<forall>x\<in>S. P (f x)"
    2.19 -  with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2
    2.20 -  obtain A where "open A" "f a \<in> A" "(\<forall>y\<in>A. g y \<in> S)"
    2.21 -    by (metis UNIV_I)
    2.22 -  with P bij1 show "\<exists>S. open S \<and> f a \<in> S \<and> (\<forall>x\<in>S. P x)"
    2.23 -    by (force intro!: exI[of _ A])
    2.24 -qed
    2.25 -
    2.26  lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)"
    2.27 -  by (rule filtermap_homeomorph[where g="\<lambda>x. x + d"]) (auto intro: continuous_intros)
    2.28 +  by (rule filtermap_fun_inverse[where g="\<lambda>x. x + d"])
    2.29 +     (auto intro!: tendsto_eq_intros filterlim_ident)
    2.30  
    2.31  lemma filtermap_nhds_minus: "filtermap (\<lambda>x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)"
    2.32 -  by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus)
    2.33 +  by (rule filtermap_fun_inverse[where g=uminus])
    2.34 +     (auto intro!: tendsto_eq_intros filterlim_ident)
    2.35  
    2.36  lemma filtermap_at_shift: "filtermap (\<lambda>x. x - d) (at a) = at (a - d::'a::real_normed_vector)"
    2.37    by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
    2.38 @@ -960,9 +943,17 @@
    2.39    "eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (- x)) (at_right (-a))"
    2.40    unfolding at_left_minus[of a] by (simp add: eventually_filtermap)
    2.41  
    2.42 +lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
    2.43 +  unfolding filterlim_at_top eventually_at_bot_dense
    2.44 +  by (metis leI minus_less_iff order_less_asym)
    2.45 +
    2.46 +lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
    2.47 +  unfolding filterlim_at_bot eventually_at_top_dense
    2.48 +  by (metis leI less_minus_iff order_less_asym)
    2.49 +
    2.50  lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
    2.51 -  unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder
    2.52 -  by (metis le_minus_iff minus_minus)
    2.53 +  by (rule filtermap_fun_inverse[symmetric, of uminus])
    2.54 +     (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot)
    2.55  
    2.56  lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
    2.57    unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
    2.58 @@ -973,14 +964,6 @@
    2.59  lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \<longleftrightarrow> (LIM x at_top. f (-x::real) :> F)"
    2.60    unfolding filterlim_def at_bot_mirror filtermap_filtermap ..
    2.61  
    2.62 -lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top"
    2.63 -  unfolding filterlim_at_top eventually_at_bot_dense
    2.64 -  by (metis leI minus_less_iff order_less_asym)
    2.65 -
    2.66 -lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot"
    2.67 -  unfolding filterlim_at_bot eventually_at_top_dense
    2.68 -  by (metis leI less_minus_iff order_less_asym)
    2.69 -
    2.70  lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_bot)"
    2.71    using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F]
    2.72    using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
    2.73 @@ -999,20 +982,6 @@
    2.74      by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps)
    2.75  qed
    2.76  
    2.77 -lemma filterlim_inverse_at_top:
    2.78 -  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
    2.79 -  by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
    2.80 -     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
    2.81 -
    2.82 -lemma filterlim_inverse_at_bot_neg:
    2.83 -  "LIM x (at_left (0::real)). inverse x :> at_bot"
    2.84 -  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
    2.85 -
    2.86 -lemma filterlim_inverse_at_bot:
    2.87 -  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
    2.88 -  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
    2.89 -  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
    2.90 -
    2.91  lemma tendsto_inverse_0:
    2.92    fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra"
    2.93    shows "(inverse ---> (0::'a)) at_infinity"
    2.94 @@ -1029,18 +998,28 @@
    2.95    qed
    2.96  qed
    2.97  
    2.98 +lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)"
    2.99 +  unfolding filterlim_at
   2.100 +  by (auto simp: eventually_at_top_dense)
   2.101 +     (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
   2.102 +
   2.103 +lemma filterlim_inverse_at_top:
   2.104 +  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top"
   2.105 +  by (intro filterlim_compose[OF filterlim_inverse_at_top_right])
   2.106 +     (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal)
   2.107 +
   2.108 +lemma filterlim_inverse_at_bot_neg:
   2.109 +  "LIM x (at_left (0::real)). inverse x :> at_bot"
   2.110 +  by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right)
   2.111 +
   2.112 +lemma filterlim_inverse_at_bot:
   2.113 +  "(f ---> (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot"
   2.114 +  unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric]
   2.115 +  by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric])
   2.116 +
   2.117  lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top"
   2.118 -proof (rule antisym)
   2.119 -  have "(inverse ---> (0::real)) at_top"
   2.120 -    by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl)
   2.121 -  then show "filtermap inverse at_top \<le> at_right (0::real)"
   2.122 -    by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def)
   2.123 -next
   2.124 -  have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top"
   2.125 -    using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono)
   2.126 -  then show "at_right (0::real) \<le> filtermap inverse at_top"
   2.127 -    by (simp add: filtermap_ident filtermap_filtermap)
   2.128 -qed
   2.129 +  by (intro filtermap_fun_inverse[symmetric, where g=inverse])
   2.130 +     (auto intro: filterlim_inverse_at_top_right filterlim_inverse_at_right_top)
   2.131  
   2.132  lemma eventually_at_right_to_top:
   2.133    "eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top"
     3.1 --- a/src/HOL/Transcendental.thy	Tue Jul 14 13:37:44 2015 +0200
     3.2 +++ b/src/HOL/Transcendental.thy	Tue Jul 14 13:48:03 2015 +0200
     3.3 @@ -2016,6 +2016,13 @@
     3.4    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
     3.5       (auto intro: eventually_gt_at_top)
     3.6  
     3.7 +lemma filtermap_ln_at_top: "filtermap (ln::real \<Rightarrow> real) at_top = at_top"
     3.8 +  by (intro filtermap_fun_inverse[of exp] exp_at_top ln_at_top) auto
     3.9 +
    3.10 +lemma filtermap_exp_at_top: "filtermap (exp::real \<Rightarrow> real) at_top = at_top"
    3.11 +  by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top)
    3.12 +     (auto simp: eventually_at_top_dense)
    3.13 +
    3.14  lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) ---> (0::real)) at_top"
    3.15  proof (induct k)
    3.16    case 0