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 ⟷ (∀y<x. ∃a∈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 ⟷ (∀y<x. ∃i∈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) ⟷ (∀y<x. ∃i∈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) ⟷ (∀y<x. ∃i∈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_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 ntriv: "¬ trivial_limit F"
assumes le: "eventually (λn. C ≤ X n) F"
shows "C ≤ Liminf F X"
using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
lemma Limsup_bounded:
assumes ntriv: "¬ trivial_limit F"
assumes le: "eventually (λn. X n ≤ C) F"
shows "Limsup F X ≤ C"
using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
lemma le_Limsup:
assumes F: "F ≠ bot" and x: "∀⇩F x in F. l ≤ f x"
shows "l ≤ Limsup F f"
proof -
have "l = Limsup F (λx. l)"
using F by (simp add: Limsup_const)
also have "… ≤ Limsup F f"
by (intro Limsup_mono x)
finally show ?thesis .
qed
lemma le_Liminf_iff:
fixes X :: "_ ⇒ _ :: complete_linorder"
shows "C ≤ Liminf F X ⟷ (∀y<C. eventually (λx. 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: "∀y<C. eventually (λx. 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 ≤ SUPREMUM (Collect P) f"
show "y ≤ f0"
proof (cases "∃z. f0 < z ∧ z < y")
case True
then obtain z where "f0 < z ∧ z < y" ..
moreover have "SUPREMUM {x. f x < z} f ≤ z"
by (rule SUP_least) simp
ultimately show ?thesis
using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
next
case False
show ?thesis
proof (rule classical)
assume "¬ y ≤ f0"
then have "eventually (λx. f x < y) F"
using lim[THEN topological_tendstoD, of "{..< y}"] by auto
then have "eventually (λx. f x ≤ f0) F"
using False by (auto elim!: eventually_mono simp: not_less)
then have "y ≤ SUPREMUM {x. f x ≤ f0} f"
by (rule lower)
moreover have "SUPREMUM {x. f x ≤ f0} f ≤ f0"
by (intro SUP_least) simp
ultimately show "y ≤ f0" by simp
qed
qed
qed
lemma Liminf_eq_Limsup:
fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
assumes ntriv: "¬ trivial_limit F"
and lim: "Liminf F f = f0" "Limsup F f = f0"
shows "(f ⤏ f0) F"
proof (rule order_tendstoI)
fix a assume "f0 < a"
with assms have "Limsup F f < a" by simp
then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
unfolding Limsup_def INF_less_iff by auto
then show "eventually (λx. f x < a) F"
by (auto elim!: eventually_mono dest: SUP_lessD)
next
fix a assume "a < f0"
with assms have "a < Liminf F f" by simp
then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
unfolding Liminf_def less_SUP_iff by auto
then show "eventually (λx. a < f x) F"
by (auto elim!: eventually_mono dest: less_INF_D)
qed
lemma tendsto_iff_Liminf_eq_Limsup:
fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
shows "¬ trivial_limit F ⟹ (f ⤏ f0) F ⟷ (Liminf F f = f0 ∧ Limsup F f = f0)"
by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
lemma liminf_subseq_mono:
fixes X :: "nat ⇒ 'a :: complete_linorder"
assumes "subseq r"
shows "liminf X ≤ liminf (X ∘ r) "
proof-
have "⋀n. (INF m:{n..}. X m) ≤ (INF m:{n..}. (X ∘ r) m)"
proof (safe intro!: INF_mono)
fix n m :: nat assume "n ≤ m" then show "∃ma∈{n..}. X ma ≤ (X ∘ r) m"
using seq_suble[OF ‹subseq r›, of m] by (intro bexI[of _ "r m"]) auto
qed
then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
qed
lemma limsup_subseq_mono:
fixes X :: "nat ⇒ 'a :: complete_linorder"
assumes "subseq r"
shows "limsup (X ∘ r) ≤ limsup X"
proof-
have "(SUP m:{n..}. (X ∘ r) m) ≤ (SUP m:{n..}. X m)" for n
proof (safe intro!: SUP_mono)
fix m :: nat
assume "n ≤ m"
then show "∃ma∈{n..}. (X ∘ r) m ≤ X ma"
using seq_suble[OF ‹subseq r›, of m] by (intro bexI[of _ "r m"]) auto
qed
then show ?thesis
by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
qed
lemma continuous_on_imp_continuous_within:
"continuous_on s f ⟹ t ⊆ s ⟹ x ∈ s ⟹ continuous (at x within t) f"
unfolding continuous_on_eq_continuous_within
by (auto simp: continuous_within intro: tendsto_within_subset)
lemma Liminf_compose_continuous_mono:
fixes f :: "'a::{complete_linorder, linorder_topology} ⇒ 'b::{complete_linorder, linorder_topology}"
assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F ≠ bot"
shows "Liminf F (λn. f (g n)) = f (Liminf F g)"
proof -
{ fix P assume "eventually P F"
have "∃x. P x"
proof (rule ccontr)
assume "¬ (∃x. P x)" then have "P = (λx. False)"
by auto
with ‹eventually P F› F show False
by auto
qed }
note * = this
have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
unfolding Liminf_def
by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
also have "… = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis by (auto simp: Liminf_def)
qed
lemma Limsup_compose_continuous_mono:
fixes f :: "'a::{complete_linorder, linorder_topology} ⇒ 'b::{complete_linorder, linorder_topology}"
assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F ≠ bot"
shows "Limsup F (λn. f (g n)) = f (Limsup F g)"
proof -
{ fix P assume "eventually P F"
have "∃x. P x"
proof (rule ccontr)
assume "¬ (∃x. P x)" then have "P = (λx. False)"
by auto
with ‹eventually P F› F show False
by auto
qed }
note * = this
have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
unfolding Limsup_def
by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
also have "… = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis by (auto simp: Limsup_def)
qed
lemma Liminf_compose_continuous_antimono:
fixes f :: "'a::{complete_linorder,linorder_topology} ⇒ 'b::{complete_linorder,linorder_topology}"
assumes c: "continuous_on UNIV f"
and am: "antimono f"
and F: "F ≠ bot"
shows "Liminf F (λn. f (g n)) = f (Limsup F g)"
proof -
have *: "∃x. P x" if "eventually P F" for P
proof (rule ccontr)
assume "¬ (∃x. P x)" then have "P = (λx. False)"
by auto
with ‹eventually P F› F show False
by auto
qed
have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
unfolding Limsup_def
by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
also have "… = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis
by (auto simp: Liminf_def)
qed
lemma Limsup_compose_continuous_antimono:
fixes f :: "'a::{complete_linorder, linorder_topology} ⇒ 'b::{complete_linorder, linorder_topology}"
assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F ≠ bot"
shows "Limsup F (λn. f (g n)) = f (Liminf F g)"
proof -
{ fix P assume "eventually P F"
have "∃x. P x"
proof (rule ccontr)
assume "¬ (∃x. P x)" then have "P = (λx. False)"
by auto
with ‹eventually P F› F show False
by auto
qed }
note * = this
have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
unfolding Liminf_def
by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
also have "… = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis
by (auto simp: Limsup_def)
qed
subsection ‹More Limits›
lemma convergent_limsup_cl:
fixes X :: "nat ⇒ 'a::{complete_linorder,linorder_topology}"
shows "convergent X ⟹ limsup X = lim X"
by (auto simp: convergent_def limI lim_imp_Limsup)
lemma convergent_liminf_cl:
fixes X :: "nat ⇒ 'a::{complete_linorder,linorder_topology}"
shows "convergent X ⟹ liminf X = lim X"
by (auto simp: convergent_def limI lim_imp_Liminf)
lemma lim_increasing_cl:
assumes "⋀n m. n ≥ m ⟹ f n ≥ f m"
obtains l where "f ⇢ (l::'a::{complete_linorder,linorder_topology})"
proof
show "f ⇢ (SUP n. f n)"
using assms
by (intro increasing_tendsto)
(auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
qed
lemma lim_decreasing_cl:
assumes "⋀n m. n ≥ m ⟹ f n ≤ f m"
obtains l where "f ⇢ (l::'a::{complete_linorder,linorder_topology})"
proof
show "f ⇢ (INF n. f n)"
using assms
by (intro decreasing_tendsto)
(auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
qed
lemma compact_complete_linorder:
fixes X :: "nat ⇒ 'a::{complete_linorder,linorder_topology}"
shows "∃l r. subseq r ∧ (X ∘ r) ⇢ l"
proof -
obtain r where "subseq r" and mono: "monoseq (X ∘ r)"
using seq_monosub[of X]
unfolding comp_def
by auto
then have "(∀n m. m ≤ n ⟶ (X ∘ r) m ≤ (X ∘ r) n) ∨ (∀n m. m ≤ n ⟶ (X ∘ r) n ≤ (X ∘ r) m)"
by (auto simp add: monoseq_def)
then obtain l where "(X ∘ r) ⇢ l"
using lim_increasing_cl[of "X ∘ r"] lim_decreasing_cl[of "X ∘ r"]
by auto
then show ?thesis
using ‹subseq r› by auto
qed
lemma tendsto_Limsup:
fixes f :: "_ ⇒ 'a :: {complete_linorder,linorder_topology}"
shows "F ≠ bot ⟹ Limsup F f = Liminf F f ⟹ (f ⤏ Limsup F f) F"
by (subst tendsto_iff_Liminf_eq_Limsup) auto
lemma tendsto_Liminf:
fixes f :: "_ ⇒ 'a :: {complete_linorder,linorder_topology}"
shows "F ≠ bot ⟹ Limsup F f = Liminf F f ⟹ (f ⤏ Liminf F f) F"
by (subst tendsto_iff_Liminf_eq_Limsup) auto
end