author | wenzelm |
Sat, 13 Mar 2010 14:44:47 +0100 | |
changeset 35743 | c506c029a082 |
parent 31902 | 862ae16a799d |
child 36358 | 246493d61204 |
permissions | -rw-r--r-- |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
1 |
(* Title : Limits.thy |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
2 |
Author : Brian Huffman |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
3 |
*) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
4 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
5 |
header {* Filters and Limits *} |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
6 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
7 |
theory Limits |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
8 |
imports RealVector RComplete |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
9 |
begin |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
10 |
|
31392 | 11 |
subsection {* Nets *} |
12 |
||
13 |
text {* |
|
14 |
A net is now defined as a filter base. |
|
15 |
The definition also allows non-proper filter bases. |
|
16 |
*} |
|
17 |
||
18 |
typedef (open) 'a net = |
|
19 |
"{net :: 'a set set. (\<exists>A. A \<in> net) |
|
20 |
\<and> (\<forall>A\<in>net. \<forall>B\<in>net. \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B)}" |
|
21 |
proof |
|
22 |
show "UNIV \<in> ?net" by auto |
|
23 |
qed |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
24 |
|
31392 | 25 |
lemma Rep_net_nonempty: "\<exists>A. A \<in> Rep_net net" |
26 |
using Rep_net [of net] by simp |
|
27 |
||
28 |
lemma Rep_net_directed: |
|
29 |
"A \<in> Rep_net net \<Longrightarrow> B \<in> Rep_net net \<Longrightarrow> \<exists>C\<in>Rep_net net. C \<subseteq> A \<and> C \<subseteq> B" |
|
30 |
using Rep_net [of net] by simp |
|
31 |
||
32 |
lemma Abs_net_inverse': |
|
33 |
assumes "\<exists>A. A \<in> net" |
|
34 |
assumes "\<And>A B. A \<in> net \<Longrightarrow> B \<in> net \<Longrightarrow> \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B" |
|
35 |
shows "Rep_net (Abs_net net) = net" |
|
36 |
using assms by (simp add: Abs_net_inverse) |
|
37 |
||
38 |
lemma image_nonempty: "\<exists>x. x \<in> A \<Longrightarrow> \<exists>x. x \<in> f ` A" |
|
39 |
by auto |
|
40 |
||
41 |
||
42 |
subsection {* Eventually *} |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
43 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
44 |
definition |
31392 | 45 |
eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where |
46 |
[code del]: "eventually P net \<longleftrightarrow> (\<exists>A\<in>Rep_net net. \<forall>x\<in>A. P x)" |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
47 |
|
31392 | 48 |
lemma eventually_True [simp]: "eventually (\<lambda>x. True) net" |
49 |
unfolding eventually_def using Rep_net_nonempty [of net] by fast |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
50 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
51 |
lemma eventually_mono: |
31392 | 52 |
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net" |
53 |
unfolding eventually_def by blast |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
54 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
55 |
lemma eventually_conj: |
31392 | 56 |
assumes P: "eventually (\<lambda>x. P x) net" |
57 |
assumes Q: "eventually (\<lambda>x. Q x) net" |
|
58 |
shows "eventually (\<lambda>x. P x \<and> Q x) net" |
|
59 |
proof - |
|
60 |
obtain A where A: "A \<in> Rep_net net" "\<forall>x\<in>A. P x" |
|
61 |
using P unfolding eventually_def by fast |
|
62 |
obtain B where B: "B \<in> Rep_net net" "\<forall>x\<in>B. Q x" |
|
63 |
using Q unfolding eventually_def by fast |
|
64 |
obtain C where C: "C \<in> Rep_net net" "C \<subseteq> A" "C \<subseteq> B" |
|
65 |
using Rep_net_directed [OF A(1) B(1)] by fast |
|
66 |
then have "\<forall>x\<in>C. P x \<and> Q x" "C \<in> Rep_net net" |
|
67 |
using A(2) B(2) by auto |
|
68 |
then show ?thesis unfolding eventually_def .. |
|
69 |
qed |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
70 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
71 |
lemma eventually_mp: |
31392 | 72 |
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net" |
73 |
assumes "eventually (\<lambda>x. P x) net" |
|
74 |
shows "eventually (\<lambda>x. Q x) net" |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
75 |
proof (rule eventually_mono) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
76 |
show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp |
31392 | 77 |
show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
78 |
using assms by (rule eventually_conj) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
79 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
80 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
81 |
lemma eventually_rev_mp: |
31392 | 82 |
assumes "eventually (\<lambda>x. P x) net" |
83 |
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net" |
|
84 |
shows "eventually (\<lambda>x. Q x) net" |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
85 |
using assms(2) assms(1) by (rule eventually_mp) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
86 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
87 |
lemma eventually_conj_iff: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
88 |
"eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
89 |
by (auto intro: eventually_conj elim: eventually_rev_mp) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
90 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
91 |
lemma eventually_elim1: |
31392 | 92 |
assumes "eventually (\<lambda>i. P i) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
93 |
assumes "\<And>i. P i \<Longrightarrow> Q i" |
31392 | 94 |
shows "eventually (\<lambda>i. Q i) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
95 |
using assms by (auto elim!: eventually_rev_mp) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
96 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
97 |
lemma eventually_elim2: |
31392 | 98 |
assumes "eventually (\<lambda>i. P i) net" |
99 |
assumes "eventually (\<lambda>i. Q i) net" |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
100 |
assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i" |
31392 | 101 |
shows "eventually (\<lambda>i. R i) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
102 |
using assms by (auto elim!: eventually_rev_mp) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
103 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
104 |
|
31392 | 105 |
subsection {* Standard Nets *} |
106 |
||
107 |
definition |
|
108 |
sequentially :: "nat net" where |
|
109 |
[code del]: "sequentially = Abs_net (range (\<lambda>n. {n..}))" |
|
110 |
||
111 |
definition |
|
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
112 |
within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
113 |
[code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)" |
31392 | 114 |
|
115 |
definition |
|
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
116 |
at :: "'a::topological_space \<Rightarrow> 'a net" where |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
117 |
[code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})" |
31392 | 118 |
|
119 |
lemma Rep_net_sequentially: |
|
120 |
"Rep_net sequentially = range (\<lambda>n. {n..})" |
|
121 |
unfolding sequentially_def |
|
122 |
apply (rule Abs_net_inverse') |
|
123 |
apply (rule image_nonempty, simp) |
|
124 |
apply (clarsimp, rename_tac m n) |
|
125 |
apply (rule_tac x="max m n" in exI, auto) |
|
126 |
done |
|
127 |
||
128 |
lemma Rep_net_within: |
|
129 |
"Rep_net (net within S) = (\<lambda>A. A \<inter> S) ` Rep_net net" |
|
130 |
unfolding within_def |
|
131 |
apply (rule Abs_net_inverse') |
|
132 |
apply (rule image_nonempty, rule Rep_net_nonempty) |
|
133 |
apply (clarsimp, rename_tac A B) |
|
134 |
apply (drule (1) Rep_net_directed) |
|
135 |
apply (clarify, rule_tac x=C in bexI, auto) |
|
136 |
done |
|
137 |
||
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
138 |
lemma Rep_net_at: |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
139 |
"Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})" |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
140 |
unfolding at_def |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
141 |
apply (rule Abs_net_inverse') |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
142 |
apply (rule image_nonempty) |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
143 |
apply (rule_tac x="UNIV" in exI, simp) |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
144 |
apply (clarsimp, rename_tac S T) |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
145 |
apply (rule_tac x="S \<inter> T" in exI, auto simp add: open_Int) |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
146 |
done |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
147 |
|
31392 | 148 |
lemma eventually_sequentially: |
149 |
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)" |
|
150 |
unfolding eventually_def Rep_net_sequentially by auto |
|
151 |
||
152 |
lemma eventually_within: |
|
153 |
"eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net" |
|
154 |
unfolding eventually_def Rep_net_within by auto |
|
155 |
||
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
156 |
lemma eventually_at_topological: |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
157 |
"eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))" |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
158 |
unfolding eventually_def Rep_net_at by auto |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
159 |
|
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
160 |
lemma eventually_at: |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
161 |
fixes a :: "'a::metric_space" |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
162 |
shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)" |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
163 |
unfolding eventually_at_topological open_dist |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
164 |
apply safe |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
165 |
apply fast |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
166 |
apply (rule_tac x="{x. dist x a < d}" in exI, simp) |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
167 |
apply clarsimp |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
168 |
apply (rule_tac x="d - dist x a" in exI, clarsimp) |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
169 |
apply (simp only: less_diff_eq) |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
170 |
apply (erule le_less_trans [OF dist_triangle]) |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
171 |
done |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
172 |
|
31392 | 173 |
|
31355 | 174 |
subsection {* Boundedness *} |
175 |
||
176 |
definition |
|
31392 | 177 |
Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
178 |
[code del]: "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)" |
31355 | 179 |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
180 |
lemma BfunI: |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
181 |
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net" |
31355 | 182 |
unfolding Bfun_def |
183 |
proof (intro exI conjI allI) |
|
184 |
show "0 < max K 1" by simp |
|
185 |
next |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
186 |
show "eventually (\<lambda>x. norm (f x) \<le> max K 1) net" |
31355 | 187 |
using K by (rule eventually_elim1, simp) |
188 |
qed |
|
189 |
||
190 |
lemma BfunE: |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
191 |
assumes "Bfun f net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
192 |
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) net" |
31355 | 193 |
using assms unfolding Bfun_def by fast |
194 |
||
195 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
196 |
subsection {* Convergence to Zero *} |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
197 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
198 |
definition |
31392 | 199 |
Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
200 |
[code del]: "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
201 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
202 |
lemma ZfunI: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
203 |
"(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
204 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
205 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
206 |
lemma ZfunD: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
207 |
"\<lbrakk>Zfun f net; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
208 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
209 |
|
31355 | 210 |
lemma Zfun_ssubst: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
211 |
"eventually (\<lambda>x. f x = g x) net \<Longrightarrow> Zfun g net \<Longrightarrow> Zfun f net" |
31355 | 212 |
unfolding Zfun_def by (auto elim!: eventually_rev_mp) |
213 |
||
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
214 |
lemma Zfun_zero: "Zfun (\<lambda>x. 0) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
215 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
216 |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
217 |
lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) net = Zfun (\<lambda>x. f x) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
218 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
219 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
220 |
lemma Zfun_imp_Zfun: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
221 |
assumes f: "Zfun f net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
222 |
assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
223 |
shows "Zfun (\<lambda>x. g x) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
224 |
proof (cases) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
225 |
assume K: "0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
226 |
show ?thesis |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
227 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
228 |
fix r::real assume "0 < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
229 |
hence "0 < r / K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
230 |
using K by (rule divide_pos_pos) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
231 |
then have "eventually (\<lambda>x. norm (f x) < r / K) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
232 |
using ZfunD [OF f] by fast |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
233 |
with g show "eventually (\<lambda>x. norm (g x) < r) net" |
31355 | 234 |
proof (rule eventually_elim2) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
235 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
236 |
assume *: "norm (g x) \<le> norm (f x) * K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
237 |
assume "norm (f x) < r / K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
238 |
hence "norm (f x) * K < r" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
239 |
by (simp add: pos_less_divide_eq K) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
240 |
thus "norm (g x) < r" |
31355 | 241 |
by (simp add: order_le_less_trans [OF *]) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
242 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
243 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
244 |
next |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
245 |
assume "\<not> 0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
246 |
hence K: "K \<le> 0" by (simp only: not_less) |
31355 | 247 |
show ?thesis |
248 |
proof (rule ZfunI) |
|
249 |
fix r :: real |
|
250 |
assume "0 < r" |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
251 |
from g show "eventually (\<lambda>x. norm (g x) < r) net" |
31355 | 252 |
proof (rule eventually_elim1) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
253 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
254 |
assume "norm (g x) \<le> norm (f x) * K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
255 |
also have "\<dots> \<le> norm (f x) * 0" |
31355 | 256 |
using K norm_ge_zero by (rule mult_left_mono) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
257 |
finally show "norm (g x) < r" |
31355 | 258 |
using `0 < r` by simp |
259 |
qed |
|
260 |
qed |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
261 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
262 |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
263 |
lemma Zfun_le: "\<lbrakk>Zfun g net; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
264 |
by (erule_tac K="1" in Zfun_imp_Zfun, simp) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
265 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
266 |
lemma Zfun_add: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
267 |
assumes f: "Zfun f net" and g: "Zfun g net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
268 |
shows "Zfun (\<lambda>x. f x + g x) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
269 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
270 |
fix r::real assume "0 < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
271 |
hence r: "0 < r / 2" by simp |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
272 |
have "eventually (\<lambda>x. norm (f x) < r/2) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
273 |
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
|
274 |
moreover |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
275 |
have "eventually (\<lambda>x. norm (g x) < r/2) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
276 |
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
|
277 |
ultimately |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
278 |
show "eventually (\<lambda>x. norm (f x + g x) < r) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
279 |
proof (rule eventually_elim2) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
280 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
281 |
assume *: "norm (f x) < r/2" "norm (g x) < r/2" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
282 |
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
|
283 |
by (rule norm_triangle_ineq) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
284 |
also have "\<dots> < r/2 + r/2" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
285 |
using * by (rule add_strict_mono) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
286 |
finally show "norm (f x + g x) < r" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
287 |
by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
288 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
289 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
290 |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
291 |
lemma Zfun_minus: "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. - f x) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
292 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
293 |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
294 |
lemma Zfun_diff: "\<lbrakk>Zfun f net; Zfun g net\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
295 |
by (simp only: diff_minus Zfun_add Zfun_minus) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
296 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
297 |
lemma (in bounded_linear) Zfun: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
298 |
assumes g: "Zfun g net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
299 |
shows "Zfun (\<lambda>x. f (g x)) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
300 |
proof - |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
301 |
obtain K where "\<And>x. norm (f x) \<le> norm x * K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
302 |
using bounded by fast |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
303 |
then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) net" |
31355 | 304 |
by simp |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
305 |
with g show ?thesis |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
306 |
by (rule Zfun_imp_Zfun) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
307 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
308 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
309 |
lemma (in bounded_bilinear) Zfun: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
310 |
assumes f: "Zfun f net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
311 |
assumes g: "Zfun g net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
312 |
shows "Zfun (\<lambda>x. f x ** g x) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
313 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
314 |
fix r::real assume r: "0 < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
315 |
obtain K where K: "0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
316 |
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
317 |
using pos_bounded by fast |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
318 |
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
|
319 |
by (rule positive_imp_inverse_positive) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
320 |
have "eventually (\<lambda>x. norm (f x) < r) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
321 |
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
|
322 |
moreover |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
323 |
have "eventually (\<lambda>x. norm (g x) < inverse K) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
324 |
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
|
325 |
ultimately |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
326 |
show "eventually (\<lambda>x. norm (f x ** g x) < r) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
327 |
proof (rule eventually_elim2) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
328 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
329 |
assume *: "norm (f x) < r" "norm (g x) < inverse K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
330 |
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
|
331 |
by (rule norm_le) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
332 |
also have "norm (f x) * norm (g x) * K < r * inverse K * K" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
333 |
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
334 |
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
|
335 |
by simp |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
336 |
finally show "norm (f x ** g x) < r" . |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
337 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
338 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
339 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
340 |
lemma (in bounded_bilinear) Zfun_left: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
341 |
"Zfun f net \<Longrightarrow> Zfun (\<lambda>x. f x ** a) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
342 |
by (rule bounded_linear_left [THEN bounded_linear.Zfun]) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
343 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
344 |
lemma (in bounded_bilinear) Zfun_right: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
345 |
"Zfun f net \<Longrightarrow> Zfun (\<lambda>x. a ** f x) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
346 |
by (rule bounded_linear_right [THEN bounded_linear.Zfun]) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
347 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
348 |
lemmas Zfun_mult = mult.Zfun |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
349 |
lemmas Zfun_mult_right = mult.Zfun_right |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
350 |
lemmas Zfun_mult_left = mult.Zfun_left |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
351 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
352 |
|
31902 | 353 |
subsection {* Limits *} |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
354 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
355 |
definition |
31488 | 356 |
tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" |
357 |
(infixr "--->" 55) |
|
358 |
where [code del]: |
|
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
359 |
"(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
360 |
|
31902 | 361 |
ML {* |
362 |
structure Tendsto_Intros = Named_Thms |
|
363 |
( |
|
364 |
val name = "tendsto_intros" |
|
365 |
val description = "introduction rules for tendsto" |
|
366 |
) |
|
31565 | 367 |
*} |
368 |
||
31902 | 369 |
setup Tendsto_Intros.setup |
31565 | 370 |
|
31488 | 371 |
lemma topological_tendstoI: |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
372 |
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
373 |
\<Longrightarrow> (f ---> l) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
374 |
unfolding tendsto_def by auto |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
375 |
|
31488 | 376 |
lemma topological_tendstoD: |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
377 |
"(f ---> l) net \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net" |
31488 | 378 |
unfolding tendsto_def by auto |
379 |
||
380 |
lemma tendstoI: |
|
381 |
assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net" |
|
382 |
shows "(f ---> l) net" |
|
383 |
apply (rule topological_tendstoI) |
|
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
384 |
apply (simp add: open_dist) |
31488 | 385 |
apply (drule (1) bspec, clarify) |
386 |
apply (drule assms) |
|
387 |
apply (erule eventually_elim1, simp) |
|
388 |
done |
|
389 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
390 |
lemma tendstoD: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
391 |
"(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net" |
31488 | 392 |
apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
393 |
apply (clarsimp simp add: open_dist) |
31488 | 394 |
apply (rule_tac x="e - dist x l" in exI, clarsimp) |
395 |
apply (simp only: less_diff_eq) |
|
396 |
apply (erule le_less_trans [OF dist_triangle]) |
|
397 |
apply simp |
|
398 |
apply simp |
|
399 |
done |
|
400 |
||
401 |
lemma tendsto_iff: |
|
402 |
"(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" |
|
403 |
using tendstoI tendstoD by fast |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
404 |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
405 |
lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net" |
31488 | 406 |
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
|
407 |
|
31565 | 408 |
lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)" |
409 |
unfolding tendsto_def eventually_at_topological by auto |
|
410 |
||
411 |
lemma tendsto_ident_at_within [tendsto_intros]: |
|
412 |
"a \<in> S \<Longrightarrow> ((\<lambda>x. x) ---> a) (at a within S)" |
|
413 |
unfolding tendsto_def eventually_within eventually_at_topological by auto |
|
414 |
||
415 |
lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net" |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
416 |
by (simp add: tendsto_def) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
417 |
|
31565 | 418 |
lemma tendsto_dist [tendsto_intros]: |
419 |
assumes f: "(f ---> l) net" and g: "(g ---> m) net" |
|
420 |
shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) net" |
|
421 |
proof (rule tendstoI) |
|
422 |
fix e :: real assume "0 < e" |
|
423 |
hence e2: "0 < e/2" by simp |
|
424 |
from tendstoD [OF f e2] tendstoD [OF g e2] |
|
425 |
show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) net" |
|
426 |
proof (rule eventually_elim2) |
|
427 |
fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2" |
|
428 |
then show "dist (dist (f x) (g x)) (dist l m) < e" |
|
429 |
unfolding dist_real_def |
|
430 |
using dist_triangle2 [of "f x" "g x" "l"] |
|
431 |
using dist_triangle2 [of "g x" "l" "m"] |
|
432 |
using dist_triangle3 [of "l" "m" "f x"] |
|
433 |
using dist_triangle [of "f x" "m" "g x"] |
|
434 |
by arith |
|
435 |
qed |
|
436 |
qed |
|
437 |
||
438 |
lemma tendsto_norm [tendsto_intros]: |
|
439 |
"(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net" |
|
31488 | 440 |
apply (simp add: tendsto_iff dist_norm, safe) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
441 |
apply (drule_tac x="e" in spec, safe) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
442 |
apply (erule eventually_elim1) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
443 |
apply (erule order_le_less_trans [OF norm_triangle_ineq3]) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
444 |
done |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
445 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
446 |
lemma add_diff_add: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
447 |
fixes a b c d :: "'a::ab_group_add" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
448 |
shows "(a + c) - (b + d) = (a - b) + (c - d)" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
449 |
by simp |
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 minus_diff_minus: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
452 |
fixes a b :: "'a::ab_group_add" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
453 |
shows "(- a) - (- b) = - (a - b)" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
454 |
by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
455 |
|
31565 | 456 |
lemma tendsto_add [tendsto_intros]: |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
457 |
fixes a b :: "'a::real_normed_vector" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
458 |
shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
459 |
by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
460 |
|
31565 | 461 |
lemma tendsto_minus [tendsto_intros]: |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
462 |
fixes a :: "'a::real_normed_vector" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
463 |
shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
464 |
by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
465 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
466 |
lemma tendsto_minus_cancel: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
467 |
fixes a :: "'a::real_normed_vector" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
468 |
shows "((\<lambda>x. - f x) ---> - a) net \<Longrightarrow> (f ---> a) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
469 |
by (drule tendsto_minus, simp) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
470 |
|
31565 | 471 |
lemma tendsto_diff [tendsto_intros]: |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
472 |
fixes a b :: "'a::real_normed_vector" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
473 |
shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
474 |
by (simp add: diff_minus tendsto_add tendsto_minus) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
475 |
|
31588 | 476 |
lemma tendsto_setsum [tendsto_intros]: |
477 |
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector" |
|
478 |
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) net" |
|
479 |
shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) net" |
|
480 |
proof (cases "finite S") |
|
481 |
assume "finite S" thus ?thesis using assms |
|
482 |
proof (induct set: finite) |
|
483 |
case empty show ?case |
|
484 |
by (simp add: tendsto_const) |
|
485 |
next |
|
486 |
case (insert i F) thus ?case |
|
487 |
by (simp add: tendsto_add) |
|
488 |
qed |
|
489 |
next |
|
490 |
assume "\<not> finite S" thus ?thesis |
|
491 |
by (simp add: tendsto_const) |
|
492 |
qed |
|
493 |
||
31565 | 494 |
lemma (in bounded_linear) tendsto [tendsto_intros]: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
495 |
"(g ---> a) net \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
496 |
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
497 |
|
31565 | 498 |
lemma (in bounded_bilinear) tendsto [tendsto_intros]: |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
499 |
"\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) net" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
500 |
by (simp only: tendsto_Zfun_iff prod_diff_prod |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
501 |
Zfun_add Zfun Zfun_left Zfun_right) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
502 |
|
31355 | 503 |
|
504 |
subsection {* Continuity of Inverse *} |
|
505 |
||
506 |
lemma (in bounded_bilinear) Zfun_prod_Bfun: |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
507 |
assumes f: "Zfun f net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
508 |
assumes g: "Bfun g net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
509 |
shows "Zfun (\<lambda>x. f x ** g x) net" |
31355 | 510 |
proof - |
511 |
obtain K where K: "0 \<le> K" |
|
512 |
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
513 |
using nonneg_bounded by fast |
|
514 |
obtain B where B: "0 < B" |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
515 |
and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
516 |
using g by (rule BfunE) |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
517 |
have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
518 |
using norm_g proof (rule eventually_elim1) |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
519 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
520 |
assume *: "norm (g x) \<le> B" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
521 |
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" |
31355 | 522 |
by (rule norm_le) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
523 |
also have "\<dots> \<le> norm (f x) * B * K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
524 |
by (intro mult_mono' order_refl norm_g norm_ge_zero |
31355 | 525 |
mult_nonneg_nonneg K *) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
526 |
also have "\<dots> = norm (f x) * (B * K)" |
31355 | 527 |
by (rule mult_assoc) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
528 |
finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" . |
31355 | 529 |
qed |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
530 |
with f show ?thesis |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
531 |
by (rule Zfun_imp_Zfun) |
31355 | 532 |
qed |
533 |
||
534 |
lemma (in bounded_bilinear) flip: |
|
535 |
"bounded_bilinear (\<lambda>x y. y ** x)" |
|
536 |
apply default |
|
537 |
apply (rule add_right) |
|
538 |
apply (rule add_left) |
|
539 |
apply (rule scaleR_right) |
|
540 |
apply (rule scaleR_left) |
|
541 |
apply (subst mult_commute) |
|
542 |
using bounded by fast |
|
543 |
||
544 |
lemma (in bounded_bilinear) Bfun_prod_Zfun: |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
545 |
assumes f: "Bfun f net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
546 |
assumes g: "Zfun g net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
547 |
shows "Zfun (\<lambda>x. f x ** g x) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
548 |
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) |
31355 | 549 |
|
550 |
lemma inverse_diff_inverse: |
|
551 |
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk> |
|
552 |
\<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)" |
|
553 |
by (simp add: algebra_simps) |
|
554 |
||
555 |
lemma Bfun_inverse_lemma: |
|
556 |
fixes x :: "'a::real_normed_div_algebra" |
|
557 |
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" |
|
558 |
apply (subst nonzero_norm_inverse, clarsimp) |
|
559 |
apply (erule (1) le_imp_inverse_le) |
|
560 |
done |
|
561 |
||
562 |
lemma Bfun_inverse: |
|
563 |
fixes a :: "'a::real_normed_div_algebra" |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
564 |
assumes f: "(f ---> a) net" |
31355 | 565 |
assumes a: "a \<noteq> 0" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
566 |
shows "Bfun (\<lambda>x. inverse (f x)) net" |
31355 | 567 |
proof - |
568 |
from a have "0 < norm a" by simp |
|
569 |
hence "\<exists>r>0. r < norm a" by (rule dense) |
|
570 |
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
571 |
have "eventually (\<lambda>x. dist (f x) a < r) net" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
572 |
using tendstoD [OF f r1] by fast |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
573 |
hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) net" |
31355 | 574 |
proof (rule eventually_elim1) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
575 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
576 |
assume "dist (f x) a < r" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
577 |
hence 1: "norm (f x - a) < r" |
31355 | 578 |
by (simp add: dist_norm) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
579 |
hence 2: "f x \<noteq> 0" using r2 by auto |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
580 |
hence "norm (inverse (f x)) = inverse (norm (f x))" |
31355 | 581 |
by (rule nonzero_norm_inverse) |
582 |
also have "\<dots> \<le> inverse (norm a - r)" |
|
583 |
proof (rule le_imp_inverse_le) |
|
584 |
show "0 < norm a - r" using r2 by simp |
|
585 |
next |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
586 |
have "norm a - norm (f x) \<le> norm (a - f x)" |
31355 | 587 |
by (rule norm_triangle_ineq2) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
588 |
also have "\<dots> = norm (f x - a)" |
31355 | 589 |
by (rule norm_minus_commute) |
590 |
also have "\<dots> < r" using 1 . |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
591 |
finally show "norm a - r \<le> norm (f x)" by simp |
31355 | 592 |
qed |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
593 |
finally show "norm (inverse (f x)) \<le> inverse (norm a - r)" . |
31355 | 594 |
qed |
595 |
thus ?thesis by (rule BfunI) |
|
596 |
qed |
|
597 |
||
598 |
lemma tendsto_inverse_lemma: |
|
599 |
fixes a :: "'a::real_normed_div_algebra" |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
600 |
shows "\<lbrakk>(f ---> a) net; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) net\<rbrakk> |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
601 |
\<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) net" |
31355 | 602 |
apply (subst tendsto_Zfun_iff) |
603 |
apply (rule Zfun_ssubst) |
|
604 |
apply (erule eventually_elim1) |
|
605 |
apply (erule (1) inverse_diff_inverse) |
|
606 |
apply (rule Zfun_minus) |
|
607 |
apply (rule Zfun_mult_left) |
|
608 |
apply (rule mult.Bfun_prod_Zfun) |
|
609 |
apply (erule (1) Bfun_inverse) |
|
610 |
apply (simp add: tendsto_Zfun_iff) |
|
611 |
done |
|
612 |
||
31565 | 613 |
lemma tendsto_inverse [tendsto_intros]: |
31355 | 614 |
fixes a :: "'a::real_normed_div_algebra" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
615 |
assumes f: "(f ---> a) net" |
31355 | 616 |
assumes a: "a \<noteq> 0" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
617 |
shows "((\<lambda>x. inverse (f x)) ---> inverse a) net" |
31355 | 618 |
proof - |
619 |
from a have "0 < norm a" by simp |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
620 |
with f have "eventually (\<lambda>x. dist (f x) a < norm a) net" |
31355 | 621 |
by (rule tendstoD) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
622 |
then have "eventually (\<lambda>x. f x \<noteq> 0) net" |
31355 | 623 |
unfolding dist_norm by (auto elim!: eventually_elim1) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
624 |
with f a show ?thesis |
31355 | 625 |
by (rule tendsto_inverse_lemma) |
626 |
qed |
|
627 |
||
31565 | 628 |
lemma tendsto_divide [tendsto_intros]: |
31355 | 629 |
fixes a b :: "'a::real_normed_field" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
630 |
shows "\<lbrakk>(f ---> a) net; (g ---> b) net; b \<noteq> 0\<rbrakk> |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
631 |
\<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) net" |
31355 | 632 |
by (simp add: mult.tendsto tendsto_inverse divide_inverse) |
633 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
634 |
end |