Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Liminf_Limsup.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Liminf_Limsup.thy
    Author:     Johannes Hölzl, TU München
    Author:     Manuel Eberl, TU München
*)

section \<open>Liminf and Limsup on conditionally complete lattices\<close>

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 \ Sup (f ` A) \ (\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) \ 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 \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>

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) \
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
  unfolding Liminf_def by (auto intro!: SUP_eqI)

lemma Limsup_eqI:
  "(\P. eventually P F \ x \ Sup (f ` (Collect P))) \
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))) \<Longrightarrow> y \<le> x) \<Longrightarrow> 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 \ (\\<^sub>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 \ (\\<^sub>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: "\\<^sub>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: "\\<^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 < 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: "\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 \ 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 \<open>y < C\<close> 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 \<open>y > C\<close> 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 \<open>strict_mono r\<close>, 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 \<open>strict_mono r\<close>, 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 \<open>eventually P F\<close> F show False
        by auto
    qed }
  note * = this

  have "f (SUP P\{P. eventually P F}. Inf (g ` Collect P)) =
    Sup (f ` (\<lambda>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 \<open>eventually P F\<close> F show False
        by auto
    qed }
  note * = this

  have "f (INF P\{P. eventually P F}. Sup (g ` Collect P)) =
    Inf (f ` (\<lambda>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 \<open>eventually P F\<close> F show False
      by auto
  qed

  have "f (INF P\{P. eventually P F}. Sup (g ` Collect P)) =
    Sup (f ` (\<lambda>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 \<open>eventually P F\<close> F show False
        by auto
    qed }
  note * = this

  have "f (SUP P\{P. eventually P F}. Inf (g ` Collect P)) =
    Inf (f ` (\<lambda>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 \<open>More Limits\<close>

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 \<open>strict_mono r\<close> 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

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.