author | haftmann |
Wed, 17 Feb 2016 21:51:56 +0100 | |
changeset 62343 | 24106dc44def |
parent 62049 | b0f941e207cf |
child 62624 | 59ceeb6f3079 |
permissions | -rw-r--r-- |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Liminf_Limsup.thy |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
2 |
Author: Johannes Hölzl, TU München |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
3 |
Author: Manuel Eberl, TU München |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
4 |
*) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
5 |
|
60500 | 6 |
section \<open>Liminf and Limsup on complete lattices\<close> |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
7 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
8 |
theory Liminf_Limsup |
51542 | 9 |
imports Complex_Main |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
10 |
begin |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
11 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
12 |
lemma le_Sup_iff_less: |
53216 | 13 |
fixes x :: "'a :: {complete_linorder, dense_linorder}" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
14 |
shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs") |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
15 |
unfolding le_SUP_iff |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
16 |
by (blast intro: less_imp_le less_trans less_le_trans dest: dense) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
17 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
18 |
lemma Inf_le_iff_less: |
53216 | 19 |
fixes x :: "'a :: {complete_linorder, dense_linorder}" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
20 |
shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
21 |
unfolding INF_le_iff |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
22 |
by (blast intro: less_imp_le less_trans le_less_trans dest: dense) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
23 |
|
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset
|
24 |
lemma SUP_pair: |
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53381
diff
changeset
|
25 |
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice" |
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53381
diff
changeset
|
26 |
shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
27 |
by (rule antisym) (auto intro!: SUP_least SUP_upper2) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
28 |
|
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset
|
29 |
lemma INF_pair: |
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53381
diff
changeset
|
30 |
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice" |
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53381
diff
changeset
|
31 |
shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
32 |
by (rule antisym) (auto intro!: INF_greatest INF_lower2) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
33 |
|
61585 | 34 |
subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close> |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
35 |
|
54261 | 36 |
definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
37 |
"Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
38 |
|
54261 | 39 |
definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
40 |
"Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
41 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
42 |
abbreviation "liminf \<equiv> Liminf sequentially" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
43 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
44 |
abbreviation "limsup \<equiv> Limsup sequentially" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
45 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
46 |
lemma Liminf_eqI: |
61730 | 47 |
"(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow> |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
48 |
(\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
49 |
unfolding Liminf_def by (auto intro!: SUP_eqI) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
50 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
51 |
lemma Limsup_eqI: |
61730 | 52 |
"(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow> |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
53 |
(\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
54 |
unfolding Limsup_def by (auto intro!: INF_eqI) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
55 |
|
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset
|
56 |
lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
57 |
unfolding Liminf_def eventually_sequentially |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset
|
58 |
by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
59 |
|
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset
|
60 |
lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
61 |
unfolding Limsup_def eventually_sequentially |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset
|
62 |
by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
63 |
|
61730 | 64 |
lemma Limsup_const: |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
65 |
assumes ntriv: "\<not> trivial_limit F" |
54261 | 66 |
shows "Limsup F (\<lambda>x. c) = c" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
67 |
proof - |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
68 |
have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
69 |
have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
70 |
using ntriv by (intro SUP_const) (auto simp: eventually_False *) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
71 |
then show ?thesis |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
72 |
unfolding Limsup_def using eventually_True |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
73 |
by (subst INF_cong[where D="\<lambda>x. c"]) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
74 |
(auto intro!: INF_const simp del: eventually_True) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
75 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
76 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
77 |
lemma Liminf_const: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
78 |
assumes ntriv: "\<not> trivial_limit F" |
54261 | 79 |
shows "Liminf F (\<lambda>x. c) = c" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
80 |
proof - |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
81 |
have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
82 |
have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
83 |
using ntriv by (intro INF_const) (auto simp: eventually_False *) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
84 |
then show ?thesis |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
85 |
unfolding Liminf_def using eventually_True |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
86 |
by (subst SUP_cong[where D="\<lambda>x. c"]) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
87 |
(auto intro!: SUP_const simp del: eventually_True) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
88 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
89 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
90 |
lemma Liminf_mono: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
91 |
assumes ev: "eventually (\<lambda>x. f x \<le> g x) F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
92 |
shows "Liminf F f \<le> Liminf F g" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
93 |
unfolding Liminf_def |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
94 |
proof (safe intro!: SUP_mono) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
95 |
fix P assume "eventually P F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
96 |
with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
97 |
then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
98 |
by (intro bexI[of _ ?Q]) (auto intro!: INF_mono) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
99 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
100 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
101 |
lemma Liminf_eq: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
102 |
assumes "eventually (\<lambda>x. f x = g x) F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
103 |
shows "Liminf F f = Liminf F g" |
61810 | 104 |
by (intro antisym Liminf_mono eventually_mono[OF assms]) auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
105 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
106 |
lemma Limsup_mono: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
107 |
assumes ev: "eventually (\<lambda>x. f x \<le> g x) F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
108 |
shows "Limsup F f \<le> Limsup F g" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
109 |
unfolding Limsup_def |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
110 |
proof (safe intro!: INF_mono) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
111 |
fix P assume "eventually P F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
112 |
with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
113 |
then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
114 |
by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
115 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
116 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
117 |
lemma Limsup_eq: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
118 |
assumes "eventually (\<lambda>x. f x = g x) net" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
119 |
shows "Limsup net f = Limsup net g" |
61810 | 120 |
by (intro antisym Limsup_mono eventually_mono[OF assms]) auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
121 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
122 |
lemma Liminf_le_Limsup: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
123 |
assumes ntriv: "\<not> trivial_limit F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
124 |
shows "Liminf F f \<le> Limsup F f" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
125 |
unfolding Limsup_def Liminf_def |
54261 | 126 |
apply (rule SUP_least) |
127 |
apply (rule INF_greatest) |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
128 |
proof safe |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
129 |
fix P Q assume "eventually P F" "eventually Q F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
130 |
then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
131 |
then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
132 |
using ntriv by (auto simp add: eventually_False) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
133 |
have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
134 |
by (rule INF_mono) auto |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
135 |
also have "\<dots> \<le> SUPREMUM (Collect ?C) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
136 |
using not_False by (intro INF_le_SUP) auto |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
137 |
also have "\<dots> \<le> SUPREMUM (Collect Q) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
138 |
by (rule SUP_mono) auto |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
139 |
finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" . |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
140 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
141 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
142 |
lemma Liminf_bounded: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
143 |
assumes ntriv: "\<not> trivial_limit F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
144 |
assumes le: "eventually (\<lambda>n. C \<le> X n) F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
145 |
shows "C \<le> Liminf F X" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
146 |
using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
147 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
148 |
lemma Limsup_bounded: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
149 |
assumes ntriv: "\<not> trivial_limit F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
150 |
assumes le: "eventually (\<lambda>n. X n \<le> C) F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
151 |
shows "Limsup F X \<le> C" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
152 |
using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
153 |
|
61245 | 154 |
lemma le_Limsup: |
155 |
assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x" |
|
156 |
shows "l \<le> Limsup F f" |
|
157 |
proof - |
|
158 |
have "l = Limsup F (\<lambda>x. l)" |
|
159 |
using F by (simp add: Limsup_const) |
|
160 |
also have "\<dots> \<le> Limsup F f" |
|
61730 | 161 |
by (intro Limsup_mono x) |
61245 | 162 |
finally show ?thesis . |
163 |
qed |
|
164 |
||
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
165 |
lemma le_Liminf_iff: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
166 |
fixes X :: "_ \<Rightarrow> _ :: complete_linorder" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
167 |
shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
168 |
proof - |
61730 | 169 |
have "eventually (\<lambda>x. y < X x) F" |
170 |
if "eventually P F" "y < INFIMUM (Collect P) X" for y P |
|
61810 | 171 |
using that by (auto elim!: eventually_mono dest: less_INF_D) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
172 |
moreover |
61730 | 173 |
have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X" |
174 |
if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P |
|
175 |
proof (cases "\<exists>z. y < z \<and> z < C") |
|
176 |
case True |
|
177 |
then obtain z where z: "y < z \<and> z < C" .. |
|
178 |
moreover from z have "z \<le> INFIMUM {x. z < X x} X" |
|
179 |
by (auto intro!: INF_greatest) |
|
180 |
ultimately show ?thesis |
|
181 |
using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto |
|
182 |
next |
|
183 |
case False |
|
184 |
then have "C \<le> INFIMUM {x. y < X x} X" |
|
185 |
by (intro INF_greatest) auto |
|
186 |
with \<open>y < C\<close> show ?thesis |
|
187 |
using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto |
|
188 |
qed |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
189 |
ultimately show ?thesis |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
190 |
unfolding Liminf_def le_SUP_iff by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
191 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
192 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
193 |
lemma Limsup_le_iff: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
194 |
fixes X :: "_ \<Rightarrow> _ :: complete_linorder" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
195 |
shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
196 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
197 |
{ fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
198 |
then have "eventually (\<lambda>x. y > X x) F" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
199 |
by (auto elim!: eventually_mono dest: SUP_lessD) } |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
200 |
moreover |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
201 |
{ fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
202 |
have "\<exists>P. eventually P F \<and> y > SUPREMUM (Collect P) X" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
203 |
proof (cases "\<exists>z. C < z \<and> z < y") |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
204 |
case True |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
205 |
then obtain z where z: "C < z \<and> z < y" .. |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
206 |
moreover from z have "z \<ge> SUPREMUM {x. z > X x} X" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
207 |
by (auto intro!: SUP_least) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
208 |
ultimately show ?thesis |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
209 |
using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
210 |
next |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
211 |
case False |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
212 |
then have "C \<ge> SUPREMUM {x. y > X x} X" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
213 |
by (intro SUP_least) (auto simp: not_less) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
214 |
with \<open>y > C\<close> show ?thesis |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
215 |
using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
216 |
qed } |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
217 |
ultimately show ?thesis |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
218 |
unfolding Limsup_def INF_le_iff by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
219 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
220 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
221 |
lemma less_LiminfD: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
222 |
"y < Liminf F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x > y) F" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
223 |
using le_Liminf_iff[of "Liminf F f" F f] by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
224 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
225 |
lemma Limsup_lessD: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
226 |
"y > Limsup F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x < y) F" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
227 |
using Limsup_le_iff[of F f "Limsup F f"] by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
228 |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
229 |
lemma lim_imp_Liminf: |
61730 | 230 |
fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
231 |
assumes ntriv: "\<not> trivial_limit F" |
61973 | 232 |
assumes lim: "(f \<longlongrightarrow> f0) F" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
233 |
shows "Liminf F f = f0" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
234 |
proof (intro Liminf_eqI) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
235 |
fix P assume P: "eventually P F" |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
236 |
then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
237 |
by eventually_elim (auto intro!: INF_lower) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
238 |
then show "INFIMUM (Collect P) f \<le> f0" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
239 |
by (rule tendsto_le[OF ntriv lim tendsto_const]) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
240 |
next |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
241 |
fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
242 |
show "f0 \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
243 |
proof cases |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
244 |
assume "\<exists>z. y < z \<and> z < f0" |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
245 |
then obtain z where "y < z \<and> z < f0" .. |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
246 |
moreover have "z \<le> INFIMUM {x. z < f x} f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
247 |
by (rule INF_greatest) simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
248 |
ultimately show ?thesis |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
249 |
using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
250 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
251 |
assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
252 |
show ?thesis |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
253 |
proof (rule classical) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
254 |
assume "\<not> f0 \<le> y" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
255 |
then have "eventually (\<lambda>x. y < f x) F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
256 |
using lim[THEN topological_tendstoD, of "{y <..}"] by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
257 |
then have "eventually (\<lambda>x. f0 \<le> f x) F" |
61810 | 258 |
using discrete by (auto elim!: eventually_mono) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
259 |
then have "INFIMUM {x. f0 \<le> f x} f \<le> y" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
260 |
by (rule upper) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
261 |
moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
262 |
by (intro INF_greatest) simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
263 |
ultimately show "f0 \<le> y" by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
264 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
265 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
266 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
267 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
268 |
lemma lim_imp_Limsup: |
61730 | 269 |
fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
270 |
assumes ntriv: "\<not> trivial_limit F" |
61973 | 271 |
assumes lim: "(f \<longlongrightarrow> f0) F" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
272 |
shows "Limsup F f = f0" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
273 |
proof (intro Limsup_eqI) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
274 |
fix P assume P: "eventually P F" |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
275 |
then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
276 |
by eventually_elim (auto intro!: SUP_upper) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
277 |
then show "f0 \<le> SUPREMUM (Collect P) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
278 |
by (rule tendsto_le[OF ntriv tendsto_const lim]) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
279 |
next |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
280 |
fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
281 |
show "y \<le> f0" |
53381 | 282 |
proof (cases "\<exists>z. f0 < z \<and> z < y") |
283 |
case True |
|
284 |
then obtain z where "f0 < z \<and> z < y" .. |
|
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
285 |
moreover have "SUPREMUM {x. f x < z} f \<le> z" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
286 |
by (rule SUP_least) simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
287 |
ultimately show ?thesis |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
288 |
using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
289 |
next |
53381 | 290 |
case False |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
291 |
show ?thesis |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
292 |
proof (rule classical) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
293 |
assume "\<not> y \<le> f0" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
294 |
then have "eventually (\<lambda>x. f x < y) F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
295 |
using lim[THEN topological_tendstoD, of "{..< y}"] by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
296 |
then have "eventually (\<lambda>x. f x \<le> f0) F" |
61810 | 297 |
using False by (auto elim!: eventually_mono simp: not_less) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
298 |
then have "y \<le> SUPREMUM {x. f x \<le> f0} f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
299 |
by (rule lower) |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
300 |
moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
301 |
by (intro SUP_least) simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
302 |
ultimately show "y \<le> f0" by simp |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
303 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
304 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
305 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
306 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
307 |
lemma Liminf_eq_Limsup: |
61730 | 308 |
fixes f0 :: "'a :: {complete_linorder,linorder_topology}" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
309 |
assumes ntriv: "\<not> trivial_limit F" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
310 |
and lim: "Liminf F f = f0" "Limsup F f = f0" |
61973 | 311 |
shows "(f \<longlongrightarrow> f0) F" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
312 |
proof (rule order_tendstoI) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
313 |
fix a assume "f0 < a" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
314 |
with assms have "Limsup F f < a" by simp |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
315 |
then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
316 |
unfolding Limsup_def INF_less_iff by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
317 |
then show "eventually (\<lambda>x. f x < a) F" |
61810 | 318 |
by (auto elim!: eventually_mono dest: SUP_lessD) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
319 |
next |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
320 |
fix a assume "a < f0" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
321 |
with assms have "a < Liminf F f" by simp |
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset
|
322 |
then obtain P where "eventually P F" "a < INFIMUM (Collect P) f" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
323 |
unfolding Liminf_def less_SUP_iff by auto |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
324 |
then show "eventually (\<lambda>x. a < f x) F" |
61810 | 325 |
by (auto elim!: eventually_mono dest: less_INF_D) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
326 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
327 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
328 |
lemma tendsto_iff_Liminf_eq_Limsup: |
61730 | 329 |
fixes f0 :: "'a :: {complete_linorder,linorder_topology}" |
61973 | 330 |
shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)" |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
331 |
by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
332 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
333 |
lemma liminf_subseq_mono: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
334 |
fixes X :: "nat \<Rightarrow> 'a :: complete_linorder" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
335 |
assumes "subseq r" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
336 |
shows "liminf X \<le> liminf (X \<circ> r) " |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
337 |
proof- |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
338 |
have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
339 |
proof (safe intro!: INF_mono) |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
340 |
fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m" |
60500 | 341 |
using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
342 |
qed |
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset
|
343 |
then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def) |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
344 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
345 |
|
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
346 |
lemma limsup_subseq_mono: |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
347 |
fixes X :: "nat \<Rightarrow> 'a :: complete_linorder" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
348 |
assumes "subseq r" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
349 |
shows "limsup (X \<circ> r) \<le> limsup X" |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
350 |
proof- |
61730 | 351 |
have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
352 |
proof (safe intro!: SUP_mono) |
61730 | 353 |
fix m :: nat |
354 |
assume "n \<le> m" |
|
355 |
then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma" |
|
60500 | 356 |
using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto |
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
357 |
qed |
61730 | 358 |
then show ?thesis |
359 |
by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def) |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
360 |
qed |
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
361 |
|
61730 | 362 |
lemma continuous_on_imp_continuous_within: |
363 |
"continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f" |
|
364 |
unfolding continuous_on_eq_continuous_within |
|
365 |
by (auto simp: continuous_within intro: tendsto_within_subset) |
|
61245 | 366 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
367 |
lemma Liminf_compose_continuous_mono: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
368 |
fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
369 |
assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
370 |
shows "Liminf F (\<lambda>n. f (g n)) = f (Liminf F g)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
371 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
372 |
{ fix P assume "eventually P F" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
373 |
have "\<exists>x. P x" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
374 |
proof (rule ccontr) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
375 |
assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
376 |
by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
377 |
with \<open>eventually P F\<close> F show False |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
378 |
by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
379 |
qed } |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
380 |
note * = this |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
381 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
382 |
have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62049
diff
changeset
|
383 |
unfolding Liminf_def |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
384 |
by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
385 |
(auto intro: eventually_True) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
386 |
also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
387 |
by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
388 |
(auto dest!: eventually_happens simp: F) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
389 |
finally show ?thesis by (auto simp: Liminf_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
390 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
391 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
392 |
lemma Limsup_compose_continuous_mono: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
393 |
fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
394 |
assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
395 |
shows "Limsup F (\<lambda>n. f (g n)) = f (Limsup F g)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
396 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
397 |
{ fix P assume "eventually P F" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
398 |
have "\<exists>x. P x" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
399 |
proof (rule ccontr) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
400 |
assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
401 |
by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
402 |
with \<open>eventually P F\<close> F show False |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
403 |
by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
404 |
qed } |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
405 |
note * = this |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
406 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
407 |
have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62049
diff
changeset
|
408 |
unfolding Limsup_def |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
409 |
by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
410 |
(auto intro: eventually_True) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
411 |
also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
412 |
by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
413 |
(auto dest!: eventually_happens simp: F) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
414 |
finally show ?thesis by (auto simp: Limsup_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
415 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
416 |
|
61245 | 417 |
lemma Liminf_compose_continuous_antimono: |
61730 | 418 |
fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}" |
419 |
assumes c: "continuous_on UNIV f" |
|
420 |
and am: "antimono f" |
|
421 |
and F: "F \<noteq> bot" |
|
61245 | 422 |
shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)" |
423 |
proof - |
|
61730 | 424 |
have *: "\<exists>x. P x" if "eventually P F" for P |
425 |
proof (rule ccontr) |
|
426 |
assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" |
|
427 |
by auto |
|
428 |
with \<open>eventually P F\<close> F show False |
|
429 |
by auto |
|
430 |
qed |
|
61245 | 431 |
have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62049
diff
changeset
|
432 |
unfolding Limsup_def |
61245 | 433 |
by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
434 |
(auto intro: eventually_True) |
|
435 |
also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" |
|
436 |
by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
|
437 |
(auto dest!: eventually_happens simp: F) |
|
438 |
finally show ?thesis |
|
439 |
by (auto simp: Liminf_def) |
|
440 |
qed |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
441 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
442 |
lemma Limsup_compose_continuous_antimono: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
443 |
fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
444 |
assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
445 |
shows "Limsup F (\<lambda>n. f (g n)) = f (Liminf F g)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
446 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
447 |
{ fix P assume "eventually P F" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
448 |
have "\<exists>x. P x" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
449 |
proof (rule ccontr) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
450 |
assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
451 |
by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
452 |
with \<open>eventually P F\<close> F show False |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
453 |
by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
454 |
qed } |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
455 |
note * = this |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
456 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
457 |
have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))" |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62049
diff
changeset
|
458 |
unfolding Liminf_def |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
459 |
by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
460 |
(auto intro: eventually_True) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
461 |
also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
462 |
by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
463 |
(auto dest!: eventually_happens simp: F) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
464 |
finally show ?thesis |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
465 |
by (auto simp: Limsup_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
466 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
467 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset
|
468 |
|
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
469 |
subsection \<open>More Limits\<close> |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
470 |
|
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
471 |
lemma convergent_limsup_cl: |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
472 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
473 |
shows "convergent X \<Longrightarrow> limsup X = lim X" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
474 |
by (auto simp: convergent_def limI lim_imp_Limsup) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
475 |
|
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
476 |
lemma convergent_liminf_cl: |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
477 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
478 |
shows "convergent X \<Longrightarrow> liminf X = lim X" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
479 |
by (auto simp: convergent_def limI lim_imp_Liminf) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
480 |
|
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
481 |
lemma lim_increasing_cl: |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
482 |
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m" |
61969 | 483 |
obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})" |
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
484 |
proof |
61969 | 485 |
show "f \<longlonglongrightarrow> (SUP n. f n)" |
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
486 |
using assms |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
487 |
by (intro increasing_tendsto) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
488 |
(auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
489 |
qed |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
490 |
|
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
491 |
lemma lim_decreasing_cl: |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
492 |
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m" |
61969 | 493 |
obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})" |
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
494 |
proof |
61969 | 495 |
show "f \<longlonglongrightarrow> (INF n. f n)" |
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
496 |
using assms |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
497 |
by (intro decreasing_tendsto) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
498 |
(auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans) |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
499 |
qed |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
500 |
|
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
501 |
lemma compact_complete_linorder: |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
502 |
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" |
61969 | 503 |
shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l" |
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
504 |
proof - |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
505 |
obtain r where "subseq r" and mono: "monoseq (X \<circ> r)" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
506 |
using seq_monosub[of X] |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
507 |
unfolding comp_def |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
508 |
by auto |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
509 |
then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)" |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
510 |
by (auto simp add: monoseq_def) |
61969 | 511 |
then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l" |
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
512 |
using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"] |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
513 |
by auto |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
514 |
then show ?thesis |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
515 |
using \<open>subseq r\<close> by auto |
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset
|
516 |
qed |
61245 | 517 |
|
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset
|
518 |
end |