src/HOL/Library/Liminf_Limsup.thy
author wenzelm
Tue, 29 Dec 2015 23:04:53 +0100
changeset 61969 e01015e49041
parent 61880 ff4d33058566
child 61973 0c7e865fa7cb
permissions -rw-r--r--
more symbols;
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
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61245
diff changeset
    33
subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<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:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
    46
  "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>
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
    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:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
    51
  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>
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
    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
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
    63
lemma Limsup_const:
51340
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"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   103
  by (intro antisym Liminf_mono eventually_mono[OF assms]) auto
51340
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"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   119
  by (intro antisym Limsup_mono eventually_mono[OF assms]) auto
51340
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
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   153
lemma le_Limsup:
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   154
  assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   155
  shows "l \<le> Limsup F f"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   156
proof -
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   157
  have "l = Limsup F (\<lambda>x. l)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   158
    using F by (simp add: Limsup_const)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   159
  also have "\<dots> \<le> Limsup F f"
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   160
    by (intro Limsup_mono x)
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   161
  finally show ?thesis .
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   162
qed
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   163
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   164
lemma le_Liminf_iff:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   165
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   166
  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
   167
proof -
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   168
  have "eventually (\<lambda>x. y < X x) F"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   169
    if "eventually P F" "y < INFIMUM (Collect P) X" for y P
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   170
    using that by (auto elim!: eventually_mono dest: less_INF_D)
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   171
  moreover
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   172
  have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   173
    if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   174
  proof (cases "\<exists>z. y < z \<and> z < C")
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   175
    case True
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   176
    then obtain z where z: "y < z \<and> z < C" ..
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   177
    moreover from z have "z \<le> INFIMUM {x. z < X x} X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   178
      by (auto intro!: INF_greatest)
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   179
    ultimately show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   180
      using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   181
  next
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   182
    case False
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   183
    then have "C \<le> INFIMUM {x. y < X x} X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   184
      by (intro INF_greatest) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   185
    with \<open>y < C\<close> show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   186
      using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   187
  qed
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   188
  ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   189
    unfolding Liminf_def le_SUP_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   190
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   191
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   192
lemma lim_imp_Liminf:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   193
  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   194
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   195
  assumes lim: "(f ---> f0) F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   196
  shows "Liminf F f = f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   197
proof (intro Liminf_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   198
  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
   199
  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
   200
    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
   201
  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
   202
    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
   203
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
   204
  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
   205
  show "f0 \<le> y"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   206
  proof cases
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   207
    assume "\<exists>z. y < z \<and> z < f0"
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   208
    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
   209
    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
   210
      by (rule INF_greatest) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   211
    ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   212
      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
   213
  next
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   214
    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
   215
    show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   216
    proof (rule classical)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   217
      assume "\<not> f0 \<le> y"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   218
      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
   219
        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
   220
      then have "eventually (\<lambda>x. f0 \<le> f x) F"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   221
        using discrete by (auto elim!: eventually_mono)
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
   222
      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
   223
        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
   224
      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
   225
        by (intro INF_greatest) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   226
      ultimately show "f0 \<le> y" by simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   227
    qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   228
  qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   229
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   230
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   231
lemma lim_imp_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   232
  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder,linorder_topology}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   233
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   234
  assumes lim: "(f ---> f0) F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   235
  shows "Limsup F f = f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   236
proof (intro Limsup_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   237
  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
   238
  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
   239
    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
   240
  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
   241
    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
   242
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
   243
  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
   244
  show "y \<le> f0"
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   245
  proof (cases "\<exists>z. f0 < z \<and> z < y")
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   246
    case True
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   247
    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
   248
    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
   249
      by (rule SUP_least) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   250
    ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   251
      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
   252
  next
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   253
    case False
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   254
    show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   255
    proof (rule classical)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   256
      assume "\<not> y \<le> f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   257
      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
   258
        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
   259
      then have "eventually (\<lambda>x. f x \<le> f0) F"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   260
        using False by (auto elim!: eventually_mono 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
   261
      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
   262
        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
   263
      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
   264
        by (intro SUP_least) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   265
      ultimately show "y \<le> f0" by simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   266
    qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   267
  qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   268
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   269
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   270
lemma Liminf_eq_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   271
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   272
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   273
    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
   274
  shows "(f ---> f0) F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   275
proof (rule order_tendstoI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   276
  fix a assume "f0 < a"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   277
  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
   278
  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
   279
    unfolding Limsup_def INF_less_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   280
  then show "eventually (\<lambda>x. f x < a) F"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   281
    by (auto elim!: eventually_mono dest: SUP_lessD)
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   282
next
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   283
  fix a assume "a < f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   284
  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
   285
  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
   286
    unfolding Liminf_def less_SUP_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   287
  then show "eventually (\<lambda>x. a < f x) F"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   288
    by (auto elim!: eventually_mono dest: less_INF_D)
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   289
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   290
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   291
lemma tendsto_iff_Liminf_eq_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   292
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   293
  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
   294
  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
   295
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   296
lemma liminf_subseq_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   297
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   298
  assumes "subseq r"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   299
  shows "liminf X \<le> liminf (X \<circ> r) "
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   300
proof-
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   301
  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
   302
  proof (safe intro!: INF_mono)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   303
    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
   304
      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
   305
  qed
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
   306
  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
   307
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   308
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   309
lemma limsup_subseq_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   310
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   311
  assumes "subseq r"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   312
  shows "limsup (X \<circ> r) \<le> limsup X"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   313
proof-
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   314
  have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   315
  proof (safe intro!: SUP_mono)
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   316
    fix m :: nat
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   317
    assume "n \<le> m"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   318
    then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   319
      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
   320
  qed
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   321
  then show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   322
    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
   323
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   324
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   325
lemma continuous_on_imp_continuous_within:
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   326
  "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> s \<Longrightarrow> continuous (at x within t) f"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   327
  unfolding continuous_on_eq_continuous_within
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   328
  by (auto simp: continuous_within intro: tendsto_within_subset)
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   329
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   330
lemma Liminf_compose_continuous_antimono:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   331
  fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   332
  assumes c: "continuous_on UNIV f"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   333
    and am: "antimono f"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   334
    and F: "F \<noteq> bot"
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   335
  shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   336
proof -
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   337
  have *: "\<exists>x. P x" if "eventually P F" for P
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   338
  proof (rule ccontr)
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   339
    assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   340
      by auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   341
    with \<open>eventually P F\<close> F show False
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   342
      by auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   343
  qed
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   344
  have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   345
    unfolding Limsup_def INF_def
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   346
    by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   347
       (auto intro: eventually_True)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   348
  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   349
    by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   350
       (auto dest!: eventually_happens simp: F)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   351
  finally show ?thesis
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   352
    by (auto simp: Liminf_def)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   353
qed
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   354
subsection \<open>More Limits\<close>
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   355
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   356
lemma convergent_limsup_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   357
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   358
  shows "convergent X \<Longrightarrow> limsup X = lim X"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   359
  by (auto simp: convergent_def limI lim_imp_Limsup)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   360
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   361
lemma convergent_liminf_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   362
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   363
  shows "convergent X \<Longrightarrow> liminf X = lim X"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   364
  by (auto simp: convergent_def limI lim_imp_Liminf)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   365
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   366
lemma lim_increasing_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   367
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   368
  obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   369
proof
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   370
  show "f \<longlonglongrightarrow> (SUP n. f n)"
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   371
    using assms
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   372
    by (intro increasing_tendsto)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   373
       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   374
qed
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   375
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   376
lemma lim_decreasing_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   377
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   378
  obtains l where "f \<longlonglongrightarrow> (l::'a::{complete_linorder,linorder_topology})"
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   379
proof
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   380
  show "f \<longlonglongrightarrow> (INF n. f n)"
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   381
    using assms
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   382
    by (intro decreasing_tendsto)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   383
       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   384
qed
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   385
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   386
lemma compact_complete_linorder:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   387
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   388
  shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   389
proof -
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   390
  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   391
    using seq_monosub[of X]
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   392
    unfolding comp_def
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   393
    by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   394
  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   395
    by (auto simp add: monoseq_def)
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   396
  then obtain l where "(X \<circ> r) \<longlonglongrightarrow> l"
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   397
     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   398
     by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   399
  then show ?thesis
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   400
    using \<open>subseq r\<close> by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   401
qed
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   402
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   403
end