author  hoelzl 
Thu, 17 Dec 2015 16:43:36 +0100  
changeset 61880  ff4d33058566 
parent 61810  3c5040d5694a 
child 61969  e01015e49041 
permissions  rwrr 
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 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

3 
*) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

4 

60500  5 
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

6 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

7 
theory Liminf_Limsup 
51542  8 
imports Complex_Main 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

9 
begin 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

10 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

11 
lemma le_Sup_iff_less: 
53216  12 
fixes x :: "'a :: {complete_linorder, dense_linorder}" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

13 
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

14 
unfolding le_SUP_iff 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

15 
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

16 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

17 
lemma Inf_le_iff_less: 
53216  18 
fixes x :: "'a :: {complete_linorder, dense_linorder}" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

19 
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

20 
unfolding INF_le_iff 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

21 
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

22 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset

23 
lemma SUP_pair: 
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53381
diff
changeset

24 
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice" 
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53381
diff
changeset

25 
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

26 
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

27 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset

28 
lemma INF_pair: 
54257
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53381
diff
changeset

29 
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice" 
5c7a3b6b05a9
generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents:
53381
diff
changeset

30 
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

31 
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

32 

61585  33 
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

34 

54261  35 
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

36 
"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

37 

54261  38 
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

39 
"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

40 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

41 
abbreviation "liminf \<equiv> Liminf sequentially" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

42 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

43 
abbreviation "limsup \<equiv> Limsup sequentially" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

44 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

45 
lemma Liminf_eqI: 
61730  46 
"(\<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

47 
(\<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

48 
unfolding Liminf_def by (auto intro!: SUP_eqI) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

49 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

50 
lemma Limsup_eqI: 
61730  51 
"(\<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

52 
(\<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

53 
unfolding Limsup_def by (auto intro!: INF_eqI) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

54 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset

55 
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

56 
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

57 
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

58 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset

59 
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

60 
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

61 
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

62 

61730  63 
lemma Limsup_const: 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

64 
assumes ntriv: "\<not> trivial_limit F" 
54261  65 
shows "Limsup F (\<lambda>x. c) = c" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

66 
proof  
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

67 
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

68 
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

69 
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

70 
then show ?thesis 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

71 
unfolding Limsup_def using eventually_True 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

72 
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

73 
(auto intro!: INF_const simp del: eventually_True) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

74 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

75 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

76 
lemma Liminf_const: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

77 
assumes ntriv: "\<not> trivial_limit F" 
54261  78 
shows "Liminf F (\<lambda>x. c) = c" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

79 
proof  
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

80 
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

81 
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

82 
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

83 
then show ?thesis 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

84 
unfolding Liminf_def using eventually_True 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

85 
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

86 
(auto intro!: SUP_const simp del: eventually_True) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

87 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

88 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

89 
lemma Liminf_mono: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

90 
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

91 
shows "Liminf F f \<le> Liminf F g" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

92 
unfolding Liminf_def 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

93 
proof (safe intro!: SUP_mono) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

94 
fix P assume "eventually P F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

95 
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

96 
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

97 
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

98 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

99 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

100 
lemma Liminf_eq: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

101 
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

102 
shows "Liminf F f = Liminf F g" 
61810  103 
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

104 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

105 
lemma Limsup_mono: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

106 
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

107 
shows "Limsup F f \<le> Limsup F g" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

108 
unfolding Limsup_def 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

109 
proof (safe intro!: INF_mono) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

110 
fix P assume "eventually P F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

111 
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

112 
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

113 
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

114 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

115 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

116 
lemma Limsup_eq: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

117 
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

118 
shows "Limsup net f = Limsup net g" 
61810  119 
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

120 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

121 
lemma Liminf_le_Limsup: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

122 
assumes ntriv: "\<not> trivial_limit F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

123 
shows "Liminf F f \<le> Limsup F f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

124 
unfolding Limsup_def Liminf_def 
54261  125 
apply (rule SUP_least) 
126 
apply (rule INF_greatest) 

51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

127 
proof safe 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

128 
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

129 
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

130 
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

131 
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

132 
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

133 
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

134 
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

135 
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

136 
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

137 
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

138 
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

139 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

140 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

141 
lemma Liminf_bounded: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

142 
assumes ntriv: "\<not> trivial_limit F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

143 
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

144 
shows "C \<le> Liminf F X" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

145 
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

146 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

147 
lemma Limsup_bounded: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

148 
assumes ntriv: "\<not> trivial_limit F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

149 
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

150 
shows "Limsup F X \<le> C" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

151 
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

152 

61245  153 
lemma le_Limsup: 
154 
assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x" 

155 
shows "l \<le> Limsup F f" 

156 
proof  

157 
have "l = Limsup F (\<lambda>x. l)" 

158 
using F by (simp add: Limsup_const) 

159 
also have "\<dots> \<le> Limsup F f" 

61730  160 
by (intro Limsup_mono x) 
61245  161 
finally show ?thesis . 
162 
qed 

163 

51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

164 
lemma le_Liminf_iff: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

165 
fixes X :: "_ \<Rightarrow> _ :: complete_linorder" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

166 
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

167 
proof  
61730  168 
have "eventually (\<lambda>x. y < X x) F" 
169 
if "eventually P F" "y < INFIMUM (Collect P) X" for y P 

61810  170 
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

171 
moreover 
61730  172 
have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X" 
173 
if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P 

174 
proof (cases "\<exists>z. y < z \<and> z < C") 

175 
case True 

176 
then obtain z where z: "y < z \<and> z < C" .. 

177 
moreover from z have "z \<le> INFIMUM {x. z < X x} X" 

178 
by (auto intro!: INF_greatest) 

179 
ultimately show ?thesis 

180 
using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto 

181 
next 

182 
case False 

183 
then have "C \<le> INFIMUM {x. y < X x} X" 

184 
by (intro INF_greatest) auto 

185 
with \<open>y < C\<close> show ?thesis 

186 
using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto 

187 
qed 

51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

188 
ultimately show ?thesis 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

189 
unfolding Liminf_def le_SUP_iff by auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

190 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

191 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

192 
lemma lim_imp_Liminf: 
61730  193 
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

194 
assumes ntriv: "\<not> trivial_limit F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

195 
assumes lim: "(f > f0) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

196 
shows "Liminf F f = f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

197 
proof (intro Liminf_eqI) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

198 
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

199 
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

200 
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

201 
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

202 
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

203 
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

204 
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

205 
show "f0 \<le> y" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

206 
proof cases 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

207 
assume "\<exists>z. y < z \<and> z < f0" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

208 
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

209 
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

210 
by (rule INF_greatest) simp 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

211 
ultimately show ?thesis 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

212 
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

213 
next 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

214 
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

215 
show ?thesis 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

216 
proof (rule classical) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

217 
assume "\<not> f0 \<le> y" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

218 
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

219 
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

220 
then have "eventually (\<lambda>x. f0 \<le> f x) F" 
61810  221 
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

222 
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

223 
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

224 
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

225 
by (intro INF_greatest) simp 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

226 
ultimately show "f0 \<le> y" by simp 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

227 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

228 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

229 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

230 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

231 
lemma lim_imp_Limsup: 
61730  232 
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

233 
assumes ntriv: "\<not> trivial_limit F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

234 
assumes lim: "(f > f0) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

235 
shows "Limsup F f = f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

236 
proof (intro Limsup_eqI) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

237 
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

238 
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

239 
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

240 
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

241 
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

242 
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

243 
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

244 
show "y \<le> f0" 
53381  245 
proof (cases "\<exists>z. f0 < z \<and> z < y") 
246 
case True 

247 
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

248 
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

249 
by (rule SUP_least) simp 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

250 
ultimately show ?thesis 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

251 
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

252 
next 
53381  253 
case False 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

254 
show ?thesis 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

255 
proof (rule classical) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

256 
assume "\<not> y \<le> f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

257 
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

258 
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

259 
then have "eventually (\<lambda>x. f x \<le> f0) F" 
61810  260 
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

261 
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

262 
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

263 
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

264 
by (intro SUP_least) simp 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

265 
ultimately show "y \<le> f0" by simp 
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 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

268 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

269 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

270 
lemma Liminf_eq_Limsup: 
61730  271 
fixes f0 :: "'a :: {complete_linorder,linorder_topology}" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

272 
assumes ntriv: "\<not> trivial_limit F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

273 
and lim: "Liminf F f = f0" "Limsup F f = f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

274 
shows "(f > f0) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

275 
proof (rule order_tendstoI) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

276 
fix a assume "f0 < a" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

277 
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

278 
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

279 
unfolding Limsup_def INF_less_iff by auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

280 
then show "eventually (\<lambda>x. f x < a) F" 
61810  281 
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

282 
next 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

283 
fix a assume "a < f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

284 
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

285 
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

286 
unfolding Liminf_def less_SUP_iff by auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

287 
then show "eventually (\<lambda>x. a < f x) F" 
61810  288 
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

289 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

290 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

291 
lemma tendsto_iff_Liminf_eq_Limsup: 
61730  292 
fixes f0 :: "'a :: {complete_linorder,linorder_topology}" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

293 
shows "\<not> trivial_limit F \<Longrightarrow> (f > f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

294 
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

295 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

296 
lemma liminf_subseq_mono: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

297 
fixes X :: "nat \<Rightarrow> 'a :: complete_linorder" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

298 
assumes "subseq r" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

299 
shows "liminf X \<le> liminf (X \<circ> r) " 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

300 
proof 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

301 
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

302 
proof (safe intro!: INF_mono) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

303 
fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m" 
60500  304 
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

305 
qed 
56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
54261
diff
changeset

306 
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

307 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

308 

5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

309 
lemma limsup_subseq_mono: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

310 
fixes X :: "nat \<Rightarrow> 'a :: complete_linorder" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

311 
assumes "subseq r" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

312 
shows "limsup (X \<circ> r) \<le> limsup X" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

313 
proof 
61730  314 
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

315 
proof (safe intro!: SUP_mono) 
61730  316 
fix m :: nat 
317 
assume "n \<le> m" 

318 
then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma" 

60500  319 
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

320 
qed 
61730  321 
then show ?thesis 
322 
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

323 
qed 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

324 

61730  325 
lemma continuous_on_imp_continuous_within: 
326 
"continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f" 

327 
unfolding continuous_on_eq_continuous_within 

328 
by (auto simp: continuous_within intro: tendsto_within_subset) 

61245  329 

330 
lemma Liminf_compose_continuous_antimono: 

61730  331 
fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}" 
332 
assumes c: "continuous_on UNIV f" 

333 
and am: "antimono f" 

334 
and F: "F \<noteq> bot" 

61245  335 
shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)" 
336 
proof  

61730  337 
have *: "\<exists>x. P x" if "eventually P F" for P 
338 
proof (rule ccontr) 

339 
assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" 

340 
by auto 

341 
with \<open>eventually P F\<close> F show False 

342 
by auto 

343 
qed 

61245  344 
have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))" 
345 
unfolding Limsup_def INF_def 

346 
by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) 

347 
(auto intro: eventually_True) 

348 
also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" 

349 
by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) 

350 
(auto dest!: eventually_happens simp: F) 

351 
finally show ?thesis 

352 
by (auto simp: Liminf_def) 

353 
qed 

61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

354 
subsection \<open>More Limits\<close> 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

355 

ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

356 
lemma convergent_limsup_cl: 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

357 
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

358 
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

359 
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

360 

ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

361 
lemma convergent_liminf_cl: 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

362 
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

363 
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

364 
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

365 

ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

366 
lemma lim_increasing_cl: 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

367 
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m" 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

368 
obtains l where "f > (l::'a::{complete_linorder,linorder_topology})" 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

369 
proof 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

370 
show "f > (SUP n. f n)" 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

371 
using assms 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

372 
by (intro increasing_tendsto) 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

373 
(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

374 
qed 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

375 

ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

376 
lemma lim_decreasing_cl: 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

377 
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m" 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

378 
obtains l where "f > (l::'a::{complete_linorder,linorder_topology})" 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

379 
proof 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

380 
show "f > (INF n. f n)" 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

381 
using assms 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

382 
by (intro decreasing_tendsto) 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

383 
(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

384 
qed 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

385 

ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

386 
lemma compact_complete_linorder: 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

387 
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

388 
shows "\<exists>l r. subseq r \<and> (X \<circ> r) > l" 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

389 
proof  
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

390 
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

391 
using seq_monosub[of X] 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

392 
unfolding comp_def 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

393 
by auto 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

394 
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

395 
by (auto simp add: monoseq_def) 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

396 
then obtain l where "(X \<circ> r) > l" 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

397 
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

398 
by auto 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

399 
then show ?thesis 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

400 
using \<open>subseq r\<close> by auto 
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

401 
qed 
61245  402 

51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

403 
end 