author | huffman |
Mon, 08 Aug 2011 19:26:53 -0700 | |
changeset 44081 | 730f7cced3a6 |
parent 44079 | bcc60791b7b9 |
child 44194 | 0639898074ae |
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 |
36822 | 8 |
imports RealVector |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
9 |
begin |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
10 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
11 |
subsection {* Filters *} |
31392 | 12 |
|
13 |
text {* |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
14 |
This definition also allows non-proper filters. |
31392 | 15 |
*} |
16 |
||
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset
|
17 |
locale is_filter = |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
18 |
fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
19 |
assumes True: "F (\<lambda>x. True)" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
20 |
assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
21 |
assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)" |
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset
|
22 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
23 |
typedef (open) 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}" |
31392 | 24 |
proof |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
25 |
show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro) |
31392 | 26 |
qed |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
27 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
28 |
lemma is_filter_Rep_filter: "is_filter (Rep_filter A)" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
29 |
using Rep_filter [of A] by simp |
31392 | 30 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
31 |
lemma Abs_filter_inverse': |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
32 |
assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
33 |
using assms by (simp add: Abs_filter_inverse) |
31392 | 34 |
|
35 |
||
36 |
subsection {* Eventually *} |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
37 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
38 |
definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
39 |
where "eventually P A \<longleftrightarrow> Rep_filter A P" |
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset
|
40 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
41 |
lemma eventually_Abs_filter: |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
42 |
assumes "is_filter F" shows "eventually P (Abs_filter F) = F P" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
43 |
unfolding eventually_def using assms by (simp add: Abs_filter_inverse) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
44 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
45 |
lemma filter_eq_iff: |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
46 |
shows "A = B \<longleftrightarrow> (\<forall>P. eventually P A = eventually P B)" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
47 |
unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def .. |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
48 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
49 |
lemma eventually_True [simp]: "eventually (\<lambda>x. True) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
50 |
unfolding eventually_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
51 |
by (rule is_filter.True [OF is_filter_Rep_filter]) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
52 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
53 |
lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P A" |
36630 | 54 |
proof - |
55 |
assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext) |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
56 |
thus "eventually P A" by simp |
36630 | 57 |
qed |
58 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
59 |
lemma eventually_mono: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
60 |
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P A \<Longrightarrow> eventually Q A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
61 |
unfolding eventually_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
62 |
by (rule is_filter.mono [OF is_filter_Rep_filter]) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
63 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
64 |
lemma eventually_conj: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
65 |
assumes P: "eventually (\<lambda>x. P x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
66 |
assumes Q: "eventually (\<lambda>x. Q x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
67 |
shows "eventually (\<lambda>x. P x \<and> Q x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
68 |
using assms unfolding eventually_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
69 |
by (rule is_filter.conj [OF is_filter_Rep_filter]) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
70 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
71 |
lemma eventually_mp: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
72 |
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
73 |
assumes "eventually (\<lambda>x. P x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
74 |
shows "eventually (\<lambda>x. Q x) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
75 |
proof (rule eventually_mono) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
76 |
show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
77 |
show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
78 |
using assms by (rule eventually_conj) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
79 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
80 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
81 |
lemma eventually_rev_mp: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
82 |
assumes "eventually (\<lambda>x. P x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
83 |
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
84 |
shows "eventually (\<lambda>x. Q x) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
85 |
using assms(2) assms(1) by (rule eventually_mp) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
86 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
87 |
lemma eventually_conj_iff: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
88 |
"eventually (\<lambda>x. P x \<and> Q x) A \<longleftrightarrow> eventually P A \<and> eventually Q A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
89 |
by (auto intro: eventually_conj elim: eventually_rev_mp) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
90 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
91 |
lemma eventually_elim1: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
92 |
assumes "eventually (\<lambda>i. P i) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
93 |
assumes "\<And>i. P i \<Longrightarrow> Q i" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
94 |
shows "eventually (\<lambda>i. Q i) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
95 |
using assms by (auto elim!: eventually_rev_mp) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
96 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
97 |
lemma eventually_elim2: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
98 |
assumes "eventually (\<lambda>i. P i) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
99 |
assumes "eventually (\<lambda>i. Q i) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
100 |
assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
101 |
shows "eventually (\<lambda>i. R i) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
102 |
using assms by (auto elim!: eventually_rev_mp) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
103 |
|
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
104 |
subsection {* Finer-than relation *} |
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
105 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
106 |
text {* @{term "A \<le> B"} means that filter @{term A} is finer than |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
107 |
filter @{term B}. *} |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
108 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
109 |
instantiation filter :: (type) complete_lattice |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
110 |
begin |
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
111 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
112 |
definition le_filter_def: |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
113 |
"A \<le> B \<longleftrightarrow> (\<forall>P. eventually P B \<longrightarrow> eventually P A)" |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
114 |
|
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
115 |
definition |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
116 |
"(A :: 'a filter) < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A" |
36360
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 |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
119 |
"top = Abs_filter (\<lambda>P. \<forall>x. P x)" |
36630 | 120 |
|
121 |
definition |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
122 |
"bot = Abs_filter (\<lambda>P. True)" |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
123 |
|
36630 | 124 |
definition |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
125 |
"sup A B = Abs_filter (\<lambda>P. eventually P A \<and> eventually P B)" |
36630 | 126 |
|
127 |
definition |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
128 |
"inf A B = Abs_filter |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
129 |
(\<lambda>P. \<exists>Q R. eventually Q A \<and> eventually R B \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))" |
36630 | 130 |
|
131 |
definition |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
132 |
"Sup S = Abs_filter (\<lambda>P. \<forall>A\<in>S. eventually P A)" |
36630 | 133 |
|
134 |
definition |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
135 |
"Inf S = Sup {A::'a filter. \<forall>B\<in>S. A \<le> B}" |
36630 | 136 |
|
137 |
lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
138 |
unfolding top_filter_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
139 |
by (rule eventually_Abs_filter, rule is_filter.intro, auto) |
36630 | 140 |
|
36629
de62713aec6e
swap ordering on nets, so x <= y means 'x is finer than y'
huffman
parents:
36360
diff
changeset
|
141 |
lemma eventually_bot [simp]: "eventually P bot" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
142 |
unfolding bot_filter_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
143 |
by (subst eventually_Abs_filter, rule is_filter.intro, auto) |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
144 |
|
36630 | 145 |
lemma eventually_sup: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
146 |
"eventually P (sup A B) \<longleftrightarrow> eventually P A \<and> eventually P B" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
147 |
unfolding sup_filter_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
148 |
by (rule eventually_Abs_filter, rule is_filter.intro) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
149 |
(auto elim!: eventually_rev_mp) |
36630 | 150 |
|
151 |
lemma eventually_inf: |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
152 |
"eventually P (inf A B) \<longleftrightarrow> |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
153 |
(\<exists>Q R. eventually Q A \<and> eventually R B \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
154 |
unfolding inf_filter_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
155 |
apply (rule eventually_Abs_filter, rule is_filter.intro) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
156 |
apply (fast intro: eventually_True) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
157 |
apply clarify |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
158 |
apply (intro exI conjI) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
159 |
apply (erule (1) eventually_conj) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
160 |
apply (erule (1) eventually_conj) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
161 |
apply simp |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
162 |
apply auto |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
163 |
done |
36630 | 164 |
|
165 |
lemma eventually_Sup: |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
166 |
"eventually P (Sup S) \<longleftrightarrow> (\<forall>A\<in>S. eventually P A)" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
167 |
unfolding Sup_filter_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
168 |
apply (rule eventually_Abs_filter, rule is_filter.intro) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
169 |
apply (auto intro: eventually_conj elim!: eventually_rev_mp) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
170 |
done |
36630 | 171 |
|
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
172 |
instance proof |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
173 |
fix A B :: "'a filter" show "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
174 |
by (rule less_filter_def) |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
175 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
176 |
fix A :: "'a filter" show "A \<le> A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
177 |
unfolding le_filter_def by simp |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
178 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
179 |
fix A B C :: "'a filter" assume "A \<le> B" and "B \<le> C" thus "A \<le> C" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
180 |
unfolding le_filter_def by simp |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
181 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
182 |
fix A B :: "'a filter" assume "A \<le> B" and "B \<le> A" thus "A = B" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
183 |
unfolding le_filter_def filter_eq_iff by fast |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
184 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
185 |
fix A :: "'a filter" show "A \<le> top" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
186 |
unfolding le_filter_def eventually_top by (simp add: always_eventually) |
36630 | 187 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
188 |
fix A :: "'a filter" show "bot \<le> A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
189 |
unfolding le_filter_def by simp |
36630 | 190 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
191 |
fix A B :: "'a filter" show "A \<le> sup A B" and "B \<le> sup A B" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
192 |
unfolding le_filter_def eventually_sup by simp_all |
36630 | 193 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
194 |
fix A B C :: "'a filter" assume "A \<le> C" and "B \<le> C" thus "sup A B \<le> C" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
195 |
unfolding le_filter_def eventually_sup by simp |
36630 | 196 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
197 |
fix A B :: "'a filter" show "inf A B \<le> A" and "inf A B \<le> B" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
198 |
unfolding le_filter_def eventually_inf by (auto intro: eventually_True) |
36630 | 199 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
200 |
fix A B C :: "'a filter" assume "A \<le> B" and "A \<le> C" thus "A \<le> inf B C" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
201 |
unfolding le_filter_def eventually_inf |
36630 | 202 |
by (auto elim!: eventually_mono intro: eventually_conj) |
203 |
next |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
204 |
fix A :: "'a filter" and S assume "A \<in> S" thus "A \<le> Sup S" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
205 |
unfolding le_filter_def eventually_Sup by simp |
36630 | 206 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
207 |
fix S and B :: "'a filter" assume "\<And>A. A \<in> S \<Longrightarrow> A \<le> B" thus "Sup S \<le> B" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
208 |
unfolding le_filter_def eventually_Sup by simp |
36630 | 209 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
210 |
fix C :: "'a filter" and S assume "C \<in> S" thus "Inf S \<le> C" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
211 |
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp |
36630 | 212 |
next |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
213 |
fix S and A :: "'a filter" assume "\<And>B. B \<in> S \<Longrightarrow> A \<le> B" thus "A \<le> Inf S" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
214 |
unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
215 |
qed |
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
216 |
|
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
217 |
end |
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
218 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
219 |
lemma filter_leD: |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
220 |
"A \<le> B \<Longrightarrow> eventually P B \<Longrightarrow> eventually P A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
221 |
unfolding le_filter_def by simp |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
222 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
223 |
lemma filter_leI: |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
224 |
"(\<And>P. eventually P B \<Longrightarrow> eventually P A) \<Longrightarrow> A \<le> B" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
225 |
unfolding le_filter_def by simp |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
226 |
|
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
227 |
lemma eventually_False: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
228 |
"eventually (\<lambda>x. False) A \<longleftrightarrow> A = bot" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
229 |
unfolding filter_eq_iff by (auto elim: eventually_rev_mp) |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
230 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
231 |
subsection {* Map function for filters *} |
36654 | 232 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
233 |
definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
234 |
where "filtermap f A = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) A)" |
36654 | 235 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
236 |
lemma eventually_filtermap: |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
237 |
"eventually P (filtermap f A) = eventually (\<lambda>x. P (f x)) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
238 |
unfolding filtermap_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
239 |
apply (rule eventually_Abs_filter) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
240 |
apply (rule is_filter.intro) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
241 |
apply (auto elim!: eventually_rev_mp) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
242 |
done |
36654 | 243 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
244 |
lemma filtermap_ident: "filtermap (\<lambda>x. x) A = A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
245 |
by (simp add: filter_eq_iff eventually_filtermap) |
36654 | 246 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
247 |
lemma filtermap_filtermap: |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
248 |
"filtermap f (filtermap g A) = filtermap (\<lambda>x. f (g x)) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
249 |
by (simp add: filter_eq_iff eventually_filtermap) |
36654 | 250 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
251 |
lemma filtermap_mono: "A \<le> B \<Longrightarrow> filtermap f A \<le> filtermap f B" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
252 |
unfolding le_filter_def eventually_filtermap by simp |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
253 |
|
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
254 |
lemma filtermap_bot [simp]: "filtermap f bot = bot" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
255 |
by (simp add: filter_eq_iff eventually_filtermap) |
36654 | 256 |
|
257 |
||
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
258 |
subsection {* Sequentially *} |
31392 | 259 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
260 |
definition sequentially :: "nat filter" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
261 |
where "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)" |
31392 | 262 |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
263 |
lemma eventually_sequentially: |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
264 |
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)" |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
265 |
unfolding sequentially_def |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
266 |
proof (rule eventually_Abs_filter, rule is_filter.intro) |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
267 |
fix P Q :: "nat \<Rightarrow> bool" |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
268 |
assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n" |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
269 |
then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
270 |
then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
271 |
then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" .. |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
272 |
qed auto |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
273 |
|
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
274 |
lemma sequentially_bot [simp]: "sequentially \<noteq> bot" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
275 |
unfolding filter_eq_iff eventually_sequentially by auto |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
276 |
|
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
277 |
lemma eventually_False_sequentially [simp]: |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
278 |
"\<not> eventually (\<lambda>n. False) sequentially" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
279 |
by (simp add: eventually_False) |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
280 |
|
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
281 |
lemma le_sequentially: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
282 |
"A \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) A)" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
283 |
unfolding le_filter_def eventually_sequentially |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
284 |
by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
285 |
|
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
286 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
287 |
definition trivial_limit :: "'a filter \<Rightarrow> bool" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
288 |
where "trivial_limit A \<longleftrightarrow> eventually (\<lambda>x. False) A" |
41970 | 289 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
290 |
lemma trivial_limit_sequentially [intro]: "\<not> trivial_limit sequentially" |
41970 | 291 |
by (auto simp add: trivial_limit_def eventually_sequentially) |
292 |
||
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
293 |
subsection {* Standard filters *} |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
294 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
295 |
definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
296 |
where "A within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) A)" |
31392 | 297 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
298 |
definition nhds :: "'a::topological_space \<Rightarrow> 'a filter" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
299 |
where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))" |
36654 | 300 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
301 |
definition at :: "'a::topological_space \<Rightarrow> 'a filter" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
302 |
where "at a = nhds a within - {a}" |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
303 |
|
31392 | 304 |
lemma eventually_within: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
305 |
"eventually P (A within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
306 |
unfolding within_def |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
307 |
by (rule eventually_Abs_filter, rule is_filter.intro) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
308 |
(auto elim!: eventually_rev_mp) |
31392 | 309 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
310 |
lemma within_UNIV: "A within UNIV = A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
311 |
unfolding filter_eq_iff eventually_within by simp |
36360
9d8f7efd9289
define finer-than ordering on net type; move some theorems into Limits.thy
huffman
parents:
36358
diff
changeset
|
312 |
|
36654 | 313 |
lemma eventually_nhds: |
314 |
"eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))" |
|
315 |
unfolding nhds_def |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
316 |
proof (rule eventually_Abs_filter, rule is_filter.intro) |
36654 | 317 |
have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp |
318 |
thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" by - rule |
|
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset
|
319 |
next |
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset
|
320 |
fix P Q |
36654 | 321 |
assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)" |
322 |
and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" |
|
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset
|
323 |
then obtain S T where |
36654 | 324 |
"open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)" |
325 |
"open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto |
|
326 |
hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)" |
|
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset
|
327 |
by (simp add: open_Int) |
36654 | 328 |
thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" by - rule |
36358
246493d61204
define nets directly as filters, instead of as filter bases
huffman
parents:
31902
diff
changeset
|
329 |
qed auto |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
330 |
|
36656
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
331 |
lemma eventually_nhds_metric: |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
332 |
"eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)" |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
333 |
unfolding eventually_nhds open_dist |
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
334 |
apply safe |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
335 |
apply fast |
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31488
diff
changeset
|
336 |
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
|
337 |
apply clarsimp |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
338 |
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
|
339 |
apply (simp only: less_diff_eq) |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
340 |
apply (erule le_less_trans [OF dist_triangle]) |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
341 |
done |
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31392
diff
changeset
|
342 |
|
36656
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
343 |
lemma eventually_at_topological: |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
344 |
"eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))" |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
345 |
unfolding at_def eventually_within eventually_nhds by simp |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
346 |
|
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
347 |
lemma eventually_at: |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
348 |
fixes a :: "'a::metric_space" |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
349 |
shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)" |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
350 |
unfolding at_def eventually_within eventually_nhds_metric by auto |
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
351 |
|
31392 | 352 |
|
31355 | 353 |
subsection {* Boundedness *} |
354 |
||
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
355 |
definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
356 |
where "Bfun f A = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) A)" |
31355 | 357 |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
358 |
lemma BfunI: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
359 |
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) A" shows "Bfun f A" |
31355 | 360 |
unfolding Bfun_def |
361 |
proof (intro exI conjI allI) |
|
362 |
show "0 < max K 1" by simp |
|
363 |
next |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
364 |
show "eventually (\<lambda>x. norm (f x) \<le> max K 1) A" |
31355 | 365 |
using K by (rule eventually_elim1, simp) |
366 |
qed |
|
367 |
||
368 |
lemma BfunE: |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
369 |
assumes "Bfun f A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
370 |
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) A" |
31355 | 371 |
using assms unfolding Bfun_def by fast |
372 |
||
373 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
374 |
subsection {* Convergence to Zero *} |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
375 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
376 |
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
377 |
where "Zfun f A = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) A)" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
378 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
379 |
lemma ZfunI: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
380 |
"(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) A) \<Longrightarrow> Zfun f A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
381 |
unfolding Zfun_def by simp |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
382 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
383 |
lemma ZfunD: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
384 |
"\<lbrakk>Zfun f A; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
385 |
unfolding Zfun_def by simp |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
386 |
|
31355 | 387 |
lemma Zfun_ssubst: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
388 |
"eventually (\<lambda>x. f x = g x) A \<Longrightarrow> Zfun g A \<Longrightarrow> Zfun f A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
389 |
unfolding Zfun_def by (auto elim!: eventually_rev_mp) |
31355 | 390 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
391 |
lemma Zfun_zero: "Zfun (\<lambda>x. 0) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
392 |
unfolding Zfun_def by simp |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
393 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
394 |
lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) A = Zfun (\<lambda>x. f x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
395 |
unfolding Zfun_def by simp |
31349
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 Zfun_imp_Zfun: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
398 |
assumes f: "Zfun f A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
399 |
assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
400 |
shows "Zfun (\<lambda>x. g x) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
401 |
proof (cases) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
402 |
assume K: "0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
403 |
show ?thesis |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
404 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
405 |
fix r::real assume "0 < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
406 |
hence "0 < r / K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
407 |
using K by (rule divide_pos_pos) |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
408 |
then have "eventually (\<lambda>x. norm (f x) < r / K) A" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
409 |
using ZfunD [OF f] by fast |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
410 |
with g show "eventually (\<lambda>x. norm (g x) < r) A" |
31355 | 411 |
proof (rule eventually_elim2) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
412 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
413 |
assume *: "norm (g x) \<le> norm (f x) * K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
414 |
assume "norm (f x) < r / K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
415 |
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
|
416 |
by (simp add: pos_less_divide_eq K) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
417 |
thus "norm (g x) < r" |
31355 | 418 |
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
|
419 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
420 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
421 |
next |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
422 |
assume "\<not> 0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
423 |
hence K: "K \<le> 0" by (simp only: not_less) |
31355 | 424 |
show ?thesis |
425 |
proof (rule ZfunI) |
|
426 |
fix r :: real |
|
427 |
assume "0 < r" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
428 |
from g show "eventually (\<lambda>x. norm (g x) < r) A" |
31355 | 429 |
proof (rule eventually_elim1) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
430 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
431 |
assume "norm (g x) \<le> norm (f x) * K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
432 |
also have "\<dots> \<le> norm (f x) * 0" |
31355 | 433 |
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
|
434 |
finally show "norm (g x) < r" |
31355 | 435 |
using `0 < r` by simp |
436 |
qed |
|
437 |
qed |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
438 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
439 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
440 |
lemma Zfun_le: "\<lbrakk>Zfun g A; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
441 |
by (erule_tac K="1" in Zfun_imp_Zfun, simp) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
442 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
443 |
lemma Zfun_add: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
444 |
assumes f: "Zfun f A" and g: "Zfun g A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
445 |
shows "Zfun (\<lambda>x. f x + g x) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
446 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
447 |
fix r::real assume "0 < r" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
448 |
hence r: "0 < r / 2" by simp |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
449 |
have "eventually (\<lambda>x. norm (f x) < r/2) A" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
450 |
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
|
451 |
moreover |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
452 |
have "eventually (\<lambda>x. norm (g x) < r/2) A" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
453 |
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
|
454 |
ultimately |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
455 |
show "eventually (\<lambda>x. norm (f x + g x) < r) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
456 |
proof (rule eventually_elim2) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
457 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
458 |
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
|
459 |
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
|
460 |
by (rule norm_triangle_ineq) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
461 |
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
|
462 |
using * by (rule add_strict_mono) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
463 |
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
|
464 |
by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
465 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
466 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
467 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
468 |
lemma Zfun_minus: "Zfun f A \<Longrightarrow> Zfun (\<lambda>x. - f x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
469 |
unfolding Zfun_def by simp |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
470 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
471 |
lemma Zfun_diff: "\<lbrakk>Zfun f A; Zfun g A\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
472 |
by (simp only: diff_minus Zfun_add Zfun_minus) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
473 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
474 |
lemma (in bounded_linear) Zfun: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
475 |
assumes g: "Zfun g A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
476 |
shows "Zfun (\<lambda>x. f (g x)) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
477 |
proof - |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
478 |
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
|
479 |
using bounded by fast |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
480 |
then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) A" |
31355 | 481 |
by simp |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
482 |
with g show ?thesis |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
483 |
by (rule Zfun_imp_Zfun) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
484 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
485 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
486 |
lemma (in bounded_bilinear) Zfun: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
487 |
assumes f: "Zfun f A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
488 |
assumes g: "Zfun g A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
489 |
shows "Zfun (\<lambda>x. f x ** g x) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
490 |
proof (rule ZfunI) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
491 |
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
|
492 |
obtain K where K: "0 < K" |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
493 |
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
|
494 |
using pos_bounded by fast |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
495 |
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
|
496 |
by (rule positive_imp_inverse_positive) |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
497 |
have "eventually (\<lambda>x. norm (f x) < r) A" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
498 |
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
|
499 |
moreover |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
500 |
have "eventually (\<lambda>x. norm (g x) < inverse K) A" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
501 |
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
|
502 |
ultimately |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
503 |
show "eventually (\<lambda>x. norm (f x ** g x) < r) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
504 |
proof (rule eventually_elim2) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
505 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
506 |
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
|
507 |
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
|
508 |
by (rule norm_le) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
509 |
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
|
510 |
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
|
511 |
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
|
512 |
by simp |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
513 |
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
|
514 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
515 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
516 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
517 |
lemma (in bounded_bilinear) Zfun_left: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
518 |
"Zfun f A \<Longrightarrow> Zfun (\<lambda>x. f x ** a) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
519 |
by (rule bounded_linear_left [THEN bounded_linear.Zfun]) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
520 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
521 |
lemma (in bounded_bilinear) Zfun_right: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
522 |
"Zfun f A \<Longrightarrow> Zfun (\<lambda>x. a ** f x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
523 |
by (rule bounded_linear_right [THEN bounded_linear.Zfun]) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
524 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
525 |
lemmas Zfun_mult = mult.Zfun |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
526 |
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
|
527 |
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
|
528 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
529 |
|
31902 | 530 |
subsection {* Limits *} |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
531 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
532 |
definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool" |
37767 | 533 |
(infixr "--->" 55) where |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
534 |
"(f ---> l) A \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) A)" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
535 |
|
31902 | 536 |
ML {* |
537 |
structure Tendsto_Intros = Named_Thms |
|
538 |
( |
|
539 |
val name = "tendsto_intros" |
|
540 |
val description = "introduction rules for tendsto" |
|
541 |
) |
|
31565 | 542 |
*} |
543 |
||
31902 | 544 |
setup Tendsto_Intros.setup |
31565 | 545 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
546 |
lemma tendsto_mono: "A \<le> A' \<Longrightarrow> (f ---> l) A' \<Longrightarrow> (f ---> l) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
547 |
unfolding tendsto_def le_filter_def by fast |
36656
fec55067ae9b
add lemmas eventually_nhds_metric and tendsto_mono
huffman
parents:
36655
diff
changeset
|
548 |
|
31488 | 549 |
lemma topological_tendstoI: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
550 |
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) A) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
551 |
\<Longrightarrow> (f ---> l) A" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
552 |
unfolding tendsto_def by auto |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
553 |
|
31488 | 554 |
lemma topological_tendstoD: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
555 |
"(f ---> l) A \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) A" |
31488 | 556 |
unfolding tendsto_def by auto |
557 |
||
558 |
lemma tendstoI: |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
559 |
assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
560 |
shows "(f ---> l) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
561 |
apply (rule topological_tendstoI) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
562 |
apply (simp add: open_dist) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
563 |
apply (drule (1) bspec, clarify) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
564 |
apply (drule assms) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
565 |
apply (erule eventually_elim1, simp) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
566 |
done |
31488 | 567 |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
568 |
lemma tendstoD: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
569 |
"(f ---> l) A \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
570 |
apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
571 |
apply (clarsimp simp add: open_dist) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
572 |
apply (rule_tac x="e - dist x l" in exI, clarsimp) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
573 |
apply (simp only: less_diff_eq) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
574 |
apply (erule le_less_trans [OF dist_triangle]) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
575 |
apply simp |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
576 |
apply simp |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
577 |
done |
31488 | 578 |
|
579 |
lemma tendsto_iff: |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
580 |
"(f ---> l) A \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) A)" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
581 |
using tendstoI tendstoD by fast |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
582 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
583 |
lemma tendsto_Zfun_iff: "(f ---> a) A = Zfun (\<lambda>x. f x - a) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
584 |
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
|
585 |
|
31565 | 586 |
lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
587 |
unfolding tendsto_def eventually_at_topological by auto |
31565 | 588 |
|
589 |
lemma tendsto_ident_at_within [tendsto_intros]: |
|
36655 | 590 |
"((\<lambda>x. x) ---> a) (at a within S)" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
591 |
unfolding tendsto_def eventually_within eventually_at_topological by auto |
31565 | 592 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
593 |
lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
594 |
by (simp add: tendsto_def) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
595 |
|
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
596 |
lemma tendsto_const_iff: |
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
597 |
fixes k l :: "'a::metric_space" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
598 |
assumes "A \<noteq> bot" shows "((\<lambda>n. k) ---> l) A \<longleftrightarrow> k = l" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
599 |
apply (safe intro!: tendsto_const) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
600 |
apply (rule ccontr) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
601 |
apply (drule_tac e="dist k l" in tendstoD) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
602 |
apply (simp add: zero_less_dist_iff) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
603 |
apply (simp add: eventually_False assms) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
604 |
done |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
605 |
|
31565 | 606 |
lemma tendsto_dist [tendsto_intros]: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
607 |
assumes f: "(f ---> l) A" and g: "(g ---> m) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
608 |
shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) A" |
31565 | 609 |
proof (rule tendstoI) |
610 |
fix e :: real assume "0 < e" |
|
611 |
hence e2: "0 < e/2" by simp |
|
612 |
from tendstoD [OF f e2] tendstoD [OF g e2] |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
613 |
show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) A" |
31565 | 614 |
proof (rule eventually_elim2) |
615 |
fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2" |
|
616 |
then show "dist (dist (f x) (g x)) (dist l m) < e" |
|
617 |
unfolding dist_real_def |
|
618 |
using dist_triangle2 [of "f x" "g x" "l"] |
|
619 |
using dist_triangle2 [of "g x" "l" "m"] |
|
620 |
using dist_triangle3 [of "l" "m" "f x"] |
|
621 |
using dist_triangle [of "f x" "m" "g x"] |
|
622 |
by arith |
|
623 |
qed |
|
624 |
qed |
|
625 |
||
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
626 |
lemma norm_conv_dist: "norm x = dist x 0" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
627 |
unfolding dist_norm by simp |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
628 |
|
31565 | 629 |
lemma tendsto_norm [tendsto_intros]: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
630 |
"(f ---> a) A \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
631 |
unfolding norm_conv_dist by (intro tendsto_intros) |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
632 |
|
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
633 |
lemma tendsto_norm_zero: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
634 |
"(f ---> 0) A \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
635 |
by (drule tendsto_norm, simp) |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
636 |
|
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
637 |
lemma tendsto_norm_zero_cancel: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
638 |
"((\<lambda>x. norm (f x)) ---> 0) A \<Longrightarrow> (f ---> 0) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
639 |
unfolding tendsto_iff dist_norm by simp |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
640 |
|
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
641 |
lemma tendsto_norm_zero_iff: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
642 |
"((\<lambda>x. norm (f x)) ---> 0) A \<longleftrightarrow> (f ---> 0) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
643 |
unfolding tendsto_iff dist_norm by simp |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
644 |
|
31565 | 645 |
lemma tendsto_add [tendsto_intros]: |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
646 |
fixes a b :: "'a::real_normed_vector" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
647 |
shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
648 |
by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
649 |
|
31565 | 650 |
lemma tendsto_minus [tendsto_intros]: |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
651 |
fixes a :: "'a::real_normed_vector" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
652 |
shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
653 |
by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
654 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
655 |
lemma tendsto_minus_cancel: |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
656 |
fixes a :: "'a::real_normed_vector" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
657 |
shows "((\<lambda>x. - f x) ---> - a) A \<Longrightarrow> (f ---> a) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
658 |
by (drule tendsto_minus, simp) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
659 |
|
31565 | 660 |
lemma tendsto_diff [tendsto_intros]: |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
661 |
fixes a b :: "'a::real_normed_vector" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
662 |
shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
663 |
by (simp add: diff_minus tendsto_add tendsto_minus) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
664 |
|
31588 | 665 |
lemma tendsto_setsum [tendsto_intros]: |
666 |
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
667 |
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
668 |
shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) A" |
31588 | 669 |
proof (cases "finite S") |
670 |
assume "finite S" thus ?thesis using assms |
|
671 |
proof (induct set: finite) |
|
672 |
case empty show ?case |
|
673 |
by (simp add: tendsto_const) |
|
674 |
next |
|
675 |
case (insert i F) thus ?case |
|
676 |
by (simp add: tendsto_add) |
|
677 |
qed |
|
678 |
next |
|
679 |
assume "\<not> finite S" thus ?thesis |
|
680 |
by (simp add: tendsto_const) |
|
681 |
qed |
|
682 |
||
31565 | 683 |
lemma (in bounded_linear) tendsto [tendsto_intros]: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
684 |
"(g ---> a) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
685 |
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
686 |
|
31565 | 687 |
lemma (in bounded_bilinear) tendsto [tendsto_intros]: |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
688 |
"\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
689 |
by (simp only: tendsto_Zfun_iff prod_diff_prod |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
690 |
Zfun_add Zfun Zfun_left Zfun_right) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
691 |
|
31355 | 692 |
|
693 |
subsection {* Continuity of Inverse *} |
|
694 |
||
695 |
lemma (in bounded_bilinear) Zfun_prod_Bfun: |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
696 |
assumes f: "Zfun f A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
697 |
assumes g: "Bfun g A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
698 |
shows "Zfun (\<lambda>x. f x ** g x) A" |
31355 | 699 |
proof - |
700 |
obtain K where K: "0 \<le> K" |
|
701 |
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K" |
|
702 |
using nonneg_bounded by fast |
|
703 |
obtain B where B: "0 < B" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
704 |
and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) A" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
705 |
using g by (rule BfunE) |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
706 |
have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) A" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
707 |
using norm_g proof (rule eventually_elim1) |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
708 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
709 |
assume *: "norm (g x) \<le> B" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
710 |
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" |
31355 | 711 |
by (rule norm_le) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
712 |
also have "\<dots> \<le> norm (f x) * B * K" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
713 |
by (intro mult_mono' order_refl norm_g norm_ge_zero |
31355 | 714 |
mult_nonneg_nonneg K *) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
715 |
also have "\<dots> = norm (f x) * (B * K)" |
31355 | 716 |
by (rule mult_assoc) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
717 |
finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" . |
31355 | 718 |
qed |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
719 |
with f show ?thesis |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
720 |
by (rule Zfun_imp_Zfun) |
31355 | 721 |
qed |
722 |
||
723 |
lemma (in bounded_bilinear) flip: |
|
724 |
"bounded_bilinear (\<lambda>x y. y ** x)" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
725 |
apply default |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
726 |
apply (rule add_right) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
727 |
apply (rule add_left) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
728 |
apply (rule scaleR_right) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
729 |
apply (rule scaleR_left) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
730 |
apply (subst mult_commute) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
731 |
using bounded by fast |
31355 | 732 |
|
733 |
lemma (in bounded_bilinear) Bfun_prod_Zfun: |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
734 |
assumes f: "Bfun f A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
735 |
assumes g: "Zfun g A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
736 |
shows "Zfun (\<lambda>x. f x ** g x) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
737 |
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) |
31355 | 738 |
|
739 |
lemma Bfun_inverse_lemma: |
|
740 |
fixes x :: "'a::real_normed_div_algebra" |
|
741 |
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
742 |
apply (subst nonzero_norm_inverse, clarsimp) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
743 |
apply (erule (1) le_imp_inverse_le) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
744 |
done |
31355 | 745 |
|
746 |
lemma Bfun_inverse: |
|
747 |
fixes a :: "'a::real_normed_div_algebra" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
748 |
assumes f: "(f ---> a) A" |
31355 | 749 |
assumes a: "a \<noteq> 0" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
750 |
shows "Bfun (\<lambda>x. inverse (f x)) A" |
31355 | 751 |
proof - |
752 |
from a have "0 < norm a" by simp |
|
753 |
hence "\<exists>r>0. r < norm a" by (rule dense) |
|
754 |
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
755 |
have "eventually (\<lambda>x. dist (f x) a < r) A" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
756 |
using tendstoD [OF f r1] by fast |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
757 |
hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) A" |
31355 | 758 |
proof (rule eventually_elim1) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
759 |
fix x |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
760 |
assume "dist (f x) a < r" |
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
761 |
hence 1: "norm (f x - a) < r" |
31355 | 762 |
by (simp add: dist_norm) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
763 |
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
|
764 |
hence "norm (inverse (f x)) = inverse (norm (f x))" |
31355 | 765 |
by (rule nonzero_norm_inverse) |
766 |
also have "\<dots> \<le> inverse (norm a - r)" |
|
767 |
proof (rule le_imp_inverse_le) |
|
768 |
show "0 < norm a - r" using r2 by simp |
|
769 |
next |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
770 |
have "norm a - norm (f x) \<le> norm (a - f x)" |
31355 | 771 |
by (rule norm_triangle_ineq2) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
772 |
also have "\<dots> = norm (f x - a)" |
31355 | 773 |
by (rule norm_minus_commute) |
774 |
also have "\<dots> < r" using 1 . |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
775 |
finally show "norm a - r \<le> norm (f x)" by simp |
31355 | 776 |
qed |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
777 |
finally show "norm (inverse (f x)) \<le> inverse (norm a - r)" . |
31355 | 778 |
qed |
779 |
thus ?thesis by (rule BfunI) |
|
780 |
qed |
|
781 |
||
782 |
lemma tendsto_inverse_lemma: |
|
783 |
fixes a :: "'a::real_normed_div_algebra" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
784 |
shows "\<lbrakk>(f ---> a) A; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) A\<rbrakk> |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
785 |
\<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
786 |
apply (subst tendsto_Zfun_iff) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
787 |
apply (rule Zfun_ssubst) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
788 |
apply (erule eventually_elim1) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
789 |
apply (erule (1) inverse_diff_inverse) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
790 |
apply (rule Zfun_minus) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
791 |
apply (rule Zfun_mult_left) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
792 |
apply (rule mult.Bfun_prod_Zfun) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
793 |
apply (erule (1) Bfun_inverse) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
794 |
apply (simp add: tendsto_Zfun_iff) |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
795 |
done |
31355 | 796 |
|
31565 | 797 |
lemma tendsto_inverse [tendsto_intros]: |
31355 | 798 |
fixes a :: "'a::real_normed_div_algebra" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
799 |
assumes f: "(f ---> a) A" |
31355 | 800 |
assumes a: "a \<noteq> 0" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
801 |
shows "((\<lambda>x. inverse (f x)) ---> inverse a) A" |
31355 | 802 |
proof - |
803 |
from a have "0 < norm a" by simp |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
804 |
with f have "eventually (\<lambda>x. dist (f x) a < norm a) A" |
31355 | 805 |
by (rule tendstoD) |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
806 |
then have "eventually (\<lambda>x. f x \<noteq> 0) A" |
31355 | 807 |
unfolding dist_norm by (auto elim!: eventually_elim1) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
808 |
with f a show ?thesis |
31355 | 809 |
by (rule tendsto_inverse_lemma) |
810 |
qed |
|
811 |
||
31565 | 812 |
lemma tendsto_divide [tendsto_intros]: |
31355 | 813 |
fixes a b :: "'a::real_normed_field" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
814 |
shows "\<lbrakk>(f ---> a) A; (g ---> b) A; b \<noteq> 0\<rbrakk> |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
815 |
\<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
816 |
by (simp add: mult.tendsto tendsto_inverse divide_inverse) |
31355 | 817 |
|
41970 | 818 |
lemma tendsto_unique: |
819 |
fixes f :: "'a \<Rightarrow> 'b::t2_space" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
820 |
assumes "\<not> trivial_limit A" "(f ---> l) A" "(f ---> l') A" |
41970 | 821 |
shows "l = l'" |
822 |
proof (rule ccontr) |
|
823 |
assume "l \<noteq> l'" |
|
824 |
obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}" |
|
825 |
using hausdorff [OF `l \<noteq> l'`] by fast |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
826 |
have "eventually (\<lambda>x. f x \<in> U) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
827 |
using `(f ---> l) A` `open U` `l \<in> U` by (rule topological_tendstoD) |
41970 | 828 |
moreover |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
829 |
have "eventually (\<lambda>x. f x \<in> V) A" |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
830 |
using `(f ---> l') A` `open V` `l' \<in> V` by (rule topological_tendstoD) |
41970 | 831 |
ultimately |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
832 |
have "eventually (\<lambda>x. False) A" |
41970 | 833 |
proof (rule eventually_elim2) |
834 |
fix x |
|
835 |
assume "f x \<in> U" "f x \<in> V" |
|
836 |
hence "f x \<in> U \<inter> V" by simp |
|
837 |
with `U \<inter> V = {}` show "False" by simp |
|
838 |
qed |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
839 |
with `\<not> trivial_limit A` show "False" |
41970 | 840 |
by (simp add: trivial_limit_def) |
841 |
qed |
|
842 |
||
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
843 |
end |