(* Title: HOL/Library/Liminf_Limsup.thy
Author: Johannes Hölzl, TU München
Author: Manuel Eberl, TU München
*)
section \Liminf and Limsup on conditionally complete lattices\
theory Liminf_Limsup
imports Complex_Main
begin
lemma (in conditionally_complete_linorder) le_cSup_iff:
assumes "A \ {}" "bdd_above A"
shows "x \ Sup A \ (\ya\A. y < a)"
proof safe
fix y assume "x \ Sup A" "y < x"
then have "y < Sup A" by auto
then show "\a\A. y < a"
unfolding less_cSup_iff[OF assms] .
qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms)
lemma (in conditionally_complete_linorder) le_cSUP_iff:
"A \ {} \ bdd_above (f`A) \ x \ SUPREMUM A f \ (\yi\A. y < f i)"
using le_cSup_iff [of "f ` A"] by simp
lemma le_cSup_iff_less:
fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
shows "A \ {} \ bdd_above (f`A) \ x \ (SUP i:A. f i) \ (\yi\A. y \ f i)"
by (simp add: le_cSUP_iff)
(blast intro: less_imp_le less_trans less_le_trans dest: dense)
lemma le_Sup_iff_less:
fixes x :: "'a :: {complete_linorder, dense_linorder}"
shows "x \ (SUP i:A. f i) \ (\yi\A. y \ f i)" (is "?lhs = ?rhs")
unfolding le_SUP_iff
by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
lemma (in conditionally_complete_linorder) cInf_le_iff:
assumes "A \ {}" "bdd_below A"
shows "Inf A \ x \ (\y>x. \a\A. y > a)"
proof safe
fix y assume "x \ Inf A" "y > x"
then have "y > Inf A" by auto
then show "\a\A. y > a"
unfolding cInf_less_iff[OF assms] .
qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms)
lemma (in conditionally_complete_linorder) cINF_le_iff:
"A \ {} \ bdd_below (f`A) \ INFIMUM A f \ x \ (\y>x. \i\A. y > f i)"
using cInf_le_iff [of "f ` A"] by simp
lemma cInf_le_iff_less:
fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
shows "A \ {} \ bdd_below (f`A) \ (INF i:A. f i) \ x \ (\y>x. \i\A. f i \ y)"
by (simp add: cINF_le_iff)
(blast intro: less_imp_le less_trans le_less_trans dest: dense)
lemma Inf_le_iff_less:
fixes x :: "'a :: {complete_linorder, dense_linorder}"
shows "(INF i:A. f i) \ x \ (\y>x. \i\A. f i \ y)"
unfolding INF_le_iff
by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
lemma SUP_pair:
fixes f :: "_ \ _ \ _ :: complete_lattice"
shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \ B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: SUP_least SUP_upper2)
lemma INF_pair:
fixes f :: "_ \ _ \ _ :: complete_lattice"
shows "(INF i : A. INF j : B. f i j) = (INF p : A \ B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: INF_greatest INF_lower2)
subsubsection \\Liminf\ and \Limsup\\
definition Liminf :: "'a filter \ ('a \ 'b) \ 'b :: complete_lattice" where
"Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
definition Limsup :: "'a filter \ ('a \ 'b) \ 'b :: complete_lattice" where
"Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
abbreviation "liminf \ Liminf sequentially"
abbreviation "limsup \ Limsup sequentially"
lemma Liminf_eqI:
"(\P. eventually P F \ INFIMUM (Collect P) f \ x) \
(\y. (\P. eventually P F \ INFIMUM (Collect P) f \ y) \ x \ y) \ Liminf F f = x"
unfolding Liminf_def by (auto intro!: SUP_eqI)
lemma Limsup_eqI:
"(\P. eventually P F \ x \ SUPREMUM (Collect P) f) \
(\y. (\P. eventually P F \ y \ SUPREMUM (Collect P) f) \ y \ x) \ Limsup F f = x"
unfolding Limsup_def by (auto intro!: INF_eqI)
lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
unfolding Liminf_def eventually_sequentially
by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)"
unfolding Limsup_def eventually_sequentially
by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
lemma Limsup_const:
assumes ntriv: "\ trivial_limit F"
shows "Limsup F (\x. c) = c"
proof -
have *: "\P. Ex P \ P \ (\x. False)" by auto
have "\P. eventually P F \ (SUP x : {x. P x}. c) = c"
using ntriv by (intro SUP_const) (auto simp: eventually_False *)
then show ?thesis
unfolding Limsup_def using eventually_True
by (subst INF_cong[where D="\x. c"])
(auto intro!: INF_const simp del: eventually_True)
qed
lemma Liminf_const:
assumes ntriv: "\ trivial_limit F"
shows "Liminf F (\x. c) = c"
proof -
have *: "\P. Ex P \ P \ (\x. False)" by auto
have "\P. eventually P F \ (INF x : {x. P x}. c) = c"
using ntriv by (intro INF_const) (auto simp: eventually_False *)
then show ?thesis
unfolding Liminf_def using eventually_True
by (subst SUP_cong[where D="\x. c"])
(auto intro!: SUP_const simp del: eventually_True)
qed
lemma Liminf_mono:
assumes ev: "eventually (\x. f x \ g x) F"
shows "Liminf F f \ Liminf F g"
unfolding Liminf_def
proof (safe intro!: SUP_mono)
fix P assume "eventually P F"
with ev have "eventually (\x. f x \ g x \ P x) F" (is "eventually ?Q F") by (rule eventually_conj)
then show "\Q\{P. eventually P F}. INFIMUM (Collect P) f \ INFIMUM (Collect Q) g"
by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
qed
lemma Liminf_eq:
assumes "eventually (\x. f x = g x) F"
shows "Liminf F f = Liminf F g"
by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
lemma Limsup_mono:
assumes ev: "eventually (\x. f x \ g x) F"
shows "Limsup F f \ Limsup F g"
unfolding Limsup_def
proof (safe intro!: INF_mono)
fix P assume "eventually P F"
with ev have "eventually (\x. f x \ g x \ P x) F" (is "eventually ?Q F") by (rule eventually_conj)
then show "\Q\{P. eventually P F}. SUPREMUM (Collect Q) f \ SUPREMUM (Collect P) g"
by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
qed
lemma Limsup_eq:
assumes "eventually (\x. f x = g x) net"
shows "Limsup net f = Limsup net g"
by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
lemma Liminf_bot[simp]: "Liminf bot f = top"
unfolding Liminf_def top_unique[symmetric]
by (rule SUP_upper2[where i="\x. False"]) simp_all
lemma Limsup_bot[simp]: "Limsup bot f = bot"
unfolding Limsup_def bot_unique[symmetric]
by (rule INF_lower2[where i="\x. False"]) simp_all
lemma Liminf_le_Limsup:
assumes ntriv: "\ trivial_limit F"
shows "Liminf F f \ Limsup F f"
unfolding Limsup_def Liminf_def
apply (rule SUP_least)
apply (rule INF_greatest)
proof safe
fix P Q assume "eventually P F" "eventually Q F"
then have "eventually (\x. P x \ Q x) F" (is "eventually ?C F") by (rule eventually_conj)
then have not_False: "(\x. P x \ Q x) \ (\x. False)"
using ntriv by (auto simp add: eventually_False)
have "INFIMUM (Collect P) f \ INFIMUM (Collect ?C) f"
by (rule INF_mono) auto
also have "\ \ SUPREMUM (Collect ?C) f"
using not_False by (intro INF_le_SUP) auto
also have "\ \ SUPREMUM (Collect Q) f"
by (rule SUP_mono) auto
finally show "INFIMUM (Collect P) f \ SUPREMUM (Collect Q) f" .
qed
lemma Liminf_bounded:
assumes le: "eventually (\n. C \ X n) F"
shows "C \ Liminf F X"
using Liminf_mono[OF le] Liminf_const[of F C]
by (cases "F = bot") simp_all
lemma Limsup_bounded:
assumes le: "eventually (\n. X n \ C) F"
shows "Limsup F X \ C"
using Limsup_mono[OF le] Limsup_const[of F C]
by (cases "F = bot") simp_all
lemma le_Limsup:
assumes F: "F \ bot" and x: "\\<^sub>F x in F. l \ f x"
shows "l \ Limsup F f"
using F Liminf_bounded Liminf_le_Limsup order.trans x by blast
lemma Liminf_le:
assumes F: "F \ bot" and x: "\\<^sub>F x in F. f x \ l"
shows "Liminf F f \ l"
using F Liminf_le_Limsup Limsup_bounded order.trans x by blast
lemma le_Liminf_iff:
fixes X :: "_ \ _ :: complete_linorder"
shows "C \ Liminf F X \ (\yx. y < X x) F)"
proof -
have "eventually (\x. y < X x) F"
if "eventually P F" "y < INFIMUM (Collect P) X" for y P
using that by (auto elim!: eventually_mono dest: less_INF_D)
moreover
have "\P. eventually P F \ y < INFIMUM (Collect P) X"
if "y < C" and y: "\yx. y < X x) F" for y P
proof (cases "\z. y < z \ z < C")
case True
then obtain z where z: "y < z \ z < C" ..
moreover from z have "z \ INFIMUM {x. z < X x} X"
by (auto intro!: INF_greatest)
ultimately show ?thesis
using y by (intro exI[of _ "\x. z < X x"]) auto
next
case False
then have "C \ INFIMUM {x. y < X x} X"
by (intro INF_greatest) auto
with \y < C\ show ?thesis
using y by (intro exI[of _ "\x. y < X x"]) auto
qed
ultimately show ?thesis
unfolding Liminf_def le_SUP_iff by auto
qed
lemma Limsup_le_iff:
fixes X :: "_ \ _ :: complete_linorder"
shows "C \ Limsup F X \ (\y>C. eventually (\x. y > X x) F)"
proof -
{ fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X"
then have "eventually (\x. y > X x) F"
by (auto elim!: eventually_mono dest: SUP_lessD) }
moreover
{ fix y P assume "y > C" and y: "\y>C. eventually (\x. y > X x) F"
have "\P. eventually P F \ y > SUPREMUM (Collect P) X"
proof (cases "\z. C < z \ z < y")
case True
then obtain z where z: "C < z \ z < y" ..
moreover from z have "z \ SUPREMUM {x. z > X x} X"
by (auto intro!: SUP_least)
ultimately show ?thesis
using y by (intro exI[of _ "\x. z > X x"]) auto
next
case False
then have "C \ SUPREMUM {x. y > X x} X"
by (intro SUP_least) (auto simp: not_less)
with \y > C\ show ?thesis
using y by (intro exI[of _ "\x. y > X x"]) auto
qed }
ultimately show ?thesis
unfolding Limsup_def INF_le_iff by auto
qed
lemma less_LiminfD:
"y < Liminf F (f :: _ \ 'a :: complete_linorder) \ eventually (\x. f x > y) F"
using le_Liminf_iff[of "Liminf F f" F f] by simp
lemma Limsup_lessD:
"y > Limsup F (f :: _ \ 'a :: complete_linorder) \ eventually (\x. f x < y) F"
using Limsup_le_iff[of F f "Limsup F f"] by simp
lemma lim_imp_Liminf:
fixes f :: "'a \ _ :: {complete_linorder,linorder_topology}"
assumes ntriv: "\ trivial_limit F"
assumes lim: "(f \ f0) F"
shows "Liminf F f = f0"
proof (intro Liminf_eqI)
fix P assume P: "eventually P F"
then have "eventually (\x. INFIMUM (Collect P) f \ f x) F"
by eventually_elim (auto intro!: INF_lower)
then show "INFIMUM (Collect P) f \ f0"
by (rule tendsto_le[OF ntriv lim tendsto_const])
next
fix y assume upper: "\P. eventually P F \ INFIMUM (Collect P) f \ y"
show "f0 \ y"
proof cases
assume "\z. y < z \ z < f0"
then obtain z where "y < z \ z < f0" ..
moreover have "z \ INFIMUM {x. z < f x} f"
by (rule INF_greatest) simp
ultimately show ?thesis
using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
next
assume discrete: "\ (\z. y < z \ z < f0)"
show ?thesis
proof (rule classical)
assume "\ f0 \ y"
then have "eventually (\x. y < f x) F"
using lim[THEN topological_tendstoD, of "{y <..}"] by auto
then have "eventually (\x. f0 \ f x) F"
using discrete by (auto elim!: eventually_mono)
then have "INFIMUM {x. f0 \ f x} f \ y"
by (rule upper)
moreover have "f0 \ INFIMUM {x. f0 \ f x} f"
by (intro INF_greatest) simp
ultimately show "f0 \ y" by simp
qed
qed
qed
lemma lim_imp_Limsup:
fixes f :: "'a \ _ :: {complete_linorder,linorder_topology}"
assumes ntriv: "\ trivial_limit F"
assumes lim: "(f \ f0) F"
shows "Limsup F f = f0"
proof (intro Limsup_eqI)
fix P assume P: "eventually P F"
then have "eventually (\x. f x \ SUPREMUM (Collect P) f) F"
by eventually_elim (auto intro!: SUP_upper)
then show "f0 \ SUPREMUM (Collect P) f"
by (rule tendsto_le[OF ntriv tendsto_const lim])
next
fix y assume lower: "\P. eventually P F \ y \