1.1 --- a/src/HOL/Library/Liminf_Limsup.thy Tue Nov 05 09:44:59 2013 +0100
1.2 +++ b/src/HOL/Library/Liminf_Limsup.thy Tue Nov 05 09:45:00 2013 +0100
1.3 @@ -32,10 +32,10 @@
1.4
1.5 subsubsection {* @{text Liminf} and @{text Limsup} *}
1.6
1.7 -definition
1.8 +definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
1.9 "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
1.10
1.11 -definition
1.12 +definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
1.13 "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
1.14
1.15 abbreviation "liminf \<equiv> Liminf sequentially"
1.16 @@ -43,32 +43,26 @@
1.17 abbreviation "limsup \<equiv> Limsup sequentially"
1.18
1.19 lemma Liminf_eqI:
1.20 - fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
1.21 - shows "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>
1.22 + "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>
1.23 (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
1.24 unfolding Liminf_def by (auto intro!: SUP_eqI)
1.25
1.26 lemma Limsup_eqI:
1.27 - fixes f :: "_ \<Rightarrow> _ :: complete_lattice"
1.28 - shows "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>
1.29 + "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>
1.30 (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
1.31 unfolding Limsup_def by (auto intro!: INF_eqI)
1.32
1.33 -lemma liminf_SUPR_INFI:
1.34 - fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
1.35 - shows "liminf f = (SUP n. INF m:{n..}. f m)"
1.36 +lemma liminf_SUPR_INFI: "liminf f = (SUP n. INF m:{n..}. f m)"
1.37 unfolding Liminf_def eventually_sequentially
1.38 by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
1.39
1.40 -lemma limsup_INFI_SUPR:
1.41 - fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
1.42 - shows "limsup f = (INF n. SUP m:{n..}. f m)"
1.43 +lemma limsup_INFI_SUPR: "limsup f = (INF n. SUP m:{n..}. f m)"
1.44 unfolding Limsup_def eventually_sequentially
1.45 by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
1.46
1.47 lemma Limsup_const:
1.48 assumes ntriv: "\<not> trivial_limit F"
1.49 - shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
1.50 + shows "Limsup F (\<lambda>x. c) = c"
1.51 proof -
1.52 have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
1.53 have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
1.54 @@ -81,7 +75,7 @@
1.55
1.56 lemma Liminf_const:
1.57 assumes ntriv: "\<not> trivial_limit F"
1.58 - shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
1.59 + shows "Liminf F (\<lambda>x. c) = c"
1.60 proof -
1.61 have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
1.62 have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
1.63 @@ -93,7 +87,6 @@
1.64 qed
1.65
1.66 lemma Liminf_mono:
1.67 - fixes f g :: "'a => 'b :: complete_lattice"
1.68 assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
1.69 shows "Liminf F f \<le> Liminf F g"
1.70 unfolding Liminf_def
1.71 @@ -105,13 +98,11 @@
1.72 qed
1.73
1.74 lemma Liminf_eq:
1.75 - fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
1.76 assumes "eventually (\<lambda>x. f x = g x) F"
1.77 shows "Liminf F f = Liminf F g"
1.78 by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
1.79
1.80 lemma Limsup_mono:
1.81 - fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
1.82 assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
1.83 shows "Limsup F f \<le> Limsup F g"
1.84 unfolding Limsup_def
1.85 @@ -123,18 +114,16 @@
1.86 qed
1.87
1.88 lemma Limsup_eq:
1.89 - fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
1.90 assumes "eventually (\<lambda>x. f x = g x) net"
1.91 shows "Limsup net f = Limsup net g"
1.92 by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
1.93
1.94 lemma Liminf_le_Limsup:
1.95 - fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
1.96 assumes ntriv: "\<not> trivial_limit F"
1.97 shows "Liminf F f \<le> Limsup F f"
1.98 unfolding Limsup_def Liminf_def
1.99 - apply (rule complete_lattice_class.SUP_least)
1.100 - apply (rule complete_lattice_class.INF_greatest)
1.101 + apply (rule SUP_least)
1.102 + apply (rule INF_greatest)
1.103 proof safe
1.104 fix P Q assume "eventually P F" "eventually Q F"
1.105 then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
1.106 @@ -150,14 +139,12 @@
1.107 qed
1.108
1.109 lemma Liminf_bounded:
1.110 - fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
1.111 assumes ntriv: "\<not> trivial_limit F"
1.112 assumes le: "eventually (\<lambda>n. C \<le> X n) F"
1.113 shows "C \<le> Liminf F X"
1.114 using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
1.115
1.116 lemma Limsup_bounded:
1.117 - fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
1.118 assumes ntriv: "\<not> trivial_limit F"
1.119 assumes le: "eventually (\<lambda>n. X n \<le> C) F"
1.120 shows "Limsup F X \<le> C"