author  hoelzl 
Fri, 22 Mar 2013 10:41:43 +0100  
changeset 51474  1e9e68247ad1 
parent 51472  adb441e4b9e9 
child 51478  270b21f3ae0a 
permissions  rwrr 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

1 
(* Title : Limits.thy 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

2 
Author : Brian Huffman 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

3 
*) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

4 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

5 
header {* Filters and Limits *} 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

6 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

7 
theory Limits 
36822  8 
imports RealVector 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

9 
begin 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

10 

50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

11 
definition at_infinity :: "'a::real_normed_vector filter" where 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

12 
"at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

13 

0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

14 
lemma eventually_at_infinity: 
50325  15 
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

16 
unfolding at_infinity_def 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

17 
proof (rule eventually_Abs_filter, rule is_filter.intro) 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

18 
fix P Q :: "'a \<Rightarrow> bool" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

19 
assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

20 
then obtain r s where 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

21 
"\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

22 
then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

23 
then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" .. 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

24 
qed auto 
31392  25 

50325  26 
lemma at_infinity_eq_at_top_bot: 
27 
"(at_infinity \<Colon> real filter) = sup at_top at_bot" 

28 
unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder 

29 
proof (intro arg_cong[where f=Abs_filter] ext iffI) 

30 
fix P :: "real \<Rightarrow> bool" assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" 

31 
then guess r .. 

32 
then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>r. P x)" by auto 

33 
then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto 

34 
next 

35 
fix P :: "real \<Rightarrow> bool" assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" 

36 
then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto 

37 
then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" 

38 
by (intro exI[of _ "max p (q)"]) 

39 
(auto simp: abs_real_def) 

40 
qed 

41 

42 
lemma at_top_le_at_infinity: 

43 
"at_top \<le> (at_infinity :: real filter)" 

44 
unfolding at_infinity_eq_at_top_bot by simp 

45 

46 
lemma at_bot_le_at_infinity: 

47 
"at_bot \<le> (at_infinity :: real filter)" 

48 
unfolding at_infinity_eq_at_top_bot by simp 

49 

31355  50 
subsection {* Boundedness *} 
51 

51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

52 
lemma Bfun_def: 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

53 
"Bfun f F \<longleftrightarrow> (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)" 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

54 
unfolding Bfun_metric_def norm_conv_dist 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

55 
proof safe 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

56 
fix y K assume "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F" 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

57 
moreover have "eventually (\<lambda>x. dist (f x) 0 \<le> dist (f x) y + dist 0 y) F" 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

58 
by (intro always_eventually) (metis dist_commute dist_triangle) 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

59 
with * have "eventually (\<lambda>x. dist (f x) 0 \<le> K + dist 0 y) F" 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

60 
by eventually_elim auto 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

61 
with `0 < K` show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F" 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

62 
by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto 
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

63 
qed auto 
31355  64 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

65 
lemma BfunI: 
44195  66 
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" shows "Bfun f F" 
31355  67 
unfolding Bfun_def 
68 
proof (intro exI conjI allI) 

69 
show "0 < max K 1" by simp 

70 
next 

44195  71 
show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F" 
31355  72 
using K by (rule eventually_elim1, simp) 
73 
qed 

74 

75 
lemma BfunE: 

44195  76 
assumes "Bfun f F" 
77 
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F" 

31355  78 
using assms unfolding Bfun_def by fast 
79 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

80 
subsection {* Convergence to Zero *} 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

81 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

82 
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" 
44195  83 
where "Zfun f F = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) F)" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

84 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

85 
lemma ZfunI: 
44195  86 
"(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F) \<Longrightarrow> Zfun f F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

87 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

88 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

89 
lemma ZfunD: 
44195  90 
"\<lbrakk>Zfun f F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

91 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

92 

31355  93 
lemma Zfun_ssubst: 
44195  94 
"eventually (\<lambda>x. f x = g x) F \<Longrightarrow> Zfun g F \<Longrightarrow> Zfun f F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

95 
unfolding Zfun_def by (auto elim!: eventually_rev_mp) 
31355  96 

44195  97 
lemma Zfun_zero: "Zfun (\<lambda>x. 0) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

98 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

99 

44195  100 
lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) F = Zfun (\<lambda>x. f x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

101 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

102 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

103 
lemma Zfun_imp_Zfun: 
44195  104 
assumes f: "Zfun f F" 
105 
assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F" 

106 
shows "Zfun (\<lambda>x. g x) F" 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

107 
proof (cases) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

108 
assume K: "0 < K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

109 
show ?thesis 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

110 
proof (rule ZfunI) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

111 
fix r::real assume "0 < r" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

112 
hence "0 < r / K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

113 
using K by (rule divide_pos_pos) 
44195  114 
then have "eventually (\<lambda>x. norm (f x) < r / K) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

115 
using ZfunD [OF f] by fast 
44195  116 
with g show "eventually (\<lambda>x. norm (g x) < r) F" 
46887  117 
proof eventually_elim 
118 
case (elim x) 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

119 
hence "norm (f x) * K < r" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

120 
by (simp add: pos_less_divide_eq K) 
46887  121 
thus ?case 
122 
by (simp add: order_le_less_trans [OF elim(1)]) 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

123 
qed 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

124 
qed 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

125 
next 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

126 
assume "\<not> 0 < K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

127 
hence K: "K \<le> 0" by (simp only: not_less) 
31355  128 
show ?thesis 
129 
proof (rule ZfunI) 

130 
fix r :: real 

131 
assume "0 < r" 

44195  132 
from g show "eventually (\<lambda>x. norm (g x) < r) F" 
46887  133 
proof eventually_elim 
134 
case (elim x) 

135 
also have "norm (f x) * K \<le> norm (f x) * 0" 

31355  136 
using K norm_ge_zero by (rule mult_left_mono) 
46887  137 
finally show ?case 
31355  138 
using `0 < r` by simp 
139 
qed 

140 
qed 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

141 
qed 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

142 

44195  143 
lemma Zfun_le: "\<lbrakk>Zfun g F; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

144 
by (erule_tac K="1" in Zfun_imp_Zfun, simp) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

145 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

146 
lemma Zfun_add: 
44195  147 
assumes f: "Zfun f F" and g: "Zfun g F" 
148 
shows "Zfun (\<lambda>x. f x + g x) F" 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

149 
proof (rule ZfunI) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

150 
fix r::real assume "0 < r" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

151 
hence r: "0 < r / 2" by simp 
44195  152 
have "eventually (\<lambda>x. norm (f x) < r/2) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

153 
using f r by (rule ZfunD) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

154 
moreover 
44195  155 
have "eventually (\<lambda>x. norm (g x) < r/2) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

156 
using g r by (rule ZfunD) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

157 
ultimately 
44195  158 
show "eventually (\<lambda>x. norm (f x + g x) < r) F" 
46887  159 
proof eventually_elim 
160 
case (elim x) 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

161 
have "norm (f x + g x) \<le> norm (f x) + norm (g x)" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

162 
by (rule norm_triangle_ineq) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

163 
also have "\<dots> < r/2 + r/2" 
46887  164 
using elim by (rule add_strict_mono) 
165 
finally show ?case 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

166 
by simp 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

167 
qed 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

168 
qed 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

169 

44195  170 
lemma Zfun_minus: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x.  f x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

171 
unfolding Zfun_def by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

172 

44195  173 
lemma Zfun_diff: "\<lbrakk>Zfun f F; Zfun g F\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x  g x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

174 
by (simp only: diff_minus Zfun_add Zfun_minus) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

175 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

176 
lemma (in bounded_linear) Zfun: 
44195  177 
assumes g: "Zfun g F" 
178 
shows "Zfun (\<lambda>x. f (g x)) F" 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

179 
proof  
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

180 
obtain K where "\<And>x. norm (f x) \<le> norm x * K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

181 
using bounded by fast 
44195  182 
then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) F" 
31355  183 
by simp 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

184 
with g show ?thesis 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

185 
by (rule Zfun_imp_Zfun) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

186 
qed 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

187 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

188 
lemma (in bounded_bilinear) Zfun: 
44195  189 
assumes f: "Zfun f F" 
190 
assumes g: "Zfun g F" 

191 
shows "Zfun (\<lambda>x. f x ** g x) F" 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

192 
proof (rule ZfunI) 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

193 
fix r::real assume r: "0 < r" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

194 
obtain K where K: "0 < K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

195 
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

196 
using pos_bounded by fast 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

197 
from K have K': "0 < inverse K" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

198 
by (rule positive_imp_inverse_positive) 
44195  199 
have "eventually (\<lambda>x. norm (f x) < r) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

200 
using f r by (rule ZfunD) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

201 
moreover 
44195  202 
have "eventually (\<lambda>x. norm (g x) < inverse K) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

203 
using g K' by (rule ZfunD) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

204 
ultimately 
44195  205 
show "eventually (\<lambda>x. norm (f x ** g x) < r) F" 
46887  206 
proof eventually_elim 
207 
case (elim x) 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

208 
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

209 
by (rule norm_le) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

210 
also have "norm (f x) * norm (g x) * K < r * inverse K * K" 
46887  211 
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

212 
also from K have "r * inverse K * K = r" 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

213 
by simp 
46887  214 
finally show ?case . 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

215 
qed 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

216 
qed 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

217 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

218 
lemma (in bounded_bilinear) Zfun_left: 
44195  219 
"Zfun f F \<Longrightarrow> Zfun (\<lambda>x. f x ** a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

220 
by (rule bounded_linear_left [THEN bounded_linear.Zfun]) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

221 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

222 
lemma (in bounded_bilinear) Zfun_right: 
44195  223 
"Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

224 
by (rule bounded_linear_right [THEN bounded_linear.Zfun]) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

225 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

226 
lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

227 
lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

228 
lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

229 

44195  230 
lemma tendsto_Zfun_iff: "(f > a) F = Zfun (\<lambda>x. f x  a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

231 
by (simp only: tendsto_iff Zfun_def dist_norm) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

232 

44205
18da2a87421c
generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman
parents:
44195
diff
changeset

233 
subsubsection {* Distance and norms *} 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

234 

31565  235 
lemma tendsto_norm [tendsto_intros]: 
44195  236 
"(f > a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) > norm a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

237 
unfolding norm_conv_dist by (intro tendsto_intros) 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

238 

621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

239 
lemma tendsto_norm_zero: 
44195  240 
"(f > 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) > 0) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

241 
by (drule tendsto_norm, simp) 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

242 

621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

243 
lemma tendsto_norm_zero_cancel: 
44195  244 
"((\<lambda>x. norm (f x)) > 0) F \<Longrightarrow> (f > 0) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

245 
unfolding tendsto_iff dist_norm by simp 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

246 

621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

247 
lemma tendsto_norm_zero_iff: 
44195  248 
"((\<lambda>x. norm (f x)) > 0) F \<longleftrightarrow> (f > 0) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

249 
unfolding tendsto_iff dist_norm by simp 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

250 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

251 
lemma tendsto_rabs [tendsto_intros]: 
44195  252 
"(f > (l::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) > \<bar>l\<bar>) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

253 
by (fold real_norm_def, rule tendsto_norm) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

254 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

255 
lemma tendsto_rabs_zero: 
44195  256 
"(f > (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

257 
by (fold real_norm_def, rule tendsto_norm_zero) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

258 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

259 
lemma tendsto_rabs_zero_cancel: 
44195  260 
"((\<lambda>x. \<bar>f x\<bar>) > (0::real)) F \<Longrightarrow> (f > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

261 
by (fold real_norm_def, rule tendsto_norm_zero_cancel) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

262 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

263 
lemma tendsto_rabs_zero_iff: 
44195  264 
"((\<lambda>x. \<bar>f x\<bar>) > (0::real)) F \<longleftrightarrow> (f > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

265 
by (fold real_norm_def, rule tendsto_norm_zero_iff) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

266 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

267 
subsubsection {* Addition and subtraction *} 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

268 

31565  269 
lemma tendsto_add [tendsto_intros]: 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

270 
fixes a b :: "'a::real_normed_vector" 
44195  271 
shows "\<lbrakk>(f > a) F; (g > b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) > a + b) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

272 
by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

273 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

274 
lemma tendsto_add_zero: 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

275 
fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector" 
44195  276 
shows "\<lbrakk>(f > 0) F; (g > 0) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

277 
by (drule (1) tendsto_add, simp) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

278 

31565  279 
lemma tendsto_minus [tendsto_intros]: 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

280 
fixes a :: "'a::real_normed_vector" 
44195  281 
shows "(f > a) F \<Longrightarrow> ((\<lambda>x.  f x) >  a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

282 
by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

283 

2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

284 
lemma tendsto_minus_cancel: 
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

285 
fixes a :: "'a::real_normed_vector" 
44195  286 
shows "((\<lambda>x.  f x) >  a) F \<Longrightarrow> (f > a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

287 
by (drule tendsto_minus, simp) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

288 

50330
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

289 
lemma tendsto_minus_cancel_left: 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

290 
"(f >  (y::_::real_normed_vector)) F \<longleftrightarrow> ((\<lambda>x.  f x) > y) F" 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

291 
using tendsto_minus_cancel[of f " y" F] tendsto_minus[of f " y" F] 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

292 
by auto 
d0b12171118e
conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
hoelzl
parents:
50327
diff
changeset

293 

31565  294 
lemma tendsto_diff [tendsto_intros]: 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

295 
fixes a b :: "'a::real_normed_vector" 
44195  296 
shows "\<lbrakk>(f > a) F; (g > b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x  g x) > a  b) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

297 
by (simp add: diff_minus tendsto_add tendsto_minus) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

298 

31588  299 
lemma tendsto_setsum [tendsto_intros]: 
300 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector" 

44195  301 
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i > a i) F" 
302 
shows "((\<lambda>x. \<Sum>i\<in>S. f i x) > (\<Sum>i\<in>S. a i)) F" 

31588  303 
proof (cases "finite S") 
304 
assume "finite S" thus ?thesis using assms 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

305 
by (induct, simp add: tendsto_const, simp add: tendsto_add) 
31588  306 
next 
307 
assume "\<not> finite S" thus ?thesis 

308 
by (simp add: tendsto_const) 

309 
qed 

310 

50999  311 
lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real] 
312 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

313 
subsubsection {* Linear operators and multiplication *} 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

314 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

315 
lemma (in bounded_linear) tendsto: 
44195  316 
"(g > a) F \<Longrightarrow> ((\<lambda>x. f (g x)) > f a) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

317 
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

318 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

319 
lemma (in bounded_linear) tendsto_zero: 
44195  320 
"(g > 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

321 
by (drule tendsto, simp only: zero) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

322 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

323 
lemma (in bounded_bilinear) tendsto: 
44195  324 
"\<lbrakk>(f > a) F; (g > b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) > a ** b) F" 
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

325 
by (simp only: tendsto_Zfun_iff prod_diff_prod 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

326 
Zfun_add Zfun Zfun_left Zfun_right) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

327 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

328 
lemma (in bounded_bilinear) tendsto_zero: 
44195  329 
assumes f: "(f > 0) F" 
330 
assumes g: "(g > 0) F" 

331 
shows "((\<lambda>x. f x ** g x) > 0) F" 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

332 
using tendsto [OF f g] by (simp add: zero_left) 
31355  333 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

334 
lemma (in bounded_bilinear) tendsto_left_zero: 
44195  335 
"(f > 0) F \<Longrightarrow> ((\<lambda>x. f x ** c) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

336 
by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

337 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

338 
lemma (in bounded_bilinear) tendsto_right_zero: 
44195  339 
"(f > 0) F \<Longrightarrow> ((\<lambda>x. c ** f x) > 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

340 
by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

341 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

342 
lemmas tendsto_of_real [tendsto_intros] = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

343 
bounded_linear.tendsto [OF bounded_linear_of_real] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

344 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

345 
lemmas tendsto_scaleR [tendsto_intros] = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

346 
bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

347 

f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

348 
lemmas tendsto_mult [tendsto_intros] = 
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

349 
bounded_bilinear.tendsto [OF bounded_bilinear_mult] 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

350 

44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

351 
lemmas tendsto_mult_zero = 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

352 
bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

353 

e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

354 
lemmas tendsto_mult_left_zero = 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

355 
bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

356 

e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

357 
lemmas tendsto_mult_right_zero = 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

358 
bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] 
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44342
diff
changeset

359 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

360 
lemma tendsto_power [tendsto_intros]: 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

361 
fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" 
44195  362 
shows "(f > a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) > a ^ n) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

363 
by (induct n) (simp_all add: tendsto_const tendsto_mult) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

364 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

365 
lemma tendsto_setprod [tendsto_intros]: 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

366 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 
44195  367 
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i > L i) F" 
368 
shows "((\<lambda>x. \<Prod>i\<in>S. f i x) > (\<Prod>i\<in>S. L i)) F" 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

369 
proof (cases "finite S") 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

370 
assume "finite S" thus ?thesis using assms 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

371 
by (induct, simp add: tendsto_const, simp add: tendsto_mult) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

372 
next 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

373 
assume "\<not> finite S" thus ?thesis 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

374 
by (simp add: tendsto_const) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

375 
qed 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

376 

0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

377 
subsubsection {* Inverse and division *} 
31355  378 

379 
lemma (in bounded_bilinear) Zfun_prod_Bfun: 

44195  380 
assumes f: "Zfun f F" 
381 
assumes g: "Bfun g F" 

382 
shows "Zfun (\<lambda>x. f x ** g x) F" 

31355  383 
proof  
384 
obtain K where K: "0 \<le> K" 

385 
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" 

386 
using nonneg_bounded by fast 

387 
obtain B where B: "0 < B" 

44195  388 
and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

389 
using g by (rule BfunE) 
44195  390 
have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) F" 
46887  391 
using norm_g proof eventually_elim 
392 
case (elim x) 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

393 
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" 
31355  394 
by (rule norm_le) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

395 
also have "\<dots> \<le> norm (f x) * B * K" 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

396 
by (intro mult_mono' order_refl norm_g norm_ge_zero 
46887  397 
mult_nonneg_nonneg K elim) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

398 
also have "\<dots> = norm (f x) * (B * K)" 
31355  399 
by (rule mult_assoc) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

400 
finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" . 
31355  401 
qed 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

402 
with f show ?thesis 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

403 
by (rule Zfun_imp_Zfun) 
31355  404 
qed 
405 

406 
lemma (in bounded_bilinear) flip: 

407 
"bounded_bilinear (\<lambda>x y. y ** x)" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

408 
apply default 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

409 
apply (rule add_right) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

410 
apply (rule add_left) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

411 
apply (rule scaleR_right) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

412 
apply (rule scaleR_left) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

413 
apply (subst mult_commute) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

414 
using bounded by fast 
31355  415 

416 
lemma (in bounded_bilinear) Bfun_prod_Zfun: 

44195  417 
assumes f: "Bfun f F" 
418 
assumes g: "Zfun g F" 

419 
shows "Zfun (\<lambda>x. f x ** g x) F" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

420 
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) 
31355  421 

422 
lemma Bfun_inverse_lemma: 

423 
fixes x :: "'a::real_normed_div_algebra" 

424 
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" 

44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

425 
apply (subst nonzero_norm_inverse, clarsimp) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

426 
apply (erule (1) le_imp_inverse_le) 
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset

427 
done 
31355  428 

429 
lemma Bfun_inverse: 

430 
fixes a :: "'a::real_normed_div_algebra" 

44195  431 
assumes f: "(f > a) F" 
31355  432 
assumes a: "a \<noteq> 0" 
44195  433 
shows "Bfun (\<lambda>x. inverse (f x)) F" 
31355  434 
proof  
435 
from a have "0 < norm a" by simp 

436 
hence "\<exists>r>0. r < norm a" by (rule dense) 

437 
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast 

44195  438 
have "eventually (\<lambda>x. dist (f x) a < r) F" 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

439 
using tendstoD [OF f r1] by fast 
44195  440 
hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a  r)) F" 
46887  441 
proof eventually_elim 
442 
case (elim x) 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

443 
hence 1: "norm (f x  a) < r" 
31355  444 
by (simp add: dist_norm) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

445 
hence 2: "f x \<noteq> 0" using r2 by auto 
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

446 
hence "norm (inverse (f x)) = inverse (norm (f x))" 
31355  447 
by (rule nonzero_norm_inverse) 
448 
also have "\<dots> \<le> inverse (norm a  r)" 

449 
proof (rule le_imp_inverse_le) 

450 
show "0 < norm a  r" using r2 by simp 

451 
next 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

452 
have "norm a  norm (f x) \<le> norm (a  f x)" 
31355  453 
by (rule norm_triangle_ineq2) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

454 
also have "\<dots> = norm (f x  a)" 
31355  455 
by (rule norm_minus_commute) 
456 
also have "\<dots> < r" using 1 . 

31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

457 
finally show "norm a  r \<le> norm (f x)" by simp 
31355  458 
qed 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

459 
finally show "norm (inverse (f x)) \<le> inverse (norm a  r)" . 
31355  460 
qed 
461 
thus ?thesis by (rule BfunI) 

462 
qed 

463 

31565  464 
lemma tendsto_inverse [tendsto_intros]: 
31355  465 
fixes a :: "'a::real_normed_div_algebra" 
44195  466 
assumes f: "(f > a) F" 
31355  467 
assumes a: "a \<noteq> 0" 
44195  468 
shows "((\<lambda>x. inverse (f x)) > inverse a) F" 
31355  469 
proof  
470 
from a have "0 < norm a" by simp 

44195  471 
with f have "eventually (\<lambda>x. dist (f x) a < norm a) F" 
31355  472 
by (rule tendstoD) 
44195  473 
then have "eventually (\<lambda>x. f x \<noteq> 0) F" 
31355  474 
unfolding dist_norm by (auto elim!: eventually_elim1) 
44627  475 
with a have "eventually (\<lambda>x. inverse (f x)  inverse a = 
476 
 (inverse (f x) * (f x  a) * inverse a)) F" 

477 
by (auto elim!: eventually_elim1 simp: inverse_diff_inverse) 

478 
moreover have "Zfun (\<lambda>x.  (inverse (f x) * (f x  a) * inverse a)) F" 

479 
by (intro Zfun_minus Zfun_mult_left 

480 
bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] 

481 
Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff]) 

482 
ultimately show ?thesis 

483 
unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) 

31355  484 
qed 
485 

31565  486 
lemma tendsto_divide [tendsto_intros]: 
31355  487 
fixes a b :: "'a::real_normed_field" 
44195  488 
shows "\<lbrakk>(f > a) F; (g > b) F; b \<noteq> 0\<rbrakk> 
489 
\<Longrightarrow> ((\<lambda>x. f x / g x) > a / b) F" 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

490 
by (simp add: tendsto_mult tendsto_inverse divide_inverse) 
31355  491 

44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

492 
lemma tendsto_sgn [tendsto_intros]: 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

493 
fixes l :: "'a::real_normed_vector" 
44195  494 
shows "\<lbrakk>(f > l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) > sgn l) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

495 
unfolding sgn_div_norm by (simp add: tendsto_intros) 
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

496 

50325  497 
lemma filterlim_at_infinity: 
498 
fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector" 

499 
assumes "0 \<le> c" 

500 
shows "(LIM x F. f x :> at_infinity) \<longleftrightarrow> (\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F)" 

501 
unfolding filterlim_iff eventually_at_infinity 

502 
proof safe 

503 
fix P :: "'a \<Rightarrow> bool" and b 

504 
assume *: "\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F" 

505 
and P: "\<forall>x. b \<le> norm x \<longrightarrow> P x" 

506 
have "max b (c + 1) > c" by auto 

507 
with * have "eventually (\<lambda>x. max b (c + 1) \<le> norm (f x)) F" 

508 
by auto 

509 
then show "eventually (\<lambda>x. P (f x)) F" 

510 
proof eventually_elim 

511 
fix x assume "max b (c + 1) \<le> norm (f x)" 

512 
with P show "P (f x)" by auto 

513 
qed 

514 
qed force 

515 

50347  516 
subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *} 
517 

518 
text {* 

519 

520 
This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and 

521 
@{term "at_right x"} and also @{term "at_right 0"}. 

522 

523 
*} 

524 

51471  525 
lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real] 
50323  526 

50347  527 
lemma filtermap_nhds_shift: "filtermap (\<lambda>x. x  d) (nhds a) = nhds (a  d::real)" 
528 
unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric 

529 
by (intro allI ex_cong) (auto simp: dist_real_def field_simps) 

530 

531 
lemma filtermap_nhds_minus: "filtermap (\<lambda>x.  x) (nhds a) = nhds ( a::real)" 

532 
unfolding filter_eq_iff eventually_filtermap eventually_nhds_metric 

533 
apply (intro allI ex_cong) 

534 
apply (auto simp: dist_real_def field_simps) 

535 
apply (erule_tac x="x" in allE) 

536 
apply simp 

537 
done 

538 

539 
lemma filtermap_at_shift: "filtermap (\<lambda>x. x  d) (at a) = at (a  d::real)" 

540 
unfolding at_def filtermap_nhds_shift[symmetric] 

541 
by (simp add: filter_eq_iff eventually_filtermap eventually_within) 

542 

543 
lemma filtermap_at_right_shift: "filtermap (\<lambda>x. x  d) (at_right a) = at_right (a  d::real)" 

544 
unfolding filtermap_at_shift[symmetric] 

545 
by (simp add: filter_eq_iff eventually_filtermap eventually_within) 

50323  546 

50347  547 
lemma at_right_to_0: "at_right (a::real) = filtermap (\<lambda>x. x + a) (at_right 0)" 
548 
using filtermap_at_right_shift[of "a" 0] by simp 

549 

550 
lemma filterlim_at_right_to_0: 

551 
"filterlim f F (at_right (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at_right 0)" 

552 
unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] .. 

553 

554 
lemma eventually_at_right_to_0: 

555 
"eventually P (at_right (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at_right 0)" 

556 
unfolding at_right_to_0[of a] by (simp add: eventually_filtermap) 

557 

558 
lemma filtermap_at_minus: "filtermap (\<lambda>x.  x) (at a) = at ( a::real)" 

559 
unfolding at_def filtermap_nhds_minus[symmetric] 

560 
by (simp add: filter_eq_iff eventually_filtermap eventually_within) 

561 

562 
lemma at_left_minus: "at_left (a::real) = filtermap (\<lambda>x.  x) (at_right ( a))" 

563 
by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric]) 

50323  564 

50347  565 
lemma at_right_minus: "at_right (a::real) = filtermap (\<lambda>x.  x) (at_left ( a))" 
566 
by (simp add: filter_eq_iff eventually_filtermap eventually_within filtermap_at_minus[symmetric]) 

567 

568 
lemma filterlim_at_left_to_right: 

569 
"filterlim f F (at_left (a::real)) \<longleftrightarrow> filterlim (\<lambda>x. f ( x)) F (at_right (a))" 

570 
unfolding filterlim_def filtermap_filtermap at_left_minus[of a] .. 

571 

572 
lemma eventually_at_left_to_right: 

573 
"eventually P (at_left (a::real)) \<longleftrightarrow> eventually (\<lambda>x. P ( x)) (at_right (a))" 

574 
unfolding at_left_minus[of a] by (simp add: eventually_filtermap) 

575 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

576 
lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

577 
unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

578 
by (metis le_minus_iff minus_minus) 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

579 

a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

580 
lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

581 
unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident) 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

582 

a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

583 
lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (x::real) :> F)" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

584 
unfolding filterlim_def at_top_mirror filtermap_filtermap .. 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

585 

a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

586 
lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \<longleftrightarrow> (LIM x at_top. f (x::real) :> F)" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

587 
unfolding filterlim_def at_bot_mirror filtermap_filtermap .. 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

588 

50323  589 
lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot.  x :: real :> at_top" 
590 
unfolding filterlim_at_top eventually_at_bot_dense 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

591 
by (metis leI minus_less_iff order_less_asym) 
50323  592 

593 
lemma filterlim_uminus_at_bot_at_top: "LIM x at_top.  x :: real :> at_bot" 

594 
unfolding filterlim_at_bot eventually_at_top_dense 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

595 
by (metis leI less_minus_iff order_less_asym) 
50323  596 

50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

597 
lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \<longleftrightarrow> (LIM x F.  (f x) :: real :> at_bot)" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

598 
using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F] 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

599 
using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x.  f x" F] 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

600 
by auto 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

601 

a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

602 
lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F.  (f x) :: real :> at_top)" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

603 
unfolding filterlim_uminus_at_top by simp 
50323  604 

50347  605 
lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top" 
606 
unfolding filterlim_at_top_gt[where c=0] eventually_within at_def 

607 
proof safe 

608 
fix Z :: real assume [arith]: "0 < Z" 

609 
then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)" 

610 
by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"]) 

611 
then show "eventually (\<lambda>x. x \<in>  {0} \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)" 

612 
by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps) 

613 
qed 

614 

615 
lemma filterlim_inverse_at_top: 

616 
"(f > (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> LIM x F. inverse (f x) :> at_top" 

617 
by (intro filterlim_compose[OF filterlim_inverse_at_top_right]) 

618 
(simp add: filterlim_def eventually_filtermap le_within_iff at_def eventually_elim1) 

619 

620 
lemma filterlim_inverse_at_bot_neg: 

621 
"LIM x (at_left (0::real)). inverse x :> at_bot" 

622 
by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right) 

623 

624 
lemma filterlim_inverse_at_bot: 

625 
"(f > (0 :: real)) F \<Longrightarrow> eventually (\<lambda>x. f x < 0) F \<Longrightarrow> LIM x F. inverse (f x) :> at_bot" 

626 
unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric] 

627 
by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric]) 

628 

50325  629 
lemma tendsto_inverse_0: 
630 
fixes x :: "_ \<Rightarrow> 'a\<Colon>real_normed_div_algebra" 

631 
shows "(inverse > (0::'a)) at_infinity" 

632 
unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity 

633 
proof safe 

634 
fix r :: real assume "0 < r" 

635 
show "\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> norm (inverse x :: 'a) < r" 

636 
proof (intro exI[of _ "inverse (r / 2)"] allI impI) 

637 
fix x :: 'a 

638 
from `0 < r` have "0 < inverse (r / 2)" by simp 

639 
also assume *: "inverse (r / 2) \<le> norm x" 

640 
finally show "norm (inverse x) < r" 

641 
using * `0 < r` by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps) 

642 
qed 

643 
qed 

644 

50347  645 
lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top" 
646 
proof (rule antisym) 

647 
have "(inverse > (0::real)) at_top" 

648 
by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl) 

649 
then show "filtermap inverse at_top \<le> at_right (0::real)" 

650 
unfolding at_within_eq 

651 
by (intro le_withinI) (simp_all add: eventually_filtermap eventually_gt_at_top filterlim_def) 

652 
next 

653 
have "filtermap inverse (filtermap inverse (at_right (0::real))) \<le> filtermap inverse at_top" 

654 
using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono) 

655 
then show "at_right (0::real) \<le> filtermap inverse at_top" 

656 
by (simp add: filtermap_ident filtermap_filtermap) 

657 
qed 

658 

659 
lemma eventually_at_right_to_top: 

660 
"eventually P (at_right (0::real)) \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) at_top" 

661 
unfolding at_right_to_top eventually_filtermap .. 

662 

663 
lemma filterlim_at_right_to_top: 

664 
"filterlim f F (at_right (0::real)) \<longleftrightarrow> (LIM x at_top. f (inverse x) :> F)" 

665 
unfolding filterlim_def at_right_to_top filtermap_filtermap .. 

666 

667 
lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))" 

668 
unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident .. 

669 

670 
lemma eventually_at_top_to_right: 

671 
"eventually P at_top \<longleftrightarrow> eventually (\<lambda>x. P (inverse x)) (at_right (0::real))" 

672 
unfolding at_top_to_right eventually_filtermap .. 

673 

674 
lemma filterlim_at_top_to_right: 

675 
"filterlim f F at_top \<longleftrightarrow> (LIM x (at_right (0::real)). f (inverse x) :> F)" 

676 
unfolding filterlim_def at_top_to_right filtermap_filtermap .. 

677 

50325  678 
lemma filterlim_inverse_at_infinity: 
679 
fixes x :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}" 

680 
shows "filterlim inverse at_infinity (at (0::'a))" 

681 
unfolding filterlim_at_infinity[OF order_refl] 

682 
proof safe 

683 
fix r :: real assume "0 < r" 

684 
then show "eventually (\<lambda>x::'a. r \<le> norm (inverse x)) (at 0)" 

685 
unfolding eventually_at norm_inverse 

686 
by (intro exI[of _ "inverse r"]) 

687 
(auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide) 

688 
qed 

689 

690 
lemma filterlim_inverse_at_iff: 

691 
fixes g :: "'a \<Rightarrow> 'b\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}" 

692 
shows "(LIM x F. inverse (g x) :> at 0) \<longleftrightarrow> (LIM x F. g x :> at_infinity)" 

693 
unfolding filterlim_def filtermap_filtermap[symmetric] 

694 
proof 

695 
assume "filtermap g F \<le> at_infinity" 

696 
then have "filtermap inverse (filtermap g F) \<le> filtermap inverse at_infinity" 

697 
by (rule filtermap_mono) 

698 
also have "\<dots> \<le> at 0" 

699 
using tendsto_inverse_0 

700 
by (auto intro!: le_withinI exI[of _ 1] 

701 
simp: eventually_filtermap eventually_at_infinity filterlim_def at_def) 

702 
finally show "filtermap inverse (filtermap g F) \<le> at 0" . 

703 
next 

704 
assume "filtermap inverse (filtermap g F) \<le> at 0" 

705 
then have "filtermap inverse (filtermap inverse (filtermap g F)) \<le> filtermap inverse (at 0)" 

706 
by (rule filtermap_mono) 

707 
with filterlim_inverse_at_infinity show "filtermap g F \<le> at_infinity" 

708 
by (auto intro: order_trans simp: filterlim_def filtermap_filtermap) 

709 
qed 

710 

50419  711 
lemma tendsto_inverse_0_at_top: 
712 
"LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) > 0) F" 

713 
by (metis at_top_le_at_infinity filterlim_at filterlim_inverse_at_iff filterlim_mono order_refl) 

714 

50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

715 
text {* 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

716 

0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

717 
We only show rules for multiplication and addition when the functions are either against a real 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

718 
value or against infinity. Further rules are easy to derive by using @{thm filterlim_uminus_at_top}. 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

719 

0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

720 
*} 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

721 

0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

722 
lemma filterlim_tendsto_pos_mult_at_top: 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

723 
assumes f: "(f > c) F" and c: "0 < c" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

724 
assumes g: "LIM x F. g x :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

725 
shows "LIM x F. (f x * g x :: real) :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

726 
unfolding filterlim_at_top_gt[where c=0] 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

727 
proof safe 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

728 
fix Z :: real assume "0 < Z" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

729 
from f `0 < c` have "eventually (\<lambda>x. c / 2 < f x) F" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

730 
by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

731 
simp: dist_real_def abs_real_def split: split_if_asm) 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

732 
moreover from g have "eventually (\<lambda>x. (Z / c * 2) \<le> g x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

733 
unfolding filterlim_at_top by auto 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

734 
ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

735 
proof eventually_elim 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

736 
fix x assume "c / 2 < f x" "Z / c * 2 \<le> g x" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

737 
with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) \<le> f x * g x" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

738 
by (intro mult_mono) (auto simp: zero_le_divide_iff) 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

739 
with `0 < c` show "Z \<le> f x * g x" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

740 
by simp 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

741 
qed 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

742 
qed 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

743 

0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

744 
lemma filterlim_at_top_mult_at_top: 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

745 
assumes f: "LIM x F. f x :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

746 
assumes g: "LIM x F. g x :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

747 
shows "LIM x F. (f x * g x :: real) :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

748 
unfolding filterlim_at_top_gt[where c=0] 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

749 
proof safe 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

750 
fix Z :: real assume "0 < Z" 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

751 
from f have "eventually (\<lambda>x. 1 \<le> f x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

752 
unfolding filterlim_at_top by auto 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

753 
moreover from g have "eventually (\<lambda>x. Z \<le> g x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

754 
unfolding filterlim_at_top by auto 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

755 
ultimately show "eventually (\<lambda>x. Z \<le> f x * g x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

756 
proof eventually_elim 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

757 
fix x assume "1 \<le> f x" "Z \<le> g x" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

758 
with `0 < Z` have "1 * Z \<le> f x * g x" 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

759 
by (intro mult_mono) (auto simp: zero_le_divide_iff) 
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

760 
then show "Z \<le> f x * g x" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

761 
by simp 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

762 
qed 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

763 
qed 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

764 

50419  765 
lemma filterlim_tendsto_pos_mult_at_bot: 
766 
assumes "(f > c) F" "0 < (c::real)" "filterlim g at_bot F" 

767 
shows "LIM x F. f x * g x :> at_bot" 

768 
using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\<lambda>x.  g x"] assms(3) 

769 
unfolding filterlim_uminus_at_bot by simp 

770 

50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

771 
lemma filterlim_tendsto_add_at_top: 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

772 
assumes f: "(f > c) F" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

773 
assumes g: "LIM x F. g x :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

774 
shows "LIM x F. (f x + g x :: real) :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

775 
unfolding filterlim_at_top_gt[where c=0] 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

776 
proof safe 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

777 
fix Z :: real assume "0 < Z" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

778 
from f have "eventually (\<lambda>x. c  1 < f x) F" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

779 
by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def) 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

780 
moreover from g have "eventually (\<lambda>x. Z  (c  1) \<le> g x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

781 
unfolding filterlim_at_top by auto 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

782 
ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

783 
by eventually_elim simp 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

784 
qed 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

785 

50347  786 
lemma LIM_at_top_divide: 
787 
fixes f g :: "'a \<Rightarrow> real" 

788 
assumes f: "(f > a) F" "0 < a" 

789 
assumes g: "(g > 0) F" "eventually (\<lambda>x. 0 < g x) F" 

790 
shows "LIM x F. f x / g x :> at_top" 

791 
unfolding divide_inverse 

792 
by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g]) 

793 

50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

794 
lemma filterlim_at_top_add_at_top: 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

795 
assumes f: "LIM x F. f x :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

796 
assumes g: "LIM x F. g x :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

797 
shows "LIM x F. (f x + g x :: real) :> at_top" 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

798 
unfolding filterlim_at_top_gt[where c=0] 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

799 
proof safe 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

800 
fix Z :: real assume "0 < Z" 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

801 
from f have "eventually (\<lambda>x. 0 \<le> f x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

802 
unfolding filterlim_at_top by auto 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

803 
moreover from g have "eventually (\<lambda>x. Z \<le> g x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

804 
unfolding filterlim_at_top by auto 
50346
a75c6429c3c3
add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
hoelzl
parents:
50331
diff
changeset

805 
ultimately show "eventually (\<lambda>x. Z \<le> f x + g x) F" 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

806 
by eventually_elim simp 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

807 
qed 
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

808 

50331  809 
lemma tendsto_divide_0: 
810 
fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}" 

811 
assumes f: "(f > c) F" 

812 
assumes g: "LIM x F. g x :> at_infinity" 

813 
shows "((\<lambda>x. f x / g x) > 0) F" 

814 
using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse) 

815 

816 
lemma linear_plus_1_le_power: 

817 
fixes x :: real 

818 
assumes x: "0 \<le> x" 

819 
shows "real n * x + 1 \<le> (x + 1) ^ n" 

820 
proof (induct n) 

821 
case (Suc n) 

822 
have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)" 

823 
by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x) 

824 
also have "\<dots> \<le> (x + 1)^Suc n" 

825 
using Suc x by (simp add: mult_left_mono) 

826 
finally show ?case . 

827 
qed simp 

828 

829 
lemma filterlim_realpow_sequentially_gt1: 

830 
fixes x :: "'a :: real_normed_div_algebra" 

831 
assumes x[arith]: "1 < norm x" 

832 
shows "LIM n sequentially. x ^ n :> at_infinity" 

833 
proof (intro filterlim_at_infinity[THEN iffD2] allI impI) 

834 
fix y :: real assume "0 < y" 

835 
have "0 < norm x  1" by simp 

836 
then obtain N::nat where "y < real N * (norm x  1)" by (blast dest: reals_Archimedean3) 

837 
also have "\<dots> \<le> real N * (norm x  1) + 1" by simp 

838 
also have "\<dots> \<le> (norm x  1 + 1) ^ N" by (rule linear_plus_1_le_power) simp 

839 
also have "\<dots> = norm x ^ N" by simp 

840 
finally have "\<forall>n\<ge>N. y \<le> norm x ^ n" 

841 
by (metis order_less_le_trans power_increasing order_less_imp_le x) 

842 
then show "eventually (\<lambda>n. y \<le> norm (x ^ n)) sequentially" 

843 
unfolding eventually_sequentially 

844 
by (auto simp: norm_power) 

845 
qed simp 

846 

51471  847 

848 
(* Unfortunately eventually_within was overwritten by Multivariate_Analysis. 

849 
Hence it was references as Limits.within, but now it is Basic_Topology.eventually_within *) 

850 
lemmas eventually_within = eventually_within 

851 

31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

852 
end 
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset

853 