src/HOL/Library/Liminf_Limsup.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63895 9afa979137da
child 66447 a1f5c5c26fa6
permissions -rw-r--r--
tuned proofs;
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
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
     3
    Author:     Manuel Eberl, TU München
51340
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
62624
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
     6
section \<open>Liminf and Limsup on conditionally complete lattices\<close>
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
     7
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
     8
theory Liminf_Limsup
51542
738598beeb26 tuned imports;
wenzelm
parents: 51340
diff changeset
     9
imports Complex_Main
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    10
begin
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    11
62624
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    12
lemma (in conditionally_complete_linorder) le_cSup_iff:
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    13
  assumes "A \<noteq> {}" "bdd_above A"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    14
  shows "x \<le> Sup A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    15
proof safe
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    16
  fix y assume "x \<le> Sup A" "y < x"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    17
  then have "y < Sup A" by auto
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    18
  then show "\<exists>a\<in>A. y < a"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    19
    unfolding less_cSup_iff[OF assms] .
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    20
qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms)
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    21
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    22
lemma (in conditionally_complete_linorder) le_cSUP_iff:
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    23
  "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    24
  using le_cSup_iff [of "f ` A"] by simp
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    25
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    26
lemma le_cSup_iff_less:
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    27
  fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    28
  shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    29
  by (simp add: le_cSUP_iff)
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    30
     (blast intro: less_imp_le less_trans less_le_trans dest: dense)
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    31
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    32
lemma le_Sup_iff_less:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51542
diff changeset
    33
  fixes x :: "'a :: {complete_linorder, dense_linorder}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    34
  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
    35
  unfolding le_SUP_iff
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    36
  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
    37
62624
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    38
lemma (in conditionally_complete_linorder) cInf_le_iff:
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    39
  assumes "A \<noteq> {}" "bdd_below A"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    40
  shows "Inf A \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>a\<in>A. y > a)"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    41
proof safe
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    42
  fix y assume "x \<ge> Inf A" "y > x"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    43
  then have "y > Inf A" by auto
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    44
  then show "\<exists>a\<in>A. y > a"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    45
    unfolding cInf_less_iff[OF assms] .
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    46
qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms)
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    47
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    48
lemma (in conditionally_complete_linorder) cINF_le_iff:
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    49
  "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    50
  using cInf_le_iff [of "f ` A"] by simp
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    51
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    52
lemma cInf_le_iff_less:
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    53
  fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    54
  shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    55
  by (simp add: cINF_le_iff)
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    56
     (blast intro: less_imp_le less_trans le_less_trans dest: dense)
59ceeb6f3079 generalized some Borel measurable statements to support ennreal
hoelzl
parents: 62343
diff changeset
    57
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    58
lemma Inf_le_iff_less:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51542
diff changeset
    59
  fixes x :: "'a :: {complete_linorder, dense_linorder}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    60
  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
    61
  unfolding INF_le_iff
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    62
  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
    63
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
    64
lemma SUP_pair:
54257
5c7a3b6b05a9 generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents: 53381
diff changeset
    65
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
5c7a3b6b05a9 generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents: 53381
diff changeset
    66
  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
    67
  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
    68
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
    69
lemma INF_pair:
54257
5c7a3b6b05a9 generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents: 53381
diff changeset
    70
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
5c7a3b6b05a9 generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents: 53381
diff changeset
    71
  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
    72
  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
    73
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61245
diff changeset
    74
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
    75
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    76
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
    77
  "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
    78
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    79
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
    80
  "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
    81
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    82
abbreviation "liminf \<equiv> Liminf sequentially"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    83
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    84
abbreviation "limsup \<equiv> Limsup sequentially"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    85
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    86
lemma Liminf_eqI:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
    87
  "(\<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
    88
    (\<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
    89
  unfolding Liminf_def by (auto intro!: SUP_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    90
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    91
lemma Limsup_eqI:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
    92
  "(\<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
    93
    (\<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
    94
  unfolding Limsup_def by (auto intro!: INF_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    95
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
    96
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
    97
  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
    98
  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
    99
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
   100
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
   101
  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
   102
  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
   103
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   104
lemma Limsup_const:
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   105
  assumes ntriv: "\<not> trivial_limit F"
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
   106
  shows "Limsup F (\<lambda>x. c) = c"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   107
proof -
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   108
  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
   109
  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
   110
    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
   111
  then show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   112
    unfolding Limsup_def using eventually_True
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   113
    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
   114
       (auto intro!: INF_const simp del: eventually_True)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   115
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   116
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   117
lemma Liminf_const:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   118
  assumes ntriv: "\<not> trivial_limit F"
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
   119
  shows "Liminf F (\<lambda>x. c) = c"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   120
proof -
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   121
  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
   122
  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
   123
    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
   124
  then show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   125
    unfolding Liminf_def using eventually_True
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   126
    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
   127
       (auto intro!: SUP_const simp del: eventually_True)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   128
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   129
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   130
lemma Liminf_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   131
  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
   132
  shows "Liminf F f \<le> Liminf F g"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   133
  unfolding Liminf_def
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   134
proof (safe intro!: SUP_mono)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   135
  fix P assume "eventually P F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   136
  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
   137
  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
   138
    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
   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_eq:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   142
  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
   143
  shows "Liminf F f = Liminf F g"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   144
  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
   145
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   146
lemma Limsup_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   147
  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
   148
  shows "Limsup F f \<le> Limsup F g"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   149
  unfolding Limsup_def
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   150
proof (safe intro!: INF_mono)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   151
  fix P assume "eventually P F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   152
  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
   153
  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
   154
    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
   155
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   156
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   157
lemma Limsup_eq:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   158
  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
   159
  shows "Limsup net f = Limsup net g"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   160
  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
   161
63895
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   162
lemma Liminf_bot[simp]: "Liminf bot f = top"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   163
  unfolding Liminf_def top_unique[symmetric]
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   164
  by (rule SUP_upper2[where i="\<lambda>x. False"]) simp_all
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   165
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   166
lemma Limsup_bot[simp]: "Limsup bot f = bot"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   167
  unfolding Limsup_def bot_unique[symmetric]
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   168
  by (rule INF_lower2[where i="\<lambda>x. False"]) simp_all
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   169
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   170
lemma Liminf_le_Limsup:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   171
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   172
  shows "Liminf F f \<le> Limsup F f"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   173
  unfolding Limsup_def Liminf_def
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
   174
  apply (rule SUP_least)
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
   175
  apply (rule INF_greatest)
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   176
proof safe
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   177
  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
   178
  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
   179
  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
   180
    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
   181
  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
   182
    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
   183
  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
   184
    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
   185
  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
   186
    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
   187
  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
   188
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   189
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   190
lemma Liminf_bounded:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   191
  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
   192
  shows "C \<le> Liminf F X"
63895
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   193
  using Liminf_mono[OF le] Liminf_const[of F C]
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   194
  by (cases "F = bot") simp_all
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   195
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   196
lemma Limsup_bounded:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   197
  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
   198
  shows "Limsup F X \<le> C"
63895
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   199
  using Limsup_mono[OF le] Limsup_const[of F C]
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   200
  by (cases "F = bot") simp_all
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   201
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   202
lemma le_Limsup:
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   203
  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
   204
  shows "l \<le> Limsup F f"
63895
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   205
  using F Liminf_bounded Liminf_le_Limsup order.trans x by blast
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   206
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   207
lemma Liminf_le:
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   208
  assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   209
  shows "Liminf F f \<le> l"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   210
  using F Liminf_le_Limsup Limsup_bounded order.trans x by blast
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   211
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   212
lemma le_Liminf_iff:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   213
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   214
  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
   215
proof -
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   216
  have "eventually (\<lambda>x. y < X x) F"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   217
    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
   218
    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
   219
  moreover
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   220
  have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   221
    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
   222
  proof (cases "\<exists>z. y < z \<and> z < C")
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   223
    case True
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   224
    then obtain z where z: "y < z \<and> z < C" ..
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   225
    moreover from z have "z \<le> INFIMUM {x. z < X x} X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   226
      by (auto intro!: INF_greatest)
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   227
    ultimately show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   228
      using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   229
  next
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   230
    case False
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   231
    then have "C \<le> INFIMUM {x. y < X x} X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   232
      by (intro INF_greatest) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   233
    with \<open>y < C\<close> show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   234
      using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   235
  qed
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   236
  ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   237
    unfolding Liminf_def le_SUP_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   238
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   239
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   240
lemma Limsup_le_iff:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   241
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   242
  shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   243
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   244
  { fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   245
    then have "eventually (\<lambda>x. y > X x) F"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   246
      by (auto elim!: eventually_mono dest: SUP_lessD) }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   247
  moreover
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   248
  { fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   249
    have "\<exists>P. eventually P F \<and> y > SUPREMUM (Collect P) X"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   250
    proof (cases "\<exists>z. C < z \<and> z < y")
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   251
      case True
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   252
      then obtain z where z: "C < z \<and> z < y" ..
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   253
      moreover from z have "z \<ge> SUPREMUM {x. z > X x} X"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   254
        by (auto intro!: SUP_least)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   255
      ultimately show ?thesis
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   256
        using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   257
    next
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   258
      case False
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   259
      then have "C \<ge> SUPREMUM {x. y > X x} X"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   260
        by (intro SUP_least) (auto simp: not_less)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   261
      with \<open>y > C\<close> show ?thesis
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   262
        using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   263
    qed }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   264
  ultimately show ?thesis
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   265
    unfolding Limsup_def INF_le_iff by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   266
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   267
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   268
lemma less_LiminfD:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   269
  "y < Liminf F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x > y) F"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   270
  using le_Liminf_iff[of "Liminf F f" F f] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   271
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   272
lemma Limsup_lessD:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   273
  "y > Limsup F (f :: _ \<Rightarrow> 'a :: complete_linorder) \<Longrightarrow> eventually (\<lambda>x. f x < y) F"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   274
  using Limsup_le_iff[of F f "Limsup F f"] by simp
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   275
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   276
lemma lim_imp_Liminf:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   277
  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
   278
  assumes ntriv: "\<not> trivial_limit F"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   279
  assumes lim: "(f \<longlongrightarrow> f0) F"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   280
  shows "Liminf F f = f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   281
proof (intro Liminf_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   282
  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
   283
  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
   284
    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
   285
  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
   286
    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
   287
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
   288
  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
   289
  show "f0 \<le> y"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   290
  proof cases
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   291
    assume "\<exists>z. y < z \<and> z < f0"
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   292
    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
   293
    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
   294
      by (rule INF_greatest) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   295
    ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   296
      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
   297
  next
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   298
    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
   299
    show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   300
    proof (rule classical)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   301
      assume "\<not> f0 \<le> y"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   302
      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
   303
        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
   304
      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
   305
        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
   306
      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
   307
        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
   308
      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
   309
        by (intro INF_greatest) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   310
      ultimately show "f0 \<le> y" by simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   311
    qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   312
  qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   313
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   314
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   315
lemma lim_imp_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   316
  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
   317
  assumes ntriv: "\<not> trivial_limit F"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   318
  assumes lim: "(f \<longlongrightarrow> f0) F"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   319
  shows "Limsup F f = f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   320
proof (intro Limsup_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   321
  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
   322
  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
   323
    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
   324
  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
   325
    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
   326
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
   327
  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
   328
  show "y \<le> f0"
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   329
  proof (cases "\<exists>z. f0 < z \<and> z < y")
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   330
    case True
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   331
    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
   332
    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
   333
      by (rule SUP_least) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   334
    ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   335
      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
   336
  next
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   337
    case False
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   338
    show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   339
    proof (rule classical)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   340
      assume "\<not> y \<le> f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   341
      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
   342
        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
   343
      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
   344
        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
   345
      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
   346
        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
   347
      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
   348
        by (intro SUP_least) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   349
      ultimately show "y \<le> f0" by simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   350
    qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   351
  qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   352
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   353
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   354
lemma Liminf_eq_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   355
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   356
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   357
    and lim: "Liminf F f = f0" "Limsup F f = f0"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   358
  shows "(f \<longlongrightarrow> f0) F"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   359
proof (rule order_tendstoI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   360
  fix a assume "f0 < a"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   361
  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
   362
  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
   363
    unfolding Limsup_def INF_less_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   364
  then show "eventually (\<lambda>x. f x < a) F"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   365
    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
   366
next
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   367
  fix a assume "a < f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   368
  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
   369
  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
   370
    unfolding Liminf_def less_SUP_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   371
  then show "eventually (\<lambda>x. a < f x) F"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   372
    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
   373
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   374
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   375
lemma tendsto_iff_Liminf_eq_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   376
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   377
  shows "\<not> trivial_limit F \<Longrightarrow> (f \<longlongrightarrow> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   378
  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
   379
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   380
lemma liminf_subseq_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   381
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   382
  assumes "subseq r"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   383
  shows "liminf X \<le> liminf (X \<circ> r) "
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   384
proof-
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   385
  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
   386
  proof (safe intro!: INF_mono)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   387
    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
   388
      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
   389
  qed
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
   390
  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
   391
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   392
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   393
lemma limsup_subseq_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   394
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   395
  assumes "subseq r"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   396
  shows "limsup (X \<circ> r) \<le> limsup X"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   397
proof-
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   398
  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
   399
  proof (safe intro!: SUP_mono)
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   400
    fix m :: nat
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   401
    assume "n \<le> m"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   402
    then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   403
      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
   404
  qed
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   405
  then show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   406
    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
   407
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   408
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   409
lemma continuous_on_imp_continuous_within:
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   410
  "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
   411
  unfolding continuous_on_eq_continuous_within
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   412
  by (auto simp: continuous_within intro: tendsto_within_subset)
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   413
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   414
lemma Liminf_compose_continuous_mono:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   415
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   416
  assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   417
  shows "Liminf F (\<lambda>n. f (g n)) = f (Liminf F g)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   418
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   419
  { fix P assume "eventually P F"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   420
    have "\<exists>x. P x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   421
    proof (rule ccontr)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   422
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   423
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   424
      with \<open>eventually P F\<close> F show False
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   425
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   426
    qed }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   427
  note * = this
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   428
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   429
  have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62049
diff changeset
   430
    unfolding Liminf_def
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   431
    by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   432
       (auto intro: eventually_True)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   433
  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   434
    by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   435
       (auto dest!: eventually_happens simp: F)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   436
  finally show ?thesis by (auto simp: Liminf_def)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   437
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   438
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   439
lemma Limsup_compose_continuous_mono:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   440
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   441
  assumes c: "continuous_on UNIV f" and am: "mono f" and F: "F \<noteq> bot"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   442
  shows "Limsup F (\<lambda>n. f (g n)) = f (Limsup F g)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   443
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   444
  { fix P assume "eventually P F"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   445
    have "\<exists>x. P x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   446
    proof (rule ccontr)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   447
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   448
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   449
      with \<open>eventually P F\<close> F show False
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   450
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   451
    qed }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   452
  note * = this
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   453
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   454
  have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62049
diff changeset
   455
    unfolding Limsup_def
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   456
    by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   457
       (auto intro: eventually_True)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   458
  also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   459
    by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   460
       (auto dest!: eventually_happens simp: F)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   461
  finally show ?thesis by (auto simp: Limsup_def)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   462
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   463
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   464
lemma Liminf_compose_continuous_antimono:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   465
  fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   466
  assumes c: "continuous_on UNIV f"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   467
    and am: "antimono f"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   468
    and F: "F \<noteq> bot"
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   469
  shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   470
proof -
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   471
  have *: "\<exists>x. P x" if "eventually P F" for P
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   472
  proof (rule ccontr)
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   473
    assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   474
      by auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   475
    with \<open>eventually P F\<close> F show False
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   476
      by auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   477
  qed
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   478
  have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62049
diff changeset
   479
    unfolding Limsup_def
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   480
    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
   481
       (auto intro: eventually_True)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   482
  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   483
    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
   484
       (auto dest!: eventually_happens simp: F)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   485
  finally show ?thesis
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   486
    by (auto simp: Liminf_def)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   487
qed
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   488
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   489
lemma Limsup_compose_continuous_antimono:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   490
  fixes f :: "'a::{complete_linorder, linorder_topology} \<Rightarrow> 'b::{complete_linorder, linorder_topology}"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   491
  assumes c: "continuous_on UNIV f" and am: "antimono f" and F: "F \<noteq> bot"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   492
  shows "Limsup F (\<lambda>n. f (g n)) = f (Liminf F g)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   493
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   494
  { fix P assume "eventually P F"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   495
    have "\<exists>x. P x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   496
    proof (rule ccontr)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   497
      assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   498
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   499
      with \<open>eventually P F\<close> F show False
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   500
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   501
    qed }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   502
  note * = this
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   503
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   504
  have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
62343
24106dc44def prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents: 62049
diff changeset
   505
    unfolding Liminf_def
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   506
    by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   507
       (auto intro: eventually_True)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   508
  also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   509
    by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   510
       (auto dest!: eventually_happens simp: F)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   511
  finally show ?thesis
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   512
    by (auto simp: Limsup_def)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   513
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   514
63895
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   515
lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   516
  apply (cases "F = bot", simp)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   517
  by (subst Liminf_def)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   518
    (auto simp add: INF_lower Liminf_bounded eventually_filtermap eventually_mono intro!: SUP_least)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   519
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   520
lemma Limsup_filtermap_ge: "Limsup (filtermap f F) g \<ge> Limsup F (\<lambda>x. g (f x))"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   521
  apply (cases "F = bot", simp)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   522
  by (subst Limsup_def)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   523
    (auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   524
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   525
lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x:Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   526
  by (auto intro!: SUP_least simp: Liminf_def)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   527
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   528
lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x:Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   529
  by (auto intro!: INF_greatest simp: Limsup_def)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   530
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   531
lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   532
  apply (cases "F = bot", simp)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   533
  apply (rule Liminf_least)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   534
  subgoal for P
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   535
    by (auto simp: eventually_filtermap the_inv_f_f
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   536
        intro!: Liminf_bounded INF_lower2 eventually_mono[of P])
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   537
  done
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   538
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   539
lemma Limsup_filtermap_le: "inj f \<Longrightarrow> Limsup (filtermap f F) g \<le> Limsup F (\<lambda>x. g (f x))"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   540
  apply (cases "F = bot", simp)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   541
  apply (rule Limsup_greatest)
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   542
  subgoal for P
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   543
    by (auto simp: eventually_filtermap the_inv_f_f
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   544
        intro!: Limsup_bounded SUP_upper2 eventually_mono[of P])
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   545
  done
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   546
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   547
lemma Liminf_filtermap_eq: "inj f \<Longrightarrow> Liminf (filtermap f F) g = Liminf F (\<lambda>x. g (f x))"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   548
  using Liminf_filtermap_le[of f F g] Liminf_filtermap_ge[of f F g]
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   549
  by simp
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   550
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   551
lemma Limsup_filtermap_eq: "inj f \<Longrightarrow> Limsup (filtermap f F) g = Limsup F (\<lambda>x. g (f x))"
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   552
  using Limsup_filtermap_le[of f F g] Limsup_filtermap_ge[of F g f]
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   553
  by simp
9afa979137da Liminf/Limsup and filtermap
immler
parents: 62975
diff changeset
   554
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   555
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   556
subsection \<open>More Limits\<close>
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   557
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   558
lemma convergent_limsup_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   559
  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
   560
  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
   561
  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
   562
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   563
lemma convergent_liminf_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   564
  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
   565
  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
   566
  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
   567
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   568
lemma lim_increasing_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   569
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   570
  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
   571
proof
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   572
  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
   573
    using assms
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   574
    by (intro increasing_tendsto)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   575
       (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
   576
qed
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   577
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   578
lemma lim_decreasing_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   579
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   580
  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
   581
proof
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   582
  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
   583
    using assms
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   584
    by (intro decreasing_tendsto)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   585
       (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
   586
qed
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   587
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   588
lemma compact_complete_linorder:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   589
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   590
  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
   591
proof -
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   592
  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
   593
    using seq_monosub[of X]
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   594
    unfolding comp_def
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   595
    by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   596
  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
   597
    by (auto simp add: monoseq_def)
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   598
  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
   599
     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
   600
     by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   601
  then show ?thesis
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   602
    using \<open>subseq r\<close> by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   603
qed
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   604
62975
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   605
lemma tendsto_Limsup:
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   606
  fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   607
  shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Limsup F f) F"
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   608
  by (subst tendsto_iff_Liminf_eq_Limsup) auto
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   609
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   610
lemma tendsto_Liminf:
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   611
  fixes f :: "_ \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   612
  shows "F \<noteq> bot \<Longrightarrow> Limsup F f = Liminf F f \<Longrightarrow> (f \<longlongrightarrow> Liminf F f) F"
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   613
  by (subst tendsto_iff_Liminf_eq_Limsup) auto
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents: 62624
diff changeset
   614
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   615
end