author | nipkow |
Fri, 28 Dec 2018 10:29:59 +0100 | |
changeset 69517 | dc20f278e8f3 |
parent 69272 | 15e9ed5b28fb |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
52265 | 1 |
(* Title: HOL/Limits.thy |
51526 | 2 |
Author: Brian Huffman |
3 |
Author: Jacques D. Fleuriot, University of Cambridge |
|
4 |
Author: Lawrence C Paulson |
|
5 |
Author: Jeremy Avigad |
|
31349
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 |
|
60758 | 8 |
section \<open>Limits on Real Vector Spaces\<close> |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
9 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
10 |
theory Limits |
63546 | 11 |
imports Real_Vector_Spaces |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
12 |
begin |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
13 |
|
60758 | 14 |
subsection \<open>Filter going to infinity norm\<close> |
51526 | 15 |
|
63546 | 16 |
definition at_infinity :: "'a::real_normed_vector filter" |
17 |
where "at_infinity = (INF r. principal {x. r \<le> norm x})" |
|
50324
0a1242d5e7d4
add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
hoelzl
parents:
50323
diff
changeset
|
18 |
|
57276 | 19 |
lemma eventually_at_infinity: "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)" |
20 |
unfolding at_infinity_def |
|
21 |
by (subst eventually_INF_base) |
|
22 |
(auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b]) |
|
31392 | 23 |
|
62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62369
diff
changeset
|
24 |
corollary eventually_at_infinity_pos: |
63546 | 25 |
"eventually p at_infinity \<longleftrightarrow> (\<exists>b. 0 < b \<and> (\<forall>x. norm x \<ge> b \<longrightarrow> p x))" |
68614 | 26 |
unfolding eventually_at_infinity |
27 |
by (meson le_less_trans norm_ge_zero not_le zero_less_one) |
|
63546 | 28 |
|
29 |
lemma at_infinity_eq_at_top_bot: "(at_infinity :: real filter) = sup at_top at_bot" |
|
68614 | 30 |
proof - |
31 |
have 1: "\<lbrakk>\<forall>n\<ge>u. A n; \<forall>n\<le>v. A n\<rbrakk> |
|
32 |
\<Longrightarrow> \<exists>b. \<forall>x. b \<le> \<bar>x\<bar> \<longrightarrow> A x" for A and u v::real |
|
33 |
by (rule_tac x="max (- v) u" in exI) (auto simp: abs_real_def) |
|
34 |
have 2: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. A n" for A and u::real |
|
35 |
by (meson abs_less_iff le_cases less_le_not_le) |
|
36 |
have 3: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<le>N. A n" for A and u::real |
|
37 |
by (metis (full_types) abs_ge_self abs_minus_cancel le_minus_iff order_trans) |
|
38 |
show ?thesis |
|
68615 | 39 |
by (auto simp: filter_eq_iff eventually_sup eventually_at_infinity |
68614 | 40 |
eventually_at_top_linorder eventually_at_bot_linorder intro: 1 2 3) |
41 |
qed |
|
50325 | 42 |
|
57276 | 43 |
lemma at_top_le_at_infinity: "at_top \<le> (at_infinity :: real filter)" |
50325 | 44 |
unfolding at_infinity_eq_at_top_bot by simp |
45 |
||
57276 | 46 |
lemma at_bot_le_at_infinity: "at_bot \<le> (at_infinity :: real filter)" |
50325 | 47 |
unfolding at_infinity_eq_at_top_bot by simp |
48 |
||
63546 | 49 |
lemma filterlim_at_top_imp_at_infinity: "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F" |
50 |
for f :: "_ \<Rightarrow> real" |
|
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56541
diff
changeset
|
51 |
by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl]) |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56541
diff
changeset
|
52 |
|
67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset
|
53 |
lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially" |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset
|
54 |
by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially) |
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset
|
55 |
|
63546 | 56 |
lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially" |
57 |
by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially) |
|
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
58 |
|
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
59 |
|
60758 | 60 |
subsubsection \<open>Boundedness\<close> |
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
61 |
|
63546 | 62 |
definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" |
63 |
where Bfun_metric_def: "Bfun f F = (\<exists>y. \<exists>K>0. eventually (\<lambda>x. dist (f x) y \<le> K) F)" |
|
64 |
||
65 |
abbreviation Bseq :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" |
|
66 |
where "Bseq X \<equiv> Bfun X sequentially" |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
67 |
|
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
68 |
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" .. |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
69 |
|
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
70 |
lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
71 |
unfolding Bfun_metric_def by (subst eventually_sequentially_seg) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
72 |
|
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
73 |
lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
74 |
unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg) |
31355 | 75 |
|
63546 | 76 |
lemma Bfun_def: "Bfun f F \<longleftrightarrow> (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)" |
51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset
|
77 |
unfolding Bfun_metric_def norm_conv_dist |
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset
|
78 |
proof safe |
63546 | 79 |
fix y K |
80 |
assume K: "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F" |
|
51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset
|
81 |
moreover have "eventually (\<lambda>x. dist (f x) 0 \<le> dist (f x) y + dist 0 y) F" |
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset
|
82 |
by (intro always_eventually) (metis dist_commute dist_triangle) |
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset
|
83 |
with * have "eventually (\<lambda>x. dist (f x) 0 \<le> K + dist 0 y) F" |
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset
|
84 |
by eventually_elim auto |
60758 | 85 |
with \<open>0 < K\<close> show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F" |
51474
1e9e68247ad1
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents:
51472
diff
changeset
|
86 |
by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto |
62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62369
diff
changeset
|
87 |
qed (force simp del: norm_conv_dist [symmetric]) |
31355 | 88 |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
89 |
lemma BfunI: |
63546 | 90 |
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" |
91 |
shows "Bfun f F" |
|
92 |
unfolding Bfun_def |
|
31355 | 93 |
proof (intro exI conjI allI) |
94 |
show "0 < max K 1" by simp |
|
44195 | 95 |
show "eventually (\<lambda>x. norm (f x) \<le> max K 1) F" |
63546 | 96 |
using K by (rule eventually_mono) simp |
31355 | 97 |
qed |
98 |
||
99 |
lemma BfunE: |
|
44195 | 100 |
assumes "Bfun f F" |
101 |
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F" |
|
63546 | 102 |
using assms unfolding Bfun_def by blast |
31355 | 103 |
|
68614 | 104 |
lemma Cauchy_Bseq: |
105 |
assumes "Cauchy X" shows "Bseq X" |
|
106 |
proof - |
|
107 |
have "\<exists>y K. 0 < K \<and> (\<exists>N. \<forall>n\<ge>N. dist (X n) y \<le> K)" |
|
108 |
if "\<And>m n. \<lbrakk>m \<ge> M; n \<ge> M\<rbrakk> \<Longrightarrow> dist (X m) (X n) < 1" for M |
|
109 |
by (meson order.order_iff_strict that zero_less_one) |
|
110 |
with assms show ?thesis |
|
111 |
by (force simp: Cauchy_def Bfun_metric_def eventually_sequentially) |
|
112 |
qed |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
113 |
|
60758 | 114 |
subsubsection \<open>Bounded Sequences\<close> |
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
115 |
|
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
116 |
lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
117 |
by (intro BfunI) (auto simp: eventually_sequentially) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
118 |
|
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
119 |
lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
120 |
by (intro BfunI) (auto simp: eventually_sequentially) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
121 |
|
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
122 |
lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
123 |
unfolding Bfun_def eventually_sequentially |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
124 |
proof safe |
63546 | 125 |
fix N K |
126 |
assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K" |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
127 |
then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54263
diff
changeset
|
128 |
by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2) |
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
129 |
(auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
130 |
qed auto |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
131 |
|
63546 | 132 |
lemma BseqE: "Bseq X \<Longrightarrow> (\<And>K. 0 < K \<Longrightarrow> \<forall>n. norm (X n) \<le> K \<Longrightarrow> Q) \<Longrightarrow> Q" |
133 |
unfolding Bseq_def by auto |
|
134 |
||
135 |
lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K. 0 < K \<and> (\<forall>n. norm (X n) \<le> K)" |
|
136 |
by (simp add: Bseq_def) |
|
137 |
||
138 |
lemma BseqI: "0 < K \<Longrightarrow> \<forall>n. norm (X n) \<le> K \<Longrightarrow> Bseq X" |
|
68615 | 139 |
by (auto simp: Bseq_def) |
63546 | 140 |
|
141 |
lemma Bseq_bdd_above: "Bseq X \<Longrightarrow> bdd_above (range X)" |
|
142 |
for X :: "nat \<Rightarrow> real" |
|
54263
c4159fe6fa46
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset
|
143 |
proof (elim BseqE, intro bdd_aboveI2) |
63546 | 144 |
fix K n |
145 |
assume "0 < K" "\<forall>n. norm (X n) \<le> K" |
|
146 |
then show "X n \<le> K" |
|
54263
c4159fe6fa46
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset
|
147 |
by (auto elim!: allE[of _ n]) |
c4159fe6fa46
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset
|
148 |
qed |
c4159fe6fa46
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset
|
149 |
|
63546 | 150 |
lemma Bseq_bdd_above': "Bseq X \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))" |
151 |
for X :: "nat \<Rightarrow> 'a :: real_normed_vector" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
152 |
proof (elim BseqE, intro bdd_aboveI2) |
63546 | 153 |
fix K n |
154 |
assume "0 < K" "\<forall>n. norm (X n) \<le> K" |
|
155 |
then show "norm (X n) \<le> K" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
156 |
by (auto elim!: allE[of _ n]) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
157 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
158 |
|
63546 | 159 |
lemma Bseq_bdd_below: "Bseq X \<Longrightarrow> bdd_below (range X)" |
160 |
for X :: "nat \<Rightarrow> real" |
|
54263
c4159fe6fa46
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset
|
161 |
proof (elim BseqE, intro bdd_belowI2) |
63546 | 162 |
fix K n |
163 |
assume "0 < K" "\<forall>n. norm (X n) \<le> K" |
|
164 |
then show "- K \<le> X n" |
|
54263
c4159fe6fa46
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset
|
165 |
by (auto elim!: allE[of _ n]) |
c4159fe6fa46
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset
|
166 |
qed |
c4159fe6fa46
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents:
54230
diff
changeset
|
167 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
168 |
lemma Bseq_eventually_mono: |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
169 |
assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g" |
63546 | 170 |
shows "Bseq f" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
171 |
proof - |
67958
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset
|
172 |
from assms(2) obtain K where "0 < K" and "eventually (\<lambda>n. norm (g n) \<le> K) sequentially" |
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset
|
173 |
unfolding Bfun_def by fast |
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset
|
174 |
with assms(1) have "eventually (\<lambda>n. norm (f n) \<le> K) sequentially" |
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset
|
175 |
by (fast elim: eventually_elim2 order_trans) |
69272 | 176 |
with \<open>0 < K\<close> show "Bseq f" |
67958
732c0b059463
tuned proofs and generalized some lemmas about limits
huffman
parents:
67950
diff
changeset
|
177 |
unfolding Bfun_def by fast |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
178 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
179 |
|
63546 | 180 |
lemma lemma_NBseq_def: "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
181 |
proof safe |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
182 |
fix K :: real |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
183 |
from reals_Archimedean2 obtain n :: nat where "K < real n" .. |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
184 |
then have "K \<le> real (Suc n)" by auto |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
185 |
moreover assume "\<forall>m. norm (X m) \<le> K" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
186 |
ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
187 |
by (blast intro: order_trans) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
188 |
then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" .. |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset
|
189 |
next |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset
|
190 |
show "\<And>N. \<forall>n. norm (X n) \<le> real (Suc N) \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K" |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset
|
191 |
using of_nat_0_less_iff by blast |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset
|
192 |
qed |
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
193 |
|
63546 | 194 |
text \<open>Alternative definition for \<open>Bseq\<close>.\<close> |
195 |
lemma Bseq_iff: "Bseq X \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))" |
|
196 |
by (simp add: Bseq_def) (simp add: lemma_NBseq_def) |
|
197 |
||
198 |
lemma lemma_NBseq_def2: "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))" |
|
68614 | 199 |
proof - |
200 |
have *: "\<And>N. \<forall>n. norm (X n) \<le> 1 + real N \<Longrightarrow> |
|
201 |
\<exists>N. \<forall>n. norm (X n) < 1 + real N" |
|
202 |
by (metis add.commute le_less_trans less_add_one of_nat_Suc) |
|
203 |
then show ?thesis |
|
204 |
unfolding lemma_NBseq_def |
|
205 |
by (metis less_le_not_le not_less_iff_gr_or_eq of_nat_Suc) |
|
206 |
qed |
|
63546 | 207 |
|
208 |
text \<open>Yet another definition for Bseq.\<close> |
|
209 |
lemma Bseq_iff1a: "Bseq X \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) < real (Suc N))" |
|
210 |
by (simp add: Bseq_def lemma_NBseq_def2) |
|
211 |
||
212 |
subsubsection \<open>A Few More Equivalence Theorems for Boundedness\<close> |
|
213 |
||
214 |
text \<open>Alternative formulation for boundedness.\<close> |
|
215 |
lemma Bseq_iff2: "Bseq X \<longleftrightarrow> (\<exists>k > 0. \<exists>x. \<forall>n. norm (X n + - x) \<le> k)" |
|
68614 | 216 |
by (metis BseqE BseqI' add.commute add_cancel_right_left add_uminus_conv_diff norm_add_leD |
217 |
norm_minus_cancel norm_minus_commute) |
|
63546 | 218 |
|
219 |
text \<open>Alternative formulation for boundedness.\<close> |
|
220 |
lemma Bseq_iff3: "Bseq X \<longleftrightarrow> (\<exists>k>0. \<exists>N. \<forall>n. norm (X n + - X N) \<le> k)" |
|
221 |
(is "?P \<longleftrightarrow> ?Q") |
|
53602 | 222 |
proof |
223 |
assume ?P |
|
63546 | 224 |
then obtain K where *: "0 < K" and **: "\<And>n. norm (X n) \<le> K" |
68615 | 225 |
by (auto simp: Bseq_def) |
53602 | 226 |
from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset
|
227 |
from ** have "\<forall>n. norm (X n - X 0) \<le> K + norm (X 0)" |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset
|
228 |
by (auto intro: order_trans norm_triangle_ineq4) |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset
|
229 |
then have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)" |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset
|
230 |
by simp |
60758 | 231 |
with \<open>0 < K + norm (X 0)\<close> show ?Q by blast |
53602 | 232 |
next |
63546 | 233 |
assume ?Q |
68615 | 234 |
then show ?P by (auto simp: Bseq_iff2) |
53602 | 235 |
qed |
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
236 |
|
63546 | 237 |
|
238 |
subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close> |
|
239 |
||
240 |
lemma Bseq_minus_iff: "Bseq (\<lambda>n. - (X n) :: 'a::real_normed_vector) \<longleftrightarrow> Bseq X" |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
241 |
by (simp add: Bseq_def) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
242 |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset
|
243 |
lemma Bseq_add: |
63546 | 244 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
245 |
assumes "Bseq f" |
|
246 |
shows "Bseq (\<lambda>x. f x + c)" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
247 |
proof - |
63546 | 248 |
from assms obtain K where K: "\<And>x. norm (f x) \<le> K" |
249 |
unfolding Bseq_def by blast |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
250 |
{ |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
251 |
fix x :: nat |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
252 |
have "norm (f x + c) \<le> norm (f x) + norm c" by (rule norm_triangle_ineq) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
253 |
also have "norm (f x) \<le> K" by (rule K) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
254 |
finally have "norm (f x + c) \<le> K + norm c" by simp |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
255 |
} |
63546 | 256 |
then show ?thesis by (rule BseqI') |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
257 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
258 |
|
63546 | 259 |
lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq f" |
260 |
for f :: "nat \<Rightarrow> 'a::real_normed_vector" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
261 |
using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
262 |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
61976
diff
changeset
|
263 |
lemma Bseq_mult: |
63546 | 264 |
fixes f g :: "nat \<Rightarrow> 'a::real_normed_field" |
265 |
assumes "Bseq f" and "Bseq g" |
|
266 |
shows "Bseq (\<lambda>x. f x * g x)" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
267 |
proof - |
63546 | 268 |
from assms obtain K1 K2 where K: "norm (f x) \<le> K1" "K1 > 0" "norm (g x) \<le> K2" "K2 > 0" |
269 |
for x |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
270 |
unfolding Bseq_def by blast |
63546 | 271 |
then have "norm (f x * g x) \<le> K1 * K2" for x |
272 |
by (auto simp: norm_mult intro!: mult_mono) |
|
273 |
then show ?thesis by (rule BseqI') |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
274 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
275 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
276 |
lemma Bfun_const [simp]: "Bfun (\<lambda>_. c) F" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
277 |
unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"]) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
278 |
|
63546 | 279 |
lemma Bseq_cmult_iff: |
280 |
fixes c :: "'a::real_normed_field" |
|
281 |
assumes "c \<noteq> 0" |
|
282 |
shows "Bseq (\<lambda>x. c * f x) \<longleftrightarrow> Bseq f" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
283 |
proof |
63546 | 284 |
assume "Bseq (\<lambda>x. c * f x)" |
285 |
with Bfun_const have "Bseq (\<lambda>x. inverse c * (c * f x))" |
|
286 |
by (rule Bseq_mult) |
|
287 |
with \<open>c \<noteq> 0\<close> show "Bseq f" |
|
288 |
by (simp add: divide_simps) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
289 |
qed (intro Bseq_mult Bfun_const) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
290 |
|
63546 | 291 |
lemma Bseq_subseq: "Bseq f \<Longrightarrow> Bseq (\<lambda>x. f (g x))" |
292 |
for f :: "nat \<Rightarrow> 'a::real_normed_vector" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
293 |
unfolding Bseq_def by auto |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
294 |
|
63546 | 295 |
lemma Bseq_Suc_iff: "Bseq (\<lambda>n. f (Suc n)) \<longleftrightarrow> Bseq f" |
296 |
for f :: "nat \<Rightarrow> 'a::real_normed_vector" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
297 |
using Bseq_offset[of f 1] by (auto intro: Bseq_subseq) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
298 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
299 |
lemma increasing_Bseq_subseq_iff: |
66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
65680
diff
changeset
|
300 |
assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "strict_mono g" |
63546 | 301 |
shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
302 |
proof |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
303 |
assume "Bseq (\<lambda>x. f (g x))" |
63546 | 304 |
then obtain K where K: "\<And>x. norm (f (g x)) \<le> K" |
305 |
unfolding Bseq_def by auto |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
306 |
{ |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
307 |
fix x :: nat |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
308 |
from filterlim_subseq[OF assms(2)] obtain y where "g y \<ge> x" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
309 |
by (auto simp: filterlim_at_top eventually_at_top_linorder) |
63546 | 310 |
then have "norm (f x) \<le> norm (f (g y))" |
311 |
using assms(1) by blast |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
312 |
also have "norm (f (g y)) \<le> K" by (rule K) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
313 |
finally have "norm (f x) \<le> K" . |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
314 |
} |
63546 | 315 |
then show "Bseq f" by (rule BseqI') |
316 |
qed (use Bseq_subseq[of f g] in simp_all) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
317 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
318 |
lemma nonneg_incseq_Bseq_subseq_iff: |
63546 | 319 |
fixes f :: "nat \<Rightarrow> real" |
320 |
and g :: "nat \<Rightarrow> nat" |
|
66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
65680
diff
changeset
|
321 |
assumes "\<And>x. f x \<ge> 0" "incseq f" "strict_mono g" |
63546 | 322 |
shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
323 |
using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset
|
324 |
|
63546 | 325 |
lemma Bseq_eq_bounded: "range f \<subseteq> {a..b} \<Longrightarrow> Bseq f" |
326 |
for a b :: real |
|
68614 | 327 |
proof (rule BseqI'[where K="max (norm a) (norm b)"]) |
328 |
fix n assume "range f \<subseteq> {a..b}" |
|
329 |
then have "f n \<in> {a..b}" |
|
330 |
by blast |
|
331 |
then show "norm (f n) \<le> max (norm a) (norm b)" |
|
332 |
by auto |
|
333 |
qed |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
334 |
|
63546 | 335 |
lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> B \<Longrightarrow> Bseq X" |
336 |
for B :: real |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
337 |
by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
338 |
|
63546 | 339 |
lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. B \<le> X i \<Longrightarrow> Bseq X" |
340 |
for B :: real |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
341 |
by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
342 |
|
63546 | 343 |
|
60758 | 344 |
subsection \<open>Convergence to Zero\<close> |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
345 |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
346 |
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" |
44195 | 347 |
where "Zfun f F = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) F)" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
348 |
|
63546 | 349 |
lemma ZfunI: "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F) \<Longrightarrow> Zfun f F" |
350 |
by (simp add: Zfun_def) |
|
351 |
||
352 |
lemma ZfunD: "Zfun f F \<Longrightarrow> 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) F" |
|
353 |
by (simp add: Zfun_def) |
|
354 |
||
355 |
lemma Zfun_ssubst: "eventually (\<lambda>x. f x = g x) F \<Longrightarrow> Zfun g F \<Longrightarrow> Zfun f F" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
356 |
unfolding Zfun_def by (auto elim!: eventually_rev_mp) |
31355 | 357 |
|
44195 | 358 |
lemma Zfun_zero: "Zfun (\<lambda>x. 0) F" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
359 |
unfolding Zfun_def by simp |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
360 |
|
44195 | 361 |
lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) F = Zfun (\<lambda>x. f x) F" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
362 |
unfolding Zfun_def by simp |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
363 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
364 |
lemma Zfun_imp_Zfun: |
44195 | 365 |
assumes f: "Zfun f F" |
63546 | 366 |
and g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F" |
44195 | 367 |
shows "Zfun (\<lambda>x. g x) F" |
63546 | 368 |
proof (cases "0 < K") |
369 |
case K: True |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
370 |
show ?thesis |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
371 |
proof (rule ZfunI) |
63546 | 372 |
fix r :: real |
373 |
assume "0 < r" |
|
374 |
then have "0 < r / K" using K by simp |
|
44195 | 375 |
then have "eventually (\<lambda>x. norm (f x) < r / K) F" |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset
|
376 |
using ZfunD [OF f] by blast |
44195 | 377 |
with g show "eventually (\<lambda>x. norm (g x) < r) F" |
46887 | 378 |
proof eventually_elim |
379 |
case (elim x) |
|
63546 | 380 |
then have "norm (f x) * K < r" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
381 |
by (simp add: pos_less_divide_eq K) |
63546 | 382 |
then show ?case |
46887 | 383 |
by (simp add: order_le_less_trans [OF elim(1)]) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
384 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
385 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
386 |
next |
63546 | 387 |
case False |
388 |
then have K: "K \<le> 0" by (simp only: not_less) |
|
31355 | 389 |
show ?thesis |
390 |
proof (rule ZfunI) |
|
391 |
fix r :: real |
|
392 |
assume "0 < r" |
|
44195 | 393 |
from g show "eventually (\<lambda>x. norm (g x) < r) F" |
46887 | 394 |
proof eventually_elim |
395 |
case (elim x) |
|
396 |
also have "norm (f x) * K \<le> norm (f x) * 0" |
|
31355 | 397 |
using K norm_ge_zero by (rule mult_left_mono) |
46887 | 398 |
finally show ?case |
60758 | 399 |
using \<open>0 < r\<close> by simp |
31355 | 400 |
qed |
401 |
qed |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
402 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
403 |
|
63546 | 404 |
lemma Zfun_le: "Zfun g F \<Longrightarrow> \<forall>x. norm (f x) \<le> norm (g x) \<Longrightarrow> Zfun f F" |
405 |
by (erule Zfun_imp_Zfun [where K = 1]) simp |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
406 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
407 |
lemma Zfun_add: |
63546 | 408 |
assumes f: "Zfun f F" |
409 |
and g: "Zfun g F" |
|
44195 | 410 |
shows "Zfun (\<lambda>x. f x + g x) F" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
411 |
proof (rule ZfunI) |
63546 | 412 |
fix r :: real |
413 |
assume "0 < r" |
|
414 |
then have r: "0 < r / 2" by simp |
|
44195 | 415 |
have "eventually (\<lambda>x. norm (f x) < r/2) F" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
416 |
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
|
417 |
moreover |
44195 | 418 |
have "eventually (\<lambda>x. norm (g x) < r/2) F" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
419 |
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
|
420 |
ultimately |
44195 | 421 |
show "eventually (\<lambda>x. norm (f x + g x) < r) F" |
46887 | 422 |
proof eventually_elim |
423 |
case (elim x) |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
424 |
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
|
425 |
by (rule norm_triangle_ineq) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
426 |
also have "\<dots> < r/2 + r/2" |
46887 | 427 |
using elim by (rule add_strict_mono) |
428 |
finally show ?case |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
429 |
by simp |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
430 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
431 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
432 |
|
44195 | 433 |
lemma Zfun_minus: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. - f x) F" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
434 |
unfolding Zfun_def by simp |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
435 |
|
63546 | 436 |
lemma Zfun_diff: "Zfun f F \<Longrightarrow> Zfun g F \<Longrightarrow> Zfun (\<lambda>x. f x - g x) F" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53602
diff
changeset
|
437 |
using Zfun_add [of f F "\<lambda>x. - g x"] by (simp add: Zfun_minus) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
438 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
439 |
lemma (in bounded_linear) Zfun: |
44195 | 440 |
assumes g: "Zfun g F" |
441 |
shows "Zfun (\<lambda>x. f (g x)) F" |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
442 |
proof - |
63546 | 443 |
obtain K where "norm (f x) \<le> norm x * K" for x |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset
|
444 |
using bounded by blast |
44195 | 445 |
then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) F" |
31355 | 446 |
by simp |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
447 |
with g show ?thesis |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
448 |
by (rule Zfun_imp_Zfun) |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
449 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
450 |
|
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
451 |
lemma (in bounded_bilinear) Zfun: |
44195 | 452 |
assumes f: "Zfun f F" |
63546 | 453 |
and g: "Zfun g F" |
44195 | 454 |
shows "Zfun (\<lambda>x. f x ** g x) F" |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
455 |
proof (rule ZfunI) |
63546 | 456 |
fix r :: real |
457 |
assume r: "0 < r" |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
458 |
obtain K where K: "0 < K" |
63546 | 459 |
and norm_le: "norm (x ** y) \<le> norm x * norm y * K" for x y |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset
|
460 |
using pos_bounded by blast |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
461 |
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
|
462 |
by (rule positive_imp_inverse_positive) |
44195 | 463 |
have "eventually (\<lambda>x. norm (f x) < r) F" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
464 |
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
|
465 |
moreover |
44195 | 466 |
have "eventually (\<lambda>x. norm (g x) < inverse K) F" |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
467 |
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
|
468 |
ultimately |
44195 | 469 |
show "eventually (\<lambda>x. norm (f x ** g x) < r) F" |
46887 | 470 |
proof eventually_elim |
471 |
case (elim x) |
|
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
472 |
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
|
473 |
by (rule norm_le) |
31487
93938cafc0e6
put syntax for tendsto in Limits.thy; rename variables
huffman
parents:
31447
diff
changeset
|
474 |
also have "norm (f x) * norm (g x) * K < r * inverse K * K" |
46887 | 475 |
by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K) |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
476 |
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
|
477 |
by simp |
46887 | 478 |
finally show ?case . |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
479 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
480 |
qed |
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
481 |
|
63546 | 482 |
lemma (in bounded_bilinear) Zfun_left: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. f x ** a) F" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
483 |
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
|
484 |
|
63546 | 485 |
lemma (in bounded_bilinear) Zfun_right: "Zfun f F \<Longrightarrow> Zfun (\<lambda>x. a ** f x) F" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
486 |
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
|
487 |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset
|
488 |
lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset
|
489 |
lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44253
diff
changeset
|
490 |
lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] |
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
491 |
|
61973 | 492 |
lemma tendsto_Zfun_iff: "(f \<longlongrightarrow> a) F = Zfun (\<lambda>x. f x - a) F" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
493 |
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
|
494 |
|
63546 | 495 |
lemma tendsto_0_le: |
496 |
"(f \<longlongrightarrow> 0) F \<Longrightarrow> eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F \<Longrightarrow> (g \<longlongrightarrow> 0) F" |
|
56366 | 497 |
by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) |
498 |
||
63546 | 499 |
|
60758 | 500 |
subsubsection \<open>Distance and norms\<close> |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
501 |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
502 |
lemma tendsto_dist [tendsto_intros]: |
63546 | 503 |
fixes l m :: "'a::metric_space" |
504 |
assumes f: "(f \<longlongrightarrow> l) F" |
|
505 |
and g: "(g \<longlongrightarrow> m) F" |
|
61973 | 506 |
shows "((\<lambda>x. dist (f x) (g x)) \<longlongrightarrow> dist l m) F" |
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
507 |
proof (rule tendstoI) |
63546 | 508 |
fix e :: real |
509 |
assume "0 < e" |
|
510 |
then have e2: "0 < e/2" by simp |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
511 |
from tendstoD [OF f e2] tendstoD [OF g e2] |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
512 |
show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
513 |
proof (eventually_elim) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
514 |
case (elim x) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
515 |
then show "dist (dist (f x) (g x)) (dist l m) < e" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
516 |
unfolding dist_real_def |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
517 |
using dist_triangle2 [of "f x" "g x" "l"] |
63546 | 518 |
and dist_triangle2 [of "g x" "l" "m"] |
519 |
and dist_triangle3 [of "l" "m" "f x"] |
|
520 |
and dist_triangle [of "f x" "m" "g x"] |
|
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
521 |
by arith |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
522 |
qed |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
523 |
qed |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
524 |
|
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
525 |
lemma continuous_dist[continuous_intros]: |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
526 |
fixes f g :: "_ \<Rightarrow> 'a :: metric_space" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
527 |
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. dist (f x) (g x))" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
528 |
unfolding continuous_def by (rule tendsto_dist) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
529 |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset
|
530 |
lemma continuous_on_dist[continuous_intros]: |
51531
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
531 |
fixes f g :: "_ \<Rightarrow> 'a :: metric_space" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
532 |
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. dist (f x) (g x))" |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
533 |
unfolding continuous_on_def by (auto intro: tendsto_dist) |
f415febf4234
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
hoelzl
parents:
51529
diff
changeset
|
534 |
|
63546 | 535 |
lemma tendsto_norm [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> norm a) F" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
536 |
unfolding norm_conv_dist by (intro tendsto_intros) |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
537 |
|
63546 | 538 |
lemma continuous_norm [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))" |
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
539 |
unfolding continuous_def by (rule tendsto_norm) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
540 |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset
|
541 |
lemma continuous_on_norm [continuous_intros]: |
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
542 |
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
543 |
unfolding continuous_on_def by (auto intro: tendsto_norm) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
544 |
|
63546 | 545 |
lemma tendsto_norm_zero: "(f \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F" |
546 |
by (drule tendsto_norm) simp |
|
547 |
||
548 |
lemma tendsto_norm_zero_cancel: "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> 0) F" |
|
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
549 |
unfolding tendsto_iff dist_norm by simp |
36662
621122eeb138
generalize types of LIMSEQ and LIM; generalize many lemmas
huffman
parents:
36656
diff
changeset
|
550 |
|
63546 | 551 |
lemma tendsto_norm_zero_iff: "((\<lambda>x. norm (f x)) \<longlongrightarrow> 0) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F" |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44079
diff
changeset
|
552 |
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
|
553 |
|
63546 | 554 |
lemma tendsto_rabs [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> \<bar>l\<bar>) F" |
555 |
for l :: real |
|
556 |
by (fold real_norm_def) (rule tendsto_norm) |
|
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset
|
557 |
|
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
558 |
lemma continuous_rabs [continuous_intros]: |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
559 |
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. \<bar>f x :: real\<bar>)" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
560 |
unfolding real_norm_def[symmetric] by (rule continuous_norm) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
561 |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset
|
562 |
lemma continuous_on_rabs [continuous_intros]: |
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
563 |
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. \<bar>f x :: real\<bar>)" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
564 |
unfolding real_norm_def[symmetric] by (rule continuous_on_norm) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
565 |
|
63546 | 566 |
lemma tendsto_rabs_zero: "(f \<longlongrightarrow> (0::real)) F \<Longrightarrow> ((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> 0) F" |
567 |
by (fold real_norm_def) (rule tendsto_norm_zero) |
|
568 |
||
569 |
lemma tendsto_rabs_zero_cancel: "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<Longrightarrow> (f \<longlongrightarrow> 0) F" |
|
570 |
by (fold real_norm_def) (rule tendsto_norm_zero_cancel) |
|
571 |
||
572 |
lemma tendsto_rabs_zero_iff: "((\<lambda>x. \<bar>f x\<bar>) \<longlongrightarrow> (0::real)) F \<longleftrightarrow> (f \<longlongrightarrow> 0) F" |
|
573 |
by (fold real_norm_def) (rule tendsto_norm_zero_iff) |
|
574 |
||
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset
|
575 |
|
62368 | 576 |
subsection \<open>Topological Monoid\<close> |
577 |
||
578 |
class topological_monoid_add = topological_space + monoid_add + |
|
579 |
assumes tendsto_add_Pair: "LIM x (nhds a \<times>\<^sub>F nhds b). fst x + snd x :> nhds (a + b)" |
|
580 |
||
581 |
class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add |
|
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset
|
582 |
|
31565 | 583 |
lemma tendsto_add [tendsto_intros]: |
62368 | 584 |
fixes a b :: "'a::topological_monoid_add" |
585 |
shows "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> a + b) F" |
|
586 |
using filterlim_compose[OF tendsto_add_Pair, of "\<lambda>x. (f x, g x)" a b F] |
|
587 |
by (simp add: nhds_prod[symmetric] tendsto_Pair) |
|
31349
2261c8781f73
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
huffman
parents:
diff
changeset
|
588 |
|
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
589 |
lemma continuous_add [continuous_intros]: |
62368 | 590 |
fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" |
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
591 |
shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x + g x)" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
592 |
unfolding continuous_def by (rule tendsto_add) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
593 |
|
56371
fb9ae0727548
extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents:
56366
diff
changeset
|
594 |
lemma continuous_on_add [continuous_intros]: |
62368 | 595 |
fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" |
51478
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
596 |
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)" |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
597 |
unfolding continuous_on_def by (auto intro: tendsto_add) |
270b21f3ae0a
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents:
51474
diff
changeset
|
598 |
|
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset
|
599 |
lemma tendsto_add_zero: |
62368 | 600 |
fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_add" |
63546 | 601 |
shows "(f \<longlongrightarrow> 0) F \<Longrightarrow> (g \<longlongrightarrow> 0) F \<Longrightarrow> ((\<lambda>x. f x + g x) \<longlongrightarrow> 0) F" |
602 |
by (drule (1) tendsto_add) simp |
|
44194
0639898074ae
generalize lemmas about LIM and LIMSEQ to tendsto
huffman
parents:
44081
diff
changeset
|
603 |
|
64267 | 604 |
lemma tendsto_sum [tendsto_intros]: |
62368 | 605 |
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add" |
63915 | 606 |
shows "(\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F) \<Longrightarrow> ((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F" |
607 |
by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add) |
|
62368 | 608 |
|
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
609 |
lemma tendsto_null_sum: |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
610 |
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add" |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
611 |
assumes "\<And>i. i \<in> I \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> 0) F" |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
612 |
shows "((\<lambda>i. sum (f i) I) \<longlongrightarrow> 0) F" |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
613 |
using tendsto_sum [of I "\<lambda>x y. f y x" "\<lambda>x. 0"] assms by simp |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
614 |
|
64267 | 615 |
lemma continuous_sum [continuous_intros]: |
62368 | 616 |
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add" |
63301 | 617 |
shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)" |
64267 | 618 |
unfolding continuous_def by (rule tendsto_sum) |
619 |
||
620 |
lemma continuous_on_sum [continuous_intros]: |
|
62368 | 621 |
fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_add" |
63301 | 622 |
shows "(\<And>i. i \<in> I \<Longrightarrow> continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<Sum>i\<in>I. f i x)" |
64267 | 623 |
unfolding continuous_on_def by (auto intro: tendsto_sum) |
62368 | 624 |
|
62369 | 625 |
instance nat :: topological_comm_monoid_add |
63546 | 626 |
by standard |
627 |
(simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) |
|
62369 | 628 |
|
629 |
instance int :: topological_comm_monoid_add |
|
63546 | 630 |
by standard |