Theory HOL-Library.Liminf_Limsup

(*  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. aA. y < a)"
proof safe
  fix y assume "x  Sup A" "y < x"
  then have "y < Sup A" by auto
  then show "aA. 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. iA. 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 iA. f i)  (y<x. iA. 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 iA. f i)  (y<x. iA. 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. aA. y > a)"
proof safe
  fix y assume "x  Inf A" "y > x"
  then have "y > Inf A" by auto
  then show "aA. 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. iA. 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 iA. f i)  x  (y>x. iA. 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 iA. f i)  x  (y>x. iA. 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 xCollect 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 xCollect 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