author  hoelzl 
Tue, 05 Mar 2013 15:43:08 +0100  
changeset 51340  5e6296afe08d 
child 51542  738598beeb26 
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 

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

5 
header {* Liminf and Limsup on complete lattices *} 
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 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

8 
imports "~~/src/HOL/Complex_Main" 
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: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

12 
fixes x :: "'a :: {complete_linorder, inner_dense_linorder}" 
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: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

18 
fixes x :: "'a :: {complete_linorder, inner_dense_linorder}" 
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 

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

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

24 
"(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

25 
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

26 

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

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

28 
"(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

29 
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

30 

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

31 
subsubsection {* @{text Liminf} and @{text Limsup} *} 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

32 

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

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

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

35 

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

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

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

38 

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

39 
abbreviation "liminf \<equiv> Liminf sequentially" 
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 "limsup \<equiv> Limsup 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 
lemma Liminf_eqI: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

44 
"(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow> 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

45 
(\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

47 

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

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

49 
"(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow> 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

50 
(\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

52 

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

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

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

55 
shows "liminf f = (SUP n. INF m:{n..}. f m)" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

57 
by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

58 

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

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

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

61 
shows "limsup f = (INF n. SUP m:{n..}. f m)" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

63 
by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

64 

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

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

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

67 
shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

69 
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

70 
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

71 
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

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

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

74 
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

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

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

77 

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

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

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

80 
shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

82 
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

83 
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

84 
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

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

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

87 
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

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

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

90 

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

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

92 
fixes f g :: "'a => 'b :: complete_lattice" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

93 
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

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

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

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

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

98 
with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

99 
then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

100 
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

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

102 

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

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

104 
fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

105 
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

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

107 
by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

108 

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

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

110 
fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

111 
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

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

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

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

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

116 
with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

117 
then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

118 
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

119 
qed 
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 Limsup_eq: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

122 
fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

123 
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

124 
shows "Limsup net f = Limsup net g" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

125 
by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

126 

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

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

128 
fixes f :: "'a \<Rightarrow> 'b::complete_lattice" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

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

132 
apply (rule complete_lattice_class.SUP_least) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

133 
apply (rule complete_lattice_class.INF_greatest) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

135 
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

136 
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

137 
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

138 
using ntriv by (auto simp add: eventually_False) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

139 
have "INFI (Collect P) f \<le> INFI (Collect ?C) f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

140 
by (rule INF_mono) auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

141 
also have "\<dots> \<le> SUPR (Collect ?C) f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

142 
using not_False by (intro INF_le_SUP) auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

143 
also have "\<dots> \<le> SUPR (Collect Q) f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

144 
by (rule SUP_mono) auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

145 
finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" . 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

146 
qed 
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 Liminf_bounded: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

149 
fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

151 
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

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

153 
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

154 

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

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

156 
fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

158 
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

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

160 
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

161 

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

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

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

164 
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

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

166 
{ fix y P assume "eventually P F" "y < INFI (Collect P) X" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

167 
then have "eventually (\<lambda>x. y < X x) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

168 
by (auto elim!: eventually_elim1 dest: less_INF_D) } 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

170 
{ fix y P assume "y < C" and y: "\<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

171 
have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

173 
assume "\<exists>z. y < z \<and> z < C" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

174 
then guess z .. 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

175 
moreover then have "z \<le> INFI {x. z < X x} X" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

178 
using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

180 
assume "\<not> (\<exists>z. y < z \<and> z < C)" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

181 
then have "C \<le> INFI {x. y < X x} X" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

183 
with `y < C` show ?thesis 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

184 
using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

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

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

189 

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

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

191 
fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

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

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

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

197 
then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

198 
by eventually_elim (auto intro!: INF_lower) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

199 
then show "INFI (Collect P) f \<le> f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

200 
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

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

202 
fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

205 
assume "\<exists>z. y < z \<and> z < f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

206 
then guess z .. 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

207 
moreover have "z \<le> INFI {x. z < f x} f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

210 
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

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

212 
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

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

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

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

216 
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

217 
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

218 
then have "eventually (\<lambda>x. f0 \<le> f x) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

219 
using discrete by (auto elim!: eventually_elim1) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

220 
then have "INFI {x. f0 \<le> f x} f \<le> y" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

222 
moreover have "f0 \<le> INFI {x. f0 \<le> f x} f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

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

226 
qed 
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 

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

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

230 
fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

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

234 
proof (intro Limsup_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" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

236 
then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

237 
by eventually_elim (auto intro!: SUP_upper) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

238 
then show "f0 \<le> SUPR (Collect P) f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

239 
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

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

241 
fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

242 
show "y \<le> f0" 
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. f0 < z \<and> z < y" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

245 
then guess z .. 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

246 
moreover have "SUPR {x. f x < z} f \<le> z" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

247 
by (rule SUP_least) 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 lower, 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. f0 < z \<and> z < y)" 
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> y \<le> f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

255 
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

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. f x \<le> f0) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

258 
using discrete by (auto elim!: eventually_elim1 simp: not_less) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

259 
then have "y \<le> SUPR {x. f x \<le> f0} f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

261 
moreover have "SUPR {x. f x \<le> f0} f \<le> f0" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

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

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

271 
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

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

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

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

275 
with assms have "Limsup F f < a" by simp 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

276 
then obtain P where "eventually P F" "SUPR (Collect P) f < a" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

278 
then show "eventually (\<lambda>x. f x < a) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

279 
by (auto elim!: eventually_elim1 dest: SUP_lessD) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

282 
with assms have "a < Liminf F f" by simp 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

283 
then obtain P where "eventually P F" "a < INFI (Collect P) f" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

285 
then show "eventually (\<lambda>x. a < f x) F" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

286 
by (auto elim!: eventually_elim1 dest: less_INF_D) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

288 

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

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

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

291 
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

292 
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

293 

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

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

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

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

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

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

299 
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

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

301 
fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

302 
using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto 
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 
then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def) 
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 limsup_subseq_mono: 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

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

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

312 
have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

314 
fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma" 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

315 
using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

317 
then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def) 
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

319 

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

320 
end 