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