author  paulson <lp15@cam.ac.uk> 
Wed, 09 Oct 2019 14:39:10 +0100  
changeset 70803  2d658afa1fc0 
parent 70723  4e39d87c9737 
child 70804  4eef7c6ef7bf 
permissions  rwrr 
52265  1 
(* Title: HOL/Limits.thy 
51526  2 
Author: Brian Huffman 
3 
Author: Jacques D. Fleuriot, University of Cambridge 

4 
Author: Lawrence C Paulson 

5 
Author: Jeremy Avigad 

31349
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 

60758  8 
section \<open>Limits on Real Vector Spaces\<close> 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

9 

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

10 
theory Limits 
63546  11 
imports Real_Vector_Spaces 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

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

13 

60758  14 
subsection \<open>Filter going to infinity norm\<close> 
51526  15 

63546  16 
definition at_infinity :: "'a::real_normed_vector filter" 
17 
where "at_infinity = (INF r. principal {x. r \<le> norm x})" 

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

18 

57276  19 
lemma eventually_at_infinity: "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)" 
20 
unfolding at_infinity_def 

21 
by (subst eventually_INF_base) 

22 
(auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b]) 

31392  23 

62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62369
diff
changeset

24 
corollary eventually_at_infinity_pos: 
63546  25 
"eventually p at_infinity \<longleftrightarrow> (\<exists>b. 0 < b \<and> (\<forall>x. norm x \<ge> b \<longrightarrow> p x))" 
68614  26 
unfolding eventually_at_infinity 
27 
by (meson le_less_trans norm_ge_zero not_le zero_less_one) 

63546  28 

29 
lemma at_infinity_eq_at_top_bot: "(at_infinity :: real filter) = sup at_top at_bot" 

68614  30 
proof  
31 
have 1: "\<lbrakk>\<forall>n\<ge>u. A n; \<forall>n\<le>v. A n\<rbrakk> 

32 
\<Longrightarrow> \<exists>b. \<forall>x. b \<le> \<bar>x\<bar> \<longrightarrow> A x" for A and u v::real 

33 
by (rule_tac x="max ( v) u" in exI) (auto simp: abs_real_def) 

34 
have 2: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. A n" for A and u::real 

35 
by (meson abs_less_iff le_cases less_le_not_le) 

36 
have 3: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<le>N. A n" for A and u::real 

37 
by (metis (full_types) abs_ge_self abs_minus_cancel le_minus_iff order_trans) 

38 
show ?thesis 

68615  39 
by (auto simp: filter_eq_iff eventually_sup eventually_at_infinity 
68614  40 
eventually_at_top_linorder eventually_at_bot_linorder intro: 1 2 3) 
41 
qed 

50325  42 

57276  43 
lemma at_top_le_at_infinity: "at_top \<le> (at_infinity :: real filter)" 
50325  44 
unfolding at_infinity_eq_at_top_bot by simp 
45 

57276  46 
lemma at_bot_le_at_infinity: "at_bot \<le> (at_infinity :: real filter)" 
50325  47 
unfolding at_infinity_eq_at_top_bot by simp 
48 

63546  49 
lemma filterlim_at_top_imp_at_infinity: "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F" 
50 
for f :: "_ \<Rightarrow> real" 

57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56541
diff
changeset

51 
by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl]) 
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56541
diff
changeset

52 

67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

53 
lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially" 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

54 
by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially) 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

55 

63546  56 
lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially" 
57 
by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially) 

59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

58 

7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

59 

60758  60 
subsubsection \<open>Boundedness\<close> 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

61 

63546  62 
definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" 
63 
where Bfun_metric_def: "Bfun f F = (\<exists>y. \<exists>K>0. eventually (\<lambda>x. dist (f x) y \<le> K) F)" 

64 

65 
abbreviation Bseq :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" 

66 
where "Bseq X \<equiv> Bfun X sequentially" 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

67 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

68 
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" .. 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

69 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

70 
lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

71 
unfolding Bfun_metric_def by (subst eventually_sequentially_seg) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

72 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

73 
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

74 
unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg) 
31355  75 

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

77 
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

78 
proof safe 
63546  79 
fix y K 
80 
assume K: "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F" 

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

81 
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

82 
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

83 
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

84 
by eventually_elim auto 
60758  85 
with \<open>0 < K\<close> show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F" 
51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset

86 
by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto 
62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62369
diff
changeset

87 
qed (force simp del: norm_conv_dist [symmetric]) 
31355  88 

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

89 
lemma BfunI: 
63546  90 
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" 
91 
shows "Bfun f F" 

92 
unfolding Bfun_def 

31355  93 
proof (intro exI conjI allI) 
94 
show "0 < max K 1" by simp 

44195  95 
show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F" 
63546  96 
using K by (rule eventually_mono) simp 
31355  97 
qed 
98 

99 
lemma BfunE: 

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

63546  102 
using assms unfolding Bfun_def by blast 
31355  103 

68614  104 
lemma Cauchy_Bseq: 
105 
assumes "Cauchy X" shows "Bseq X" 

106 
proof  

107 
have "\<exists>y K. 0 < K \<and> (\<exists>N. \<forall>n\<ge>N. dist (X n) y \<le> K)" 

108 
if "\<And>m n. \<lbrakk>m \<ge> M; n \<ge> M\<rbrakk> \<Longrightarrow> dist (X m) (X n) < 1" for M 

109 
by (meson order.order_iff_strict that zero_less_one) 

110 
with assms show ?thesis 

111 
by (force simp: Cauchy_def Bfun_metric_def eventually_sequentially) 

112 
qed 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

113 

60758  114 
subsubsection \<open>Bounded Sequences\<close> 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

115 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

116 
lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

117 
by (intro BfunI) (auto simp: eventually_sequentially) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

118 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

119 
lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

120 
by (intro BfunI) (auto simp: eventually_sequentially) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

121 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

122 
lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

123 
unfolding Bfun_def eventually_sequentially 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

124 
proof safe 
63546  125 
fix N K 
126 
assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K" 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

127 
then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54263
diff
changeset

128 
by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2) 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

129 
(auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

130 
qed auto 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

131 

63546  132 
lemma BseqE: "Bseq X \<Longrightarrow> (\<And>K. 0 < K \<Longrightarrow> \<forall>n. norm (X n) \<le> K \<Longrightarrow> Q) \<Longrightarrow> Q" 
133 
unfolding Bseq_def by auto 

134 

135 
lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K. 0 < K \<and> (\<forall>n. norm (X n) \<le> K)" 

136 
by (simp add: Bseq_def) 

137 

138 
lemma BseqI: "0 < K \<Longrightarrow> \<forall>n. norm (X n) \<le> K \<Longrightarrow> Bseq X" 

68615  139 
by (auto simp: Bseq_def) 
63546  140 

141 
lemma Bseq_bdd_above: "Bseq X \<Longrightarrow> bdd_above (range X)" 

142 
for X :: "nat \<Rightarrow> real" 

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

143 
proof (elim BseqE, intro bdd_aboveI2) 
63546  144 
fix K n 
145 
assume "0 < K" "\<forall>n. norm (X n) \<le> K" 

146 
then show "X n \<le> K" 

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

147 
by (auto elim!: allE[of _ n]) 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

148 
qed 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

149 

63546  150 
lemma Bseq_bdd_above': "Bseq X \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))" 
151 
for X :: "nat \<Rightarrow> 'a :: real_normed_vector" 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

152 
proof (elim BseqE, intro bdd_aboveI2) 
63546  153 
fix K n 
154 
assume "0 < K" "\<forall>n. norm (X n) \<le> K" 

155 
then show "norm (X n) \<le> K" 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

156 
by (auto elim!: allE[of _ n]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

157 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

158 

63546  159 
lemma Bseq_bdd_below: "Bseq X \<Longrightarrow> bdd_below (range X)" 
160 
for X :: "nat \<Rightarrow> real" 

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

161 
proof (elim BseqE, intro bdd_belowI2) 
63546  162 
fix K n 
163 
assume "0 < K" "\<forall>n. norm (X n) \<le> K" 

164 
then show " K \<le> X n" 

54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

165 
by (auto elim!: allE[of _ n]) 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

166 
qed 
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset

167 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

168 
lemma Bseq_eventually_mono: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

169 
assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g" 
63546  170 
shows "Bseq f" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

171 
proof  
67958
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset

172 
from assms(2) obtain K where "0 < K" and "eventually (\<lambda>n. norm (g n) \<le> K) sequentially" 
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset

173 
unfolding Bfun_def by fast 
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset

174 
with assms(1) have "eventually (\<lambda>n. norm (f n) \<le> K) sequentially" 
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset

175 
by (fast elim: eventually_elim2 order_trans) 
69272  176 
with \<open>0 < K\<close> show "Bseq f" 
67958
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset

177 
unfolding Bfun_def by fast 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

178 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

179 

63546  180 
lemma lemma_NBseq_def: "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

181 
proof safe 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

182 
fix K :: real 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

183 
from reals_Archimedean2 obtain n :: nat where "K < real n" .. 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

184 
then have "K \<le> real (Suc n)" by auto 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

185 
moreover assume "\<forall>m. norm (X m) \<le> K" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

186 
ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

187 
by (blast intro: order_trans) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

188 
then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" .. 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

189 
next 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

190 
show "\<And>N. \<forall>n. norm (X n) \<le> real (Suc N) \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K" 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

191 
using of_nat_0_less_iff by blast 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

192 
qed 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

193 

63546  194 
text \<open>Alternative definition for \<open>Bseq\<close>.\<close> 
195 
lemma Bseq_iff: "Bseq X \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" 

196 
by (simp add: Bseq_def) (simp add: lemma_NBseq_def) 

197 

198 
lemma lemma_NBseq_def2: "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" 

68614  199 
proof  
200 
have *: "\<And>N. \<forall>n. norm (X n) \<le> 1 + real N \<Longrightarrow> 

201 
\<exists>N. \<forall>n. norm (X n) < 1 + real N" 

202 
by (metis add.commute le_less_trans less_add_one of_nat_Suc) 

203 
then show ?thesis 

204 
unfolding lemma_NBseq_def 

205 
by (metis less_le_not_le not_less_iff_gr_or_eq of_nat_Suc) 

206 
qed 

63546  207 

208 
text \<open>Yet another definition for Bseq.\<close> 

209 
lemma Bseq_iff1a: "Bseq X \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) < real (Suc N))" 

210 
by (simp add: Bseq_def lemma_NBseq_def2) 

211 

212 
subsubsection \<open>A Few More Equivalence Theorems for Boundedness\<close> 

213 

214 
text \<open>Alternative formulation for boundedness.\<close> 

215 
lemma Bseq_iff2: "Bseq X \<longleftrightarrow> (\<exists>k > 0. \<exists>x. \<forall>n. norm (X n +  x) \<le> k)" 

68614  216 
by (metis BseqE BseqI' add.commute add_cancel_right_left add_uminus_conv_diff norm_add_leD 
217 
norm_minus_cancel norm_minus_commute) 

63546  218 

219 
text \<open>Alternative formulation for boundedness.\<close> 

220 
lemma Bseq_iff3: "Bseq X \<longleftrightarrow> (\<exists>k>0. \<exists>N. \<forall>n. norm (X n +  X N) \<le> k)" 

221 
(is "?P \<longleftrightarrow> ?Q") 

53602  222 
proof 
223 
assume ?P 

63546  224 
then obtain K where *: "0 < K" and **: "\<And>n. norm (X n) \<le> K" 
68615  225 
by (auto simp: Bseq_def) 
53602  226 
from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset

227 
from ** have "\<forall>n. norm (X n  X 0) \<le> K + norm (X 0)" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset

228 
by (auto intro: order_trans norm_triangle_ineq4) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset

229 
then have "\<forall>n. norm (X n +  X 0) \<le> K + norm (X 0)" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset

230 
by simp 
60758  231 
with \<open>0 < K + norm (X 0)\<close> show ?Q by blast 
53602  232 
next 
63546  233 
assume ?Q 
68615  234 
then show ?P by (auto simp: Bseq_iff2) 
53602  235 
qed 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

236 

63546  237 

238 
subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close> 

239 

240 
lemma Bseq_minus_iff: "Bseq (\<lambda>n.  (X n) :: 'a::real_normed_vector) \<longleftrightarrow> Bseq X" 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

241 
by (simp add: Bseq_def) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

242 

62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

243 
lemma Bseq_add: 
63546  244 
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" 
245 
assumes "Bseq f" 

246 
shows "Bseq (\<lambda>x. f x + c)" 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

247 
proof  
63546  248 
from assms obtain K where K: "\<And>x. norm (f x) \<le> K" 
249 
unfolding Bseq_def by blast 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

250 
{ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

251 
fix x :: nat 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

252 
have "norm (f x + c) \<le> norm (f x) + norm c" by (rule norm_triangle_ineq) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

253 
also have "norm (f x) \<le> K" by (rule K) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

254 
finally have "norm (f x + c) \<le> K + norm c" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

255 
} 
63546  256 
then show ?thesis by (rule BseqI') 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

257 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

258 

63546  259 
lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq f" 
260 
for f :: "nat \<Rightarrow> 'a::real_normed_vector" 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

261 
using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "c"] by auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

262 

62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

263 
lemma Bseq_mult: 
63546  264 
fixes f g :: "nat \<Rightarrow> 'a::real_normed_field" 
265 
assumes "Bseq f" and "Bseq g" 

266 
shows "Bseq (\<lambda>x. f x * g x)" 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

267 
proof  
63546  268 
from assms obtain K1 K2 where K: "norm (f x) \<le> K1" "K1 > 0" "norm (g x) \<le> K2" "K2 > 0" 
269 
for x 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

270 
unfolding Bseq_def by blast 
63546  271 
then have "norm (f x * g x) \<le> K1 * K2" for x 
272 
by (auto simp: norm_mult intro!: mult_mono) 

273 
then show ?thesis by (rule BseqI') 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

274 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

275 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

276 
lemma Bfun_const [simp]: "Bfun (\<lambda>_. c) F" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

277 
unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

278 

63546  279 
lemma Bseq_cmult_iff: 
280 
fixes c :: "'a::real_normed_field" 

281 
assumes "c \<noteq> 0" 

282 
shows "Bseq (\<lambda>x. c * f x) \<longleftrightarrow> Bseq f" 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

283 
proof 
63546  284 
assume "Bseq (\<lambda>x. c * f x)" 
285 
with Bfun_const have "Bseq (\<lambda>x. inverse c * (c * f x))" 

286 
by (rule Bseq_mult) 

287 
with \<open>c \<noteq> 0\<close> show "Bseq f" 

288 
by (simp add: divide_simps) 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

289 
qed (intro Bseq_mult Bfun_const) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

290 

63546  291 
lemma Bseq_subseq: "Bseq f \<Longrightarrow> Bseq (\<lambda>x. f (g x))" 
292 
for f :: "nat \<Rightarrow> 'a::real_normed_vector" 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

293 
unfolding Bseq_def by auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

294 

63546  295 
lemma Bseq_Suc_iff: "Bseq (\<lambda>n. f (Suc n)) \<longleftrightarrow> Bseq f" 
296 
for f :: "nat \<Rightarrow> 'a::real_normed_vector" 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

297 
using Bseq_offset[of f 1] by (auto intro: Bseq_subseq) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

298 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

299 
lemma increasing_Bseq_subseq_iff: 
66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
65680
diff
changeset

300 
assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "strict_mono g" 
63546  301 
shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

302 
proof 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

303 
assume "Bseq (\<lambda>x. f (g x))" 
63546  304 
then obtain K where K: "\<And>x. norm (f (g x)) \<le> K" 
305 
unfolding Bseq_def by auto 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

306 
{ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

307 
fix x :: nat 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

308 
from filterlim_subseq[OF assms(2)] obtain y where "g y \<ge> x" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

309 
by (auto simp: filterlim_at_top eventually_at_top_linorder) 
63546  310 
then have "norm (f x) \<le> norm (f (g y))" 
311 
using assms(1) by blast 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

312 
also have "norm (f (g y)) \<le> K" by (rule K) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

313 
finally have "norm (f x) \<le> K" . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

314 
} 
63546  315 
then show "Bseq f" by (rule BseqI') 
316 
qed (use Bseq_subseq[of f g] in simp_all) 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

317 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

318 
lemma nonneg_incseq_Bseq_subseq_iff: 
63546  319 
fixes f :: "nat \<Rightarrow> real" 
320 
and g :: "nat \<Rightarrow> nat" 

66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
65680
diff
changeset

321 
assumes "\<And>x. f x \<ge> 0" "incseq f" "strict_mono g" 
63546  322 
shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

323 
using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

324 

63546  325 
lemma Bseq_eq_bounded: "range f \<subseteq> {a..b} \<Longrightarrow> Bseq f" 
326 
for a b :: real 

68614  327 
proof (rule BseqI'[where K="max (norm a) (norm b)"]) 
328 
fix n assume "range f \<subseteq> {a..b}" 

329 
then have "f n \<in> {a..b}" 

330 
by blast 

331 
then show "norm (f n) \<le> max (norm a) (norm b)" 

332 
by auto 

333 
qed 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

334 

63546  335 
lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> B \<Longrightarrow> Bseq X" 
336 
for B :: real 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

337 
by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

338 

63546  339 
lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. B \<le> X i \<Longrightarrow> Bseq X" 
340 
for B :: real 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

341 
by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

342 

63546  343 

60758  344 
subsection \<open>Convergence to Zero\<close> 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

345 

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

346 
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" 
44195  347 
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

348 

63546  349 
lemma ZfunI: "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F) \<Longrightarrow> Zfun f F" 
350 
by (simp add: Zfun_def) 

351 

352 
lemma ZfunD: "Zfun f F \<Longrightarrow> 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F" 

353 
by (simp add: Zfun_def) 

354 

355 
lemma Zfun_ssubst: "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

356 
unfolding Zfun_def by (auto elim!: eventually_rev_mp) 
31355  357 

44195  358 
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

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

360 

44195  361 
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

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

363 

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

364 
lemma Zfun_imp_Zfun: 
44195  365 
assumes f: "Zfun f F" 
63546  366 
and g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F" 
44195  367 
shows "Zfun (\<lambda>x. g x) F" 
63546  368 
proof (cases "0 < K") 
369 
case K: True 

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

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

371 
proof (rule ZfunI) 
63546  372 
fix r :: real 
373 
assume "0 < r" 

374 
then have "0 < r / K" using K by simp 

44195  375 
then have "eventually (\<lambda>x. norm (f x) < r / K) F" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

376 
using ZfunD [OF f] by blast 
44195  377 
with g show "eventually (\<lambda>x. norm (g x) < r) F" 
46887  378 
proof eventually_elim 
379 
case (elim x) 

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

381 
by (simp add: pos_less_divide_eq K) 
63546  382 
then show ?case 
46887  383 
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

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

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

386 
next 
63546  387 
case False 
388 
then have K: "K \<le> 0" by (simp only: not_less) 

31355  389 
show ?thesis 
390 
proof (rule ZfunI) 

391 
fix r :: real 

392 
assume "0 < r" 

44195  393 
from g show "eventually (\<lambda>x. norm (g x) < r) F" 
46887  394 
proof eventually_elim 
395 
case (elim x) 

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

31355  397 
using K norm_ge_zero by (rule mult_left_mono) 
46887  398 
finally show ?case 
60758  399 
using \<open>0 < r\<close> by simp 
31355  400 
qed 
401 
qed 

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

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

403 

63546  404 
lemma Zfun_le: "Zfun g F \<Longrightarrow> \<forall>x. norm (f x) \<le> norm (g x) \<Longrightarrow> Zfun f F" 
405 
by (erule Zfun_imp_Zfun [where K = 1]) simp 

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

406 

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

407 
lemma Zfun_add: 
63546  408 
assumes f: "Zfun f F" 
409 
and g: "Zfun g F" 

44195  410 
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

411 
proof (rule ZfunI) 
63546  412 
fix r :: real 
413 
assume "0 < r" 

414 
then have r: "0 < r / 2" by simp 

44195  415 
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

416 
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

417 
moreover 
44195  418 
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

419 
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

420 
ultimately 
44195  421 
show "eventually (\<lambda>x. norm (f x + g x) < r) F" 
46887  422 
proof eventually_elim 
423 
case (elim x) 

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

424 
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

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

426 
also have "\<dots> < r/2 + r/2" 
46887  427 
using elim by (rule add_strict_mono) 
428 
finally show ?case 

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

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

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

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

432 

44195  433 
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

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

435 

63546  436 
lemma Zfun_diff: "Zfun f F \<Longrightarrow> Zfun g F \<Longrightarrow> Zfun (\<lambda>x. f x  g x) F" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset

437 
using Zfun_add [of f F "\<lambda>x.  g x"] by (simp add: Zfun_minus) 
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset

438 

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

439 
lemma (in bounded_linear) Zfun: 
44195  440 
assumes g: "Zfun g F" 
441 
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

442 
proof  
63546  443 
obtain K where "norm (f x) \<le> norm x * K" for x 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

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

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

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

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

450 

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

451 
lemma (in bounded_bilinear) Zfun: 
44195  452 
assumes f: "Zfun f F" 
63546  453 
and g: "Zfun g F" 
44195  454 
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

455 
proof (rule ZfunI) 
63546  456 
fix r :: real 
457 
assume r: "0 < r" 

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

458 
obtain K where K: "0 < K" 
63546  459 
and norm_le: "norm (x ** y) \<le> norm x * norm y * K" for x y 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

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

461 
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

462 
by (rule positive_imp_inverse_positive) 
44195  463 
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

464 
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

465 
moreover 
44195  466 
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

467 
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

468 
ultimately 
44195  469 
show "eventually (\<lambda>x. norm (f x ** g x) < r) F" 
46887  470 
proof eventually_elim 
471 
case (elim x) 

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

472 
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

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

474 
also have "norm (f x) * norm (g x) * K < r * inverse K * K" 
46887  475 
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

476 
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

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

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

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

481 

63546  482 
lemma (in bounded_bilinear) Zfun_left: "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

483 
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

484 

63546  485 
lemma (in bounded_bilinear) Zfun_right: "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

486 
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

487 

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

488 
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

489 
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

490 
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

491 

61973  492 
lemma tendsto_Zfun_iff: "(f \<longlongrightarrow> 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

493 
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

494 

63546  495 
lemma tendsto_0_le: 
496 
"(f \<longlongrightarrow> 0) F \<Longrightarrow> eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F \<Longrightarrow> (g \<longlongrightarrow> 0) F" 

56366  497 
by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) 
498 

63546  499 

60758  500 
subsubsection \<open>Distance and norms\<close> 
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset

501 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

502 
lemma tendsto_dist [tendsto_intros]: 
63546  503 
fixes l m :: "'a::metric_space" 
504 
assumes f: "(f \<longlongrightarrow> l) F" 

505 
and g: "(g \<longlongrightarrow> m) F" 

61973  506 
shows "((\<lambda>x. dist (f x) (g x)) \<longlongrightarrow> dist l m) F" 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

507 
proof (rule tendstoI) 
63546  508 
fix e :: real 
509 
assume "0 < e" 

510 
then have e2: "0 < e/2" by simp 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

511 
from tendstoD [OF f e2] tendstoD [OF g e2] 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

512 
show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

513 
proof (eventually_elim) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

514 
case (elim x) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

515 
then show "dist (dist (f x) (g x)) (dist l m) < e" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

516 
unfolding dist_real_def 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

517 
using dist_triangle2 [of "f x" "g x" "l"] 
63546  518 
and dist_triangle2 [of "g x" "l" "m"] 
519 
and dist_triangle3 [of "l" "m" "f x"] 

520 
and dist_triangle [of "f x" "m" "g x"] 

51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

521 
by arith 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

522 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

523 
qed 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

524 

f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

525 
lemma continuous_dist[continuous_intros]: 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

526 
fixes f g :: "_ \<Rightarrow> 'a :: metric_space" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

527 
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

528 
unfolding continuous_def by (rule tendsto_dist) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

529 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

530 
lemma continuous_on_dist[continuous_intros]: 
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

531 
fixes f g :: "_ \<Rightarrow> 'a :: metric_space" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

532 
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))" 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

533 
unfolding continuous_on_def by (auto intro: tendsto_dist) 
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset

534 

69918
eddcc7c726f3
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset

535 
lemma continuous_at_dist: "isCont (dist a) b" 
eddcc7c726f3
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset

536 
using continuous_on_dist [OF continuous_on_const continuous_on_id] continuous_on_eq_continuous_within by blast 
eddcc7c726f3
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
paulson <lp15@cam.ac.uk>
parents:
69593
diff
changeset

537 

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

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

540 

63546  541 
lemma continuous_norm [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))" 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

542 
unfolding continuous_def by (rule tendsto_norm) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

543 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

544 
lemma continuous_on_norm [continuous_intros]: 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

545 
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

546 
unfolding continuous_on_def by (auto intro: tendsto_norm) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

547 

63546  548 
lemma tendsto_norm_zero: "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F" 
549 
by (drule tendsto_norm) simp 

550 

551 
lemma tendsto_norm_zero_cancel: "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> 0) F" 

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

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

553 

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

555 
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

556 

63546  557 
lemma tendsto_rabs [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> \<bar>l\<bar>) F" 
558 
for l :: real 

559 
by (fold real_norm_def) (rule tendsto_norm) 

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

560 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

561 
lemma continuous_rabs [continuous_intros]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

562 
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

563 
unfolding real_norm_def[symmetric] by (rule continuous_norm) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

564 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

565 
lemma continuous_on_rabs [continuous_intros]: 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

566 
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

567 
unfolding real_norm_def[symmetric] by (rule continuous_on_norm) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

568 

63546  569 
lemma tendsto_rabs_zero: "(f \<longlongrightarrow> (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> 0) F" 
570 
by (fold real_norm_def) (rule tendsto_norm_zero) 

571 

572 
lemma tendsto_rabs_zero_cancel: "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<Longrightarrow> (f \<longlongrightarrow> 0) F" 

573 
by (fold real_norm_def) (rule tendsto_norm_zero_cancel) 

574 

575 
lemma tendsto_rabs_zero_iff: "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F" 

576 
by (fold real_norm_def) (rule tendsto_norm_zero_iff) 

577 

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

578 

62368  579 
subsection \<open>Topological Monoid\<close> 
580 

581 
class topological_monoid_add = topological_space + monoid_add + 

582 
assumes tendsto_add_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x + snd x :> nhds (a + b)" 

583 

584 
class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add 

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

585 

31565  586 
lemma tendsto_add [tendsto_intros]: 
62368  587 
fixes a b :: "'a::topological_monoid_add" 
588 
shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F" 

589 
using filterlim_compose[OF tendsto_add_Pair, of "\<lambda>x. (f x, g x)" a b F] 

590 
by (simp add: nhds_prod[symmetric] tendsto_Pair) 

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

591 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

592 
lemma continuous_add [continuous_intros]: 
62368  593 
fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

594 
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

595 
unfolding continuous_def by (rule tendsto_add) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

596 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

597 
lemma continuous_on_add [continuous_intros]: 
62368  598 
fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

599 
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

600 
unfolding continuous_on_def by (auto intro: tendsto_add) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

601 

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

602 
lemma tendsto_add_zero: 
62368  603 
fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" 
63546  604 
shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> (g \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> 0) F" 
605 
by (drule (1) tendsto_add) simp 

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

606 

64267  607 
lemma tendsto_sum [tendsto_intros]: 
62368  608 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add" 
63915  609 
shows "(\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F) \<Longrightarrow> ((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F" 
610 
by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add) 

62368  611 

67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

612 
lemma tendsto_null_sum: 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

613 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add" 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

614 
assumes "\<And>i. i \<in> I \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> 0) F" 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

615 
shows "((\<lambda>i. sum (f i) I) \<longlongrightarrow> 0) F" 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

616 
using tendsto_sum [of I "\<lambda>x y. f y x" "\<lambda>x. 0"] assms by simp 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

617 

64267  618 
lemma continuous_sum [continuous_intros]: 
62368  619 
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add" 
63301  620 
shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)" 
64267  621 
unfolding continuous_def by (rule tendsto_sum) 
622 

623 
lemma continuous_on_sum [continuous_intros]: 

62368  624 
fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_add" 
63301  625 
shows "(\<And>i. i \<in> I \<Longrightarrow> continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<Sum>i\<in>I. f i x)" 
64267  626 
unfolding continuous_on_def by (auto intro: tendsto_sum) 
62368  627 

62369  628 
instance nat :: topological_comm_monoid_add 
63546  629 
by standard 
630 
(simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) 

62369  631 

632 
instance int :: topological_comm_monoid_add 

63546  633 
by standard 
634 
(simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) 

635 

62369  636 

63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

637 
subsubsection \<open>Topological group\<close> 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

638 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

639 
class topological_group_add = topological_monoid_add + group_add + 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

640 
assumes tendsto_uminus_nhds: "(uminus \<longlongrightarrow>  a) (nhds a)" 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

641 
begin 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

642 

63546  643 
lemma tendsto_minus [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x.  f x) \<longlongrightarrow>  a) F" 
63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

644 
by (rule filterlim_compose[OF tendsto_uminus_nhds]) 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

645 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

646 
end 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

647 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

648 
class topological_ab_group_add = topological_group_add + ab_group_add 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

649 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

650 
instance topological_ab_group_add < topological_comm_monoid_add .. 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

651 

63546  652 
lemma continuous_minus [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x.  f x)" 
653 
for f :: "'a::t2_space \<Rightarrow> 'b::topological_group_add" 

63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

654 
unfolding continuous_def by (rule tendsto_minus) 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

655 

63546  656 
lemma continuous_on_minus [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x.  f x)" 
657 
for f :: "_ \<Rightarrow> 'b::topological_group_add" 

63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

658 
unfolding continuous_on_def by (auto intro: tendsto_minus) 
62368  659 

63546  660 
lemma tendsto_minus_cancel: "((\<lambda>x.  f x) \<longlongrightarrow>  a) F \<Longrightarrow> (f \<longlongrightarrow> a) F" 
661 
for a :: "'a::topological_group_add" 

662 
by (drule tendsto_minus) simp 

63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

663 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

664 
lemma tendsto_minus_cancel_left: 
63546  665 
"(f \<longlongrightarrow>  (y::_::topological_group_add)) F \<longleftrightarrow> ((\<lambda>x.  f x) \<longlongrightarrow> y) F" 
63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

666 
using tendsto_minus_cancel[of f " y" F] tendsto_minus[of f " y" F] 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

667 
by auto 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

668 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

669 
lemma tendsto_diff [tendsto_intros]: 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

670 
fixes a b :: "'a::topological_group_add" 
63546  671 
shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x  g x) \<longlongrightarrow> a  b) F" 
63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

672 
using tendsto_add [of f a F "\<lambda>x.  g x" " b"] by (simp add: tendsto_minus) 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

673 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

674 
lemma continuous_diff [continuous_intros]: 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

675 
fixes f g :: "'a::t2_space \<Rightarrow> 'b::topological_group_add" 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

676 
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x  g x)" 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

677 
unfolding continuous_def by (rule tendsto_diff) 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

678 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

679 
lemma continuous_on_diff [continuous_intros]: 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

680 
fixes f g :: "_ \<Rightarrow> 'b::topological_group_add" 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

681 
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x  g x)" 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

682 
unfolding continuous_on_def by (auto intro: tendsto_diff) 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

683 

67399  684 
lemma continuous_on_op_minus: "continuous_on (s::'a::topological_group_add set) (() x)" 
63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

685 
by (rule continuous_intros  simp)+ 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

686 

5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

687 
instance real_normed_vector < topological_ab_group_add 
62368  688 
proof 
63546  689 
fix a b :: 'a 
690 
show "((\<lambda>x. fst x + snd x) \<longlongrightarrow> a + b) (nhds a \<times>\<^sub>F nhds b)" 

62368  691 
unfolding tendsto_Zfun_iff add_diff_add 
692 
using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"] 

693 
by (intro Zfun_add) 

68615  694 
(auto simp: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst) 
63081
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

695 
show "(uminus \<longlongrightarrow>  a) (nhds a)" 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

696 
unfolding tendsto_Zfun_iff minus_diff_minus 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

697 
using filterlim_ident[of "nhds a"] 
5a5beb3dbe7e
introduced class topological_group between topological_monoid and real_normed_vector
immler
parents:
63040
diff
changeset

698 
by (intro Zfun_minus) (simp add: tendsto_Zfun_iff) 
62368  699 
qed 
700 

65204
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
65036
diff
changeset

701 
lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real] 
50999  702 

63546  703 

60758  704 
subsubsection \<open>Linear operators and multiplication\<close> 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

705 

63546  706 
lemma linear_times: "linear (\<lambda>x. c * x)" 
707 
for c :: "'a::real_algebra" 

61806
d2e62ae01cd8
Cauchy's integral formula for circles. Starting to fix eventually_mono.
paulson <lp15@cam.ac.uk>
parents:
61799
diff
changeset

708 
by (auto simp: linearI distrib_left) 
d2e62ae01cd8
Cauchy's integral formula for circles. Starting to fix eventually_mono.
paulson <lp15@cam.ac.uk>
parents:
61799
diff
changeset

709 

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

711 
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

712 

63546  713 
lemma (in bounded_linear) continuous: "continuous F g \<Longrightarrow> continuous F (\<lambda>x. f (g x))" 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

714 
using tendsto[of g _ F] by (auto simp: continuous_def) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

715 

63546  716 
lemma (in bounded_linear) continuous_on: "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))" 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

717 
using tendsto[of g] by (auto simp: continuous_on_def) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

718 

63546  719 
lemma (in bounded_linear) tendsto_zero: "(g \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f (g x)) \<longlongrightarrow> 0) F" 
720 
by (drule tendsto) (simp only: zero) 

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

721 

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

722 
lemma (in bounded_bilinear) tendsto: 
63546  723 
"(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x ** g x) \<longlongrightarrow> a ** b) F" 
724 
by (simp only: tendsto_Zfun_iff prod_diff_prod 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

725 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

726 
lemma (in bounded_bilinear) continuous: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

727 
"continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x ** g x)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

728 
using tendsto[of f _ F g] by (auto simp: continuous_def) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

729 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

730 
lemma (in bounded_bilinear) continuous_on: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

731 
"continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

732 
using tendsto[of f _ _ g] by (auto simp: continuous_on_def) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

733 

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

734 
lemma (in bounded_bilinear) tendsto_zero: 
61973  735 
assumes f: "(f \<longlongrightarrow> 0) F" 
63546  736 
and g: "(g \<longlongrightarrow> 0) F" 
61973  737 
shows "((\<lambda>x. f x ** g x) \<longlongrightarrow> 0) F" 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

738 
using tendsto [OF f g] by (simp add: zero_left) 
31355  739 

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

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

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

743 

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

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

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

747 

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

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

749 
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

750 

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

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

752 
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

753 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

754 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

755 
text\<open>Analogous type class for multiplication\<close> 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

756 
class topological_semigroup_mult = topological_space + semigroup_mult + 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

757 
assumes tendsto_mult_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x * snd x :> nhds (a * b)" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

758 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

759 
instance real_normed_algebra < topological_semigroup_mult 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

760 
proof 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

761 
fix a b :: 'a 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

762 
show "((\<lambda>x. fst x * snd x) \<longlongrightarrow> a * b) (nhds a \<times>\<^sub>F nhds b)" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

763 
unfolding nhds_prod[symmetric] 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

764 
using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"] 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

765 
by (simp add: bounded_bilinear.tendsto [OF bounded_bilinear_mult]) 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

766 
qed 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

767 

b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

768 
lemma tendsto_mult [tendsto_intros]: 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

769 
fixes a b :: "'a::topological_semigroup_mult" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

770 
shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x * g x) \<longlongrightarrow> a * b) F" 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

771 
using filterlim_compose[OF tendsto_mult_Pair, of "\<lambda>x. (f x, g x)" a b F] 
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

772 
by (simp add: nhds_prod[symmetric] tendsto_Pair) 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

773 

63546  774 
lemma tendsto_mult_left: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. c * (f x)) \<longlongrightarrow> c * l) F" 
68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

775 
for c :: "'a::topological_semigroup_mult" 
63546  776 
by (rule tendsto_mult [OF tendsto_const]) 
777 

778 
lemma tendsto_mult_right: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. (f x) * c) \<longlongrightarrow> l * c) F" 

68064
b249fab48c76
type class generalisations; some work on infinite products
paulson <lp15@cam.ac.uk>
parents:
67958
diff
changeset

779 
for c :: "'a::topological_semigroup_mult" 
63546  780 
by (rule tendsto_mult [OF _ tendsto_const]) 
61806
d2e62ae01cd8
Cauchy's integral formula for circles. Starting to fix eventually_mono.
paulson <lp15@cam.ac.uk>
parents:
61799
diff
changeset

781 

70803
2d658afa1fc0
Generalised two results concerning limits from the real numbers to type classes
paulson <lp15@cam.ac.uk>
parents:
70723
diff
changeset

782 
lemma tendsto_mult_left_iff: 
2d658afa1fc0
Generalised two results concerning limits from the real numbers to type classes
paulson <lp15@cam.ac.uk>
parents:
70723
diff
changeset

783 
"c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}" 
70688
3d894e1cfc75
new material on Analysis, plus some rearrangements
paulson <lp15@cam.ac.uk>
parents:
70532
diff
changeset

784 
by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"]) 
3d894e1cfc75
new material on Analysis, plus some rearrangements
paulson <lp15@cam.ac.uk>
parents:
70532
diff
changeset

785 

70803
2d658afa1fc0
Generalised two results concerning limits from the real numbers to type classes
paulson <lp15@cam.ac.uk>
parents:
70723
diff
changeset

786 
lemma tendsto_mult_right_iff: 
2d658afa1fc0
Generalised two results concerning limits from the real numbers to type classes
paulson <lp15@cam.ac.uk>
parents:
70723
diff
changeset

787 
"c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: "'a::{topological_semigroup_mult,field}" 
2d658afa1fc0
Generalised two results concerning limits from the real numbers to type classes
paulson <lp15@cam.ac.uk>
parents:
70723
diff
changeset

788 
by (auto simp: tendsto_mult_right dest: tendsto_mult_left [where c = "1/c"]) 
70688
3d894e1cfc75
new material on Analysis, plus some rearrangements
paulson <lp15@cam.ac.uk>
parents:
70532
diff
changeset

789 

70365
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

790 
lemma lim_const_over_n [tendsto_intros]: 
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

791 
fixes a :: "'a::real_normed_field" 
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

792 
shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0" 
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

793 
using tendsto_mult [OF tendsto_const [of a] lim_1_over_n] by simp 
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
69918
diff
changeset

794 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

795 
lemmas continuous_of_real [continuous_intros] = 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

796 
bounded_linear.continuous [OF bounded_linear_of_real] 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

797 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

798 
lemmas continuous_scaleR [continuous_intros] = 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

799 
bounded_bilinear.continuous [OF bounded_bilinear_scaleR] 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

800 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

801 
lemmas continuous_mult [continuous_intros] = 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

802 
bounded_bilinear.continuous [OF bounded_bilinear_mult] 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

803 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

804 
lemmas continuous_on_of_real [continuous_intros] = 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

805 
bounded_linear.continuous_on [OF bounded_linear_of_real] 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

806 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

807 
lemmas continuous_on_scaleR [continuous_intros] = 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

808 
bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR] 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

809 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

810 
lemmas continuous_on_mult [continuous_intros] = 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

811 
bounded_bilinear.continuous_on [OF bounded_bilinear_mult] 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

812 

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

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

814 
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

815 

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

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

817 
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

818 

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

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

820 
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

821 

68296
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

822 

69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

823 
lemma continuous_mult_left: 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

824 
fixes c::"'a::real_normed_algebra" 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

825 
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)" 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

826 
by (rule continuous_mult [OF continuous_const]) 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

827 

69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

828 
lemma continuous_mult_right: 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

829 
fixes c::"'a::real_normed_algebra" 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

830 
shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x * c)" 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

831 
by (rule continuous_mult [OF _ continuous_const]) 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

832 

69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

833 
lemma continuous_on_mult_left: 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

834 
fixes c::"'a::real_normed_algebra" 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

835 
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c * f x)" 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

836 
by (rule continuous_on_mult [OF continuous_on_const]) 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

837 

69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

838 
lemma continuous_on_mult_right: 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

839 
fixes c::"'a::real_normed_algebra" 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

840 
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)" 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

841 
by (rule continuous_on_mult [OF _ continuous_on_const]) 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

842 

69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

843 
lemma continuous_on_mult_const [simp]: 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

844 
fixes c::"'a::real_normed_algebra" 
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68860
diff
changeset

845 
shows "continuous_on s ((*) c)" 
68296
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

846 
by (intro continuous_on_mult_left continuous_on_id) 
69d680e94961
tidying and reorganisation around Cauchy Integral Theorem
paulson <lp15@cam.ac.uk>
parents:
68064
diff
changeset

847 

66793
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66456
diff
changeset

848 
lemma tendsto_divide_zero: 
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66456
diff
changeset

849 
fixes c :: "'a::real_normed_field" 
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66456
diff
changeset

850 
shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x / c) \<longlongrightarrow> 0) F" 
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66456
diff
changeset

851 
by (cases "c=0") (simp_all add: divide_inverse tendsto_mult_left_zero) 
deabce3ccf1f
new material about connectedness, etc.
paulson <lp15@cam.ac.uk>
parents:
66456
diff
changeset

852 

63546  853 
lemma tendsto_power [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> a ^ n) F" 
854 
for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}" 

58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57512
diff
changeset

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

856 

65680
378a2f11bec9
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset

857 
lemma tendsto_null_power: "\<lbrakk>(f \<longlongrightarrow> 0) F; 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ^ n) \<longlongrightarrow> 0) F" 
378a2f11bec9
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset

858 
for f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra_1}" 
378a2f11bec9
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset

859 
using tendsto_power [of f 0 F n] by (simp add: power_0_left) 
378a2f11bec9
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset

860 

63546  861 
lemma continuous_power [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)" 
862 
for f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

863 
unfolding continuous_def by (rule tendsto_power) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

864 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

865 
lemma continuous_on_power [continuous_intros]: 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

866 
fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

867 
shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

868 
unfolding continuous_on_def by (auto intro: tendsto_power) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

869 

64272  870 
lemma tendsto_prod [tendsto_intros]: 
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset

871 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 
63915  872 
shows "(\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> L i) F) \<Longrightarrow> ((\<lambda>x. \<Prod>i\<in>S. f i x) \<longlongrightarrow> (\<Prod>i\<in>S. L i)) F" 
873 
by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult) 

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

874 

64272  875 
lemma continuous_prod [continuous_intros]: 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

876 
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

877 
shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)" 
64272  878 
unfolding continuous_def by (rule tendsto_prod) 
879 

880 
lemma continuous_on_prod [continuous_intros]: 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

881 
fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

882 
shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)" 
64272  883 
unfolding continuous_on_def by (auto intro: tendsto_prod) 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

884 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

885 
lemma tendsto_of_real_iff: 
63546  886 
"((\<lambda>x. of_real (f x) :: 'a::real_normed_div_algebra) \<longlongrightarrow> of_real c) F \<longleftrightarrow> (f \<longlongrightarrow> c) F" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

887 
unfolding tendsto_iff by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

888 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

889 
lemma tendsto_add_const_iff: 
63546  890 
"((\<lambda>x. c + f x :: 'a::real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F" 
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset

891 
using tendsto_add[OF tendsto_const[of c], of f d] 
63546  892 
and tendsto_add[OF tendsto_const[of "c"], of "\<lambda>x. c + f x" "c + d"] by auto 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

893 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

894 

68860
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

895 
class topological_monoid_mult = topological_semigroup_mult + monoid_mult 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

896 
class topological_comm_monoid_mult = topological_monoid_mult + comm_monoid_mult 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

897 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

898 
lemma tendsto_power_strong [tendsto_intros]: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

899 
fixes f :: "_ \<Rightarrow> 'b :: topological_monoid_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

900 
assumes "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

901 
shows "((\<lambda>x. f x ^ g x) \<longlongrightarrow> a ^ b) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

902 
proof  
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

903 
have "((\<lambda>x. f x ^ b) \<longlongrightarrow> a ^ b) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

904 
by (induction b) (auto intro: tendsto_intros assms) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

905 
also from assms(2) have "eventually (\<lambda>x. g x = b) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

906 
by (simp add: nhds_discrete filterlim_principal) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

907 
hence "eventually (\<lambda>x. f x ^ b = f x ^ g x) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

908 
by eventually_elim simp 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

909 
hence "((\<lambda>x. f x ^ b) \<longlongrightarrow> a ^ b) F \<longleftrightarrow> ((\<lambda>x. f x ^ g x) \<longlongrightarrow> a ^ b) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

910 
by (intro filterlim_cong refl) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

911 
finally show ?thesis . 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

912 
qed 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

913 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

914 
lemma continuous_mult' [continuous_intros]: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

915 
fixes f g :: "_ \<Rightarrow> 'b::topological_semigroup_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

916 
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x * g x)" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

917 
unfolding continuous_def by (rule tendsto_mult) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

918 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

919 
lemma continuous_power' [continuous_intros]: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

920 
fixes f :: "_ \<Rightarrow> 'b::topological_monoid_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

921 
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x ^ g x)" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

922 
unfolding continuous_def by (rule tendsto_power_strong) auto 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

923 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

924 
lemma continuous_on_mult' [continuous_intros]: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

925 
fixes f g :: "_ \<Rightarrow> 'b::topological_semigroup_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

926 
shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x * g x)" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

927 
unfolding continuous_on_def by (auto intro: tendsto_mult) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

928 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

929 
lemma continuous_on_power' [continuous_intros]: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

930 
fixes f :: "_ \<Rightarrow> 'b::topological_monoid_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

931 
shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x ^ g x)" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

932 
unfolding continuous_on_def by (auto intro: tendsto_power_strong) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

933 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

934 
lemma tendsto_mult_one: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

935 
fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

936 
shows "(f \<longlongrightarrow> 1) F \<Longrightarrow> (g \<longlongrightarrow> 1) F \<Longrightarrow> ((\<lambda>x. f x * g x) \<longlongrightarrow> 1) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

937 
by (drule (1) tendsto_mult) simp 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

938 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

939 
lemma tendsto_prod' [tendsto_intros]: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

940 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

941 
shows "(\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F) \<Longrightarrow> ((\<lambda>x. \<Prod>i\<in>I. f i x) \<longlongrightarrow> (\<Prod>i\<in>I. a i)) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

942 
by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_mult) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

943 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

944 
lemma tendsto_one_prod': 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

945 
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

946 
assumes "\<And>i. i \<in> I \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> 1) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

947 
shows "((\<lambda>i. prod (f i) I) \<longlongrightarrow> 1) F" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

948 
using tendsto_prod' [of I "\<lambda>x y. f y x" "\<lambda>x. 1"] assms by simp 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

949 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

950 
lemma continuous_prod' [continuous_intros]: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

951 
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

952 
shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>I. f i x)" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

953 
unfolding continuous_def by (rule tendsto_prod') 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

954 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

955 
lemma continuous_on_prod' [continuous_intros]: 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

956 
fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_mult" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

957 
shows "(\<And>i. i \<in> I \<Longrightarrow> continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<Prod>i\<in>I. f i x)" 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

958 
unfolding continuous_on_def by (auto intro: tendsto_prod') 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

959 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

960 
instance nat :: topological_comm_monoid_mult 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

961 
by standard 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

962 
(simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

963 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

964 
instance int :: topological_comm_monoid_mult 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

965 
by standard 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

966 
(simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

967 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

968 
class comm_real_normed_algebra_1 = real_normed_algebra_1 + comm_monoid_mult 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

969 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

970 
context real_normed_field 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

971 
begin 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

972 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

973 
subclass comm_real_normed_algebra_1 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

974 
proof 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

975 
from norm_mult[of "1 :: 'a" 1] show "norm 1 = 1" by simp 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

976 
qed (simp_all add: norm_mult) 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

977 

f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

978 
end 
f443ec10447d
Some basic materials on filters and topology
Manuel Eberl <eberlm@in.tum.de>
parents:
68721
diff
changeset

979 

60758  980 
subsubsection \<open>Inverse and division\<close> 
31355  981 

982 
lemma (in bounded_bilinear) Zfun_prod_Bfun: 

44195  983 
assumes f: "Zfun f F" 
63546  984 
and g: "Bfun g F" 
44195  985 
shows "Zfun (\<lambda>x. f x ** g x) F" 
31355  986 
proof  
987 
obtain K where K: "0 \<le> K" 

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

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

989 
using nonneg_bounded by blast 
31355  990 
obtain B where B: "0 < B" 
44195  991 
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

992 
using g by (rule BfunE) 
44195  993 
have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) F" 
46887  994 
using norm_g proof eventually_elim 
995 
case (elim x) 

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

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

998 
also have "\<dots> \<le> norm (f x) * B * K" 
63546  999 
by (intro mult_mono' order_refl norm_g norm_ge_zero mult_nonneg_nonneg K elim) 
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset

1000 
also have "\<dots> = norm (f x) * (B * K)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57447
diff
changeset

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

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

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

1005 
by (rule Zfun_imp_Zfun) 
31355  1006 
qed 
1007 

1008 
lemma (in bounded_bilinear) Bfun_prod_Zfun: 

44195  1009 
assumes f: "Bfun f F" 
63546  1010 
and g: "Zfun g F" 
44195  1011 
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

1012 
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) 
31355  1013 

1014 
lemma Bfun_inverse: 

1015 
fixes a :: "'a::real_normed_div_algebra" 

61973  1016 
assumes f: "(f \<longlongrightarrow> a) F" 
31355  1017 
assumes a: "a \<noteq> 0" 
44195  1018 
shows "Bfun (\<lambda>x. inverse (f x)) F" 
31355  1019 
proof  
1020 
from a have "0 < norm a" by simp 

63546  1021 
then have "\<exists>r>0. r < norm a" by (rule dense) 
1022 
then obtain r where r1: "0 < r" and r2: "r < norm a" 

1023 
by blast 

44195  1024 
have "eventually (\<lambda>x. dist (f x) a < r) F" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1025 
using tendstoD [OF f r1] by blast 
63546  1026 
then have "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a  r)) F" 
46887  1027 
proof eventually_elim 
1028 
case (elim x) 

63546  1029 
then have 1: "norm (f x  a) < r" 
31355  1030 
by (simp add: dist_norm) 
63546  1031 
then have 2: "f x \<noteq> 0" using r2 by auto 
1032 
then have "norm (inverse (f x)) = inverse (norm (f x))" 

31355  1033 
by (rule nonzero_norm_inverse) 
1034 
also have "\<dots> \<le> inverse (norm a  r)" 

1035 
proof (rule le_imp_inverse_le) 

63546  1036 
show "0 < norm a  r" 
1037 
using r2 by simp 

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

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

1040 
also have "\<dots> = norm (f x  a)" 
31355  1041 
by (rule norm_minus_commute) 
1042 
also have "\<dots> < r" using 1 . 

63546  1043 
finally show "norm a  r \<le> norm (f x)" 
1044 
by simp 

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

1046 
finally show "norm (inverse (f x)) \<le> inverse (norm a  r)" . 
31355  1047 
qed 
63546  1048 
then show ?thesis by (rule BfunI) 
31355  1049 
qed 
1050 

31565  1051 
lemma tendsto_inverse [tendsto_intros]: 
31355  1052 
fixes a :: "'a::real_normed_div_algebra" 
61973  1053 
assumes f: "(f \<longlongrightarrow> a) F" 
63546  1054 
and a: "a \<noteq> 0" 
61973  1055 
shows "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse a) F" 
31355  1056 
proof  
1057 
from a have "0 < norm a" by simp 

44195  1058 
with f have "eventually (\<lambda>x. dist (f x) a < norm a) F" 
31355  1059 
by (rule tendstoD) 
44195  1060 
then have "eventually (\<lambda>x. f x \<noteq> 0) F" 
61810  1061 
unfolding dist_norm by (auto elim!: eventually_mono) 
44627  1062 
with a have "eventually (\<lambda>x. inverse (f x)  inverse a = 
1063 
 (inverse (f x) * (f x  a) * inverse a)) F" 

61810  1064 
by (auto elim!: eventually_mono simp: inverse_diff_inverse) 
44627  1065 
moreover have "Zfun (\<lambda>x.  (inverse (f x) * (f x  a) * inverse a)) F" 
1066 
by (intro Zfun_minus Zfun_mult_left 

1067 
bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] 

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

1069 
ultimately show ?thesis 

1070 
unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) 

31355  1071 
qed 
1072 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1073 
lemma continuous_inverse: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1074 
fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" 
63546  1075 
assumes "continuous F f" 
1076 
and "f (Lim F (\<lambda>x. x)) \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1077 
shows "continuous F (\<lambda>x. inverse (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1078 
using assms unfolding continuous_def by (rule tendsto_inverse) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1079 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1080 
lemma continuous_at_within_inverse[continuous_intros]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1081 
fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" 
63546  1082 
assumes "continuous (at a within s) f" 
1083 
and "f a \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1084 
shows "continuous (at a within s) (\<lambda>x. inverse (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1085 
using assms unfolding continuous_within by (rule tendsto_inverse) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1086 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

1087 
lemma continuous_on_inverse[continuous_intros]: 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1088 
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra" 
63546  1089 
assumes "continuous_on s f" 
1090 
and "\<forall>x\<in>s. f x \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1091 
shows "continuous_on s (\<lambda>x. inverse (f x))" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1092 
using assms unfolding continuous_on_def by (blast intro: tendsto_inverse) 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1093 

31565  1094 
lemma tendsto_divide [tendsto_intros]: 
31355  1095 
fixes a b :: "'a::real_normed_field" 
63546  1096 
shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> ((\<lambda>x. f x / g x) \<longlongrightarrow> a / b) F" 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset

1097 
by (simp add: tendsto_mult tendsto_inverse divide_inverse) 
31355  1098 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1099 
lemma continuous_divide: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1100 
fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field" 
63546  1101 
assumes "continuous F f" 
1102 
and "continuous F g" 

1103 
and "g (Lim F (\<lambda>x. x)) \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1104 
shows "continuous F (\<lambda>x. (f x) / (g x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1105 
using assms unfolding continuous_def by (rule tendsto_divide) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1106 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1107 
lemma continuous_at_within_divide[continuous_intros]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1108 
fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field" 
63546  1109 
assumes "continuous (at a within s) f" "continuous (at a within s) g" 
1110 
and "g a \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1111 
shows "continuous (at a within s) (\<lambda>x. (f x) / (g x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1112 
using assms unfolding continuous_within by (rule tendsto_divide) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1113 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1114 
lemma isCont_divide[continuous_intros, simp]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1115 
fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_field" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1116 
assumes "isCont f a" "isCont g a" "g a \<noteq> 0" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1117 
shows "isCont (\<lambda>x. (f x) / g x) a" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1118 
using assms unfolding continuous_at by (rule tendsto_divide) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1119 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

1120 
lemma continuous_on_divide[continuous_intros]: 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1121 
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field" 
63546  1122 
assumes "continuous_on s f" "continuous_on s g" 
1123 
and "\<forall>x\<in>s. g x \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1124 
shows "continuous_on s (\<lambda>x. (f x) / (g x))" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1125 
using assms unfolding continuous_on_def by (blast intro: tendsto_divide) 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1126 

63546  1127 
lemma tendsto_sgn [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. sgn (f x)) \<longlongrightarrow> sgn l) F" 
1128 
for l :: "'a::real_normed_vector" 

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

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

1130 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1131 
lemma continuous_sgn: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1132 
fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 
63546  1133 
assumes "continuous F f" 
1134 
and "f (Lim F (\<lambda>x. x)) \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1135 
shows "continuous F (\<lambda>x. sgn (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1136 
using assms unfolding continuous_def by (rule tendsto_sgn) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1137 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1138 
lemma continuous_at_within_sgn[continuous_intros]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1139 
fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 
63546  1140 
assumes "continuous (at a within s) f" 
1141 
and "f a \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1142 
shows "continuous (at a within s) (\<lambda>x. sgn (f x))" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1143 
using assms unfolding continuous_within by (rule tendsto_sgn) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1144 

270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1145 
lemma isCont_sgn[continuous_intros]: 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1146 
fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" 
63546  1147 
assumes "isCont f a" 
1148 
and "f a \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1149 
shows "isCont (\<lambda>x. sgn (f x)) a" 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1150 
using assms unfolding continuous_at by (rule tendsto_sgn) 
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1151 

56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset

1152 
lemma continuous_on_sgn[continuous_intros]: 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1153 
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector" 
63546  1154 
assumes "continuous_on s f" 
1155 
and "\<forall>x\<in>s. f x \<noteq> 0" 

51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1156 
shows "continuous_on s (\<lambda>x. sgn (f x))" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1157 
using assms unfolding continuous_on_def by (blast intro: tendsto_sgn) 
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset

1158 

50325  1159 
lemma filterlim_at_infinity: 
61076  1160 
fixes f :: "_ \<Rightarrow> 'a::real_normed_vector" 
50325  1161 
assumes "0 \<le> c" 
1162 
shows "(LIM x F. f x :> at_infinity) \<longleftrightarrow> (\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F)" 

1163 
unfolding filterlim_iff eventually_at_infinity 

1164 
proof safe 

63546  1165 
fix P :: "'a \<Rightarrow> bool" 
1166 
fix b 

50325  1167 
assume *: "\<forall>r>c. eventually (\<lambda>x. r \<le> norm (f x)) F" 
63546  1168 
assume P: "\<forall>x. b \<le> norm x \<longrightarrow> P x" 
50325  1169 
have "max b (c + 1) > c" by auto 
1170 
with * have "eventually (\<lambda>x. max b (c + 1) \<le> norm (f x)) F" 

1171 
by auto 

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

1173 
proof eventually_elim 

63546  1174 
case (elim x) 
50325  1175 
with P show "P (f x)" by auto 
1176 
qed 

1177 
qed force 

1178 

67371
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1179 
lemma filterlim_at_infinity_imp_norm_at_top: 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1180 
fixes F 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1181 
assumes "filterlim f at_infinity F" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1182 
shows "filterlim (\<lambda>x. norm (f x)) at_top F" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1183 
proof  
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1184 
{ 
68611  1185 
fix r :: real 
1186 
have "\<forall>\<^sub>F x in F. r \<le> norm (f x)" using filterlim_at_infinity[of 0 f F] assms 

1187 
by (cases "r > 0") 

67371
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1188 
(auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero]) 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1189 
} 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1190 
thus ?thesis by (auto simp: filterlim_at_top) 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1191 
qed 
68611  1192 

67371
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1193 
lemma filterlim_norm_at_top_imp_at_infinity: 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1194 
fixes F 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1195 
assumes "filterlim (\<lambda>x. norm (f x)) at_top F" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1196 
shows "filterlim f at_infinity F" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1197 
using filterlim_at_infinity[of 0 f F] assms by (auto simp: filterlim_at_top) 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1198 

2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1199 
lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1200 
by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident) 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1201 

67950
99eaa5cedbb7
Added some simple facts about limits
Manuel Eberl <eberlm@in.tum.de>
parents:
67707
diff
changeset

1202 
lemma filterlim_at_infinity_conv_norm_at_top: 
99eaa5cedbb7
Added some simple facts about limits
Manuel Eberl <eberlm@in.tum.de>
parents:
67707
diff
changeset

1203 
"filterlim f at_infinity G \<longleftrightarrow> filterlim (\<lambda>x. norm (f x)) at_top G" 
99eaa5cedbb7
Added some simple facts about limits
Manuel Eberl <eberlm@in.tum.de>
parents:
67707
diff
changeset

1204 
by (auto simp: filterlim_at_infinity[OF order.refl] filterlim_at_top_gt[of _ _ 0]) 
99eaa5cedbb7
Added some simple facts about limits
Manuel Eberl <eberlm@in.tum.de>
parents:
67707
diff
changeset

1205 

67371
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1206 
lemma eventually_not_equal_at_infinity: 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1207 
"eventually (\<lambda>x. x \<noteq> (a :: 'a :: {real_normed_vector})) at_infinity" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1208 
proof  
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1209 
from filterlim_norm_at_top[where 'a = 'a] 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1210 
have "\<forall>\<^sub>F x in at_infinity. norm a < norm (x::'a)" by (auto simp: filterlim_at_top_dense) 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1211 
thus ?thesis by eventually_elim auto 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1212 
qed 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1213 

2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1214 
lemma filterlim_int_of_nat_at_topD: 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1215 
fixes F 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1216 
assumes "filterlim (\<lambda>x. f (int x)) F at_top" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1217 
shows "filterlim f F at_top" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1218 
proof  
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1219 
have "filterlim (\<lambda>x. f (int (nat x))) F at_top" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1220 
by (rule filterlim_compose[OF assms filterlim_nat_sequentially]) 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1221 
also have "?this \<longleftrightarrow> filterlim f F at_top" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1222 
by (intro filterlim_cong refl eventually_mono [OF eventually_ge_at_top[of "0::int"]]) auto 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1223 
finally show ?thesis . 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1224 
qed 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1225 

2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1226 
lemma filterlim_int_sequentially [tendsto_intros]: 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1227 
"filterlim int at_top sequentially" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1228 
unfolding filterlim_at_top 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1229 
proof 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1230 
fix C :: int 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1231 
show "eventually (\<lambda>n. int n \<ge> C) at_top" 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1232 
using eventually_ge_at_top[of "nat \<lceil>C\<rceil>"] by eventually_elim linarith 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1233 
qed 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1234 

2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1235 
lemma filterlim_real_of_int_at_top [tendsto_intros]: 
2d9cf74943e1
moved in some material from EulerMacLaurin
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

1236 
"filterlim real_of_int at_top at_top" 