(* 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 ⟷ (∀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 ≤ Sup (f ` A) ⟷ (∀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) ⟹ Inf (f ` A) ≤ 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) lemma INF_Sigma: fixes f :: "_ ⇒ _ ⇒ _ :: complete_lattice" shows "(INF i ∈ A. INF j ∈ B i. f i j) = (INF p ∈ Sigma 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 ⟹ Inf (f ` (Collect P)) ≤ x) ⟹ (⋀y. (⋀P. eventually P F ⟹ Inf (f ` (Collect P)) ≤ y) ⟹ x ≤ y) ⟹ Liminf F f = x" unfolding Liminf_def by (auto intro!: SUP_eqI) lemma Limsup_eqI: "(⋀P. eventually P F ⟹ x ≤ Sup (f ` (Collect P))) ⟹ (⋀y. (⋀P. eventually P F ⟹ y ≤ Sup (f ` (Collect P))) ⟹ 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 mem_limsup_iff: "x ∈ limsup A ⟷ (∃⇩_{F}n in sequentially. x ∈ A n)" by (simp add: Limsup_def) (metis (mono_tags) eventually_mono not_frequently) lemma mem_liminf_iff: "x ∈ liminf A ⟷ (∀⇩_{F}n in sequentially. x ∈ A n)" by (simp add: Liminf_def) (metis (mono_tags) eventually_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 apply (auto simp add: Limsup_def) apply (rule INF_const) apply auto using eventually_True apply blast done 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 apply (auto simp add: Liminf_def) apply (rule SUP_const) apply auto using eventually_True apply blast done 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}. Inf (f ` (Collect P)) ≤ Inf (g ` (Collect Q))" 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}. Sup (f ` (Collect Q)) ≤ Sup (g ` (Collect P))" 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 "Inf (f ` (Collect P)) ≤ Inf (f ` (Collect ?C))" by (rule INF_mono) auto also have "… ≤ Sup (f ` (Collect ?C))" using not_False by (intro INF_le_SUP) auto also have "… ≤ Sup (f ` (Collect Q))" by (rule SUP_mono) auto finally show "Inf (f ` (Collect P)) ≤ Sup (f ` (Collect Q))" . 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: "∀⇩_{F}x in F. l ≤ f x" shows "l ≤ Limsup F f" using F Liminf_bounded[of l f F] Liminf_le_Limsup[of F f] order.trans x by blast lemma Liminf_le: assumes F: "F ≠ bot" and x: "∀⇩_{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 ⟷ (∀y<C. eventually (λx. y < X x) F)" proof - have "eventually (λx. y < X x) F" if "eventually P F" "y < Inf (X ` (Collect P))" for y P using that by (auto elim!: eventually_mono dest: less_INF_D) moreover have "∃P. eventually P F ∧ y < Inf (X ` (Collect P))" 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 ≤ Inf (X ` {x. z < 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 ≤ Inf (X ` {x. y < 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 > Sup (X ` (Collect P))" 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 > Sup (X ` (Collect P))" proof (cases "∃z. C < z ∧ z < y") case True then obtain z where z: "C < z ∧ z < y" .. moreover from z have "z ≥ Sup (X ` {x. X x < z})" 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 ≥ Sup (X ` {x. X x < y})" 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. Inf (f ` (Collect P)) ≤ f x) F" by eventually_elim (auto intro!: INF_lower) then show "Inf (f ` (Collect P)) ≤ f0" by (rule tendsto_le[OF ntriv lim tendsto_const]) next fix y assume upper: "⋀P. eventually P F ⟹ Inf (f ` (Collect P)) ≤ y" show "f0 ≤ y" proof cases assume "∃z. y < z ∧ z < f0" then obtain z where "y < z ∧ z < f0" .. moreover have "z ≤ Inf (f ` {x. z < f x})" 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 "Inf (f ` {x. f0 ≤ f x}) ≤ y" by (rule upper) moreover have "f0 ≤ Inf (f ` {x. f0 ≤ f x})" 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 ≤ Sup (f ` (Collect P))) F" by eventually_elim (auto intro!: SUP_upper) then show "f0 ≤ Sup (f ` (Collect P))" by (rule tendsto_le[OF ntriv tendsto_const lim]) next fix y assume lower: "⋀P. eventually P F ⟹ y ≤ Sup (f ` (Collect P))" show "y ≤ f0" proof (cases "∃z. f0 < z ∧ z < y") case True then obtain z where "f0 < z ∧ z < y" .. moreover have "Sup (f ` {x. f x < z}) ≤ 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 ≤ Sup (f ` {x. f x ≤ f0})" by (rule lower) moreover have "Sup (f ` {x. f x ≤ f0}) ≤ 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" "Sup (f ` (Collect P)) < 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 < Inf (f ` (Collect P))" 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 "strict_mono 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 ‹strict_mono 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 "strict_mono 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 ‹strict_mono 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 (SUP P∈{P. eventually P F}. Inf (g ` Collect P)) = Sup (f ` (λP. Inf (g ` Collect P)) ` {P. eventually P F})" using am continuous_on_imp_continuous_within [OF c] by (rule continuous_at_Sup_mono) (auto intro: eventually_True) then have "f (Liminf F g) = (SUP P ∈ {P. eventually P F}. f (Inf (g ` Collect P)))" by (simp add: Liminf_def image_comp) also have "… = (SUP P ∈ {P. eventually P F}. Inf (f ` (g ` Collect P)))" using * continuous_at_Inf_mono [OF am continuous_on_imp_continuous_within [OF c]] by auto finally show ?thesis by (auto simp: Liminf_def image_comp) 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 (INF P∈{P. eventually P F}. Sup (g ` Collect P)) = Inf (f ` (λP. Sup (g ` Collect P)) ` {P. eventually P F})" using am continuous_on_imp_continuous_within [OF c] by (rule continuous_at_Inf_mono) (auto intro: eventually_True) then have "f (Limsup F g) = (INF P ∈ {P. eventually P F}. f (Sup (g ` Collect P)))" by (simp add: Limsup_def image_comp) also have "… = (INF P ∈ {P. eventually P F}. Sup (f ` (g ` Collect P)))" using * continuous_at_Sup_mono [OF am continuous_on_imp_continuous_within [OF c]] by auto finally show ?thesis by (auto simp: Limsup_def image_comp) 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 (INF P∈{P. eventually P F}. Sup (g ` Collect P)) = Sup (f ` (λP. Sup (g ` Collect P)) ` {P. eventually P F})" using am continuous_on_imp_continuous_within [OF c] by (rule continuous_at_Inf_antimono) (auto intro: eventually_True) then have "f (Limsup F g) = (SUP P ∈ {P. eventually P F}. f (Sup (g ` Collect P)))" by (simp add: Limsup_def image_comp) also have "… = (SUP P ∈ {P. eventually P F}. Inf (f ` (g ` Collect P)))" using * continuous_at_Sup_antimono [OF am continuous_on_imp_continuous_within [OF c]] by auto finally show ?thesis by (auto simp: Liminf_def image_comp) 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 (SUP P∈{P. eventually P F}. Inf (g ` Collect P)) = Inf (f ` (λP. Inf (g ` Collect P)) ` {P. eventually P F})" using am continuous_on_imp_continuous_within [OF c] by (rule continuous_at_Sup_antimono) (auto intro: eventually_True) then have "f (Liminf F g) = (INF P ∈ {P. eventually P F}. f (Inf (g ` Collect P)))" by (simp add: Liminf_def image_comp) also have "… = (INF P ∈ {P. eventually P F}. Sup (f ` (g ` Collect P)))" using * continuous_at_Inf_antimono [OF am continuous_on_imp_continuous_within [OF c]] by auto finally show ?thesis by (auto simp: Limsup_def image_comp) qed lemma Liminf_filtermap_le: "Liminf (filtermap f F) g ≤ Liminf F (λx. g (f x))" apply (cases "F = bot", simp) by (subst Liminf_def) (auto simp add: INF_lower Liminf_bounded eventually_filtermap eventually_mono intro!: SUP_least) lemma Limsup_filtermap_ge: "Limsup (filtermap f F) g ≥ Limsup F (λx. g (f x))" apply (cases "F = bot", simp) by (subst Limsup_def) (auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest) lemma Liminf_least: "(⋀P. eventually P F ⟹ (INF x∈Collect P. f x) ≤ x) ⟹ Liminf F f ≤ x" by (auto intro!: SUP_least simp: Liminf_def) lemma Limsup_greatest: "(⋀P. eventually P F ⟹ x ≤ (SUP x∈Collect P. f x)) ⟹ Limsup F f ≥ x" by (auto intro!: INF_greatest simp: Limsup_def) lemma Liminf_filtermap_ge: "inj f ⟹ Liminf (filtermap f F) g ≥ Liminf F (λx. g (f x))" apply (cases "F = bot", simp) apply (rule Liminf_least) subgoal for P by (auto simp: eventually_filtermap the_inv_f_f intro!: Liminf_bounded INF_lower2 eventually_mono[of P]) done lemma Limsup_filtermap_le: "inj f ⟹ Limsup (filtermap f F) g ≤ Limsup F (λx. g (f x))" apply (cases "F = bot", simp) apply (rule Limsup_greatest) subgoal for P by (auto simp: eventually_filtermap the_inv_f_f intro!: Limsup_bounded SUP_upper2 eventually_mono[of P]) done lemma Liminf_filtermap_eq: "inj f ⟹ Liminf (filtermap f F) g = Liminf F (λx. g (f x))" using Liminf_filtermap_le[of f F g] Liminf_filtermap_ge[of f F g] by simp lemma Limsup_filtermap_eq: "inj f ⟹ Limsup (filtermap f F) g = Limsup F (λx. g (f x))" using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f] by simp 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. strict_mono r ∧ (X ∘ r) ⇢ l" proof - obtain r where "strict_mono 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 ‹strict_mono 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