src/HOL/Library/Liminf_Limsup.thy
changeset 69313 b021008c5397
parent 69260 0a9688695a1b
child 69661 a03a63b81f44
     1.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -20,7 +20,7 @@
     1.4  qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms)
     1.5  
     1.6  lemma (in conditionally_complete_linorder) le_cSUP_iff:
     1.7 -  "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
     1.8 +  "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> Sup (f ` A) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
     1.9    using le_cSup_iff [of "f ` A"] by simp
    1.10  
    1.11  lemma le_cSup_iff_less:
    1.12 @@ -46,7 +46,7 @@
    1.13  qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms)
    1.14  
    1.15  lemma (in conditionally_complete_linorder) cINF_le_iff:
    1.16 -  "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
    1.17 +  "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> Inf (f ` A) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
    1.18    using cInf_le_iff [of "f ` A"] by simp
    1.19  
    1.20  lemma cInf_le_iff_less:
    1.21 @@ -89,13 +89,13 @@
    1.22  abbreviation "limsup \<equiv> Limsup sequentially"
    1.23  
    1.24  lemma Liminf_eqI:
    1.25 -  "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>
    1.26 -    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    1.27 +  "(\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> x) \<Longrightarrow>
    1.28 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
    1.29    unfolding Liminf_def by (auto intro!: SUP_eqI)
    1.30  
    1.31  lemma Limsup_eqI:
    1.32 -  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>
    1.33 -    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    1.34 +  "(\<And>P. eventually P F \<Longrightarrow> x \<le> Sup (f ` (Collect P))) \<Longrightarrow>
    1.35 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    1.36    unfolding Limsup_def by (auto intro!: INF_eqI)
    1.37  
    1.38  lemma liminf_SUP_INF: "liminf f = (SUP n. INF m\<in>{n..}. f m)"
    1.39 @@ -139,7 +139,7 @@
    1.40  proof (safe intro!: SUP_mono)
    1.41    fix P assume "eventually P F"
    1.42    with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
    1.43 -  then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g"
    1.44 +  then show "\<exists>Q\<in>{P. eventually P F}. Inf (f ` (Collect P)) \<le> Inf (g ` (Collect Q))"
    1.45      by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
    1.46  qed
    1.47  
    1.48 @@ -155,7 +155,7 @@
    1.49  proof (safe intro!: INF_mono)
    1.50    fix P assume "eventually P F"
    1.51    with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
    1.52 -  then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g"
    1.53 +  then show "\<exists>Q\<in>{P. eventually P F}. Sup (f ` (Collect Q)) \<le> Sup (g ` (Collect P))"
    1.54      by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
    1.55  qed
    1.56  
    1.57 @@ -183,13 +183,13 @@
    1.58    then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
    1.59    then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
    1.60      using ntriv by (auto simp add: eventually_False)
    1.61 -  have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f"
    1.62 +  have "Inf (f ` (Collect P)) \<le> Inf (f ` (Collect ?C))"
    1.63      by (rule INF_mono) auto
    1.64 -  also have "\<dots> \<le> SUPREMUM (Collect ?C) f"
    1.65 +  also have "\<dots> \<le> Sup (f ` (Collect ?C))"
    1.66      using not_False by (intro INF_le_SUP) auto
    1.67 -  also have "\<dots> \<le> SUPREMUM (Collect Q) f"
    1.68 +  also have "\<dots> \<le> Sup (f ` (Collect Q))"
    1.69      by (rule SUP_mono) auto
    1.70 -  finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
    1.71 +  finally show "Inf (f ` (Collect P)) \<le> Sup (f ` (Collect Q))" .
    1.72  qed
    1.73  
    1.74  lemma Liminf_bounded:
    1.75 @@ -219,21 +219,21 @@
    1.76    shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
    1.77  proof -
    1.78    have "eventually (\<lambda>x. y < X x) F"
    1.79 -    if "eventually P F" "y < INFIMUM (Collect P) X" for y P
    1.80 +    if "eventually P F" "y < Inf (X ` (Collect P))" for y P
    1.81      using that by (auto elim!: eventually_mono dest: less_INF_D)
    1.82    moreover
    1.83 -  have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
    1.84 +  have "\<exists>P. eventually P F \<and> y < Inf (X ` (Collect P))"
    1.85      if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
    1.86    proof (cases "\<exists>z. y < z \<and> z < C")
    1.87      case True
    1.88      then obtain z where z: "y < z \<and> z < C" ..
    1.89 -    moreover from z have "z \<le> INFIMUM {x. z < X x} X"
    1.90 +    moreover from z have "z \<le> Inf (X ` {x. z < X x})"
    1.91        by (auto intro!: INF_greatest)
    1.92      ultimately show ?thesis
    1.93        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
    1.94    next
    1.95      case False
    1.96 -    then have "C \<le> INFIMUM {x. y < X x} X"
    1.97 +    then have "C \<le> Inf (X ` {x. y < X x})"
    1.98        by (intro INF_greatest) auto
    1.99      with \<open>y < C\<close> show ?thesis
   1.100        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
   1.101 @@ -246,22 +246,22 @@
   1.102    fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   1.103    shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)"
   1.104  proof -
   1.105 -  { fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X"
   1.106 +  { fix y P assume "eventually P F" "y > Sup (X ` (Collect P))"
   1.107      then have "eventually (\<lambda>x. y > X x) F"
   1.108        by (auto elim!: eventually_mono dest: SUP_lessD) }
   1.109    moreover
   1.110    { fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F"
   1.111 -    have "\<exists>P. eventually P F \<and> y > SUPREMUM (Collect P) X"
   1.112 +    have "\<exists>P. eventually P F \<and> y > Sup (X ` (Collect P))"
   1.113      proof (cases "\<exists>z. C < z \<and> z < y")
   1.114        case True
   1.115        then obtain z where z: "C < z \<and> z < y" ..
   1.116 -      moreover from z have "z \<ge> SUPREMUM {x. z > X x} X"
   1.117 +      moreover from z have "z \<ge> Sup (X ` {x. X x < z})"
   1.118          by (auto intro!: SUP_least)
   1.119        ultimately show ?thesis
   1.120          using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto
   1.121      next
   1.122        case False
   1.123 -      then have "C \<ge> SUPREMUM {x. y > X x} X"
   1.124 +      then have "C \<ge> Sup (X ` {x. X x < y})"
   1.125          by (intro SUP_least) (auto simp: not_less)
   1.126        with \<open>y > C\<close> show ?thesis
   1.127          using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto
   1.128 @@ -285,17 +285,17 @@
   1.129    shows "Liminf F f = f0"
   1.130  proof (intro Liminf_eqI)
   1.131    fix P assume P: "eventually P F"
   1.132 -  then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F"
   1.133 +  then have "eventually (\<lambda>x. Inf (f ` (Collect P)) \<le> f x) F"
   1.134      by eventually_elim (auto intro!: INF_lower)
   1.135 -  then show "INFIMUM (Collect P) f \<le> f0"
   1.136 +  then show "Inf (f ` (Collect P)) \<le> f0"
   1.137      by (rule tendsto_le[OF ntriv lim tendsto_const])
   1.138  next
   1.139 -  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y"
   1.140 +  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y"
   1.141    show "f0 \<le> y"
   1.142    proof cases
   1.143      assume "\<exists>z. y < z \<and> z < f0"
   1.144      then obtain z where "y < z \<and> z < f0" ..
   1.145 -    moreover have "z \<le> INFIMUM {x. z < f x} f"
   1.146 +    moreover have "z \<le> Inf (f ` {x. z < f x})"
   1.147        by (rule INF_greatest) simp
   1.148      ultimately show ?thesis
   1.149        using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
   1.150 @@ -308,9 +308,9 @@
   1.151          using lim[THEN topological_tendstoD, of "{y <..}"] by auto
   1.152        then have "eventually (\<lambda>x. f0 \<le> f x) F"
   1.153          using discrete by (auto elim!: eventually_mono)
   1.154 -      then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
   1.155 +      then have "Inf (f ` {x. f0 \<le> f x}) \<le> y"
   1.156          by (rule upper)
   1.157 -      moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
   1.158 +      moreover have "f0 \<le> Inf (f ` {x. f0 \<le> f x})"
   1.159          by (intro INF_greatest) simp
   1.160        ultimately show "f0 \<le> y" by simp
   1.161      qed
   1.162 @@ -324,17 +324,17 @@
   1.163    shows "Limsup F f = f0"
   1.164  proof (intro Limsup_eqI)
   1.165    fix P assume P: "eventually P F"
   1.166 -  then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F"
   1.167 +  then have "eventually (\<lambda>x. f x \<le> Sup (f ` (Collect P))) F"
   1.168      by eventually_elim (auto intro!: SUP_upper)
   1.169 -  then show "f0 \<le> SUPREMUM (Collect P) f"
   1.170 +  then show "f0 \<le> Sup (f ` (Collect P))"
   1.171      by (rule tendsto_le[OF ntriv tendsto_const lim])
   1.172  next
   1.173 -  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f"
   1.174 +  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))"
   1.175    show "y \<le> f0"
   1.176    proof (cases "\<exists>z. f0 < z \<and> z < y")
   1.177      case True
   1.178      then obtain z where "f0 < z \<and> z < y" ..
   1.179 -    moreover have "SUPREMUM {x. f x < z} f \<le> z"
   1.180 +    moreover have "Sup (f ` {x. f x < z}) \<le> z"
   1.181        by (rule SUP_least) simp
   1.182      ultimately show ?thesis
   1.183        using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
   1.184 @@ -347,9 +347,9 @@
   1.185          using lim[THEN topological_tendstoD, of "{..< y}"] by auto
   1.186        then have "eventually (\<lambda>x. f x \<le> f0) F"
   1.187          using False by (auto elim!: eventually_mono simp: not_less)
   1.188 -      then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
   1.189 +      then have "y \<le> Sup (f ` {x. f x \<le> f0})"
   1.190          by (rule lower)
   1.191 -      moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
   1.192 +      moreover have "Sup (f ` {x. f x \<le> f0}) \<le> f0"
   1.193          by (intro SUP_least) simp
   1.194        ultimately show "y \<le> f0" by simp
   1.195      qed
   1.196 @@ -364,14 +364,14 @@
   1.197  proof (rule order_tendstoI)
   1.198    fix a assume "f0 < a"
   1.199    with assms have "Limsup F f < a" by simp
   1.200 -  then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
   1.201 +  then obtain P where "eventually P F" "Sup (f ` (Collect P)) < a"
   1.202      unfolding Limsup_def INF_less_iff by auto
   1.203    then show "eventually (\<lambda>x. f x < a) F"
   1.204      by (auto elim!: eventually_mono dest: SUP_lessD)
   1.205  next
   1.206    fix a assume "a < f0"
   1.207    with assms have "a < Liminf F f" by simp
   1.208 -  then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
   1.209 +  then obtain P where "eventually P F" "a < Inf (f ` (Collect P))"
   1.210      unfolding Liminf_def less_SUP_iff by auto
   1.211    then show "eventually (\<lambda>x. a < f x) F"
   1.212      by (auto elim!: eventually_mono dest: less_INF_D)
   1.213 @@ -435,7 +435,7 @@
   1.214      unfolding Liminf_def
   1.215      by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
   1.216         (auto intro: eventually_True)
   1.217 -  also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
   1.218 +  also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
   1.219      by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
   1.220         (auto dest!: eventually_happens simp: F)
   1.221    finally show ?thesis by (auto simp: Liminf_def)
   1.222 @@ -460,7 +460,7 @@
   1.223      unfolding Limsup_def
   1.224      by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
   1.225         (auto intro: eventually_True)
   1.226 -  also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
   1.227 +  also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
   1.228      by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
   1.229         (auto dest!: eventually_happens simp: F)
   1.230    finally show ?thesis by (auto simp: Limsup_def)
   1.231 @@ -484,7 +484,7 @@
   1.232      unfolding Limsup_def
   1.233      by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   1.234         (auto intro: eventually_True)
   1.235 -  also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
   1.236 +  also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
   1.237      by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   1.238         (auto dest!: eventually_happens simp: F)
   1.239    finally show ?thesis
   1.240 @@ -510,7 +510,7 @@
   1.241      unfolding Liminf_def
   1.242      by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   1.243         (auto intro: eventually_True)
   1.244 -  also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
   1.245 +  also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
   1.246      by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   1.247         (auto dest!: eventually_happens simp: F)
   1.248    finally show ?thesis