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