src/HOL/Library/Liminf_Limsup.thy
author eberlm
Mon, 04 Jan 2016 17:45:36 +0100
changeset 62049 b0f941e207cf
parent 61973 0c7e865fa7cb
child 62343 24106dc44def
permissions -rw-r--r--
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     6
section \<open>Liminf and Limsup on complete lattices\<close>
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
     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
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    12
lemma le_Sup_iff_less:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51542
diff changeset
    13
  fixes x :: "'a :: {complete_linorder, dense_linorder}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    14
  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
    15
  unfolding le_SUP_iff
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    16
  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
    17
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    18
lemma Inf_le_iff_less:
53216
ad2e09c30aa8 renamed inner_dense_linorder to dense_linorder
hoelzl
parents: 51542
diff changeset
    19
  fixes x :: "'a :: {complete_linorder, dense_linorder}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    20
  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
    21
  unfolding INF_le_iff
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    22
  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
    23
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
    24
lemma SUP_pair:
54257
5c7a3b6b05a9 generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents: 53381
diff changeset
    25
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
5c7a3b6b05a9 generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents: 53381
diff changeset
    26
  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
    27
  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
    28
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
    29
lemma INF_pair:
54257
5c7a3b6b05a9 generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents: 53381
diff changeset
    30
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
5c7a3b6b05a9 generalize SUP and INF to the syntactic type classes Sup and Inf
hoelzl
parents: 53381
diff changeset
    31
  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
    32
  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
    33
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61245
diff changeset
    34
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
    35
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    36
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
    37
  "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
    38
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    39
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
    40
  "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
    41
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    42
abbreviation "liminf \<equiv> Liminf sequentially"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    43
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    44
abbreviation "limsup \<equiv> Limsup sequentially"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    45
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    46
lemma Liminf_eqI:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
    47
  "(\<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
    48
    (\<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
    49
  unfolding Liminf_def by (auto intro!: SUP_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    50
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    51
lemma Limsup_eqI:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
    52
  "(\<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
    53
    (\<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
    54
  unfolding Limsup_def by (auto intro!: INF_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    55
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
    56
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
    57
  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
    58
  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
    59
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
    60
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
    61
  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
    62
  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
    63
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
    64
lemma Limsup_const:
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    65
  assumes ntriv: "\<not> trivial_limit F"
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    66
  shows "Limsup F (\<lambda>x. c) = c"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    67
proof -
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    68
  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
    69
  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
    70
    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
    71
  then show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    72
    unfolding Limsup_def using eventually_True
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    73
    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
    74
       (auto intro!: INF_const simp del: eventually_True)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    75
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    76
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    77
lemma Liminf_const:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    78
  assumes ntriv: "\<not> trivial_limit F"
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
    79
  shows "Liminf F (\<lambda>x. c) = c"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    80
proof -
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    81
  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
    82
  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
    83
    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
    84
  then show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    85
    unfolding Liminf_def using eventually_True
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    86
    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
    87
       (auto intro!: SUP_const simp del: eventually_True)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    88
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    89
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    90
lemma Liminf_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    91
  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
    92
  shows "Liminf F f \<le> Liminf F g"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    93
  unfolding Liminf_def
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    94
proof (safe intro!: SUP_mono)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    95
  fix P assume "eventually P F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
    96
  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
    97
  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
    98
    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
    99
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   100
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   101
lemma Liminf_eq:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   102
  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
   103
  shows "Liminf F f = Liminf F g"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   104
  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
   105
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   106
lemma Limsup_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   107
  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
   108
  shows "Limsup F f \<le> Limsup F g"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   109
  unfolding Limsup_def
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   110
proof (safe intro!: INF_mono)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   111
  fix P assume "eventually P F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   112
  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
   113
  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
   114
    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
   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 Limsup_eq:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   118
  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
   119
  shows "Limsup net f = Limsup net g"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   120
  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
   121
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   122
lemma Liminf_le_Limsup:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   123
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   124
  shows "Liminf F f \<le> Limsup F f"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   125
  unfolding Limsup_def Liminf_def
54261
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
   126
  apply (rule SUP_least)
89991ef58448 restrict Limsup and Liminf to complete lattices
hoelzl
parents: 54257
diff changeset
   127
  apply (rule INF_greatest)
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   128
proof safe
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   129
  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
   130
  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
   131
  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
   132
    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
   133
  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
   134
    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
   135
  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
   136
    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
   137
  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
   138
    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
   139
  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
   140
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   141
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   142
lemma Liminf_bounded:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   143
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   144
  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
   145
  shows "C \<le> Liminf F X"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   146
  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   147
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   148
lemma Limsup_bounded:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   149
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   150
  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
   151
  shows "Limsup F X \<le> C"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   152
  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   153
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   154
lemma le_Limsup:
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   155
  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
   156
  shows "l \<le> Limsup F f"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   157
proof -
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   158
  have "l = Limsup F (\<lambda>x. l)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   159
    using F by (simp add: Limsup_const)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   160
  also have "\<dots> \<le> Limsup F f"
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   161
    by (intro Limsup_mono x)
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   162
  finally show ?thesis .
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   163
qed
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   164
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   165
lemma le_Liminf_iff:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   166
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   167
  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
   168
proof -
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   169
  have "eventually (\<lambda>x. y < X x) F"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   170
    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
   171
    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
   172
  moreover
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   173
  have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   174
    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
   175
  proof (cases "\<exists>z. y < z \<and> z < C")
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   176
    case True
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   177
    then obtain z where z: "y < z \<and> z < C" ..
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   178
    moreover from z have "z \<le> INFIMUM {x. z < X x} X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   179
      by (auto intro!: INF_greatest)
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   180
    ultimately show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   181
      using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   182
  next
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   183
    case False
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   184
    then have "C \<le> INFIMUM {x. y < X x} X"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   185
      by (intro INF_greatest) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   186
    with \<open>y < C\<close> show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   187
      using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   188
  qed
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   189
  ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   190
    unfolding Liminf_def le_SUP_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   191
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   192
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   193
lemma Limsup_le_iff:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   194
  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   195
  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
   196
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   197
  { 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
   198
    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
   199
      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
   200
  moreover
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   201
  { 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
   202
    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
   203
    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
   204
      case True
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   205
      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
   206
      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
   207
        by (auto intro!: SUP_least)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   208
      ultimately show ?thesis
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   209
        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
   210
    next
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   211
      case False
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   212
      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
   213
        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
   214
      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
   215
        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
   216
    qed }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   217
  ultimately show ?thesis
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   218
    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
   219
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   220
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   221
lemma less_LiminfD:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   222
  "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
   223
  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
   224
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   225
lemma Limsup_lessD:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   226
  "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
   227
  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
   228
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   229
lemma lim_imp_Liminf:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   230
  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
   231
  assumes ntriv: "\<not> trivial_limit F"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   232
  assumes lim: "(f \<longlongrightarrow> f0) F"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   233
  shows "Liminf F f = f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   234
proof (intro Liminf_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   235
  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
   236
  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
   237
    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
   238
  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
   239
    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
   240
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
   241
  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
   242
  show "f0 \<le> y"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   243
  proof cases
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   244
    assume "\<exists>z. y < z \<and> z < f0"
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 53216
diff changeset
   245
    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
   246
    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
   247
      by (rule INF_greatest) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   248
    ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   249
      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
   250
  next
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   251
    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
   252
    show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   253
    proof (rule classical)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   254
      assume "\<not> f0 \<le> y"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   255
      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
   256
        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
   257
      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
   258
        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
   259
      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
   260
        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
   261
      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
   262
        by (intro INF_greatest) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   263
      ultimately show "f0 \<le> y" by simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   264
    qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   265
  qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   266
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   267
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   268
lemma lim_imp_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   269
  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
   270
  assumes ntriv: "\<not> trivial_limit F"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   271
  assumes lim: "(f \<longlongrightarrow> f0) F"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   272
  shows "Limsup F f = f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   273
proof (intro Limsup_eqI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   274
  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
   275
  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
   276
    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
   277
  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
   278
    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
   279
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
   280
  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
   281
  show "y \<le> f0"
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   282
  proof (cases "\<exists>z. f0 < z \<and> z < y")
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   283
    case True
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   284
    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
   285
    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
   286
      by (rule SUP_least) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   287
    ultimately show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   288
      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
   289
  next
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   290
    case False
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   291
    show ?thesis
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   292
    proof (rule classical)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   293
      assume "\<not> y \<le> f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   294
      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
   295
        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
   296
      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
   297
        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
   298
      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
   299
        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
   300
      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
   301
        by (intro SUP_least) simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   302
      ultimately show "y \<le> f0" by simp
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   303
    qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   304
  qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   305
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   306
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   307
lemma Liminf_eq_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   308
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   309
  assumes ntriv: "\<not> trivial_limit F"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   310
    and lim: "Liminf F f = f0" "Limsup F f = f0"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   311
  shows "(f \<longlongrightarrow> f0) F"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   312
proof (rule order_tendstoI)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   313
  fix a assume "f0 < a"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   314
  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
   315
  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
   316
    unfolding Limsup_def INF_less_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   317
  then show "eventually (\<lambda>x. f x < a) F"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   318
    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
   319
next
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   320
  fix a assume "a < f0"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   321
  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
   322
  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
   323
    unfolding Liminf_def less_SUP_iff by auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   324
  then show "eventually (\<lambda>x. a < f x) F"
61810
3c5040d5694a sorted out eventually_mono
paulson <lp15@cam.ac.uk>
parents: 61806
diff changeset
   325
    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
   326
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   327
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   328
lemma tendsto_iff_Liminf_eq_Limsup:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   329
  fixes f0 :: "'a :: {complete_linorder,linorder_topology}"
61973
0c7e865fa7cb more symbols;
wenzelm
parents: 61969
diff changeset
   330
  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
   331
  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
   332
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   333
lemma liminf_subseq_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   334
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   335
  assumes "subseq r"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   336
  shows "liminf X \<le> liminf (X \<circ> r) "
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   337
proof-
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   338
  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
   339
  proof (safe intro!: INF_mono)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   340
    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
   341
      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
   342
  qed
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 54261
diff changeset
   343
  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
   344
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   345
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   346
lemma limsup_subseq_mono:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   347
  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   348
  assumes "subseq r"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   349
  shows "limsup (X \<circ> r) \<le> limsup X"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   350
proof-
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   351
  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
   352
  proof (safe intro!: SUP_mono)
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   353
    fix m :: nat
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   354
    assume "n \<le> m"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   355
    then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   356
      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
   357
  qed
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   358
  then show ?thesis
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   359
    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
   360
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   361
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   362
lemma continuous_on_imp_continuous_within:
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   363
  "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
   364
  unfolding continuous_on_eq_continuous_within
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   365
  by (auto simp: continuous_within intro: tendsto_within_subset)
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   366
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   367
lemma Liminf_compose_continuous_mono:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   368
  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
   369
  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
   370
  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
   371
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   372
  { 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
   373
    have "\<exists>x. P x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   374
    proof (rule ccontr)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   375
      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
   376
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   377
      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
   378
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   379
    qed }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   380
  note * = this
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   381
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   382
  have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   383
    unfolding Liminf_def SUP_def
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   384
    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
   385
       (auto intro: eventually_True)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   386
  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
   387
    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
   388
       (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
   389
  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
   390
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   391
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   392
lemma Limsup_compose_continuous_mono:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   393
  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
   394
  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
   395
  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
   396
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   397
  { 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
   398
    have "\<exists>x. P x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   399
    proof (rule ccontr)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   400
      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
   401
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   402
      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
   403
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   404
    qed }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   405
  note * = this
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   406
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   407
  have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   408
    unfolding Limsup_def INF_def
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   409
    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
   410
       (auto intro: eventually_True)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   411
  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
   412
    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
   413
       (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
   414
  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
   415
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   416
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   417
lemma Liminf_compose_continuous_antimono:
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   418
  fixes f :: "'a::{complete_linorder,linorder_topology} \<Rightarrow> 'b::{complete_linorder,linorder_topology}"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   419
  assumes c: "continuous_on UNIV f"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   420
    and am: "antimono f"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   421
    and F: "F \<noteq> bot"
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   422
  shows "Liminf F (\<lambda>n. f (g n)) = f (Limsup F g)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   423
proof -
61730
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   424
  have *: "\<exists>x. P x" if "eventually P F" for P
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   425
  proof (rule ccontr)
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   426
    assume "\<not> (\<exists>x. P x)" then have "P = (\<lambda>x. False)"
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   427
      by auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   428
    with \<open>eventually P F\<close> F show False
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   429
      by auto
2b775b888897 tuned proofs;
wenzelm
parents: 61585
diff changeset
   430
  qed
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   431
  have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   432
    unfolding Limsup_def INF_def
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   433
    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
   434
       (auto intro: eventually_True)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   435
  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   436
    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
   437
       (auto dest!: eventually_happens simp: F)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   438
  finally show ?thesis
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   439
    by (auto simp: Liminf_def)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   440
qed
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   441
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   442
lemma Limsup_compose_continuous_antimono:
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   443
  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
   444
  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
   445
  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
   446
proof -
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   447
  { 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
   448
    have "\<exists>x. P x"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   449
    proof (rule ccontr)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   450
      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
   451
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   452
      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
   453
        by auto
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   454
    qed }
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   455
  note * = this
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   456
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   457
  have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   458
    unfolding Liminf_def SUP_def
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   459
    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
   460
       (auto intro: eventually_True)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   461
  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
   462
    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
   463
       (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
   464
  finally show ?thesis
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   465
    by (auto simp: Limsup_def)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   466
qed
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   467
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents: 61973
diff changeset
   468
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   469
subsection \<open>More Limits\<close>
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   470
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   471
lemma convergent_limsup_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   472
  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
   473
  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
   474
  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
   475
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   476
lemma convergent_liminf_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   477
  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
   478
  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
   479
  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
   480
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   481
lemma lim_increasing_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   482
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   483
  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
   484
proof
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   485
  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
   486
    using assms
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   487
    by (intro increasing_tendsto)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   488
       (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
   489
qed
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   490
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   491
lemma lim_decreasing_cl:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   492
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   493
  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
   494
proof
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   495
  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
   496
    using assms
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   497
    by (intro decreasing_tendsto)
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   498
       (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
   499
qed
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   500
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   501
lemma compact_complete_linorder:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   502
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   503
  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
   504
proof -
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   505
  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
   506
    using seq_monosub[of X]
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   507
    unfolding comp_def
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   508
    by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   509
  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
   510
    by (auto simp add: monoseq_def)
61969
e01015e49041 more symbols;
wenzelm
parents: 61880
diff changeset
   511
  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
   512
     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
   513
     by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   514
  then show ?thesis
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   515
    using \<open>subseq r\<close> by auto
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61810
diff changeset
   516
qed
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 60500
diff changeset
   517
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents:
diff changeset
   518
end