src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
author hoelzl
Tue, 05 Nov 2013 09:44:59 +0100
changeset 54260 6a967667fd45
parent 54258 adfc759263ab
child 55522 23d2cbac6dce
permissions -rw-r--r--
use INF and SUP on conditionally complete lattices in multivariate analysis
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41983
2dc6e382a58b standardized headers;
wenzelm
parents: 41981
diff changeset
     1
(*  Title:      HOL/Multivariate_Analysis/Extended_Real_Limits.thy
2dc6e382a58b standardized headers;
wenzelm
parents: 41981
diff changeset
     2
    Author:     Johannes Hölzl, TU München
2dc6e382a58b standardized headers;
wenzelm
parents: 41981
diff changeset
     3
    Author:     Robert Himmelmann, TU München
2dc6e382a58b standardized headers;
wenzelm
parents: 41981
diff changeset
     4
    Author:     Armin Heller, TU München
2dc6e382a58b standardized headers;
wenzelm
parents: 41981
diff changeset
     5
    Author:     Bogdan Grechuk, University of Edinburgh
2dc6e382a58b standardized headers;
wenzelm
parents: 41981
diff changeset
     6
*)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
     7
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
     8
header {* Limits on the Extended real number line *}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
     9
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    10
theory Extended_Real_Limits
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
    11
  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    12
begin
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    13
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    14
lemma convergent_limsup_cl:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    15
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    16
  shows "convergent X \<Longrightarrow> limsup X = lim X"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    17
  by (auto simp: convergent_def limI lim_imp_Limsup)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    18
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    19
lemma lim_increasing_cl:
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    20
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    21
  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    22
proof
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    23
  show "f ----> (SUP n. f n)"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    24
    using assms
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    25
    by (intro increasing_tendsto)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    26
       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    27
qed
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    28
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    29
lemma lim_decreasing_cl:
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    30
  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    31
  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    32
proof
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    33
  show "f ----> (INF n. f n)"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    34
    using assms
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    35
    by (intro decreasing_tendsto)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    36
       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    37
qed
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    38
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    39
lemma compact_complete_linorder:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    40
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    41
  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    42
proof -
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    43
  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    44
    using seq_monosub[of X]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    45
    unfolding comp_def
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    46
    by auto
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    47
  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)"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    48
    by (auto simp add: monoseq_def)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    49
  then obtain l where "(X \<circ> r) ----> l"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    50
     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    51
     by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    52
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    53
    using `subseq r` by auto
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    54
qed
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    55
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    56
lemma compact_UNIV:
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    57
  "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    58
  using compact_complete_linorder
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    59
  by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    60
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    61
lemma compact_eq_closed:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    62
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    63
  shows "compact S \<longleftrightarrow> closed S"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    64
  using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    65
  by auto
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    66
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    67
lemma closed_contains_Sup_cl:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    68
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    69
  assumes "closed S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    70
    and "S \<noteq> {}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    71
  shows "Sup S \<in> S"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    72
proof -
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    73
  from compact_eq_closed[of S] compact_attains_sup[of S] assms
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    74
  obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    75
    by auto
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 51641
diff changeset
    76
  then have "Sup S = s"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    77
    by (auto intro!: Sup_eqI)
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 51641
diff changeset
    78
  with S show ?thesis
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    79
    by simp
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    80
qed
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    81
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    82
lemma closed_contains_Inf_cl:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    83
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    84
  assumes "closed S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    85
    and "S \<noteq> {}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    86
  shows "Inf S \<in> S"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    87
proof -
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    88
  from compact_eq_closed[of S] compact_attains_inf[of S] assms
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    89
  obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    90
    by auto
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 51641
diff changeset
    91
  then have "Inf S = s"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    92
    by (auto intro!: Inf_eqI)
53374
a14d2a854c02 tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents: 51641
diff changeset
    93
  with S show ?thesis
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    94
    by simp
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    95
qed
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
    96
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    97
lemma ereal_dense3:
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    98
  fixes x y :: ereal
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
    99
  shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   100
proof (cases x y rule: ereal2_cases, simp_all)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   101
  fix r q :: real
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   102
  assume "r < q"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   103
  from Rats_dense_in_real[OF this] show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   104
    by (fastforce simp: Rats_def)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   105
next
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   106
  fix r :: real
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   107
  show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   108
    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   109
    by (auto simp: Rats_def)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   110
qed
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   111
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   112
instance ereal :: second_countable_topology
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   113
proof (default, intro exI conjI)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   114
  let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   115
  show "countable ?B"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   116
    by (auto intro: countable_rat)
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   117
  show "open = generate_topology ?B"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   118
  proof (intro ext iffI)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   119
    fix S :: "ereal set"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   120
    assume "open S"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   121
    then show "generate_topology ?B S"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   122
      unfolding open_generated_order
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   123
    proof induct
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   124
      case (Basis b)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   125
      then obtain e where "b = {..<e} \<or> b = {e<..}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   126
        by auto
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   127
      moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   128
        by (auto dest: ereal_dense3
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   129
                 simp del: ex_simps
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   130
                 simp add: ex_simps[symmetric] conj_commute Rats_def image_iff)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   131
      ultimately show ?case
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   132
        by (auto intro: generate_topology.intros)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   133
    qed (auto intro: generate_topology.intros)
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   134
  next
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   135
    fix S
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   136
    assume "generate_topology ?B S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   137
    then show "open S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   138
      by induct auto
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   139
  qed
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   140
qed
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   141
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   142
lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   143
  unfolding continuous_on_topological open_ereal_def
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   144
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   145
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   146
lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   147
  using continuous_on_eq_continuous_at[of UNIV]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   148
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   149
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   150
lemma continuous_within_ereal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   151
  using continuous_on_eq_continuous_within[of A]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   152
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   153
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   154
lemma ereal_open_uminus:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   155
  fixes S :: "ereal set"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   156
  assumes "open S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   157
  shows "open (uminus ` S)"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
   158
  using `open S`[unfolded open_generated_order]
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
   159
proof induct
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
   160
  have "range uminus = (UNIV :: ereal set)"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
   161
    by (auto simp: image_iff ereal_uminus_eq_reorder)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   162
  then show "open (range uminus :: ereal set)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   163
    by simp
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
   164
qed (auto simp add: image_Union image_Int)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   165
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   166
lemma ereal_uminus_complement:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   167
  fixes S :: "ereal set"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   168
  shows "uminus ` (- S) = - uminus ` S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   169
  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   170
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   171
lemma ereal_closed_uminus:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   172
  fixes S :: "ereal set"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   173
  assumes "closed S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   174
  shows "closed (uminus ` S)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   175
  using assms
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   176
  unfolding closed_def ereal_uminus_complement[symmetric]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   177
  by (rule ereal_open_uminus)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   178
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   179
lemma ereal_open_closed_aux:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   180
  fixes S :: "ereal set"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   181
  assumes "open S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   182
    and "closed S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   183
    and S: "(-\<infinity>) \<notin> S"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   184
  shows "S = {}"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   185
proof (rule ccontr)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   186
  assume "\<not> ?thesis"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   187
  then have *: "Inf S \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   188
    by (metis assms(2) closed_contains_Inf_cl)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   189
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   190
    assume "Inf S = -\<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   191
    then have False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   192
      using * assms(3) by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   193
  }
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   194
  moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   195
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   196
    assume "Inf S = \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   197
    then have "S = {\<infinity>}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   198
      by (metis Inf_eq_PInfty `S \<noteq> {}`)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   199
    then have False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   200
      by (metis assms(1) not_open_singleton)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   201
  }
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   202
  moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   203
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   204
    assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   205
    from ereal_open_cont_interval[OF assms(1) * fin]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   206
    obtain e where e: "e > 0" "{Inf S - e<..<Inf S + e} \<subseteq> S" .
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   207
    then obtain b where b: "Inf S - e < b" "b < Inf S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   208
      using fin ereal_between[of "Inf S" e] dense[of "Inf S - e"]
44918
6a80fbc4e72c tune simpset for Complete_Lattices
noschinl
parents: 44571
diff changeset
   209
      by auto
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   210
    then have "b: {Inf S - e <..< Inf S + e}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   211
      using e fin ereal_between[of "Inf S" e]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   212
      by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   213
    then have "b \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   214
      using e by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   215
    then have False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   216
      using b by (metis complete_lattice_class.Inf_lower leD)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   217
  }
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   218
  ultimately show False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   219
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   220
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   221
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   222
lemma ereal_open_closed:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   223
  fixes S :: "ereal set"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   224
  shows "open S \<and> closed S \<longleftrightarrow> S = {} \<or> S = UNIV"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   225
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   226
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   227
    assume lhs: "open S \<and> closed S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   228
    {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   229
      assume "-\<infinity> \<notin> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   230
      then have "S = {}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   231
        using lhs ereal_open_closed_aux by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   232
    }
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   233
    moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   234
    {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   235
      assume "-\<infinity> \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   236
      then have "- S = {}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   237
        using lhs ereal_open_closed_aux[of "-S"] by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   238
    }
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   239
    ultimately have "S = {} \<or> S = UNIV"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   240
      by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   241
  }
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   242
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   243
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   244
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   245
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   246
lemma ereal_open_affinity_pos:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   247
  fixes S :: "ereal set"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   248
  assumes "open S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   249
    and m: "m \<noteq> \<infinity>" "0 < m"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   250
    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   251
  shows "open ((\<lambda>x. m * x + t) ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   252
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   253
  obtain r where r[simp]: "m = ereal r"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   254
    using m by (cases m) auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   255
  obtain p where p[simp]: "t = ereal p"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   256
    using t by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   257
  have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   258
    using m by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   259
  from `open S` [THEN ereal_openE] guess l u . note T = this
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   260
  let ?f = "(\<lambda>x. m * x + t)"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   261
  show ?thesis
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   262
    unfolding open_ereal_def
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   263
  proof (intro conjI impI exI subsetI)
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   264
    have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   265
    proof safe
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   266
      fix x y
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   267
      assume "ereal y = m * x + t" "x \<in> S"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   268
      then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   269
        using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   270
    qed force
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   271
    then show "open (ereal -` ?f ` S)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   272
      using open_affinity[OF T(1) `r \<noteq> 0`]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   273
      by (auto simp: ac_simps)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   274
  next
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   275
    assume "\<infinity> \<in> ?f`S"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   276
    with `0 < r` have "\<infinity> \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   277
      by auto
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   278
    fix x
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   279
    assume "x \<in> {ereal (r * l + p)<..}"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   280
    then have [simp]: "ereal (r * l + p) < x"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   281
      by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   282
    show "x \<in> ?f`S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   283
    proof (rule image_eqI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   284
      show "x = m * ((x - t) / m) + t"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   285
        using m t
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   286
        by (cases rule: ereal3_cases[of m x t]) auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   287
      have "ereal l < (x - t) / m"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   288
        using m t
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   289
        by (simp add: ereal_less_divide_pos ereal_less_minus)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   290
      then show "(x - t) / m \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   291
        using T(2)[OF `\<infinity> \<in> S`] by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   292
    qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   293
  next
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   294
    assume "-\<infinity> \<in> ?f ` S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   295
    with `0 < r` have "-\<infinity> \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   296
      by auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   297
    fix x assume "x \<in> {..<ereal (r * u + p)}"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   298
    then have [simp]: "x < ereal (r * u + p)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   299
      by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   300
    show "x \<in> ?f`S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   301
    proof (rule image_eqI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   302
      show "x = m * ((x - t) / m) + t"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   303
        using m t
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   304
        by (cases rule: ereal3_cases[of m x t]) auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   305
      have "(x - t)/m < ereal u"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   306
        using m t
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   307
        by (simp add: ereal_divide_less_pos ereal_minus_less)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   308
      then show "(x - t)/m \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   309
        using T(3)[OF `-\<infinity> \<in> S`]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   310
        by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   311
    qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   312
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   313
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   314
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   315
lemma ereal_open_affinity:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   316
  fixes S :: "ereal set"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   317
  assumes "open S"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   318
    and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   319
    and t: "\<bar>t\<bar> \<noteq> \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   320
  shows "open ((\<lambda>x. m * x + t) ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   321
proof cases
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   322
  assume "0 < m"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   323
  then show ?thesis
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   324
    using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   325
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   326
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   327
  assume "\<not> 0 < m" then
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   328
  have "0 < -m"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   329
    using `m \<noteq> 0`
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   330
    by (cases m) auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   331
  then have m: "-m \<noteq> \<infinity>" "0 < -m"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   332
    using `\<bar>m\<bar> \<noteq> \<infinity>`
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   333
    by (auto simp: ereal_uminus_eq_reorder)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   334
  from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t] show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   335
    unfolding image_image by simp
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   336
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   337
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   338
lemma ereal_lim_mult:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   339
  fixes X :: "'a \<Rightarrow> ereal"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   340
  assumes lim: "(X ---> L) net"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   341
    and a: "\<bar>a\<bar> \<noteq> \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   342
  shows "((\<lambda>i. a * X i) ---> a * L) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   343
proof cases
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   344
  assume "a \<noteq> 0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   345
  show ?thesis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   346
  proof (rule topological_tendstoI)
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   347
    fix S
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   348
    assume "open S" and "a * L \<in> S"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   349
    have "a * L / a = L"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   350
      using `a \<noteq> 0` a
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   351
      by (cases rule: ereal2_cases[of a L]) auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   352
    then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   353
      using `a * L \<in> S`
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   354
      by (force simp: image_iff)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   355
    moreover have "open ((\<lambda>x. x / a) ` S)"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   356
      using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   357
      by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   358
    note * = lim[THEN topological_tendstoD, OF this L]
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   359
    {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   360
      fix x
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   361
      from a `a \<noteq> 0` have "a * (x / a) = x"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   362
        by (cases rule: ereal2_cases[of a x]) auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   363
    }
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   364
    note this[simp]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   365
    show "eventually (\<lambda>x. a * X x \<in> S) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   366
      by (rule eventually_mono[OF _ *]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   367
  qed
44918
6a80fbc4e72c tune simpset for Complete_Lattices
noschinl
parents: 44571
diff changeset
   368
qed auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   369
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   370
lemma ereal_lim_uminus:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   371
  fixes X :: "'a \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   372
  shows "((\<lambda>i. - X i) ---> - L) net \<longleftrightarrow> (X ---> L) net"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   373
  using ereal_lim_mult[of X L net "ereal (-1)"]
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   374
    ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   375
  by (auto simp add: algebra_simps)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   376
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   377
lemma ereal_open_atLeast:
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   378
  fixes x :: ereal
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   379
  shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   380
proof
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   381
  assume "x = -\<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   382
  then have "{x..} = UNIV"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   383
    by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   384
  then show "open {x..}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   385
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   386
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   387
  assume "open {x..}"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   388
  then have "open {x..} \<and> closed {x..}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   389
    by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   390
  then have "{x..} = UNIV"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   391
    unfolding ereal_open_closed by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   392
  then show "x = -\<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   393
    by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   394
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   395
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   396
lemma open_uminus_iff:
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   397
  fixes S :: "ereal set"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   398
  shows "open (uminus ` S) \<longleftrightarrow> open S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   399
  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   400
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   401
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   402
lemma ereal_Liminf_uminus:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   403
  fixes f :: "'a \<Rightarrow> ereal"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   404
  shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   405
  using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   406
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   407
lemma ereal_Lim_uminus:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   408
  fixes f :: "'a \<Rightarrow> ereal"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   409
  shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   410
  using
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   411
    ereal_lim_mult[of f f0 net "- 1"]
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   412
    ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   413
  by (auto simp: ereal_uminus_reorder)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   414
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   415
lemma Liminf_PInfty:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   416
  fixes f :: "'a \<Rightarrow> ereal"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   417
  assumes "\<not> trivial_limit net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   418
  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   419
  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   420
  using Liminf_le_Limsup[OF assms, of f]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   421
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   422
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   423
lemma Limsup_MInfty:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   424
  fixes f :: "'a \<Rightarrow> ereal"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   425
  assumes "\<not> trivial_limit net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   426
  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   427
  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   428
  using Liminf_le_Limsup[OF assms, of f]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   429
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   430
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
   431
lemma convergent_ereal:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   432
  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder,linorder_topology}"
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
   433
  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
   434
  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
   435
  by (auto simp: convergent_def)
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
   436
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   437
lemma liminf_PInfty:
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   438
  fixes X :: "nat \<Rightarrow> ereal"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   439
  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   440
  by (metis Liminf_PInfty trivial_limit_sequentially)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   441
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   442
lemma limsup_MInfty:
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   443
  fixes X :: "nat \<Rightarrow> ereal"
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   444
  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   445
  by (metis Limsup_MInfty trivial_limit_sequentially)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   446
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   447
lemma ereal_lim_mono:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   448
  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   449
  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   450
    and "X ----> x"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   451
    and "Y ----> y"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   452
  shows "x \<le> y"
51000
c9adb50f74ad use order topology for extended reals
hoelzl
parents: 50104
diff changeset
   453
  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   454
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   455
lemma incseq_le_ereal:
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   456
  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   457
  assumes inc: "incseq X"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   458
    and lim: "X ----> L"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   459
  shows "X N \<le> L"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   460
  using inc
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   461
  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   462
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   463
lemma decseq_ge_ereal:
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   464
  assumes dec: "decseq X"
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   465
    and lim: "X ----> (L::'a::linorder_topology)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   466
  shows "X N \<ge> L"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   467
  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   468
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   469
lemma bounded_abs:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   470
  fixes a :: real
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   471
  assumes "a \<le> x"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   472
    and "x \<le> b"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   473
  shows "abs x \<le> max (abs a) (abs b)"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   474
  by (metis abs_less_iff assms leI le_max_iff_disj
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   475
    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   476
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   477
lemma ereal_Sup_lim:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   478
  fixes a :: "'a::{complete_linorder,linorder_topology}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   479
  assumes "\<And>n. b n \<in> s"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   480
    and "b ----> a"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   481
  shows "a \<le> Sup s"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   482
  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   483
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   484
lemma ereal_Inf_lim:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   485
  fixes a :: "'a::{complete_linorder,linorder_topology}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   486
  assumes "\<And>n. b n \<in> s"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   487
    and "b ----> a"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   488
  shows "Inf s \<le> a"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   489
  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   490
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   491
lemma SUP_Lim_ereal:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   492
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   493
  assumes inc: "incseq X"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   494
    and l: "X ----> l"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   495
  shows "(SUP n. X n) = l"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   496
  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   497
  by simp
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   498
51351
dd1dd470690b generalized lemmas in Extended_Real_Limits
hoelzl
parents: 51340
diff changeset
   499
lemma INF_Lim_ereal:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   500
  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   501
  assumes dec: "decseq X"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   502
    and l: "X ----> l"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   503
  shows "(INF n. X n) = l"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   504
  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   505
  by simp
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   506
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   507
lemma SUP_eq_LIMSEQ:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   508
  assumes "mono f"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   509
  shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f ----> x"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   510
proof
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   511
  have inc: "incseq (\<lambda>i. ereal (f i))"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   512
    using `mono f` unfolding mono_def incseq_def by auto
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   513
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   514
    assume "f ----> x"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   515
    then have "(\<lambda>i. ereal (f i)) ----> ereal x"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   516
      by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   517
    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   518
  next
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   519
    assume "(SUP n. ereal (f n)) = ereal x"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   520
    with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   521
  }
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   522
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   523
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   524
lemma liminf_ereal_cminus:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   525
  fixes f :: "nat \<Rightarrow> ereal"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   526
  assumes "c \<noteq> -\<infinity>"
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   527
  shows "liminf (\<lambda>x. c - f x) = c - limsup f"
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   528
proof (cases c)
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   529
  case PInf
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   530
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   531
    by (simp add: Liminf_const)
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   532
next
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   533
  case (real r)
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   534
  then show ?thesis
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   535
    unfolding liminf_SUPR_INFI limsup_INFI_SUPR
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   536
    apply (subst INFI_ereal_cminus)
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   537
    apply auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   538
    apply (subst SUPR_ereal_cminus)
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   539
    apply auto
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   540
    done
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   541
qed (insert `c \<noteq> -\<infinity>`, simp)
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
   542
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   543
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   544
subsubsection {* Continuity *}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   545
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   546
lemma continuous_at_of_ereal:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   547
  fixes x0 :: ereal
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   548
  assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   549
  shows "continuous (at x0) real"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   550
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   551
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   552
    fix T
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   553
    assume T: "open T" "real x0 \<in> T"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   554
    def S \<equiv> "ereal ` T"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   555
    then have "ereal (real x0) \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   556
      using T by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   557
    then have "x0 \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   558
      using assms ereal_real by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   559
    moreover have "open S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   560
      using open_ereal S_def T by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   561
    moreover have "\<forall>y\<in>S. real y \<in> T"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   562
      using S_def T by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   563
    ultimately have "\<exists>S. x0 \<in> S \<and> open S \<and> (\<forall>y\<in>S. real y \<in> T)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   564
      by auto
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   565
  }
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   566
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   567
    unfolding continuous_at_open by blast
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   568
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   569
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   570
lemma continuous_at_iff_ereal:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   571
  fixes f :: "'a::t2_space \<Rightarrow> real"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   572
  shows "continuous (at x0) f \<longleftrightarrow> continuous (at x0) (ereal \<circ> f)"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   573
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   574
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   575
    assume "continuous (at x0) f"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   576
    then have "continuous (at x0) (ereal \<circ> f)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   577
      using continuous_at_ereal continuous_at_compose[of x0 f ereal]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   578
      by auto
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   579
  }
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   580
  moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   581
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   582
    assume "continuous (at x0) (ereal \<circ> f)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   583
    then have "continuous (at x0) (real \<circ> (ereal \<circ> f))"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   584
      using continuous_at_of_ereal
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   585
      by (intro continuous_at_compose[of x0 "ereal \<circ> f"]) auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   586
    moreover have "real \<circ> (ereal \<circ> f) = f"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   587
      using real_ereal_id by (simp add: o_assoc)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   588
    ultimately have "continuous (at x0) f"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   589
      by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   590
  }
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   591
  ultimately show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   592
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   593
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   594
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   595
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   596
lemma continuous_on_iff_ereal:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   597
  fixes f :: "'a::t2_space => real"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   598
  assumes "open A"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   599
  shows "continuous_on A f \<longleftrightarrow> continuous_on A (ereal \<circ> f)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   600
  using continuous_at_iff_ereal assms
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   601
  by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   602
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   603
lemma continuous_on_real: "continuous_on (UNIV - {\<infinity>, -\<infinity>::ereal}) real"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   604
  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   605
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   606
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   607
lemma continuous_on_iff_real:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   608
  fixes f :: "'a::t2_space \<Rightarrow> ereal"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   609
  assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   610
  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   611
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   612
  have "f ` A \<subseteq> UNIV - {\<infinity>, -\<infinity>}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   613
    using assms by force
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   614
  then have *: "continuous_on (f ` A) real"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   615
    using continuous_on_real by (simp add: continuous_on_subset)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   616
  have **: "continuous_on ((real \<circ> f) ` A) ereal"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   617
    using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real \<circ> f) ` A"]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   618
    by blast
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   619
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   620
    assume "continuous_on A f"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   621
    then have "continuous_on A (real \<circ> f)"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   622
      apply (subst continuous_on_compose)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   623
      using *
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   624
      apply auto
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   625
      done
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   626
  }
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   627
  moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   628
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   629
    assume "continuous_on A (real \<circ> f)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   630
    then have "continuous_on A (ereal \<circ> (real \<circ> f))"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   631
      apply (subst continuous_on_compose)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   632
      using **
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   633
      apply auto
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   634
      done
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   635
    then have "continuous_on A f"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   636
      apply (subst continuous_on_eq[of A "ereal \<circ> (real \<circ> f)" f])
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   637
      using assms ereal_real
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   638
      apply auto
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   639
      done
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   640
  }
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   641
  ultimately show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   642
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   643
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   644
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   645
lemma continuous_at_const:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   646
  fixes f :: "'a::t2_space \<Rightarrow> ereal"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   647
  assumes "\<forall>x. f x = C"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   648
  shows "\<forall>x. continuous (at x) f"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   649
  unfolding continuous_at_open
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   650
  using assms t1_space
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   651
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   652
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   653
lemma mono_closed_real:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   654
  fixes S :: "real set"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   655
  assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   656
    and "closed S"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   657
  shows "S = {} \<or> S = UNIV \<or> (\<exists>a. S = {a..})"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   658
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   659
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   660
    assume "S \<noteq> {}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   661
    { assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   662
      then have *: "\<forall>x\<in>S. Inf S \<le> x"
54258
adfc759263ab use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents: 54257
diff changeset
   663
        using cInf_lower[of _ S] ex by (metis bdd_below_def)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   664
      then have "Inf S \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   665
        apply (subst closed_contains_Inf)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   666
        using ex `S \<noteq> {}` `closed S`
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   667
        apply auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   668
        done
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   669
      then have "\<forall>x. Inf S \<le> x \<longleftrightarrow> x \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   670
        using mono[rule_format, of "Inf S"] *
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   671
        by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   672
      then have "S = {Inf S ..}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   673
        by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   674
      then have "\<exists>a. S = {a ..}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   675
        by auto
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   676
    }
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   677
    moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   678
    {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   679
      assume "\<not> (\<exists>B. \<forall>x\<in>S. B \<le> x)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   680
      then have nex: "\<forall>B. \<exists>x\<in>S. x < B"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   681
        by (simp add: not_le)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   682
      {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   683
        fix y
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   684
        obtain x where "x\<in>S" and "x < y"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   685
          using nex by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   686
        then have "y \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   687
          using mono[rule_format, of x y] by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   688
      }
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   689
      then have "S = UNIV"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   690
        by auto
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   691
    }
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   692
    ultimately have "S = UNIV \<or> (\<exists>a. S = {a ..})"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   693
      by blast
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   694
  }
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   695
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   696
    by blast
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   697
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   698
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   699
lemma mono_closed_ereal:
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   700
  fixes S :: "real set"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   701
  assumes mono: "\<forall>y z. y \<in> S \<and> y \<le> z \<longrightarrow> z \<in> S"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   702
    and "closed S"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   703
  shows "\<exists>a. S = {x. a \<le> ereal x}"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   704
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   705
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   706
    assume "S = {}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   707
    then have ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   708
      apply (rule_tac x=PInfty in exI)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   709
      apply auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   710
      done
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   711
  }
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   712
  moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   713
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   714
    assume "S = UNIV"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   715
    then have ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   716
      apply (rule_tac x="-\<infinity>" in exI)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   717
      apply auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   718
      done
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   719
  }
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   720
  moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   721
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   722
    assume "\<exists>a. S = {a ..}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   723
    then obtain a where "S = {a ..}"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   724
      by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   725
    then have ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   726
      apply (rule_tac x="ereal a" in exI)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   727
      apply auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   728
      done
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   729
  }
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   730
  ultimately show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   731
    using mono_closed_real[of S] assms by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   732
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   733
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   734
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   735
subsection {* Sums *}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   736
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   737
lemma setsum_ereal[simp]: "(\<Sum>x\<in>A. ereal (f x)) = ereal (\<Sum>x\<in>A. f x)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   738
proof (cases "finite A")
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   739
  case True
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   740
  then show ?thesis by induct auto
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   741
next
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   742
  case False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   743
  then show ?thesis by simp
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   744
qed
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   745
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   746
lemma setsum_Pinfty:
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   747
  fixes f :: "'a \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   748
  shows "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> finite P \<and> (\<exists>i\<in>P. f i = \<infinity>)"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   749
proof safe
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   750
  assume *: "setsum f P = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   751
  show "finite P"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   752
  proof (rule ccontr)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   753
    assume "infinite P"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   754
    with * show False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   755
      by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   756
  qed
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   757
  show "\<exists>i\<in>P. f i = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   758
  proof (rule ccontr)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   759
    assume "\<not> ?thesis"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   760
    then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   761
      by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   762
    with `finite P` have "setsum f P \<noteq> \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   763
      by induct auto
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   764
    with * show False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   765
      by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   766
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   767
next
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   768
  fix i
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   769
  assume "finite P" and "i \<in> P" and "f i = \<infinity>"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   770
  then show "setsum f P = \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   771
  proof induct
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   772
    case (insert x A)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   773
    show ?case using insert by (cases "x = i") auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   774
  qed simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   775
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   776
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   777
lemma setsum_Inf:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   778
  fixes f :: "'a \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   779
  shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   780
proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   781
  assume *: "\<bar>setsum f A\<bar> = \<infinity>"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   782
  have "finite A"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   783
    by (rule ccontr) (insert *, auto)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   784
  moreover have "\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   785
  proof (rule ccontr)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   786
    assume "\<not> ?thesis"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   787
    then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   788
      by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   789
    from bchoice[OF this] obtain r where "\<forall>x\<in>A. f x = ereal (r x)" ..
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   790
    with * show False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   791
      by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   792
  qed
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   793
  ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   794
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   795
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   796
  assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   797
  then obtain i where "finite A" "i \<in> A" and "\<bar>f i\<bar> = \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   798
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   799
  then show "\<bar>setsum f A\<bar> = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   800
  proof induct
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   801
    case (insert j A)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   802
    then show ?case
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   803
      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   804
  qed simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   805
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   806
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   807
lemma setsum_real_of_ereal:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   808
  fixes f :: "'i \<Rightarrow> ereal"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   809
  assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   810
  shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   811
proof -
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   812
  have "\<forall>x\<in>S. \<exists>r. f x = ereal r"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   813
  proof
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   814
    fix x
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   815
    assume "x \<in> S"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   816
    from assms[OF this] show "\<exists>r. f x = ereal r"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   817
      by (cases "f x") auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   818
  qed
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   819
  from bchoice[OF this] obtain r where "\<forall>x\<in>S. f x = ereal (r x)" ..
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   820
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   821
    by simp
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   822
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   823
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   824
lemma setsum_ereal_0:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   825
  fixes f :: "'a \<Rightarrow> ereal"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   826
  assumes "finite A"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   827
    and "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   828
  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   829
proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   830
  assume *: "(\<Sum>x\<in>A. f x) = 0"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   831
  then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   832
    by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   833
  then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   834
    using assms by (force simp: setsum_Pinfty)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   835
  then have "\<forall>i\<in>A. \<exists>r. f i = ereal r"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   836
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   837
  from bchoice[OF this] * assms show "\<forall>i\<in>A. f i = 0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   838
    using setsum_nonneg_eq_0_iff[of A "\<lambda>i. real (f i)"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   839
qed (rule setsum_0')
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   840
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   841
lemma setsum_ereal_right_distrib:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   842
  fixes f :: "'a \<Rightarrow> ereal"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   843
  assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   844
  shows "r * setsum f A = (\<Sum>n\<in>A. r * f n)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   845
proof cases
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   846
  assume "finite A"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   847
  then show ?thesis using assms
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   848
    by induct (auto simp: ereal_right_distrib setsum_nonneg)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   849
qed simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   850
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   851
lemma sums_ereal_positive:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   852
  fixes f :: "nat \<Rightarrow> ereal"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   853
  assumes "\<And>i. 0 \<le> f i"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   854
  shows "f sums (SUP n. \<Sum>i<n. f i)"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   855
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   856
  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   857
    using ereal_add_mono[OF _ assms]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   858
    by (auto intro!: incseq_SucI)
51000
c9adb50f74ad use order topology for extended reals
hoelzl
parents: 50104
diff changeset
   859
  from LIMSEQ_SUP[OF this]
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   860
  show ?thesis unfolding sums_def
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   861
    by (simp add: atLeast0LessThan)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   862
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   863
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   864
lemma summable_ereal_pos:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   865
  fixes f :: "nat \<Rightarrow> ereal"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   866
  assumes "\<And>i. 0 \<le> f i"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   867
  shows "summable f"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   868
  using sums_ereal_positive[of f, OF assms]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   869
  unfolding summable_def
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   870
  by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   871
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   872
lemma suminf_ereal_eq_SUPR:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   873
  fixes f :: "nat \<Rightarrow> ereal"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   874
  assumes "\<And>i. 0 \<le> f i"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   875
  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   876
  using sums_ereal_positive[of f, OF assms, THEN sums_unique]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   877
  by simp
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   878
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   879
lemma sums_ereal: "(\<lambda>x. ereal (f x)) sums ereal x \<longleftrightarrow> f sums x"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   880
  unfolding sums_def by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   881
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   882
lemma suminf_bound:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   883
  fixes f :: "nat \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   884
  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   885
    and pos: "\<And>n. 0 \<le> f n"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   886
  shows "suminf f \<le> x"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   887
proof (rule Lim_bounded_ereal)
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   888
  have "summable f" using pos[THEN summable_ereal_pos] .
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   889
  then show "(\<lambda>N. \<Sum>n<N. f n) ----> suminf f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   890
    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   891
  show "\<forall>n\<ge>0. setsum f {..<n} \<le> x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   892
    using assms by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   893
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   894
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   895
lemma suminf_bound_add:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   896
  fixes f :: "nat \<Rightarrow> ereal"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   897
  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   898
    and pos: "\<And>n. 0 \<le> f n"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   899
    and "y \<noteq> -\<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   900
  shows "suminf f + y \<le> x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   901
proof (cases y)
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   902
  case (real r)
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   903
  then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   904
    using assms by (simp add: ereal_le_minus)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   905
  then have "(\<Sum> n. f n) \<le> x - y"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   906
    using pos by (rule suminf_bound)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   907
  then show "(\<Sum> n. f n) + y \<le> x"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   908
    using assms real by (simp add: ereal_le_minus)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   909
qed (insert assms, auto)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   910
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   911
lemma suminf_upper:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   912
  fixes f :: "nat \<Rightarrow> ereal"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   913
  assumes "\<And>n. 0 \<le> f n"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   914
  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44918
diff changeset
   915
  unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
45031
9583f2b56f85 add lemmas within_empty and tendsto_bot;
huffman
parents: 44928
diff changeset
   916
  by (auto intro: complete_lattice_class.Sup_upper)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   917
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   918
lemma suminf_0_le:
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   919
  fixes f :: "nat \<Rightarrow> ereal"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   920
  assumes "\<And>n. 0 \<le> f n"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   921
  shows "0 \<le> (\<Sum>n. f n)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   922
  using suminf_upper[of f 0, OF assms]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   923
  by simp
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   924
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   925
lemma suminf_le_pos:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   926
  fixes f g :: "nat \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   927
  assumes "\<And>N. f N \<le> g N"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   928
    and "\<And>N. 0 \<le> f N"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   929
  shows "suminf f \<le> suminf g"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   930
proof (safe intro!: suminf_bound)
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   931
  fix n
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   932
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   933
    fix N
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   934
    have "0 \<le> g N"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   935
      using assms(2,1)[of N] by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   936
  }
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   937
  have "setsum f {..<n} \<le> setsum g {..<n}"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   938
    using assms by (auto intro: setsum_mono)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   939
  also have "\<dots> \<le> suminf g"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   940
    using `\<And>N. 0 \<le> g N`
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   941
    by (rule suminf_upper)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   942
  finally show "setsum f {..<n} \<le> suminf g" .
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   943
qed (rule assms(2))
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   944
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   945
lemma suminf_half_series_ereal: "(\<Sum>n. (1/2 :: ereal) ^ Suc n) = 1"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   946
  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   947
  by (simp add: one_ereal_def)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   948
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   949
lemma suminf_add_ereal:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   950
  fixes f g :: "nat \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   951
  assumes "\<And>i. 0 \<le> f i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   952
    and "\<And>i. 0 \<le> g i"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   953
  shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   954
  apply (subst (1 2 3) suminf_ereal_eq_SUPR)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   955
  unfolding setsum_addf
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   956
  apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
   957
  done
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   958
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   959
lemma suminf_cmult_ereal:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   960
  fixes f g :: "nat \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   961
  assumes "\<And>i. 0 \<le> f i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   962
    and "0 \<le> a"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   963
  shows "(\<Sum>i. a * f i) = a * suminf f"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   964
  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   965
       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   966
       intro!: SUPR_ereal_cmult )
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   967
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   968
lemma suminf_PInfty:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
   969
  fixes f :: "nat \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   970
  assumes "\<And>i. 0 \<le> f i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   971
    and "suminf f \<noteq> \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   972
  shows "f i \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   973
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   974
  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   975
  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   976
    by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   977
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   978
    unfolding setsum_Pinfty by simp
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   979
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   981
lemma suminf_PInfty_fun:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   982
  assumes "\<And>i. 0 \<le> f i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   983
    and "suminf f \<noteq> \<infinity>"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   984
  shows "\<exists>f'. f = (\<lambda>x. ereal (f' x))"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   985
proof -
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   986
  have "\<forall>i. \<exists>r. f i = ereal r"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   987
  proof
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   988
    fix i
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   989
    show "\<exists>r. f i = ereal r"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   990
      using suminf_PInfty[OF assms] assms(1)[of i]
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   991
      by (cases "f i") auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   992
  qed
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   993
  from choice[OF this] show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   994
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   995
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   996
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
   997
lemma summable_ereal:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   998
  assumes "\<And>i. 0 \<le> f i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
   999
    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1000
  shows "summable f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1001
proof -
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1002
  have "0 \<le> (\<Sum>i. ereal (f i))"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1003
    using assms by (intro suminf_0_le) auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1004
  with assms obtain r where r: "(\<Sum>i. ereal (f i)) = ereal r"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1005
    by (cases "\<Sum>i. ereal (f i)") auto
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1006
  from summable_ereal_pos[of "\<lambda>x. ereal (f x)"]
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1007
  have "summable (\<lambda>x. ereal (f x))"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1008
    using assms by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1009
  from summable_sums[OF this]
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1010
  have "(\<lambda>x. ereal (f x)) sums (\<Sum>x. ereal (f x))"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1011
    by auto
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1012
  then show "summable f"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1013
    unfolding r sums_ereal summable_def ..
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1014
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1015
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1016
lemma suminf_ereal:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1017
  assumes "\<And>i. 0 \<le> f i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1018
    and "(\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1019
  shows "(\<Sum>i. ereal (f i)) = ereal (suminf f)"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1020
proof (rule sums_unique[symmetric])
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1021
  from summable_ereal[OF assms]
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1022
  show "(\<lambda>x. ereal (f x)) sums (ereal (suminf f))"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1023
    unfolding sums_ereal
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1024
    using assms
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1025
    by (intro summable_sums summable_ereal)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1026
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1027
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1028
lemma suminf_ereal_minus:
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1029
  fixes f g :: "nat \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1030
  assumes ord: "\<And>i. g i \<le> f i" "\<And>i. 0 \<le> g i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1031
    and fin: "suminf f \<noteq> \<infinity>" "suminf g \<noteq> \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1032
  shows "(\<Sum>i. f i - g i) = suminf f - suminf g"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1033
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1034
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1035
    fix i
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1036
    have "0 \<le> f i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1037
      using ord[of i] by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1038
  }
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1039
  moreover
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1040
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] obtain f' where [simp]: "f = (\<lambda>x. ereal (f' x))" ..
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1041
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] obtain g' where [simp]: "g = (\<lambda>x. ereal (g' x))" ..
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1042
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1043
    fix i
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1044
    have "0 \<le> f i - g i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1045
      using ord[of i] by (auto simp: ereal_le_minus_iff)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1046
  }
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1047
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1048
  have "suminf (\<lambda>i. f i - g i) \<le> suminf f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1049
    using assms by (auto intro!: suminf_le_pos simp: field_simps)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1050
  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1051
    using fin by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1052
  ultimately show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1053
    using assms `\<And>i. 0 \<le> f i`
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1054
    apply simp
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1055
    apply (subst (1 2 3) suminf_ereal)
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1056
    apply (auto intro!: suminf_diff[symmetric] summable_ereal)
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1057
    done
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1058
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1059
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1060
lemma suminf_ereal_PInf [simp]: "(\<Sum>x. \<infinity>::ereal) = \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1061
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1062
  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>::ereal)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1063
    by (rule suminf_upper) auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1064
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1065
    by simp
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1066
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1067
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1068
lemma summable_real_of_ereal:
43923
ab93d0190a5d add ereal to typeclass infinity
hoelzl
parents: 43920
diff changeset
  1069
  fixes f :: "nat \<Rightarrow> ereal"
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1070
  assumes f: "\<And>i. 0 \<le> f i"
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1071
    and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1072
  shows "summable (\<lambda>i. real (f i))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1073
proof (rule summable_def[THEN iffD2])
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1074
  have "0 \<le> (\<Sum>i. f i)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1075
    using assms by (auto intro: suminf_0_le)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1076
  with fin obtain r where r: "ereal r = (\<Sum>i. f i)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1077
    by (cases "(\<Sum>i. f i)") auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1078
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1079
    fix i
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1080
    have "f i \<noteq> \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1081
      using f by (intro suminf_PInfty[OF _ fin]) auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1082
    then have "\<bar>f i\<bar> \<noteq> \<infinity>"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1083
      using f[of i] by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1084
  }
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1085
  note fin = this
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1086
  have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1087
    using f
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1088
    by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1089
  also have "\<dots> = ereal r"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1090
    using fin r by (auto simp: ereal_real)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1091
  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1092
    by (auto simp: sums_ereal)
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1093
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1094
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
  1095
lemma suminf_SUP_eq:
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1096
  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ereal"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1097
  assumes "\<And>i. incseq (\<lambda>n. f n i)"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1098
    and "\<And>n i. 0 \<le> f n i"
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
  1099
  shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
  1100
proof -
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1101
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1102
    fix n :: nat
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
  1103
    have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1104
      using assms
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1105
      by (auto intro!: SUPR_ereal_setsum[symmetric])
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1106
  }
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
  1107
  note * = this
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1108
  show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1109
    using assms
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 42950
diff changeset
  1110
    apply (subst (1 2) suminf_ereal_eq_SUPR)
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
  1111
    unfolding *
44928
7ef6505bde7f renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents: 44918
diff changeset
  1112
    apply (auto intro!: SUP_upper2)
49664
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1113
    apply (subst SUP_commute)
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1114
    apply rule
f099b8006a3c tuned proofs;
wenzelm
parents: 47761
diff changeset
  1115
    done
42950
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
  1116
qed
6e5c2a3c69da move lemmas to Extended_Reals and Extended_Real_Limits
hoelzl
parents: 41983
diff changeset
  1117
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 45051
diff changeset
  1118
lemma suminf_setsum_ereal:
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 45051
diff changeset
  1119
  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 45051
diff changeset
  1120
  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 45051
diff changeset
  1121
  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1122
proof (cases "finite A")
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1123
  case True
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1124
  then show ?thesis
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1125
    using nonneg
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 45051
diff changeset
  1126
    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1127
next
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1128
  case False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1129
  then show ?thesis by simp
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1130
qed
47761
dfe747e72fa8 moved lemmas to appropriate places
hoelzl
parents: 45051
diff changeset
  1131
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1132
lemma suminf_ereal_eq_0:
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1133
  fixes f :: "nat \<Rightarrow> ereal"
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1134
  assumes nneg: "\<And>i. 0 \<le> f i"
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1135
  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1136
proof
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1137
  assume "(\<Sum>i. f i) = 0"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1138
  {
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1139
    fix i
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1140
    assume "f i \<noteq> 0"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1141
    with nneg have "0 < f i"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1142
      by (auto simp: less_le)
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1143
    also have "f i = (\<Sum>j. if j = i then f i else 0)"
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1144
      by (subst suminf_finite[where N="{i}"]) auto
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1145
    also have "\<dots> \<le> (\<Sum>i. f i)"
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1146
      using nneg
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1147
      by (auto intro!: suminf_le_pos)
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1148
    finally have False
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1149
      using `(\<Sum>i. f i) = 0` by auto
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1150
  }
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1151
  then show "\<forall>i. f i = 0"
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1152
    by auto
50104
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1153
qed simp
de19856feb54 move theorems to be more generally useable
hoelzl
parents: 49664
diff changeset
  1154
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1155
lemma Liminf_within:
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1156
  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1157
  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51530
diff changeset
  1158
  unfolding Liminf_def eventually_at
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1159
proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1160
  fix P d
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1161
  assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1162
  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1163
    by (auto simp: zero_less_dist_iff dist_commute)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1164
  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1165
    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1166
next
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1167
  fix d :: real
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1168
  assume "0 < d"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51530
diff changeset
  1169
  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1170
    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1171
    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1172
       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1173
qed
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1174
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1175
lemma Limsup_within:
53788
b319a0c8b8a2 tuned proofs;
wenzelm
parents: 53374
diff changeset
  1176
  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: 51329
diff changeset
  1177
  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51530
diff changeset
  1178
  unfolding Limsup_def eventually_at
51340
5e6296afe08d move Liminf / Limsup lemmas on complete_lattices to its own file
hoelzl
parents: