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