src/HOL/Limits.thy
changeset 50247 491c5c81c2e8
parent 49834 b27bbb021df1
child 50322 b06b95a5fda2
     1.1 --- a/src/HOL/Limits.thy	Tue Nov 27 13:48:40 2012 +0100
     1.2 +++ b/src/HOL/Limits.thy	Tue Nov 27 19:31:11 2012 +0100
     1.3 @@ -280,23 +280,70 @@
     1.4  lemma filtermap_bot [simp]: "filtermap f bot = bot"
     1.5    by (simp add: filter_eq_iff eventually_filtermap)
     1.6  
     1.7 -
     1.8 -subsection {* Sequentially *}
     1.9 +subsection {* Order filters *}
    1.10  
    1.11 -definition sequentially :: "nat filter"
    1.12 -  where "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
    1.13 +definition at_top :: "('a::order) filter"
    1.14 +  where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
    1.15  
    1.16 -lemma eventually_sequentially:
    1.17 -  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
    1.18 -unfolding sequentially_def
    1.19 +lemma eventually_at_top_linorder:
    1.20 +  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_top \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
    1.21 +  unfolding at_top_def
    1.22  proof (rule eventually_Abs_filter, rule is_filter.intro)
    1.23 -  fix P Q :: "nat \<Rightarrow> bool"
    1.24 +  fix P Q :: "'a \<Rightarrow> bool"
    1.25    assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
    1.26    then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
    1.27    then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
    1.28    then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
    1.29  qed auto
    1.30  
    1.31 +lemma eventually_at_top_dense:
    1.32 +  fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_top \<longleftrightarrow> (\<exists>N. \<forall>n>N. P n)"
    1.33 +  unfolding eventually_at_top_linorder
    1.34 +proof safe
    1.35 +  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.36 +next
    1.37 +  fix N assume "\<forall>n>N. P n" 
    1.38 +  moreover from gt_ex[of N] guess y ..
    1.39 +  ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])
    1.40 +qed
    1.41 +
    1.42 +definition at_bot :: "('a::order) filter"
    1.43 +  where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)"
    1.44 +
    1.45 +lemma eventually_at_bot_linorder:
    1.46 +  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"
    1.47 +  unfolding at_bot_def
    1.48 +proof (rule eventually_Abs_filter, rule is_filter.intro)
    1.49 +  fix P Q :: "'a \<Rightarrow> bool"
    1.50 +  assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n"
    1.51 +  then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto
    1.52 +  then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp
    1.53 +  then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" ..
    1.54 +qed auto
    1.55 +
    1.56 +lemma eventually_at_bot_dense:
    1.57 +  fixes P :: "'a::dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"
    1.58 +  unfolding eventually_at_bot_linorder
    1.59 +proof safe
    1.60 +  fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])
    1.61 +next
    1.62 +  fix N assume "\<forall>n<N. P n" 
    1.63 +  moreover from lt_ex[of N] guess y ..
    1.64 +  ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])
    1.65 +qed
    1.66 +
    1.67 +subsection {* Sequentially *}
    1.68 +
    1.69 +abbreviation sequentially :: "nat filter"
    1.70 +  where "sequentially == at_top"
    1.71 +
    1.72 +lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
    1.73 +  unfolding at_top_def by simp
    1.74 +
    1.75 +lemma eventually_sequentially:
    1.76 +  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
    1.77 +  by (rule eventually_at_top_linorder)
    1.78 +
    1.79  lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"
    1.80    unfolding filter_eq_iff eventually_sequentially by auto
    1.81  
    1.82 @@ -340,6 +387,9 @@
    1.83  lemma within_empty [simp]: "F within {} = bot"
    1.84    unfolding filter_eq_iff eventually_within by simp
    1.85  
    1.86 +lemma within_le: "F within S \<le> F"
    1.87 +  unfolding le_filter_def eventually_within by (auto elim: eventually_elim1)
    1.88 +
    1.89  lemma eventually_nhds:
    1.90    "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    1.91  unfolding nhds_def
    1.92 @@ -564,12 +614,24 @@
    1.93  
    1.94  subsection {* Limits *}
    1.95  
    1.96 -definition (in topological_space)
    1.97 +definition filter_lim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
    1.98 +  "filter_lim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
    1.99 +
   1.100 +syntax
   1.101 +  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
   1.102 +
   1.103 +translations
   1.104 +  "LIM x F1. f :> F2"   == "CONST filter_lim (%x. f) F2 F1"
   1.105 +
   1.106 +lemma filter_limE: "(LIM x F1. f x :> F2) \<Longrightarrow> eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1"
   1.107 +  by (auto simp: filter_lim_def eventually_filtermap le_filter_def)
   1.108 +
   1.109 +lemma filter_limI: "(\<And>P. eventually P F2 \<Longrightarrow> eventually (\<lambda>x. P (f x)) F1) \<Longrightarrow> (LIM x F1. f x :> F2)"
   1.110 +  by (auto simp: filter_lim_def eventually_filtermap le_filter_def)
   1.111 +
   1.112 +abbreviation (in topological_space)
   1.113    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   1.114 -  "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
   1.115 -
   1.116 -definition real_tendsto_inf :: "('a \<Rightarrow> real) \<Rightarrow> 'a filter \<Rightarrow> bool" where
   1.117 -  "real_tendsto_inf f F \<equiv> \<forall>x. eventually (\<lambda>y. x < f y) F"
   1.118 +  "(f ---> l) F \<equiv> filter_lim f (nhds l) F"
   1.119  
   1.120  ML {*
   1.121  structure Tendsto_Intros = Named_Thms
   1.122 @@ -581,6 +643,15 @@
   1.123  
   1.124  setup Tendsto_Intros.setup
   1.125  
   1.126 +lemma tendsto_def: "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
   1.127 +  unfolding filter_lim_def
   1.128 +proof safe
   1.129 +  fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"
   1.130 +  then show "eventually (\<lambda>x. f x \<in> S) F"
   1.131 +    unfolding eventually_nhds eventually_filtermap le_filter_def
   1.132 +    by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
   1.133 +qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
   1.134 +
   1.135  lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
   1.136    unfolding tendsto_def le_filter_def by fast
   1.137  
   1.138 @@ -706,15 +777,6 @@
   1.139      using le_less_trans by (rule eventually_elim2)
   1.140  qed
   1.141  
   1.142 -lemma real_tendsto_inf_real: "real_tendsto_inf real sequentially"
   1.143 -proof (unfold real_tendsto_inf_def, rule allI)
   1.144 -  fix x show "eventually (\<lambda>y. x < real y) sequentially"
   1.145 -    by (rule eventually_sequentiallyI[of "natceiling (x + 1)"])
   1.146 -        (simp add: natceiling_le_eq)
   1.147 -qed
   1.148 -
   1.149 -
   1.150 -
   1.151  subsubsection {* Distance and norms *}
   1.152  
   1.153  lemma tendsto_dist [tendsto_intros]:
   1.154 @@ -1011,4 +1073,25 @@
   1.155    shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
   1.156    unfolding sgn_div_norm by (simp add: tendsto_intros)
   1.157  
   1.158 +subsection {* Limits to @{const at_top} and @{const at_bot} *}
   1.159 +
   1.160 +lemma filter_lim_at_top:
   1.161 +  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
   1.162 +  shows "(LIM x F. f x :> at_top) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. Z < f x) F)"
   1.163 +  by (safe elim!: filter_limE intro!: filter_limI)
   1.164 +     (auto simp: eventually_at_top_dense elim!: eventually_elim1)
   1.165 +
   1.166 +lemma filter_lim_at_bot: 
   1.167 +  fixes f :: "'a \<Rightarrow> ('b::dense_linorder)"
   1.168 +  shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z. eventually (\<lambda>x. f x < Z) F)"
   1.169 +  by (safe elim!: filter_limE intro!: filter_limI)
   1.170 +     (auto simp: eventually_at_bot_dense elim!: eventually_elim1)
   1.171 +
   1.172 +lemma filter_lim_real_sequentially: "LIM x sequentially. real x :> at_top"
   1.173 +  unfolding filter_lim_at_top
   1.174 +  apply (intro allI)
   1.175 +  apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI)
   1.176 +  apply (auto simp: natceiling_le_eq)
   1.177 +  done
   1.178 +
   1.179  end