src/HOL/Library/Liminf_Limsup.thy
author hoelzl
Tue, 05 Nov 2013 09:45:00 +0100
changeset 54261 89991ef58448
parent 54257 5c7a3b6b05a9
child 56212 3253aaf73a01
permissions -rw-r--r--
restrict Limsup and Liminf to complete lattices
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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
     5
header {* Liminf and Limsup on complete lattices *}
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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    23
lemma SUPR_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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    28
lemma INFI_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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    33
subsubsection {* @{text Liminf} and @{text Limsup} *}
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:
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    46
  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    47
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
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:
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    51
  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    52
    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
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
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    55
lemma liminf_SUPR_INFI: "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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    57
  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    58
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    59
lemma limsup_INFI_SUPR: "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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    61
  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
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)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    96
  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
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)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   112
  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
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)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   132
  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   133
    by (rule INF_mono) auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   134
  also have "\<dots> \<le> SUPR (Collect ?C) f"
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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   136
  also have "\<dots> \<le> SUPR (Collect Q) f"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   137
    by (rule SUP_mono) auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   138
  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
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 -
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   157
  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
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"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   162
    have "\<exists>P. eventually P F \<and> y < INFI (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" ..
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   166
      moreover from z have "z \<le> INFI {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
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   172
      then have "C \<le> INFI {x. y < X x} X"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   173
        by (intro INF_greatest) auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   174
      with `y < C` show ?thesis
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"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   188
  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   189
    by eventually_elim (auto intro!: INF_lower)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   190
  then show "INFI (Collect P) f \<le> f0"
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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   193
  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
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" ..
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   198
    moreover have "z \<le> INFI {x. z < f x} f"
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)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   211
      then have "INFI {x. f0 \<le> f x} f \<le> y"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   212
        by (rule upper)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   213
      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
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"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   227
  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   228
    by eventually_elim (auto intro!: SUP_upper)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   229
  then show "f0 \<le> SUPR (Collect P) f"
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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   232
  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
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" ..
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   237
    moreover have "SUPR {x. f x < z} f \<le> z"
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)
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   250
      then have "y \<le> SUPR {x. f x \<le> f0} f"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   251
        by (rule lower)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   252
      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   267
  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   274
  then obtain P where "eventually P F" "a < INFI (Collect P) f"
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"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   293
      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   294
  qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   295
  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
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"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   306
      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   307
  qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   308
  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
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