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