src/HOL/Library/Liminf_Limsup.thy
changeset 51340 5e6296afe08d
child 51542 738598beeb26
equal deleted inserted replaced
51339:04ebef4ee844 51340:5e6296afe08d
       
     1 (*  Title:      HOL/Library/Liminf_Limsup.thy
       
     2     Author:     Johannes Hölzl, TU München
       
     3 *)
       
     4 
       
     5 header {* Liminf and Limsup on complete lattices *}
       
     6 
       
     7 theory Liminf_Limsup
       
     8 imports "~~/src/HOL/Complex_Main"
       
     9 begin
       
    10 
       
    11 lemma le_Sup_iff_less:
       
    12   fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
       
    13   shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
       
    14   unfolding le_SUP_iff
       
    15   by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
       
    16 
       
    17 lemma Inf_le_iff_less:
       
    18   fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
       
    19   shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
       
    20   unfolding INF_le_iff
       
    21   by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
       
    22 
       
    23 lemma SUPR_pair:
       
    24   "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
       
    25   by (rule antisym) (auto intro!: SUP_least SUP_upper2)
       
    26 
       
    27 lemma INFI_pair:
       
    28   "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
       
    29   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
       
    30 
       
    31 subsubsection {* @{text Liminf} and @{text Limsup} *}
       
    32 
       
    33 definition
       
    34   "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
       
    35 
       
    36 definition
       
    37   "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
       
    38 
       
    39 abbreviation "liminf \<equiv> Liminf sequentially"
       
    40 
       
    41 abbreviation "limsup \<equiv> Limsup sequentially"
       
    42 
       
    43 lemma Liminf_eqI:
       
    44   "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
       
    45     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
       
    46   unfolding Liminf_def by (auto intro!: SUP_eqI)
       
    47 
       
    48 lemma Limsup_eqI:
       
    49   "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
       
    50     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
       
    51   unfolding Limsup_def by (auto intro!: INF_eqI)
       
    52 
       
    53 lemma liminf_SUPR_INFI:
       
    54   fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
       
    55   shows "liminf f = (SUP n. INF m:{n..}. f m)"
       
    56   unfolding Liminf_def eventually_sequentially
       
    57   by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
       
    58 
       
    59 lemma limsup_INFI_SUPR:
       
    60   fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
       
    61   shows "limsup f = (INF n. SUP m:{n..}. f m)"
       
    62   unfolding Limsup_def eventually_sequentially
       
    63   by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
       
    64 
       
    65 lemma Limsup_const: 
       
    66   assumes ntriv: "\<not> trivial_limit F"
       
    67   shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
       
    68 proof -
       
    69   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
       
    70   have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
       
    71     using ntriv by (intro SUP_const) (auto simp: eventually_False *)
       
    72   then show ?thesis
       
    73     unfolding Limsup_def using eventually_True
       
    74     by (subst INF_cong[where D="\<lambda>x. c"])
       
    75        (auto intro!: INF_const simp del: eventually_True)
       
    76 qed
       
    77 
       
    78 lemma Liminf_const:
       
    79   assumes ntriv: "\<not> trivial_limit F"
       
    80   shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
       
    81 proof -
       
    82   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
       
    83   have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
       
    84     using ntriv by (intro INF_const) (auto simp: eventually_False *)
       
    85   then show ?thesis
       
    86     unfolding Liminf_def using eventually_True
       
    87     by (subst SUP_cong[where D="\<lambda>x. c"])
       
    88        (auto intro!: SUP_const simp del: eventually_True)
       
    89 qed
       
    90 
       
    91 lemma Liminf_mono:
       
    92   fixes f g :: "'a => 'b :: complete_lattice"
       
    93   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
       
    94   shows "Liminf F f \<le> Liminf F g"
       
    95   unfolding Liminf_def
       
    96 proof (safe intro!: SUP_mono)
       
    97   fix P assume "eventually P F"
       
    98   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
       
    99   then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
       
   100     by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
       
   101 qed
       
   102 
       
   103 lemma Liminf_eq:
       
   104   fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
       
   105   assumes "eventually (\<lambda>x. f x = g x) F"
       
   106   shows "Liminf F f = Liminf F g"
       
   107   by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
       
   108 
       
   109 lemma Limsup_mono:
       
   110   fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
       
   111   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
       
   112   shows "Limsup F f \<le> Limsup F g"
       
   113   unfolding Limsup_def
       
   114 proof (safe intro!: INF_mono)
       
   115   fix P assume "eventually P F"
       
   116   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
       
   117   then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
       
   118     by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
       
   119 qed
       
   120 
       
   121 lemma Limsup_eq:
       
   122   fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
       
   123   assumes "eventually (\<lambda>x. f x = g x) net"
       
   124   shows "Limsup net f = Limsup net g"
       
   125   by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
       
   126 
       
   127 lemma Liminf_le_Limsup:
       
   128   fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
       
   129   assumes ntriv: "\<not> trivial_limit F"
       
   130   shows "Liminf F f \<le> Limsup F f"
       
   131   unfolding Limsup_def Liminf_def
       
   132   apply (rule complete_lattice_class.SUP_least)
       
   133   apply (rule complete_lattice_class.INF_greatest)
       
   134 proof safe
       
   135   fix P Q assume "eventually P F" "eventually Q F"
       
   136   then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
       
   137   then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
       
   138     using ntriv by (auto simp add: eventually_False)
       
   139   have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
       
   140     by (rule INF_mono) auto
       
   141   also have "\<dots> \<le> SUPR (Collect ?C) f"
       
   142     using not_False by (intro INF_le_SUP) auto
       
   143   also have "\<dots> \<le> SUPR (Collect Q) f"
       
   144     by (rule SUP_mono) auto
       
   145   finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
       
   146 qed
       
   147 
       
   148 lemma Liminf_bounded:
       
   149   fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
       
   150   assumes ntriv: "\<not> trivial_limit F"
       
   151   assumes le: "eventually (\<lambda>n. C \<le> X n) F"
       
   152   shows "C \<le> Liminf F X"
       
   153   using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
       
   154 
       
   155 lemma Limsup_bounded:
       
   156   fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
       
   157   assumes ntriv: "\<not> trivial_limit F"
       
   158   assumes le: "eventually (\<lambda>n. X n \<le> C) F"
       
   159   shows "Limsup F X \<le> C"
       
   160   using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
       
   161 
       
   162 lemma le_Liminf_iff:
       
   163   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
       
   164   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
       
   165 proof -
       
   166   { fix y P assume "eventually P F" "y < INFI (Collect P) X"
       
   167     then have "eventually (\<lambda>x. y < X x) F"
       
   168       by (auto elim!: eventually_elim1 dest: less_INF_D) }
       
   169   moreover
       
   170   { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
       
   171     have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
       
   172     proof cases
       
   173       assume "\<exists>z. y < z \<and> z < C"
       
   174       then guess z ..
       
   175       moreover then have "z \<le> INFI {x. z < X x} X"
       
   176         by (auto intro!: INF_greatest)
       
   177       ultimately show ?thesis
       
   178         using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
       
   179     next
       
   180       assume "\<not> (\<exists>z. y < z \<and> z < C)"
       
   181       then have "C \<le> INFI {x. y < X x} X"
       
   182         by (intro INF_greatest) auto
       
   183       with `y < C` show ?thesis
       
   184         using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
       
   185     qed }
       
   186   ultimately show ?thesis
       
   187     unfolding Liminf_def le_SUP_iff by auto
       
   188 qed
       
   189 
       
   190 lemma lim_imp_Liminf:
       
   191   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
       
   192   assumes ntriv: "\<not> trivial_limit F"
       
   193   assumes lim: "(f ---> f0) F"
       
   194   shows "Liminf F f = f0"
       
   195 proof (intro Liminf_eqI)
       
   196   fix P assume P: "eventually P F"
       
   197   then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
       
   198     by eventually_elim (auto intro!: INF_lower)
       
   199   then show "INFI (Collect P) f \<le> f0"
       
   200     by (rule tendsto_le[OF ntriv lim tendsto_const])
       
   201 next
       
   202   fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
       
   203   show "f0 \<le> y"
       
   204   proof cases
       
   205     assume "\<exists>z. y < z \<and> z < f0"
       
   206     then guess z ..
       
   207     moreover have "z \<le> INFI {x. z < f x} f"
       
   208       by (rule INF_greatest) simp
       
   209     ultimately show ?thesis
       
   210       using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
       
   211   next
       
   212     assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
       
   213     show ?thesis
       
   214     proof (rule classical)
       
   215       assume "\<not> f0 \<le> y"
       
   216       then have "eventually (\<lambda>x. y < f x) F"
       
   217         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
       
   218       then have "eventually (\<lambda>x. f0 \<le> f x) F"
       
   219         using discrete by (auto elim!: eventually_elim1)
       
   220       then have "INFI {x. f0 \<le> f x} f \<le> y"
       
   221         by (rule upper)
       
   222       moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
       
   223         by (intro INF_greatest) simp
       
   224       ultimately show "f0 \<le> y" by simp
       
   225     qed
       
   226   qed
       
   227 qed
       
   228 
       
   229 lemma lim_imp_Limsup:
       
   230   fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
       
   231   assumes ntriv: "\<not> trivial_limit F"
       
   232   assumes lim: "(f ---> f0) F"
       
   233   shows "Limsup F f = f0"
       
   234 proof (intro Limsup_eqI)
       
   235   fix P assume P: "eventually P F"
       
   236   then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
       
   237     by eventually_elim (auto intro!: SUP_upper)
       
   238   then show "f0 \<le> SUPR (Collect P) f"
       
   239     by (rule tendsto_le[OF ntriv tendsto_const lim])
       
   240 next
       
   241   fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
       
   242   show "y \<le> f0"
       
   243   proof cases
       
   244     assume "\<exists>z. f0 < z \<and> z < y"
       
   245     then guess z ..
       
   246     moreover have "SUPR {x. f x < z} f \<le> z"
       
   247       by (rule SUP_least) simp
       
   248     ultimately show ?thesis
       
   249       using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
       
   250   next
       
   251     assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
       
   252     show ?thesis
       
   253     proof (rule classical)
       
   254       assume "\<not> y \<le> f0"
       
   255       then have "eventually (\<lambda>x. f x < y) F"
       
   256         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
       
   257       then have "eventually (\<lambda>x. f x \<le> f0) F"
       
   258         using discrete by (auto elim!: eventually_elim1 simp: not_less)
       
   259       then have "y \<le> SUPR {x. f x \<le> f0} f"
       
   260         by (rule lower)
       
   261       moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
       
   262         by (intro SUP_least) simp
       
   263       ultimately show "y \<le> f0" by simp
       
   264     qed
       
   265   qed
       
   266 qed
       
   267 
       
   268 lemma Liminf_eq_Limsup:
       
   269   fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
       
   270   assumes ntriv: "\<not> trivial_limit F"
       
   271     and lim: "Liminf F f = f0" "Limsup F f = f0"
       
   272   shows "(f ---> f0) F"
       
   273 proof (rule order_tendstoI)
       
   274   fix a assume "f0 < a"
       
   275   with assms have "Limsup F f < a" by simp
       
   276   then obtain P where "eventually P F" "SUPR (Collect P) f < a"
       
   277     unfolding Limsup_def INF_less_iff by auto
       
   278   then show "eventually (\<lambda>x. f x < a) F"
       
   279     by (auto elim!: eventually_elim1 dest: SUP_lessD)
       
   280 next
       
   281   fix a assume "a < f0"
       
   282   with assms have "a < Liminf F f" by simp
       
   283   then obtain P where "eventually P F" "a < INFI (Collect P) f"
       
   284     unfolding Liminf_def less_SUP_iff by auto
       
   285   then show "eventually (\<lambda>x. a < f x) F"
       
   286     by (auto elim!: eventually_elim1 dest: less_INF_D)
       
   287 qed
       
   288 
       
   289 lemma tendsto_iff_Liminf_eq_Limsup:
       
   290   fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
       
   291   shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
       
   292   by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
       
   293 
       
   294 lemma liminf_subseq_mono:
       
   295   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
       
   296   assumes "subseq r"
       
   297   shows "liminf X \<le> liminf (X \<circ> r) "
       
   298 proof-
       
   299   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
       
   300   proof (safe intro!: INF_mono)
       
   301     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
       
   302       using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
       
   303   qed
       
   304   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
       
   305 qed
       
   306 
       
   307 lemma limsup_subseq_mono:
       
   308   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
       
   309   assumes "subseq r"
       
   310   shows "limsup (X \<circ> r) \<le> limsup X"
       
   311 proof-
       
   312   have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
       
   313   proof (safe intro!: SUP_mono)
       
   314     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
       
   315       using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
       
   316   qed
       
   317   then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
       
   318 qed
       
   319 
       
   320 end