author | huffman |
Mon, 01 Jun 2009 16:27:54 -0700 | |
changeset 31357 | df6acdd9dd37 |
parent 31356 | ec8b9b6c47dc |
child 31392 | 69570155ddf8 |
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 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
11 |
subsection {* Filters *} |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
12 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
13 |
typedef (open) 'a filter = |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
14 |
"{f :: ('a \<Rightarrow> bool) \<Rightarrow> bool. f (\<lambda>x. True) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
15 |
\<and> (\<forall>P Q. (\<forall>x. P x \<longrightarrow> Q x) \<longrightarrow> f P \<longrightarrow> f Q) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
16 |
\<and> (\<forall>P Q. f P \<longrightarrow> f Q \<longrightarrow> f (\<lambda>x. P x \<and> Q x))}" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
17 |
proof |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
18 |
show "(\<lambda>P. True) \<in> ?filter" by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
19 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
20 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
21 |
definition |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
22 |
eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" where |
31356 | 23 |
[code del]: "eventually P F \<longleftrightarrow> Rep_filter F P" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
24 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
25 |
lemma eventually_True [simp]: "eventually (\<lambda>x. True) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
26 |
unfolding eventually_def using Rep_filter [of F] by blast |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
27 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
28 |
lemma eventually_mono: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
29 |
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
30 |
unfolding eventually_def using Rep_filter [of F] by blast |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
31 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
32 |
lemma eventually_conj: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
33 |
"\<lbrakk>eventually (\<lambda>x. P x) F; eventually (\<lambda>x. Q x) F\<rbrakk> |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
34 |
\<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
35 |
unfolding eventually_def using Rep_filter [of F] by blast |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
36 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
37 |
lemma eventually_mp: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
38 |
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
39 |
assumes "eventually (\<lambda>x. P x) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
40 |
shows "eventually (\<lambda>x. Q x) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
41 |
proof (rule eventually_mono) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
42 |
show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
43 |
show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
44 |
using assms by (rule eventually_conj) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
45 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
46 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
47 |
lemma eventually_rev_mp: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
48 |
assumes "eventually (\<lambda>x. P x) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
49 |
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
50 |
shows "eventually (\<lambda>x. Q x) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
51 |
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
|
52 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
53 |
lemma eventually_conj_iff: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
54 |
"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
|
55 |
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
|
56 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
57 |
lemma eventually_Abs_filter: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
58 |
assumes "f (\<lambda>x. True)" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
59 |
assumes "\<And>P Q. (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> f P \<Longrightarrow> f Q" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
60 |
assumes "\<And>P Q. f P \<Longrightarrow> f Q \<Longrightarrow> f (\<lambda>x. P x \<and> Q x)" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
61 |
shows "eventually P (Abs_filter f) \<longleftrightarrow> f P" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
62 |
unfolding eventually_def using assms |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
63 |
by (subst Abs_filter_inverse, auto) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
64 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
65 |
lemma filter_ext: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
66 |
"(\<And>P. eventually P F \<longleftrightarrow> eventually P F') \<Longrightarrow> F = F'" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
67 |
unfolding eventually_def |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
68 |
by (simp add: Rep_filter_inject [THEN iffD1] ext) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
69 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
70 |
lemma eventually_elim1: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
71 |
assumes "eventually (\<lambda>i. P i) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
72 |
assumes "\<And>i. P i \<Longrightarrow> Q i" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
73 |
shows "eventually (\<lambda>i. Q i) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
74 |
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
|
75 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
76 |
lemma eventually_elim2: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
77 |
assumes "eventually (\<lambda>i. P i) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
78 |
assumes "eventually (\<lambda>i. Q i) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
79 |
assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
80 |
shows "eventually (\<lambda>i. R i) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
81 |
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
|
82 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
83 |
|
31355 | 84 |
subsection {* Boundedness *} |
85 |
||
86 |
definition |
|
87 |
Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where |
|
31357 | 88 |
[code del]: "Bfun S F = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) F)" |
31355 | 89 |
|
90 |
lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) F" shows "Bfun X F" |
|
91 |
unfolding Bfun_def |
|
92 |
proof (intro exI conjI allI) |
|
93 |
show "0 < max K 1" by simp |
|
94 |
next |
|
95 |
show "eventually (\<lambda>i. norm (X i) \<le> max K 1) F" |
|
96 |
using K by (rule eventually_elim1, simp) |
|
97 |
qed |
|
98 |
||
99 |
lemma BfunE: |
|
100 |
assumes "Bfun S F" |
|
101 |
obtains B where "0 < B" and "eventually (\<lambda>i. norm (S i) \<le> B) F" |
|
102 |
using assms unfolding Bfun_def by fast |
|
103 |
||
104 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
105 |
subsection {* Convergence to Zero *} |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
106 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
107 |
definition |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
108 |
Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where |
31353 | 109 |
[code del]: "Zfun S F = (\<forall>r>0. eventually (\<lambda>i. norm (S i) < r) F)" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
110 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
111 |
lemma ZfunI: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
112 |
"(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F) \<Longrightarrow> Zfun S F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
113 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
114 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
115 |
lemma ZfunD: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
116 |
"\<lbrakk>Zfun S F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
117 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
118 |
|
31355 | 119 |
lemma Zfun_ssubst: |
120 |
"eventually (\<lambda>i. X i = Y i) F \<Longrightarrow> Zfun Y F \<Longrightarrow> Zfun X F" |
|
121 |
unfolding Zfun_def by (auto elim!: eventually_rev_mp) |
|
122 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
123 |
lemma Zfun_zero: "Zfun (\<lambda>i. 0) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
124 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
125 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
126 |
lemma Zfun_norm_iff: "Zfun (\<lambda>i. norm (S i)) F = Zfun (\<lambda>i. S i) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
127 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
128 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
129 |
lemma Zfun_imp_Zfun: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
130 |
assumes X: "Zfun X F" |
31355 | 131 |
assumes Y: "eventually (\<lambda>i. norm (Y i) \<le> norm (X i) * K) F" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
132 |
shows "Zfun (\<lambda>n. Y n) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
133 |
proof (cases) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
134 |
assume K: "0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
135 |
show ?thesis |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
136 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
137 |
fix r::real assume "0 < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
138 |
hence "0 < r / K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
139 |
using K by (rule divide_pos_pos) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
140 |
then have "eventually (\<lambda>i. norm (X i) < r / K) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
141 |
using ZfunD [OF X] by fast |
31355 | 142 |
with Y show "eventually (\<lambda>i. norm (Y i) < r) F" |
143 |
proof (rule eventually_elim2) |
|
144 |
fix i |
|
145 |
assume *: "norm (Y i) \<le> norm (X i) * K" |
|
146 |
assume "norm (X i) < r / K" |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
147 |
hence "norm (X i) * K < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
148 |
by (simp add: pos_less_divide_eq K) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
149 |
thus "norm (Y i) < r" |
31355 | 150 |
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
|
151 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
152 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
153 |
next |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
154 |
assume "\<not> 0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
155 |
hence K: "K \<le> 0" by (simp only: not_less) |
31355 | 156 |
show ?thesis |
157 |
proof (rule ZfunI) |
|
158 |
fix r :: real |
|
159 |
assume "0 < r" |
|
160 |
from Y show "eventually (\<lambda>i. norm (Y i) < r) F" |
|
161 |
proof (rule eventually_elim1) |
|
162 |
fix i |
|
163 |
assume "norm (Y i) \<le> norm (X i) * K" |
|
164 |
also have "\<dots> \<le> norm (X i) * 0" |
|
165 |
using K norm_ge_zero by (rule mult_left_mono) |
|
166 |
finally show "norm (Y i) < r" |
|
167 |
using `0 < r` by simp |
|
168 |
qed |
|
169 |
qed |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
170 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
171 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
172 |
lemma Zfun_le: "\<lbrakk>Zfun Y F; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zfun X F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
173 |
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
|
174 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
175 |
lemma Zfun_add: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
176 |
assumes X: "Zfun X F" and Y: "Zfun Y F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
177 |
shows "Zfun (\<lambda>n. X n + Y n) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
178 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
179 |
fix r::real assume "0 < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
180 |
hence r: "0 < r / 2" by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
181 |
have "eventually (\<lambda>i. norm (X i) < r/2) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
182 |
using X r by (rule ZfunD) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
183 |
moreover |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
184 |
have "eventually (\<lambda>i. norm (Y i) < r/2) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
185 |
using Y r by (rule ZfunD) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
186 |
ultimately |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
187 |
show "eventually (\<lambda>i. norm (X i + Y i) < r) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
188 |
proof (rule eventually_elim2) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
189 |
fix i |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
190 |
assume *: "norm (X i) < r/2" "norm (Y i) < r/2" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
191 |
have "norm (X i + Y i) \<le> norm (X i) + norm (Y i)" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
192 |
by (rule norm_triangle_ineq) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
193 |
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
|
194 |
using * by (rule add_strict_mono) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
195 |
finally show "norm (X i + Y i) < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
196 |
by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
197 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
198 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
199 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
200 |
lemma Zfun_minus: "Zfun X F \<Longrightarrow> Zfun (\<lambda>i. - X i) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
201 |
unfolding Zfun_def by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
202 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
203 |
lemma Zfun_diff: "\<lbrakk>Zfun X F; Zfun Y F\<rbrakk> \<Longrightarrow> Zfun (\<lambda>i. X i - Y i) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
204 |
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
|
205 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
206 |
lemma (in bounded_linear) Zfun: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
207 |
assumes X: "Zfun X F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
208 |
shows "Zfun (\<lambda>n. f (X n)) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
209 |
proof - |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
210 |
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
|
211 |
using bounded by fast |
31355 | 212 |
then have "eventually (\<lambda>i. norm (f (X i)) \<le> norm (X i) * K) F" |
213 |
by simp |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
214 |
with X show ?thesis |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
215 |
by (rule Zfun_imp_Zfun) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
216 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
217 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
218 |
lemma (in bounded_bilinear) Zfun: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
219 |
assumes X: "Zfun X F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
220 |
assumes Y: "Zfun Y F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
221 |
shows "Zfun (\<lambda>n. X n ** Y n) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
222 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
223 |
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
|
224 |
obtain K where K: "0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
225 |
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
|
226 |
using pos_bounded by fast |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
227 |
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
|
228 |
by (rule positive_imp_inverse_positive) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
229 |
have "eventually (\<lambda>i. norm (X i) < r) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
230 |
using X r by (rule ZfunD) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
231 |
moreover |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
232 |
have "eventually (\<lambda>i. norm (Y i) < inverse K) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
233 |
using Y K' by (rule ZfunD) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
234 |
ultimately |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
235 |
show "eventually (\<lambda>i. norm (X i ** Y i) < r) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
236 |
proof (rule eventually_elim2) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
237 |
fix i |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
238 |
assume *: "norm (X i) < r" "norm (Y i) < inverse K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
239 |
have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
240 |
by (rule norm_le) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
241 |
also have "norm (X i) * norm (Y i) * K < r * inverse K * K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
242 |
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
|
243 |
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
|
244 |
by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
245 |
finally show "norm (X i ** Y i) < r" . |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
246 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
247 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
248 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
249 |
lemma (in bounded_bilinear) Zfun_left: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
250 |
"Zfun X F \<Longrightarrow> Zfun (\<lambda>n. X n ** a) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
251 |
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
|
252 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
253 |
lemma (in bounded_bilinear) Zfun_right: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
254 |
"Zfun X F \<Longrightarrow> Zfun (\<lambda>n. a ** X n) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
255 |
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
|
256 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
257 |
lemmas Zfun_mult = mult.Zfun |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
258 |
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
|
259 |
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
|
260 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
261 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
262 |
subsection{* Limits *} |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
263 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
264 |
definition |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
265 |
tendsto :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool" where |
31353 | 266 |
[code del]: "tendsto f l net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
267 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
268 |
lemma tendstoI: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
269 |
"(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
270 |
\<Longrightarrow> tendsto f l net" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
271 |
unfolding tendsto_def by auto |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
272 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
273 |
lemma tendstoD: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
274 |
"tendsto f l net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
275 |
unfolding tendsto_def by auto |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
276 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
277 |
lemma tendsto_Zfun_iff: "tendsto (\<lambda>n. X n) L F = Zfun (\<lambda>n. X n - L) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
278 |
by (simp only: tendsto_def Zfun_def dist_norm) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
279 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
280 |
lemma tendsto_const: "tendsto (\<lambda>n. k) k F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
281 |
by (simp add: tendsto_def) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
282 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
283 |
lemma tendsto_norm: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
284 |
fixes a :: "'a::real_normed_vector" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
285 |
shows "tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. norm (X n)) (norm a) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
286 |
apply (simp add: tendsto_def dist_norm, safe) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
287 |
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
|
288 |
apply (erule eventually_elim1) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
289 |
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
|
290 |
done |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
291 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
292 |
lemma add_diff_add: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
293 |
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
|
294 |
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
|
295 |
by simp |
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 minus_diff_minus: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
298 |
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
|
299 |
shows "(- a) - (- b) = - (a - b)" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
300 |
by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
301 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
302 |
lemma tendsto_add: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
303 |
fixes a b :: "'a::real_normed_vector" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
304 |
shows "\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n + Y n) (a + b) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
305 |
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
|
306 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
307 |
lemma tendsto_minus: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
308 |
fixes a :: "'a::real_normed_vector" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
309 |
shows "tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. - X n) (- a) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
310 |
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
|
311 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
312 |
lemma tendsto_minus_cancel: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
313 |
fixes a :: "'a::real_normed_vector" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
314 |
shows "tendsto (\<lambda>n. - X n) (- a) F \<Longrightarrow> tendsto X a F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
315 |
by (drule tendsto_minus, simp) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
316 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
317 |
lemma tendsto_diff: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
318 |
fixes a b :: "'a::real_normed_vector" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
319 |
shows "\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n - Y n) (a - b) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
320 |
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
|
321 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
322 |
lemma (in bounded_linear) tendsto: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
323 |
"tendsto X a F \<Longrightarrow> tendsto (\<lambda>n. f (X n)) (f a) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
324 |
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
|
325 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
326 |
lemma (in bounded_bilinear) tendsto: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
327 |
"\<lbrakk>tendsto X a F; tendsto Y b F\<rbrakk> \<Longrightarrow> tendsto (\<lambda>n. X n ** Y n) (a ** b) F" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
328 |
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
|
329 |
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
|
330 |
|
31355 | 331 |
|
332 |
subsection {* Continuity of Inverse *} |
|
333 |
||
334 |
lemma (in bounded_bilinear) Zfun_prod_Bfun: |
|
335 |
assumes X: "Zfun X F" |
|
336 |
assumes Y: "Bfun Y F" |
|
337 |
shows "Zfun (\<lambda>n. X n ** Y n) F" |
|
338 |
proof - |
|
339 |
obtain K where K: "0 \<le> K" |
|
340 |
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
341 |
using nonneg_bounded by fast |
|
342 |
obtain B where B: "0 < B" |
|
343 |
and norm_Y: "eventually (\<lambda>i. norm (Y i) \<le> B) F" |
|
344 |
using Y by (rule BfunE) |
|
345 |
have "eventually (\<lambda>i. norm (X i ** Y i) \<le> norm (X i) * (B * K)) F" |
|
346 |
using norm_Y proof (rule eventually_elim1) |
|
347 |
fix i |
|
348 |
assume *: "norm (Y i) \<le> B" |
|
349 |
have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K" |
|
350 |
by (rule norm_le) |
|
351 |
also have "\<dots> \<le> norm (X i) * B * K" |
|
352 |
by (intro mult_mono' order_refl norm_Y norm_ge_zero |
|
353 |
mult_nonneg_nonneg K *) |
|
354 |
also have "\<dots> = norm (X i) * (B * K)" |
|
355 |
by (rule mult_assoc) |
|
356 |
finally show "norm (X i ** Y i) \<le> norm (X i) * (B * K)" . |
|
357 |
qed |
|
358 |
with X show ?thesis |
|
359 |
by (rule Zfun_imp_Zfun) |
|
360 |
qed |
|
361 |
||
362 |
lemma (in bounded_bilinear) flip: |
|
363 |
"bounded_bilinear (\<lambda>x y. y ** x)" |
|
364 |
apply default |
|
365 |
apply (rule add_right) |
|
366 |
apply (rule add_left) |
|
367 |
apply (rule scaleR_right) |
|
368 |
apply (rule scaleR_left) |
|
369 |
apply (subst mult_commute) |
|
370 |
using bounded by fast |
|
371 |
||
372 |
lemma (in bounded_bilinear) Bfun_prod_Zfun: |
|
373 |
assumes X: "Bfun X F" |
|
374 |
assumes Y: "Zfun Y F" |
|
375 |
shows "Zfun (\<lambda>n. X n ** Y n) F" |
|
376 |
using flip Y X by (rule bounded_bilinear.Zfun_prod_Bfun) |
|
377 |
||
378 |
lemma inverse_diff_inverse: |
|
379 |
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk> |
|
380 |
\<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)" |
|
381 |
by (simp add: algebra_simps) |
|
382 |
||
383 |
lemma Bfun_inverse_lemma: |
|
384 |
fixes x :: "'a::real_normed_div_algebra" |
|
385 |
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" |
|
386 |
apply (subst nonzero_norm_inverse, clarsimp) |
|
387 |
apply (erule (1) le_imp_inverse_le) |
|
388 |
done |
|
389 |
||
390 |
lemma Bfun_inverse: |
|
391 |
fixes a :: "'a::real_normed_div_algebra" |
|
392 |
assumes X: "tendsto X a F" |
|
393 |
assumes a: "a \<noteq> 0" |
|
394 |
shows "Bfun (\<lambda>n. inverse (X n)) F" |
|
395 |
proof - |
|
396 |
from a have "0 < norm a" by simp |
|
397 |
hence "\<exists>r>0. r < norm a" by (rule dense) |
|
398 |
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast |
|
399 |
have "eventually (\<lambda>i. dist (X i) a < r) F" |
|
400 |
using tendstoD [OF X r1] by fast |
|
401 |
hence "eventually (\<lambda>i. norm (inverse (X i)) \<le> inverse (norm a - r)) F" |
|
402 |
proof (rule eventually_elim1) |
|
403 |
fix i |
|
404 |
assume "dist (X i) a < r" |
|
405 |
hence 1: "norm (X i - a) < r" |
|
406 |
by (simp add: dist_norm) |
|
407 |
hence 2: "X i \<noteq> 0" using r2 by auto |
|
408 |
hence "norm (inverse (X i)) = inverse (norm (X i))" |
|
409 |
by (rule nonzero_norm_inverse) |
|
410 |
also have "\<dots> \<le> inverse (norm a - r)" |
|
411 |
proof (rule le_imp_inverse_le) |
|
412 |
show "0 < norm a - r" using r2 by simp |
|
413 |
next |
|
414 |
have "norm a - norm (X i) \<le> norm (a - X i)" |
|
415 |
by (rule norm_triangle_ineq2) |
|
416 |
also have "\<dots> = norm (X i - a)" |
|
417 |
by (rule norm_minus_commute) |
|
418 |
also have "\<dots> < r" using 1 . |
|
419 |
finally show "norm a - r \<le> norm (X i)" by simp |
|
420 |
qed |
|
421 |
finally show "norm (inverse (X i)) \<le> inverse (norm a - r)" . |
|
422 |
qed |
|
423 |
thus ?thesis by (rule BfunI) |
|
424 |
qed |
|
425 |
||
426 |
lemma tendsto_inverse_lemma: |
|
427 |
fixes a :: "'a::real_normed_div_algebra" |
|
428 |
shows "\<lbrakk>tendsto X a F; a \<noteq> 0; eventually (\<lambda>i. X i \<noteq> 0) F\<rbrakk> |
|
429 |
\<Longrightarrow> tendsto (\<lambda>i. inverse (X i)) (inverse a) F" |
|
430 |
apply (subst tendsto_Zfun_iff) |
|
431 |
apply (rule Zfun_ssubst) |
|
432 |
apply (erule eventually_elim1) |
|
433 |
apply (erule (1) inverse_diff_inverse) |
|
434 |
apply (rule Zfun_minus) |
|
435 |
apply (rule Zfun_mult_left) |
|
436 |
apply (rule mult.Bfun_prod_Zfun) |
|
437 |
apply (erule (1) Bfun_inverse) |
|
438 |
apply (simp add: tendsto_Zfun_iff) |
|
439 |
done |
|
440 |
||
441 |
lemma tendsto_inverse: |
|
442 |
fixes a :: "'a::real_normed_div_algebra" |
|
443 |
assumes X: "tendsto X a F" |
|
444 |
assumes a: "a \<noteq> 0" |
|
445 |
shows "tendsto (\<lambda>i. inverse (X i)) (inverse a) F" |
|
446 |
proof - |
|
447 |
from a have "0 < norm a" by simp |
|
448 |
with X have "eventually (\<lambda>i. dist (X i) a < norm a) F" |
|
449 |
by (rule tendstoD) |
|
450 |
then have "eventually (\<lambda>i. X i \<noteq> 0) F" |
|
451 |
unfolding dist_norm by (auto elim!: eventually_elim1) |
|
452 |
with X a show ?thesis |
|
453 |
by (rule tendsto_inverse_lemma) |
|
454 |
qed |
|
455 |
||
456 |
lemma tendsto_divide: |
|
457 |
fixes a b :: "'a::real_normed_field" |
|
458 |
shows "\<lbrakk>tendsto X a F; tendsto Y b F; b \<noteq> 0\<rbrakk> |
|
459 |
\<Longrightarrow> tendsto (\<lambda>n. X n / Y n) (a / b) F" |
|
460 |
by (simp add: mult.tendsto tendsto_inverse divide_inverse) |
|
461 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
462 |
end |