author  immler 
Thu, 15 Sep 2016 16:07:20 +0200  
changeset 63895  9afa979137da 
parent 62975  1d066f6ab25d 
child 66447  a1f5c5c26fa6 
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 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

3 
Author: Manuel Eberl, TU München 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

5 

62624
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

6 
section \<open>Liminf and Limsup on conditionally complete lattices\<close> 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

7 

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

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

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

11 

62624
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

12 
lemma (in conditionally_complete_linorder) le_cSup_iff: 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

13 
assumes "A \<noteq> {}" "bdd_above A" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

14 
shows "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

15 
proof safe 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

16 
fix y assume "x \<le> Sup A" "y < x" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

17 
then have "y < Sup A" by auto 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

18 
then show "\<exists>a\<in>A. y < a" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

19 
unfolding less_cSup_iff[OF assms] . 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

20 
qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms) 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

21 

59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

22 
lemma (in conditionally_complete_linorder) le_cSUP_iff: 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

23 
"A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

24 
using le_cSup_iff [of "f ` A"] by simp 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

25 

59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

26 
lemma le_cSup_iff_less: 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

27 
fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

28 
shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

29 
by (simp add: le_cSUP_iff) 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

30 
(blast intro: less_imp_le less_trans less_le_trans dest: dense) 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

31 

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

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

34 
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

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

36 
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

37 

62624
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

38 
lemma (in conditionally_complete_linorder) cInf_le_iff: 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

39 
assumes "A \<noteq> {}" "bdd_below A" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

40 
shows "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

41 
proof safe 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

42 
fix y assume "x \<ge> Inf A" "y > x" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

43 
then have "y > Inf A" by auto 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

44 
then show "\<exists>a\<in>A. y > a" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

45 
unfolding cInf_less_iff[OF assms] . 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

46 
qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms) 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

47 

59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

48 
lemma (in conditionally_complete_linorder) cINF_le_iff: 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

49 
"A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

50 
using cInf_le_iff [of "f ` A"] by simp 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

51 

59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

52 
lemma cInf_le_iff_less: 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

53 
fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

54 
shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)" 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

55 
by (simp add: cINF_le_iff) 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

56 
(blast intro: less_imp_le less_trans le_less_trans dest: dense) 
59ceeb6f3079
generalized some Borel measurable statements to support ennreal
hoelzl
parents:
62343
diff
changeset

57 

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

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

60 
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

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

62 
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

63 

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

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

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

66 
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

67 
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

68 

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

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

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

71 
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

72 
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

73 

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

75 

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

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

78 

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

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

81 

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

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

83 

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

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

85 

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

86 
lemma Liminf_eqI: 
61730  87 
"(\<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

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

89 
unfolding Liminf_def by (auto intro!: SUP_eqI) 
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 Limsup_eqI: 
61730  92 
"(\<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

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

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

95 

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

96 
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

97 
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

98 
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

99 

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

100 
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

101 
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

102 
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

103 

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

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

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

108 
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

109 
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

110 
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

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

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

113 
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

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

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

116 

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

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

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

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

121 
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

122 
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

123 
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

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

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

126 
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

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

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

129 

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

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

131 
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

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

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

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

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

136 
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

137 
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

138 
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

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

142 
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

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

145 

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

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

147 
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

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

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

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

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

152 
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

153 
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

154 
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

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

156 

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

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

158 
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

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

161 

63895  162 
lemma Liminf_bot[simp]: "Liminf bot f = top" 
163 
unfolding Liminf_def top_unique[symmetric] 

164 
by (rule SUP_upper2[where i="\<lambda>x. False"]) simp_all 

165 

166 
lemma Limsup_bot[simp]: "Limsup bot f = bot" 

167 
unfolding Limsup_def bot_unique[symmetric] 

168 
by (rule INF_lower2[where i="\<lambda>x. False"]) simp_all 

169 

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

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

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

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

173 
unfolding Limsup_def Liminf_def 
54261  174 
apply (rule SUP_least) 
175 
apply (rule INF_greatest) 

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

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

177 
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

178 
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

179 
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

180 
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

181 
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

182 
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

183 
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

184 
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

185 
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

186 
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

187 
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

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

191 
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

192 
shows "C \<le> Liminf F X" 
63895  193 
using Liminf_mono[OF le] Liminf_const[of F C] 
194 
by (cases "F = bot") simp_all 

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

195 

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

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

197 
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

198 
shows "Limsup F X \<le> C" 
63895  199 
using Limsup_mono[OF le] Limsup_const[of F C] 
200 
by (cases "F = bot") simp_all 

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

201 

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

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

63895  205 
using F Liminf_bounded Liminf_le_Limsup order.trans x by blast 
206 

207 
lemma Liminf_le: 

208 
assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l" 

209 
shows "Liminf F f \<le> l" 

210 
using F Liminf_le_Limsup Limsup_bounded order.trans x by blast 

61245  211 

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

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

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

214 
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

215 
proof  
61730  216 
have "eventually (\<lambda>x. y < X x) F" 
217 
if "eventually P F" "y < INFIMUM (Collect P) X" for y P 

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

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

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

223 
case True 

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

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

226 
by (auto intro!: INF_greatest) 

227 
ultimately show ?thesis 

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

229 
next 

230 
case False 

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

232 
by (intro INF_greatest) auto 

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

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

235 
qed 

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

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

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

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

239 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

240 
lemma Limsup_le_iff: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

241 
fixes X :: "_ \<Rightarrow> _ :: complete_linorder" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

242 
shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

243 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

244 
{ fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

245 
then have "eventually (\<lambda>x. y > X x) F" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

246 
by (auto elim!: eventually_mono dest: SUP_lessD) } 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

247 
moreover 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

248 
{ fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

249 
have "\<exists>P. eventually P F \<and> y > SUPREMUM (Collect P) X" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

250 
proof (cases "\<exists>z. C < z \<and> z < y") 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

251 
case True 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

252 
then obtain z where z: "C < z \<and> z < y" .. 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

253 
moreover from z have "z \<ge> SUPREMUM {x. z > X x} X" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

254 
by (auto intro!: SUP_least) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

255 
ultimately show ?thesis 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

256 
using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

257 
next 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

258 
case False 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

259 
then have "C \<ge> SUPREMUM {x. y > X x} X" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

260 
by (intro SUP_least) (auto simp: not_less) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

261 
with \<open>y > C\<close> show ?thesis 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

262 
using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

263 
qed } 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

264 
ultimately show ?thesis 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

265 
unfolding Limsup_def INF_le_iff by auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

266 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

267 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

268 
lemma less_LiminfD: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

269 
"y < Liminf F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x > y) F" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

270 
using le_Liminf_iff[of "Liminf F f" F f] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

271 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

272 
lemma Limsup_lessD: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

273 
"y > Limsup F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x < y) F" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

274 
using Limsup_le_iff[of F f "Limsup F f"] by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

275 

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

276 
lemma lim_imp_Liminf: 
61730  277 
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

278 
assumes ntriv: "\<not> trivial_limit F" 
61973  279 
assumes lim: "(f \<longlongrightarrow> f0) F" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

282 
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

283 
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

284 
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

285 
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

286 
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

287 
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

288 
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

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

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

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

292 
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

293 
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

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

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

296 
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

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

298 
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

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

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

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

302 
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

303 
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

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

306 
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

307 
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

308 
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

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

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

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

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

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

314 

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

315 
lemma lim_imp_Limsup: 
61730  316 
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

317 
assumes ntriv: "\<not> trivial_limit F" 
61973  318 
assumes lim: "(f \<longlongrightarrow> f0) F" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

321 
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

322 
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

323 
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

324 
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

325 
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

326 
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

327 
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

328 
show "y \<le> f0" 
53381  329 
proof (cases "\<exists>z. f0 < z \<and> z < y") 
330 
case True 

331 
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

332 
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

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

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

335 
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

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

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

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

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

341 
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

342 
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

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

345 
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

346 
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

347 
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

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

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

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

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

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

353 

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

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

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

357 
and lim: "Liminf F f = f0" "Limsup F f = f0" 
61973  358 
shows "(f \<longlongrightarrow> f0) F" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

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

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

361 
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

362 
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

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

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

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

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

368 
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

369 
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

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

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

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

374 

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

375 
lemma tendsto_iff_Liminf_eq_Limsup: 
61730  376 
fixes f0 :: "'a :: {complete_linorder,linorder_topology}" 
61973  377 
shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)" 
51340
5e6296afe08d
move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff
changeset

378 
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

379 

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

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

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

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

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

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

385 
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

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

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

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

390 
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

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

392 

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

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

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

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

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

397 
proof 
61730  398 
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

399 
proof (safe intro!: SUP_mono) 
61730  400 
fix m :: nat 
401 
assume "n \<le> m" 

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

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

404 
qed 
61730  405 
then show ?thesis 
406 
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

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

408 

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

411 
unfolding continuous_on_eq_continuous_within 

412 
by (auto simp: continuous_within intro: tendsto_within_subset) 

61245  413 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

414 
lemma Liminf_compose_continuous_mono: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

415 
fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

416 
assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

417 
shows "Liminf F (\<lambda>n. f (g n)) = f (Liminf F g)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

418 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

419 
{ fix P assume "eventually P F" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

420 
have "\<exists>x. P x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

421 
proof (rule ccontr) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

422 
assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

423 
by auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

424 
with \<open>eventually P F\<close> F show False 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

425 
by auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

426 
qed } 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

427 
note * = this 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

428 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

429 
have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))" 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62049
diff
changeset

430 
unfolding Liminf_def 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

431 
by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

432 
(auto intro: eventually_True) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

433 
also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

434 
by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

435 
(auto dest!: eventually_happens simp: F) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

436 
finally show ?thesis by (auto simp: Liminf_def) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

437 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

438 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

439 
lemma Limsup_compose_continuous_mono: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

440 
fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

441 
assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

442 
shows "Limsup F (\<lambda>n. f (g n)) = f (Limsup F g)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

443 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

444 
{ fix P assume "eventually P F" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

445 
have "\<exists>x. P x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

446 
proof (rule ccontr) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

447 
assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

448 
by auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

449 
with \<open>eventually P F\<close> F show False 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

450 
by auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

451 
qed } 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

452 
note * = this 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

453 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

454 
have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))" 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62049
diff
changeset

455 
unfolding Limsup_def 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

456 
by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]]) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

457 
(auto intro: eventually_True) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

458 
also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

459 
by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]]) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

460 
(auto dest!: eventually_happens simp: F) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

461 
finally show ?thesis by (auto simp: Limsup_def) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

462 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

463 

61245  464 
lemma Liminf_compose_continuous_antimono: 
61730  465 
fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}" 
466 
assumes c: "continuous_on UNIV f" 

467 
and am: "antimono f" 

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

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

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

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

474 
by auto 

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

476 
by auto 

477 
qed 

61245  478 
have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))" 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62049
diff
changeset

479 
unfolding Limsup_def 
61245  480 
by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) 
481 
(auto intro: eventually_True) 

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

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

484 
(auto dest!: eventually_happens simp: F) 

485 
finally show ?thesis 

486 
by (auto simp: Liminf_def) 

487 
qed 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

488 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

489 
lemma Limsup_compose_continuous_antimono: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

490 
fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

491 
assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

492 
shows "Limsup F (\<lambda>n. f (g n)) = f (Liminf F g)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

493 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

494 
{ fix P assume "eventually P F" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

495 
have "\<exists>x. P x" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

496 
proof (rule ccontr) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

497 
assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

498 
by auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

499 
with \<open>eventually P F\<close> F show False 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

500 
by auto 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

501 
qed } 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

502 
note * = this 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

503 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

504 
have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))" 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62049
diff
changeset

505 
unfolding Liminf_def 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

506 
by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]]) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

507 
(auto intro: eventually_True) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

508 
also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

509 
by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]]) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

510 
(auto dest!: eventually_happens simp: F) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

511 
finally show ?thesis 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

512 
by (auto simp: Limsup_def) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

513 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

514 

63895  515 
lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))" 
516 
apply (cases "F = bot", simp) 

517 
by (subst Liminf_def) 

518 
(auto simp add: INF_lower Liminf_bounded eventually_filtermap eventually_mono intro!: SUP_least) 

519 

520 
lemma Limsup_filtermap_ge: "Limsup (filtermap f F) g \<ge> Limsup F (\<lambda>x. g (f x))" 

521 
apply (cases "F = bot", simp) 

522 
by (subst Limsup_def) 

523 
(auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest) 

524 

525 
lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x:Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x" 

526 
by (auto intro!: SUP_least simp: Liminf_def) 

527 

528 
lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x:Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x" 

529 
by (auto intro!: INF_greatest simp: Limsup_def) 

530 

531 
lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))" 

532 
apply (cases "F = bot", simp) 

533 
apply (rule Liminf_least) 

534 
subgoal for P 

535 
by (auto simp: eventually_filtermap the_inv_f_f 

536 
intro!: Liminf_bounded INF_lower2 eventually_mono[of P]) 

537 
done 

538 

539 
lemma Limsup_filtermap_le: "inj f \<Longrightarrow> Limsup (filtermap f F) g \<le> Limsup F (\<lambda>x. g (f x))" 

540 
apply (cases "F = bot", simp) 

541 
apply (rule Limsup_greatest) 

542 
subgoal for P 

543 
by (auto simp: eventually_filtermap the_inv_f_f 

544 
intro!: Limsup_bounded SUP_upper2 eventually_mono[of P]) 

545 
done 

546 

547 
lemma Liminf_filtermap_eq: "inj f \<Longrightarrow> Liminf (filtermap f F) g = Liminf F (\<lambda>x. g (f x))" 

548 
using Liminf_filtermap_le[of f F g] Liminf_filtermap_ge[of f F g] 

549 
by simp 

550 

551 
lemma Limsup_filtermap_eq: "inj f \<Longrightarrow> Limsup (filtermap f F) g = Limsup F (\<lambda>x. g (f x))" 

552 
using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f] 

553 
by simp 

554 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61973
diff
changeset

555 

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

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

557 

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

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

559 
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

560 
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

561 
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

562 

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

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

564 
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

565 
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

566 
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

567 

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

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

569 
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m" 
61969  570 
obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})" 
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

571 
proof 
61969  572 
show "f \<longlonglongrightarrow> (SUP n. f n)" 
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

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

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

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

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

577 

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

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

579 
assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m" 
61969  580 
obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})" 
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

581 
proof 
61969  582 
show "f \<longlonglongrightarrow> (INF n. f n)" 
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

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

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

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

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

587 

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

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

589 
fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}" 
61969  590 
shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l" 
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

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

592 
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

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

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

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

596 
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

597 
by (auto simp add: monoseq_def) 
61969  598 
then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l" 
61880
ff4d33058566
moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents:
61810
diff
changeset

599 
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

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

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

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

603 
qed 
61245  604 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

605 
lemma tendsto_Limsup: 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

606 
fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

607 
shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Limsup F f) F" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

608 
by (subst tendsto_iff_Liminf_eq_Limsup) auto 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

609 

1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

610 
lemma tendsto_Liminf: 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

611 
fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

612 
shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Liminf F f) F" 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

613 
by (subst tendsto_iff_Liminf_eq_Limsup) auto 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62624
diff
changeset

614 

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

615 
end 