src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
author wenzelm
Mon, 14 Mar 2011 16:59:37 +0100
changeset 41983 2dc6e382a58b
parent 41981 cdf7693bbe08
child 42950 6e5c2a3c69da
permissions -rw-r--r--
standardized headers;
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
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    11
  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Reals"
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
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    14
lemma continuous_on_extreal[intro, simp]: "continuous_on A extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    15
  unfolding continuous_on_topological open_extreal_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    16
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    17
lemma continuous_at_extreal[intro, simp]: "continuous (at x) extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    18
  using continuous_on_eq_continuous_at[of UNIV] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    19
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    20
lemma continuous_within_extreal[intro, simp]: "x \<in> A \<Longrightarrow> continuous (at x within A) extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    21
  using continuous_on_eq_continuous_within[of A] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    22
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    23
lemma extreal_open_uminus:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    24
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    25
  assumes "open S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    26
  shows "open (uminus ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    27
  unfolding open_extreal_def
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    28
proof (intro conjI impI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    29
  obtain x y where S: "open (extreal -` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    30
    "\<infinity> \<in> S \<Longrightarrow> {extreal x<..} \<subseteq> S" "-\<infinity> \<in> S \<Longrightarrow> {..< extreal y} \<subseteq> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    31
    using `open S` unfolding open_extreal_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    32
  have "extreal -` uminus ` S = uminus ` (extreal -` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    33
  proof safe
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    34
    fix x y assume "extreal x = - y" "y \<in> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    35
    then show "x \<in> uminus ` extreal -` S" by (cases y) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    36
  next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    37
    fix x assume "extreal x \<in> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    38
    then show "- x \<in> extreal -` uminus ` S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    39
      by (auto intro: image_eqI[of _ _ "extreal x"])
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    40
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    41
  then show "open (extreal -` uminus ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    42
    using S by (auto intro: open_negations)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    43
  { assume "\<infinity> \<in> uminus ` S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    44
    then have "-\<infinity> \<in> S" by (metis image_iff extreal_uminus_uminus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    45
    then have "uminus ` {..<extreal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    46
    then show "\<exists>x. {extreal x<..} \<subseteq> uminus ` S" using extreal_uminus_lessThan by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    47
  { assume "-\<infinity> \<in> uminus ` S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    48
    then have "\<infinity> : S" by (metis image_iff extreal_uminus_uminus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    49
    then have "uminus ` {extreal x<..} <= uminus ` S" using S by (intro image_mono) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    50
    then show "\<exists>y. {..<extreal y} <= uminus ` S" using extreal_uminus_greaterThan by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    51
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    52
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    53
lemma extreal_uminus_complement:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    54
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    55
  shows "uminus ` (- S) = - uminus ` S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    56
  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
    57
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    58
lemma extreal_closed_uminus:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    59
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    60
  assumes "closed S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    61
  shows "closed (uminus ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    62
using assms unfolding closed_def
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    63
using extreal_open_uminus[of "- S"] extreal_uminus_complement by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    64
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    65
lemma not_open_extreal_singleton:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    66
  "\<not> (open {a :: extreal})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    67
proof(rule ccontr)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    68
  assume "\<not> \<not> open {a}" hence a: "open {a}" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    69
  show False
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    70
  proof (cases a)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    71
    case MInf
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    72
    then obtain y where "{..<extreal y} <= {a}" using a open_MInfty2[of "{a}"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    73
    hence "extreal(y - 1):{a}" apply (subst subsetD[of "{..<extreal y}"]) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    74
    then show False using `a=(-\<infinity>)` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    75
  next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    76
    case PInf
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    77
    then obtain y where "{extreal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    78
    hence "extreal(y+1):{a}" apply (subst subsetD[of "{extreal y<..}"]) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    79
    then show False using `a=\<infinity>` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    80
  next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    81
    case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    82
    from extreal_open_cont_interval[OF a singletonI this] guess e . note e = this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    83
    then obtain b where b_def: "a<b & b<a+e"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    84
      using fin extreal_between extreal_dense[of a "a+e"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    85
    then have "b: {a-e <..< a+e}" using fin extreal_between[of a e] e by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    86
    then show False using b_def e by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    87
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    88
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    89
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    90
lemma extreal_closed_contains_Inf:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    91
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    92
  assumes "closed S" "S ~= {}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    93
  shows "Inf S : S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    94
proof(rule ccontr)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    95
  assume "Inf S \<notin> S" hence a: "open (-S)" "Inf S:(- S)" using assms by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    96
  show False
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    97
  proof (cases "Inf S")
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    98
    case MInf hence "(-\<infinity>) : - S" using a by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
    99
    then obtain y where "{..<extreal y} <= (-S)" using a open_MInfty2[of "- S"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   100
    hence "extreal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   101
      complete_lattice_class.Inf_greatest double_complement set_rev_mp)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   102
    then show False using MInf by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   103
  next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   104
    case PInf then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   105
    then show False by (metis `Inf S ~: S` insert_code mem_def PInf)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   106
  next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   107
    case (real r) then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   108
    from extreal_open_cont_interval[OF a this] guess e . note e = this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   109
    { fix x assume "x:S" hence "x>=Inf S" by (rule complete_lattice_class.Inf_lower)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   110
      hence *: "x>Inf S-e" using e by (metis fin extreal_between(1) order_less_le_trans)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   111
      { assume "x<Inf S+e" hence "x:{Inf S-e <..< Inf S+e}" using * by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   112
        hence False using e `x:S` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   113
      } hence "x>=Inf S+e" by (metis linorder_le_less_linear)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   114
    } hence "Inf S + e <= Inf S" by (metis le_Inf_iff)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   115
    then show False using real e by (cases e) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   116
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   117
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   118
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   119
lemma extreal_closed_contains_Sup:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   120
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   121
  assumes "closed S" "S ~= {}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   122
  shows "Sup S : S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   123
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   124
  have "closed (uminus ` S)" by (metis assms(1) extreal_closed_uminus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   125
  hence "Inf (uminus ` S) : uminus ` S" using assms extreal_closed_contains_Inf[of "uminus ` S"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   126
  hence "- Sup S : uminus ` S" using extreal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   127
  thus ?thesis by (metis imageI extreal_uminus_uminus extreal_minus_minus_image)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   128
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   129
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   130
lemma extreal_open_closed_aux:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   131
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   132
  assumes "open S" "closed S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   133
  assumes S: "(-\<infinity>) ~: S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   134
  shows "S = {}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   135
proof(rule ccontr)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   136
  assume "S ~= {}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   137
  hence *: "(Inf S):S" by (metis assms(2) extreal_closed_contains_Inf)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   138
  { assume "Inf S=(-\<infinity>)" hence False using * assms(3) by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   139
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   140
  { assume "Inf S=\<infinity>" hence "S={\<infinity>}" by (metis Inf_eq_PInfty `S ~= {}`)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   141
    hence False by (metis assms(1) not_open_extreal_singleton) }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   142
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   143
  { assume fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   144
    from extreal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   145
    then obtain b where b_def: "Inf S-e<b & b<Inf S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   146
      using fin extreal_between[of "Inf S" e] extreal_dense[of "Inf S-e"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   147
    hence "b: {Inf S-e <..< Inf S+e}" using e fin extreal_between[of "Inf S" e] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   148
    hence "b:S" using e by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   149
    hence False using b_def by (metis complete_lattice_class.Inf_lower leD)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   150
  } ultimately show False by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   151
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   152
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   153
lemma extreal_open_closed:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   154
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   155
  shows "(open S & closed S) <-> (S = {} | S = UNIV)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   156
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   157
{ assume lhs: "open S & closed S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   158
  { assume "(-\<infinity>) ~: S" hence "S={}" using lhs extreal_open_closed_aux by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   159
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   160
  { assume "(-\<infinity>) : S" hence "(- S)={}" using lhs extreal_open_closed_aux[of "-S"] by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   161
  ultimately have "S = {} | S = UNIV" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   162
} thus ?thesis by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   163
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   164
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   165
lemma extreal_open_affinity_pos:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   166
  assumes "open S" and m: "m \<noteq> \<infinity>" "0 < m" and t: "\<bar>t\<bar> \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   167
  shows "open ((\<lambda>x. m * x + t) ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   168
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   169
  obtain r where r[simp]: "m = extreal r" using m by (cases m) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   170
  obtain p where p[simp]: "t = extreal p" using t by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   171
  have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0" using m by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   172
  from `open S`[THEN extreal_openE] guess l u . note T = this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   173
  let ?f = "(\<lambda>x. m * x + t)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   174
  show ?thesis unfolding open_extreal_def
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   175
  proof (intro conjI impI exI subsetI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   176
    have "extreal -` ?f ` S = (\<lambda>x. r * x + p) ` (extreal -` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   177
    proof safe
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   178
      fix x y assume "extreal y = m * x + t" "x \<in> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   179
      then show "y \<in> (\<lambda>x. r * x + p) ` extreal -` S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   180
        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
   181
    qed force
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   182
    then show "open (extreal -` ?f ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   183
      using open_affinity[OF T(1) `r \<noteq> 0`] by (auto simp: ac_simps)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   184
  next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   185
    assume "\<infinity> \<in> ?f`S" with `0 < r` have "\<infinity> \<in> S" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   186
    fix x assume "x \<in> {extreal (r * l + p)<..}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   187
    then have [simp]: "extreal (r * l + p) < x" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   188
    show "x \<in> ?f`S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   189
    proof (rule image_eqI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   190
      show "x = m * ((x - t) / m) + t"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   191
        using m t by (cases rule: extreal3_cases[of m x t]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   192
      have "extreal l < (x - t)/m"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   193
        using m t by (simp add: extreal_less_divide_pos extreal_less_minus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   194
      then show "(x - t)/m \<in> S" using T(2)[OF `\<infinity> \<in> S`] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   195
    qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   196
  next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   197
    assume "-\<infinity> \<in> ?f`S" with `0 < r` have "-\<infinity> \<in> S" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   198
    fix x assume "x \<in> {..<extreal (r * u + p)}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   199
    then have [simp]: "x < extreal (r * u + p)" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   200
    show "x \<in> ?f`S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   201
    proof (rule image_eqI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   202
      show "x = m * ((x - t) / m) + t"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   203
        using m t by (cases rule: extreal3_cases[of m x t]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   204
      have "(x - t)/m < extreal u"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   205
        using m t by (simp add: extreal_divide_less_pos extreal_minus_less)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   206
      then show "(x - t)/m \<in> S" using T(3)[OF `-\<infinity> \<in> S`] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   207
    qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   208
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   209
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   210
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   211
lemma extreal_open_affinity:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   212
  assumes "open S" and m: "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" and t: "\<bar>t\<bar> \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   213
  shows "open ((\<lambda>x. m * x + t) ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   214
proof cases
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   215
  assume "0 < m" then show ?thesis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   216
    using extreal_open_affinity_pos[OF `open S` _ _ t, of m] m by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   217
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   218
  assume "\<not> 0 < m" then
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   219
  have "0 < -m" using `m \<noteq> 0` by (cases m) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   220
  then have m: "-m \<noteq> \<infinity>" "0 < -m" using `\<bar>m\<bar> \<noteq> \<infinity>`
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   221
    by (auto simp: extreal_uminus_eq_reorder)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   222
  from extreal_open_affinity_pos[OF extreal_open_uminus[OF `open S`] m t]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   223
  show ?thesis unfolding image_image by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   224
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   225
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   226
lemma extreal_lim_mult:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   227
  fixes X :: "'a \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   228
  assumes lim: "(X ---> L) net" and a: "\<bar>a\<bar> \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   229
  shows "((\<lambda>i. a * X i) ---> a * L) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   230
proof cases
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   231
  assume "a \<noteq> 0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   232
  show ?thesis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   233
  proof (rule topological_tendstoI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   234
    fix S assume "open S" "a * L \<in> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   235
    have "a * L / a = L"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   236
      using `a \<noteq> 0` a by (cases rule: extreal2_cases[of a L]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   237
    then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   238
      using `a * L \<in> S` by (force simp: image_iff)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   239
    moreover have "open ((\<lambda>x. x / a) ` S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   240
      using extreal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   241
      by (auto simp: extreal_divide_eq extreal_inverse_eq_0 divide_extreal_def ac_simps)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   242
    note * = lim[THEN topological_tendstoD, OF this L]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   243
    { fix x from a `a \<noteq> 0` have "a * (x / a) = x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   244
        by (cases rule: extreal2_cases[of a x]) auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   245
    note this[simp]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   246
    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
   247
      by (rule eventually_mono[OF _ *]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   248
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   249
qed auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   250
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   251
lemma extreal_lim_uminus:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   252
  fixes X :: "'a \<Rightarrow> extreal" shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   253
  using extreal_lim_mult[of X L net "extreal (-1)"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   254
        extreal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "extreal (-1)"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   255
  by (auto simp add: algebra_simps)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   256
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   257
lemma Lim_bounded2_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   258
  assumes lim:"f ----> (l :: extreal)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   259
  and ge: "ALL n>=N. f n >= C"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   260
  shows "l>=C"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   261
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   262
def g == "(%i. -(f i))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   263
{ fix n assume "n>=N" hence "g n <= -C" using assms extreal_minus_le_minus g_def by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   264
hence "ALL n>=N. g n <= -C" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   265
moreover have limg: "g ----> (-l)" using g_def extreal_lim_uminus lim by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   266
ultimately have "-l <= -C" using Lim_bounded_extreal[of g "-l" _ "-C"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   267
from this show ?thesis using extreal_minus_le_minus by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   268
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   269
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   270
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   271
lemma extreal_open_atLeast: "open {x..} \<longleftrightarrow> x = -\<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   272
proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   273
  assume "x = -\<infinity>" then have "{x..} = UNIV" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   274
  then show "open {x..}" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   275
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   276
  assume "open {x..}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   277
  then have "open {x..} \<and> closed {x..}" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   278
  then have "{x..} = UNIV" unfolding extreal_open_closed by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   279
  then show "x = -\<infinity>" by (simp add: bot_extreal_def atLeast_eq_UNIV_iff)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   280
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   281
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   282
lemma extreal_open_mono_set:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   283
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   284
  defines "a \<equiv> Inf S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   285
  shows "(open S \<and> mono S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   286
  by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff extreal_open_atLeast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   287
            extreal_open_closed mono_set_iff open_extreal_greaterThan)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   288
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   289
lemma extreal_closed_mono_set:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   290
  fixes S :: "extreal set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   291
  shows "(closed S \<and> mono S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   292
  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_extreal_atLeast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   293
            extreal_open_closed mono_empty mono_set_iff open_extreal_greaterThan)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   294
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   295
lemma extreal_Liminf_Sup_monoset:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   296
  fixes f :: "'a => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   297
  shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   298
  unfolding Liminf_Sup
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   299
proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   300
  fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono S" "l \<in> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   301
  then have "S = UNIV \<or> S = {Inf S <..}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   302
    using extreal_open_mono_set[of S] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   303
  then show "eventually (\<lambda>x. f x \<in> S) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   304
  proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   305
    assume S: "S = {Inf S<..}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   306
    then have "Inf S < l" using `l \<in> S` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   307
    then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   308
    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   309
  qed auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   310
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   311
  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   312
  have "eventually  (\<lambda>x. f x \<in> {y <..}) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   313
    using `y < l` by (intro S[rule_format]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   314
  then show "eventually (\<lambda>x. y < f x) net" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   315
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   316
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   317
lemma extreal_Limsup_Inf_monoset:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   318
  fixes f :: "'a => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   319
  shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   320
  unfolding Limsup_Inf
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   321
proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   322
  fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono (uminus`S)" "l \<in> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   323
  then have "open (uminus`S) \<and> mono (uminus`S)" by (simp add: extreal_open_uminus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   324
  then have "S = UNIV \<or> S = {..< Sup S}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   325
    unfolding extreal_open_mono_set extreal_Inf_uminus_image_eq extreal_image_uminus_shift by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   326
  then show "eventually (\<lambda>x. f x \<in> S) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   327
  proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   328
    assume S: "S = {..< Sup S}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   329
    then have "l < Sup S" using `l \<in> S` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   330
    then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   331
    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   332
  qed auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   333
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   334
  fix l y assume S: "\<forall>S. open S \<longrightarrow> mono (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "l < y"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   335
  have "eventually  (\<lambda>x. f x \<in> {..< y}) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   336
    using `l < y` by (intro S[rule_format]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   337
  then show "eventually (\<lambda>x. f x < y) net" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   338
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   339
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   340
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   341
lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::extreal set)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   342
  using extreal_open_uminus[of S] extreal_open_uminus[of "uminus`S"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   343
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   344
lemma extreal_Limsup_uminus:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   345
  fixes f :: "'a => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   346
  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   347
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   348
  { fix P l have "(\<exists>x. (l::extreal) = -x \<and> P x) \<longleftrightarrow> P (-l)" by (auto intro!: exI[of _ "-l"]) }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   349
  note Ex_cancel = this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   350
  { fix P :: "extreal set \<Rightarrow> bool" have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   351
      apply auto by (erule_tac x="uminus`S" in allE) (auto simp: image_image) }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   352
  note add_uminus_image = this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   353
  { fix x S have "(x::extreal) \<in> uminus`S \<longleftrightarrow> -x\<in>S" by (auto intro!: image_eqI[of _ _ "-x"]) }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   354
  note remove_uminus_image = this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   355
  show ?thesis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   356
    unfolding extreal_Limsup_Inf_monoset extreal_Liminf_Sup_monoset
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   357
    unfolding extreal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   358
    by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   359
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   360
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   361
lemma extreal_Liminf_uminus:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   362
  fixes f :: "'a => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   363
  shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   364
  using extreal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   365
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   366
lemma extreal_Lim_uminus:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   367
  fixes f :: "'a \<Rightarrow> extreal" shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   368
  using
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   369
    extreal_lim_mult[of f f0 net "- 1"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   370
    extreal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   371
  by (auto simp: extreal_uminus_reorder)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   372
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   373
lemma lim_imp_Limsup:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   374
  fixes f :: "'a => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   375
  assumes "\<not> trivial_limit net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   376
  assumes lim: "(f ---> f0) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   377
  shows "Limsup net f = f0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   378
  using extreal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   379
     extreal_Liminf_uminus[of net f] assms by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   380
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   381
lemma Liminf_PInfty:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   382
  fixes f :: "'a \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   383
  assumes "\<not> trivial_limit net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   384
  shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   385
proof (intro lim_imp_Liminf iffI assms)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   386
  assume rhs: "Liminf net f = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   387
  { fix S assume "open S & \<infinity> : S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   388
    then obtain m where "{extreal m<..} <= S" using open_PInfty2 by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   389
    moreover have "eventually (\<lambda>x. f x \<in> {extreal m<..}) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   390
      using rhs unfolding Liminf_Sup top_extreal_def[symmetric] Sup_eq_top_iff
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   391
      by (auto elim!: allE[where x="extreal m"] simp: top_extreal_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   392
    ultimately have "eventually (%x. f x : S) net" apply (subst eventually_mono) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   393
  } then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto
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
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   396
lemma Limsup_MInfty:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   397
  fixes f :: "'a \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   398
  assumes "\<not> trivial_limit net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   399
  shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   400
  using assms extreal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   401
        extreal_Liminf_uminus[of _ f] by (auto simp: extreal_uminus_eq_reorder)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   402
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   403
lemma extreal_Liminf_eq_Limsup:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   404
  fixes f :: "'a \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   405
  assumes ntriv: "\<not> trivial_limit net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   406
  assumes lim: "Liminf net f = f0" "Limsup net f = f0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   407
  shows "(f ---> f0) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   408
proof (cases f0)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   409
  case PInf then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   410
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   411
  case MInf then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   412
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   413
  case (real r)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   414
  show "(f ---> f0) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   415
  proof (rule topological_tendstoI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   416
    fix S assume "open S""f0 \<in> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   417
    then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   418
      using extreal_open_cont_interval2[of S f0] real lim by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   419
    then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   420
      unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   421
      by (auto intro!: eventually_conj simp add: greaterThanLessThan_iff)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   422
    with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   423
      by (rule_tac eventually_mono) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   424
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   425
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   426
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   427
lemma extreal_Liminf_eq_Limsup_iff:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   428
  fixes f :: "'a \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   429
  assumes "\<not> trivial_limit net"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   430
  shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   431
  by (metis assms extreal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   432
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   433
lemma limsup_INFI_SUPR:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   434
  fixes f :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   435
  shows "limsup f = (INF n. SUP m:{n..}. f m)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   436
  using extreal_Limsup_uminus[of sequentially "\<lambda>x. - f x"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   437
  by (simp add: liminf_SUPR_INFI extreal_INFI_uminus extreal_SUPR_uminus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   438
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   439
lemma liminf_PInfty:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   440
  fixes X :: "nat => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   441
  shows "X ----> \<infinity> <-> liminf X = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   442
by (metis Liminf_PInfty trivial_limit_sequentially)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   443
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   444
lemma limsup_MInfty:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   445
  fixes X :: "nat => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   446
  shows "X ----> (-\<infinity>) <-> limsup X = (-\<infinity>)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   447
by (metis Limsup_MInfty trivial_limit_sequentially)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   448
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   449
lemma extreal_lim_mono:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   450
  fixes X Y :: "nat => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   451
  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   452
  assumes "X ----> x" "Y ----> y"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   453
  shows "x <= y"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   454
  by (metis extreal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   455
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   456
lemma incseq_le_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   457
  fixes X :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   458
  assumes inc: "incseq X" and lim: "X ----> L"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   459
  shows "X N \<le> L"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   460
  using inc
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   461
  by (intro extreal_lim_mono[of N, OF _ Lim_const lim]) (simp add: incseq_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   462
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   463
lemma decseq_ge_extreal: assumes dec: "decseq X"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   464
  and lim: "X ----> (L::extreal)" shows "X N >= L"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   465
  using dec
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   466
  by (intro extreal_lim_mono[of N, OF _ lim Lim_const]) (simp add: decseq_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   467
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   468
lemma liminf_bounded_open:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   469
  fixes x :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   470
  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))" 
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   471
  (is "_ \<longleftrightarrow> ?P x0")
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   472
proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   473
  assume "?P x0" then show "x0 \<le> liminf x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   474
    unfolding extreal_Liminf_Sup_monoset eventually_sequentially
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   475
    by (intro complete_lattice_class.Sup_upper) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   476
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   477
  assume "x0 \<le> liminf x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   478
  { fix S :: "extreal set" assume om: "open S & mono S & x0:S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   479
    { assume "S = UNIV" hence "EX N. (ALL n>=N. x n : S)" by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   480
    moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   481
    { assume "~(S=UNIV)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   482
      then obtain B where B_def: "S = {B<..}" using om extreal_open_mono_set by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   483
      hence "B<x0" using om by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   484
      hence "EX N. ALL n>=N. x n : S" unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   485
    } ultimately have "EX N. (ALL n>=N. x n : S)" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   486
  } then show "?P x0" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   487
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   488
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   489
lemma limsup_subseq_mono:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   490
  fixes X :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   491
  assumes "subseq r"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   492
  shows "limsup (X \<circ> r) \<le> limsup X"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   493
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   494
  have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   495
  then have "- limsup X \<le> - limsup (X \<circ> r)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   496
     using liminf_subseq_mono[of r "(%n. - X n)"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   497
       extreal_Liminf_uminus[of sequentially X]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   498
       extreal_Liminf_uminus[of sequentially "X o r"] assms by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   499
  then show ?thesis by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   500
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   501
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   502
lemma bounded_abs:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   503
  assumes "(a::real)<=x" "x<=b"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   504
  shows "abs x <= max (abs a) (abs b)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   505
by (metis abs_less_iff assms leI le_max_iff_disj less_eq_real_def less_le_not_le less_minus_iff minus_minus)
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 bounded_increasing_convergent2: fixes f::"nat => real"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   508
  assumes "ALL n. f n <= B"  "ALL n m. n>=m --> f n >= f m"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   509
  shows "EX l. (f ---> l) sequentially"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   510
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   511
def N == "max (abs (f 0)) (abs B)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   512
{ fix n have "abs (f n) <= N" unfolding N_def apply (subst bounded_abs) using assms by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   513
hence "bounded {f n| n::nat. True}" unfolding bounded_real by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   514
from this show ?thesis apply(rule Topology_Euclidean_Space.bounded_increasing_convergent)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   515
   using assms by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   516
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   517
lemma lim_extreal_increasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   518
  obtains l where "f ----> (l::extreal)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   519
proof(cases "f = (\<lambda>x. - \<infinity>)")
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   520
  case True then show thesis using Lim_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   521
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   522
  case False
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   523
  from this obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   524
  have "ALL n>=N. f n >= f N" using assms by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   525
  hence minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   526
  def Y == "(%n. (if n>=N then f n else f N))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   527
  hence incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   528
  from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   529
  show thesis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   530
  proof(cases "EX B. ALL n. f n < extreal B")
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   531
    case False thus thesis apply- apply(rule that[of \<infinity>]) unfolding Lim_PInfty not_ex not_all
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   532
    apply safe apply(erule_tac x=B in allE,safe) apply(rule_tac x=x in exI,safe)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   533
    apply(rule order_trans[OF _ assms[rule_format]]) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   534
  next case True then guess B ..
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   535
    hence "ALL n. Y n < extreal B" using Y_def by auto note B = this[rule_format]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   536
    { fix n have "Y n < \<infinity>" using B[of n] apply (subst less_le_trans) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   537
      hence "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   538
    } hence *: "ALL n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   539
    { fix n have "real (Y n) < B" proof- case goal1 thus ?case
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   540
        using B[of n] apply-apply(subst(asm) extreal_real'[THEN sym]) defer defer
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   541
        unfolding extreal_less using * by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   542
      qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   543
    }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   544
    hence B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   545
    have "EX l. (%n. real (Y n)) ----> l"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   546
      apply(rule bounded_increasing_convergent2)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   547
    proof safe show "!!n. real (Y n) <= B" using B' by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   548
      fix n m::nat assume "n<=m"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   549
      hence "extreal (real (Y n)) <= extreal (real (Y m))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   550
        using incy[rule_format,of n m] apply(subst extreal_real)+
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   551
        using *[rule_format, of n] *[rule_format, of m] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   552
      thus "real (Y n) <= real (Y m)" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   553
    qed then guess l .. note l=this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   554
    have "Y ----> extreal l" using l apply-apply(subst(asm) lim_extreal[THEN sym])
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   555
    unfolding extreal_real using * by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   556
    thus thesis apply-apply(rule that[of "extreal l"])
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   557
       apply (subst tail_same_limit[of Y _ N]) using Y_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   558
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   559
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   560
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   561
lemma lim_extreal_decreasing: assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   562
  obtains l where "f ----> (l::extreal)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   563
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   564
  from lim_extreal_increasing[of "\<lambda>x. - f x"] assms
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   565
  obtain l where "(\<lambda>x. - f x) ----> l" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   566
  from extreal_lim_mult[OF this, of "- 1"] show thesis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   567
    by (intro that[of "-l"]) (simp add: extreal_uminus_eq_reorder)
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
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   570
lemma compact_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   571
  fixes X :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   572
  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   573
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   574
  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   575
    using seq_monosub[of X] unfolding comp_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   576
  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)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   577
    by (auto simp add: monoseq_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   578
  then obtain l where "(X\<circ>r) ----> l"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   579
     using lim_extreal_increasing[of "X \<circ> r"] lim_extreal_decreasing[of "X \<circ> r"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   580
  then show ?thesis using `subseq r` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   581
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   582
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   583
lemma extreal_Sup_lim:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   584
  assumes "\<And>n. b n \<in> s" "b ----> (a::extreal)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   585
  shows "a \<le> Sup s"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   586
by (metis Lim_bounded_extreal assms complete_lattice_class.Sup_upper)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   587
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   588
lemma extreal_Inf_lim:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   589
  assumes "\<And>n. b n \<in> s" "b ----> (a::extreal)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   590
  shows "Inf s \<le> a"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   591
by (metis Lim_bounded2_extreal assms complete_lattice_class.Inf_lower)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   592
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   593
lemma SUP_Lim_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   594
  fixes X :: "nat \<Rightarrow> extreal" assumes "incseq X" "X ----> l" shows "(SUP n. X n) = l"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   595
proof (rule extreal_SUPI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   596
  fix n from assms show "X n \<le> l"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   597
    by (intro incseq_le_extreal) (simp add: incseq_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   598
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   599
  fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   600
  with extreal_Sup_lim[OF _ `X ----> l`, of "{..y}"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   601
  show "l \<le> y" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   602
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   603
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   604
lemma LIMSEQ_extreal_SUPR:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   605
  fixes X :: "nat \<Rightarrow> extreal" assumes "incseq X" shows "X ----> (SUP n. X n)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   606
proof (rule lim_extreal_increasing)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   607
  fix n m :: nat assume "m \<le> n" then show "X m \<le> X n"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   608
    using `incseq X` by (simp add: incseq_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   609
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   610
  fix l assume "X ----> l"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   611
  with SUP_Lim_extreal[of X, OF assms this] show ?thesis by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   612
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   613
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   614
lemma INF_Lim_extreal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::extreal)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   615
  using SUP_Lim_extreal[of "\<lambda>i. - X i" "- l"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   616
  by (simp add: extreal_SUPR_uminus extreal_lim_uminus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   617
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   618
lemma LIMSEQ_extreal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: extreal)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   619
  using LIMSEQ_extreal_SUPR[of "\<lambda>i. - X i"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   620
  by (simp add: extreal_SUPR_uminus extreal_lim_uminus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   621
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   622
lemma SUP_eq_LIMSEQ:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   623
  assumes "mono f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   624
  shows "(SUP n. extreal (f n)) = extreal x \<longleftrightarrow> f ----> x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   625
proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   626
  have inc: "incseq (\<lambda>i. extreal (f i))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   627
    using `mono f` unfolding mono_def incseq_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   628
  { assume "f ----> x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   629
   then have "(\<lambda>i. extreal (f i)) ----> extreal x" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   630
   from SUP_Lim_extreal[OF inc this]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   631
   show "(SUP n. extreal (f n)) = extreal x" . }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   632
  { assume "(SUP n. extreal (f n)) = extreal x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   633
    with LIMSEQ_extreal_SUPR[OF inc]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   634
    show "f ----> x" by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   635
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   636
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   637
lemma Liminf_within:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   638
  fixes f :: "'a::metric_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   639
  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   640
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   641
let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   642
{ fix T assume T_def: "open T & mono T & ?l:T"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   643
  have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   644
  proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   645
  { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   646
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   647
  { assume "~(T=UNIV)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   648
    then obtain B where "T={B<..}" using T_def extreal_open_mono_set[of T] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   649
    hence "B<?l" using T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   650
    then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   651
      unfolding less_SUP_iff by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   652
    { fix y assume "y:S & 0 < dist y x & dist y x < d"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   653
      hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   654
      hence "f y:T" using d_def INF_leI[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   655
    } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   656
  } ultimately show ?thesis by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   657
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   658
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   659
moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   660
{ fix z
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   661
  assume a: "ALL T. open T --> mono T --> z : T -->
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   662
     (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   663
  { fix B assume "B<z"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   664
    then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   665
       using a[rule_format, of "{B<..}"] mono_greaterThan by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   666
    { fix y assume "y:(S Int ball x d - {x})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   667
      hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   668
         by (metis dist_eq_0_iff real_less_def zero_le_dist)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   669
      hence "B <= f y" using d_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   670
    } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst le_INFI) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   671
    also have "...<=?l" apply (subst le_SUPI) using d_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   672
    finally have "B<=?l" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   673
  } hence "z <= ?l" using extreal_le_extreal[of z "?l"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   674
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   675
ultimately show ?thesis unfolding extreal_Liminf_Sup_monoset eventually_within
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   676
   apply (subst extreal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"]) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   677
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   678
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   679
lemma Limsup_within:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   680
  fixes f :: "'a::metric_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   681
  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   682
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   683
let ?l="(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   684
{ fix T assume T_def: "open T & mono (uminus ` T) & ?l:T"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   685
  have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   686
  proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   687
  { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   688
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   689
  { assume "~(T=UNIV)" hence "~(uminus ` T = UNIV)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   690
       by (metis Int_UNIV_right Int_absorb1 image_mono extreal_minus_minus_image subset_UNIV)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   691
    hence "uminus ` T = {Inf (uminus ` T)<..}" using T_def extreal_open_mono_set[of "uminus ` T"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   692
       extreal_open_uminus[of T] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   693
    then obtain B where "T={..<B}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   694
      unfolding extreal_Inf_uminus_image_eq extreal_uminus_lessThan[symmetric]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   695
      unfolding inj_image_eq_iff[OF extreal_inj_on_uminus] by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   696
    hence "?l<B" using T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   697
    then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   698
      unfolding INF_less_iff by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   699
    { fix y assume "y:S & 0 < dist y x & dist y x < d"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   700
      hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   701
      hence "f y:T" using d_def le_SUPI[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   702
    } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   703
  } ultimately show ?thesis by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   704
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   705
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   706
moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   707
{ fix z
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   708
  assume a: "ALL T. open T --> mono (uminus ` T) --> z : T -->
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   709
     (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   710
  { fix B assume "z<B"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   711
    then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   712
       using a[rule_format, of "{..<B}"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   713
    { fix y assume "y:(S Int ball x d - {x})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   714
      hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   715
         by (metis dist_eq_0_iff real_less_def zero_le_dist)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   716
      hence "f y <= B" using d_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   717
    } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_leI) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   718
    moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_leI) using d_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   719
    ultimately have "?l<=B" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   720
  } hence "?l <= z" using extreal_ge_extreal[of z "?l"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   721
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   722
ultimately show ?thesis unfolding extreal_Limsup_Inf_monoset eventually_within
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   723
   apply (subst extreal_InfI) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   724
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   725
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   726
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   727
lemma Liminf_within_UNIV:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   728
  fixes f :: "'a::metric_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   729
  shows "Liminf (at x) f = Liminf (at x within UNIV) f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   730
by (metis within_UNIV)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   731
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   732
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   733
lemma Liminf_at:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   734
  fixes f :: "'a::metric_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   735
  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   736
using Liminf_within[of x UNIV f] Liminf_within_UNIV[of x f] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   737
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   738
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   739
lemma Limsup_within_UNIV:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   740
  fixes f :: "'a::metric_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   741
  shows "Limsup (at x) f = Limsup (at x within UNIV) f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   742
by (metis within_UNIV)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   743
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   744
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   745
lemma Limsup_at:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   746
  fixes f :: "'a::metric_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   747
  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   748
using Limsup_within[of x UNIV f] Limsup_within_UNIV[of x f] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   749
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   750
lemma Lim_within_constant:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   751
  fixes f :: "'a::metric_space => 'b::topological_space"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   752
  assumes "ALL y:S. f y = C"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   753
  shows "(f ---> C) (at x within S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   754
unfolding tendsto_def eventually_within
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   755
by (metis assms(1) linorder_le_less_linear n_not_Suc_n real_of_nat_le_zero_cancel_iff)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   756
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   757
lemma Liminf_within_constant:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   758
  fixes f :: "'a::metric_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   759
  assumes "ALL y:S. f y = C"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   760
  assumes "~trivial_limit (at x within S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   761
  shows "Liminf (at x within S) f = C"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   762
by (metis Lim_within_constant assms lim_imp_Liminf)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   763
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   764
lemma Limsup_within_constant:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   765
  fixes f :: "'a::metric_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   766
  assumes "ALL y:S. f y = C"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   767
  assumes "~trivial_limit (at x within S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   768
  shows "Limsup (at x within S) f = C"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   769
by (metis Lim_within_constant assms lim_imp_Limsup)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   770
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   771
lemma islimpt_punctured:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   772
"x islimpt S = x islimpt (S-{x})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   773
unfolding islimpt_def by blast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   774
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   775
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   776
lemma islimpt_in_closure:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   777
"(x islimpt S) = (x:closure(S-{x}))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   778
unfolding closure_def using islimpt_punctured by blast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   779
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   780
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   781
lemma not_trivial_limit_within:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   782
  "~trivial_limit (at x within S) = (x:closure(S-{x}))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   783
using islimpt_in_closure by (metis trivial_limit_within)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   784
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   785
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   786
lemma not_trivial_limit_within_ball:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   787
  "(~trivial_limit (at x within S)) = (ALL e>0. S Int ball x e - {x} ~= {})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   788
  (is "?lhs = ?rhs")
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   789
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   790
{ assume "?lhs"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   791
  { fix e :: real assume "e>0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   792
    then obtain y where "y:(S-{x}) & dist y x < e"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   793
       using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   794
    hence "y : (S Int ball x e - {x})" unfolding ball_def by (simp add: dist_commute)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   795
    hence "S Int ball x e - {x} ~= {}" by blast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   796
  } hence "?rhs" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   797
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   798
moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   799
{ assume "?rhs"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   800
  { fix e :: real assume "e>0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   801
    then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   802
    hence "y:(S-{x}) & dist y x < e" unfolding ball_def by (simp add: dist_commute)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   803
    hence "EX y:(S-{x}). dist y x < e" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   804
  } hence "?lhs" using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   805
} ultimately show ?thesis by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   806
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   807
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   808
subsubsection {* Continuity *}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   809
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   810
lemma continuous_imp_tendsto:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   811
  assumes "continuous (at x0) f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   812
  assumes "x ----> x0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   813
  shows "(f o x) ----> (f x0)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   814
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   815
{ fix S assume "open S & (f x0):S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   816
  from this obtain T where T_def: "open T & x0 : T & (ALL x:T. f x : S)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   817
     using assms continuous_at_open by metis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   818
  hence "(EX N. ALL n>=N. x n : T)" using assms tendsto_explicit T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   819
  hence "(EX N. ALL n>=N. f(x n) : S)" using T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   820
} from this show ?thesis using tendsto_explicit[of "f o x" "f x0"] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   821
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   822
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   823
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   824
lemma continuous_at_sequentially2:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   825
fixes f :: "'a::metric_space => 'b:: topological_space"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   826
shows "continuous (at x0) f <-> (ALL x. (x ----> x0) --> (f o x) ----> (f x0))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   827
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   828
{ assume "~(continuous (at x0) f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   829
  from this obtain T where T_def:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   830
     "open T & f x0 : T & (ALL S. (open S & x0 : S) --> (EX x':S. f x' ~: T))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   831
     using continuous_at_open[of x0 f] by metis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   832
  def X == "{x'. f x' ~: T}" hence "x0 islimpt X" unfolding islimpt_def using T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   833
  from this obtain x where x_def: "(ALL n. x n : X) & x ----> x0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   834
     using islimpt_sequential[of x0 X] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   835
  hence "~(f o x) ----> (f x0)" unfolding tendsto_explicit using X_def T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   836
  hence "EX x. x ----> x0 & (~(f o x) ----> (f x0))" using x_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   837
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   838
from this show ?thesis using continuous_imp_tendsto by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   839
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   840
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   841
lemma continuous_at_of_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   842
  fixes x0 :: extreal
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   843
  assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   844
  shows "continuous (at x0) real"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   845
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   846
{ fix T assume T_def: "open T & real x0 : T"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   847
  def S == "extreal ` T"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   848
  hence "extreal (real x0) : S" using T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   849
  hence "x0 : S" using assms extreal_real by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   850
  moreover have "open S" using open_extreal S_def T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   851
  moreover have "ALL y:S. real y : T" using S_def T_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   852
  ultimately have "EX S. x0 : S & open S & (ALL y:S. real y : T)" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   853
} from this show ?thesis unfolding continuous_at_open by blast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   854
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   855
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   856
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   857
lemma continuous_at_iff_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   858
fixes f :: "'a::t2_space => real"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   859
shows "continuous (at x0) f <-> continuous (at x0) (extreal o f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   860
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   861
{ assume "continuous (at x0) f" hence "continuous (at x0) (extreal o f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   862
     using continuous_at_extreal continuous_at_compose[of x0 f extreal] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   863
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   864
moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   865
{ assume "continuous (at x0) (extreal o f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   866
  hence "continuous (at x0) (real o (extreal o f))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   867
     using continuous_at_of_extreal by (intro continuous_at_compose[of x0 "extreal o f"]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   868
  moreover have "real o (extreal o f) = f" using real_extreal_id by (simp add: o_assoc)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   869
  ultimately have "continuous (at x0) f" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   870
} ultimately show ?thesis by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   871
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   872
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   873
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   874
lemma continuous_on_iff_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   875
fixes f :: "'a::t2_space => real"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   876
fixes A assumes "open A"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   877
shows "continuous_on A f <-> continuous_on A (extreal o f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   878
   using continuous_at_iff_extreal assms by (auto simp add: continuous_on_eq_continuous_at)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   879
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   880
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   881
lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>)}) real"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   882
   using continuous_at_of_extreal continuous_on_eq_continuous_at open_image_extreal by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   883
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   884
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   885
lemma continuous_on_iff_real:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   886
  fixes f :: "'a::t2_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   887
  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
   888
  shows "continuous_on A f \<longleftrightarrow> continuous_on A (real \<circ> f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   889
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   890
  have "f ` A <= UNIV-{\<infinity>,(-\<infinity>)}" using assms by force
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   891
  hence *: "continuous_on (f ` A) real"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   892
     using continuous_on_real by (simp add: continuous_on_subset)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   893
have **: "continuous_on ((real o f) ` A) extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   894
   using continuous_on_extreal continuous_on_subset[of "UNIV" "extreal" "(real o f) ` A"] by blast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   895
{ assume "continuous_on A f" hence "continuous_on A (real o f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   896
  apply (subst continuous_on_compose) using * by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   897
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   898
moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   899
{ assume "continuous_on A (real o f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   900
  hence "continuous_on A (extreal o (real o f))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   901
     apply (subst continuous_on_compose) using ** by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   902
  hence "continuous_on A f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   903
     apply (subst continuous_on_eq[of A "extreal o (real o f)" f])
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   904
     using assms extreal_real by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   905
}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   906
ultimately show ?thesis by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   907
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   908
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   909
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   910
lemma continuous_at_const:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   911
  fixes f :: "'a::t2_space => extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   912
  assumes "ALL x. (f x = C)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   913
  shows "ALL x. continuous (at x) f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   914
unfolding continuous_at_open using assms t1_space by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   915
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   916
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   917
lemma closure_contains_Inf:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   918
  fixes S :: "real set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   919
  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   920
  shows "Inf S : closure S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   921
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   922
have *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] assms by metis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   923
{ fix e assume "e>(0 :: real)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   924
  from this obtain x where x_def: "x:S & x < Inf S + e" using Inf_close `S ~= {}` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   925
  moreover hence "x > Inf S - e" using * by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   926
  ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   927
  hence "EX x:S. abs (x - Inf S) < e" using x_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   928
} from this show ?thesis apply (subst closure_approachable) unfolding dist_norm by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   929
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   930
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   931
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   932
lemma closed_contains_Inf:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   933
  fixes S :: "real set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   934
  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   935
  assumes "closed S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   936
  shows "Inf S : S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   937
by (metis closure_contains_Inf closure_closed assms)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   938
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   939
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   940
lemma mono_closed_real:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   941
  fixes S :: "real set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   942
  assumes mono: "ALL y z. y:S & y<=z --> z:S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   943
  assumes "closed S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   944
  shows "S = {} | S = UNIV | (EX a. S = {a ..})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   945
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   946
{ assume "S ~= {}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   947
  { assume ex: "EX B. ALL x:S. B<=x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   948
    hence *: "ALL x:S. Inf S <= x" using Inf_lower_EX[of _ S] ex by metis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   949
    hence "Inf S : S" apply (subst closed_contains_Inf) using ex `S ~= {}` `closed S` by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   950
    hence "ALL x. (Inf S <= x <-> x:S)" using mono[rule_format, of "Inf S"] * by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   951
    hence "S = {Inf S ..}" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   952
    hence "EX a. S = {a ..}" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   953
  }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   954
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   955
  { assume "~(EX B. ALL x:S. B<=x)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   956
    hence nex: "ALL B. EX x:S. x<B" by (simp add: not_le)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   957
    { fix y obtain x where "x:S & x < y" using nex by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   958
      hence "y:S" using mono[rule_format, of x y] by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   959
    } hence "S = UNIV" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   960
  } ultimately have "S = UNIV | (EX a. S = {a ..})" by blast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   961
} from this show ?thesis by blast
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   962
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   963
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   964
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   965
lemma mono_closed_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   966
  fixes S :: "real set"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   967
  assumes mono: "ALL y z. y:S & y<=z --> z:S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   968
  assumes "closed S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   969
  shows "EX a. S = {x. a <= extreal x}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   970
proof-
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   971
{ assume "S = {}" hence ?thesis apply(rule_tac x=PInfty in exI) by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   972
moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   973
{ assume "S = UNIV" hence ?thesis apply(rule_tac x="-\<infinity>" in exI) by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   974
moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   975
{ assume "EX a. S = {a ..}"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   976
  from this obtain a where "S={a ..}" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   977
  hence ?thesis apply(rule_tac x="extreal a" in exI) by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   978
} ultimately show ?thesis using mono_closed_real[of S] assms by auto
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
subsection {* Sums *}
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   982
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   983
lemma setsum_extreal[simp]:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   984
  "(\<Sum>x\<in>A. extreal (f x)) = extreal (\<Sum>x\<in>A. f x)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   985
proof cases
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   986
  assume "finite A" then show ?thesis by induct auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   987
qed simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   988
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   989
lemma setsum_Pinfty: "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   990
proof safe
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   991
  assume *: "setsum f P = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   992
  show "finite P"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   993
  proof (rule ccontr) assume "infinite P" with * show False by auto qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   994
  show "\<exists>i\<in>P. f i = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   995
  proof (rule ccontr)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   996
    assume "\<not> ?thesis" then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   997
    from `finite P` this have "setsum f P \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   998
      by induct auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
   999
    with * show False by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1000
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1001
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1002
  fix i assume "finite P" "i \<in> P" "f i = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1003
  thus "setsum f P = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1004
  proof induct
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1005
    case (insert x A)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1006
    show ?case using insert by (cases "x = i") auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1007
  qed simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1008
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1009
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1010
lemma setsum_Inf:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1011
  shows "\<bar>setsum f A\<bar> = \<infinity> \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1012
proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1013
  assume *: "\<bar>setsum f A\<bar> = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1014
  have "finite A" by (rule ccontr) (insert *, auto)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1015
  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
  1016
  proof (rule ccontr)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1017
    assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = extreal r" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1018
    from bchoice[OF this] guess r ..
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1019
    with * show False by (auto simp: setsum_extreal)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1020
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1021
  ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1022
next
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1023
  assume "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1024
  then obtain i where "finite A" "i \<in> A" "\<bar>f i\<bar> = \<infinity>" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1025
  then show "\<bar>setsum f A\<bar> = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1026
  proof induct
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1027
    case (insert j A) then show ?case
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1028
      by (cases rule: extreal3_cases[of "f i" "f j" "setsum f A"]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1029
  qed simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1030
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1031
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41980
diff changeset
  1032
lemma setsum_real_of_extreal:
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1033
  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
  1034
  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
  1035
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1036
  have "\<forall>x\<in>S. \<exists>r. f x = extreal r"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1037
  proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1038
    fix x assume "x \<in> S"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1039
    from assms[OF this] show "\<exists>r. f x = extreal r" by (cases "f x") auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1040
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1041
  from bchoice[OF this] guess r ..
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1042
  then show ?thesis by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1043
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1044
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1045
lemma setsum_extreal_0:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1046
  fixes f :: "'a \<Rightarrow> extreal" assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1047
  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
  1048
proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1049
  assume *: "(\<Sum>x\<in>A. f x) = 0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1050
  then have "(\<Sum>x\<in>A. f x) \<noteq> \<infinity>" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1051
  then have "\<forall>i\<in>A. \<bar>f i\<bar> \<noteq> \<infinity>" using assms by (force simp: setsum_Pinfty)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1052
  then have "\<forall>i\<in>A. \<exists>r. f i = extreal r" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1053
  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
  1054
    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
  1055
qed (rule setsum_0')
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1056
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1057
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1058
lemma setsum_extreal_right_distrib:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1059
  fixes f :: "'a \<Rightarrow> extreal" assumes "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1060
  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
  1061
proof cases
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1062
  assume "finite A" then show ?thesis using assms
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1063
    by induct (auto simp: extreal_right_distrib setsum_nonneg)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1064
qed simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1065
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1066
lemma sums_extreal_positive:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1067
  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" shows "f sums (SUP n. \<Sum>i<n. f i)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1068
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1069
  have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1070
    using extreal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1071
  from LIMSEQ_extreal_SUPR[OF this]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1072
  show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1073
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1074
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1075
lemma summable_extreal_pos:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1076
  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" shows "summable f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1077
  using sums_extreal_positive[of f, OF assms] unfolding summable_def by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1078
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1079
lemma suminf_extreal_eq_SUPR:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1080
  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1081
  shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1082
  using sums_extreal_positive[of f, OF assms, THEN sums_unique] by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1083
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1084
lemma sums_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1085
  "(\<lambda>x. extreal (f x)) sums extreal x \<longleftrightarrow> f sums x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1086
  unfolding sums_def by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1087
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1088
lemma suminf_bound:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1089
  fixes f :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1090
  assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x" and pos: "\<And>n. 0 \<le> f n"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1091
  shows "suminf f \<le> x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1092
proof (rule Lim_bounded_extreal)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1093
  have "summable f" using pos[THEN summable_extreal_pos] .
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1094
  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
  1095
    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1096
  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
  1097
    using assms by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1098
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1099
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1100
lemma suminf_bound_add:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1101
  fixes f :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1102
  assumes "\<forall>N. (\<Sum>n<N. f n) + y \<le> x" and pos: "\<And>n. 0 \<le> f n" and "y \<noteq> -\<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1103
  shows "suminf f + y \<le> x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1104
proof (cases y)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1105
  case (real r) then have "\<forall>N. (\<Sum>n<N. f n) \<le> x - y"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1106
    using assms by (simp add: extreal_le_minus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1107
  then have "(\<Sum> n. f n) \<le> x - y" using pos by (rule suminf_bound)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1108
  then show "(\<Sum> n. f n) + y \<le> x"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1109
    using assms real by (simp add: extreal_le_minus)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1110
qed (insert assms, auto)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1111
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1112
lemma sums_finite:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1113
  assumes "\<forall>N\<ge>n. f N = 0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1114
  shows "f sums (\<Sum>N<n. f N)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1115
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1116
  { fix i have "(\<Sum>N<i + n. f N) = (\<Sum>N<n. f N)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1117
      by (induct i) (insert assms, auto) }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1118
  note this[simp]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1119
  show ?thesis unfolding sums_def
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1120
    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1121
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1122
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1123
lemma suminf_finite:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1124
  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}" assumes "\<forall>N\<ge>n. f N = 0"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1125
  shows "suminf f = (\<Sum>N<n. f N)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1126
  using sums_finite[OF assms, THEN sums_unique] by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1127
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1128
lemma suminf_extreal_0[simp]: "(\<Sum>i. 0) = (0::'a::{comm_monoid_add,t2_space})"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1129
  using suminf_finite[of 0 "\<lambda>x. 0"] by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1130
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1131
lemma suminf_upper:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1132
  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>n. 0 \<le> f n"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1133
  shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1134
  unfolding suminf_extreal_eq_SUPR[OF assms] SUPR_def
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1135
  by (auto intro: complete_lattice_class.Sup_upper image_eqI)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1136
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1137
lemma suminf_0_le:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1138
  fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>n. 0 \<le> f n"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1139
  shows "0 \<le> (\<Sum>n. f n)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1140
  using suminf_upper[of f 0, OF assms] by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1141
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1142
lemma suminf_le_pos:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1143
  fixes f g :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1144
  assumes "\<And>N. f N \<le> g N" "\<And>N. 0 \<le> f N"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1145
  shows "suminf f \<le> suminf g"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1146
proof (safe intro!: suminf_bound)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1147
  fix n { fix N have "0 \<le> g N" using assms(2,1)[of N] by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1148
  have "setsum f {..<n} \<le> setsum g {..<n}" using assms by (auto intro: setsum_mono)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1149
  also have "... \<le> suminf g" using `\<And>N. 0 \<le> g N` by (rule suminf_upper)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1150
  finally show "setsum f {..<n} \<le> suminf g" .
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1151
qed (rule assms(2))
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1152
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1153
lemma suminf_half_series_extreal: "(\<Sum>n. (1/2 :: extreal)^Suc n) = 1"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1154
  using sums_extreal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1155
  by (simp add: one_extreal_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1156
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1157
lemma suminf_add_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1158
  fixes f g :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1159
  assumes "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1160
  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
  1161
  apply (subst (1 2 3) suminf_extreal_eq_SUPR)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1162
  unfolding setsum_addf
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1163
  by (intro assms extreal_add_nonneg_nonneg SUPR_extreal_add_pos incseq_setsumI setsum_nonneg ballI)+
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1164
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1165
lemma suminf_cmult_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1166
  fixes f g :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1167
  assumes "\<And>i. 0 \<le> f i" "0 \<le> a"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1168
  shows "(\<Sum>i. a * f i) = a * suminf f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1169
  by (auto simp: setsum_extreal_right_distrib[symmetric] assms
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1170
                 extreal_zero_le_0_iff setsum_nonneg suminf_extreal_eq_SUPR
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1171
           intro!: SUPR_extreal_cmult )
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1172
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1173
lemma suminf_PInfty:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1174
  assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1175
  shows "f i \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1176
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1177
  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1178
  have "(\<Sum>i<Suc i. f i) \<noteq> \<infinity>" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1179
  then show ?thesis
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1180
    unfolding setsum_Pinfty by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1181
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1182
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1183
lemma suminf_PInfty_fun:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1184
  assumes "\<And>i. 0 \<le> f i" "suminf f \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1185
  shows "\<exists>f'. f = (\<lambda>x. extreal (f' x))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1186
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1187
  have "\<forall>i. \<exists>r. f i = extreal r"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1188
  proof
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1189
    fix i show "\<exists>r. f i = extreal r"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1190
      using suminf_PInfty[OF assms] assms(1)[of i] by (cases "f i") auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1191
  qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1192
  from choice[OF this] show ?thesis by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1193
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1194
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1195
lemma summable_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1196
  assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. extreal (f i)) \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1197
  shows "summable f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1198
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1199
  have "0 \<le> (\<Sum>i. extreal (f i))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1200
    using assms by (intro suminf_0_le) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1201
  with assms obtain r where r: "(\<Sum>i. extreal (f i)) = extreal r"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1202
    by (cases "\<Sum>i. extreal (f i)") auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1203
  from summable_extreal_pos[of "\<lambda>x. extreal (f x)"]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1204
  have "summable (\<lambda>x. extreal (f x))" using assms by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1205
  from summable_sums[OF this]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1206
  have "(\<lambda>x. extreal (f x)) sums (\<Sum>x. extreal (f x))" by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1207
  then show "summable f"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1208
    unfolding r sums_extreal summable_def ..
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1209
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1210
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1211
lemma suminf_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1212
  assumes "\<And>i. 0 \<le> f i" "(\<Sum>i. extreal (f i)) \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1213
  shows "(\<Sum>i. extreal (f i)) = extreal (suminf f)"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1214
proof (rule sums_unique[symmetric])
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1215
  from summable_extreal[OF assms]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1216
  show "(\<lambda>x. extreal (f x)) sums (extreal (suminf f))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1217
    unfolding sums_extreal using assms by (intro summable_sums summable_extreal)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1218
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1219
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1220
lemma suminf_extreal_minus:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1221
  fixes f g :: "nat \<Rightarrow> extreal"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1222
  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>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1223
  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
  1224
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1225
  { fix i have "0 \<le> f i" using ord[of i] by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1226
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1227
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> f i` fin(1)] guess f' .. note this[simp]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1228
  from suminf_PInfty_fun[OF `\<And>i. 0 \<le> g i` fin(2)] guess g' .. note this[simp]
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1229
  { fix i have "0 \<le> f i - g i" using ord[of i] by (auto simp: extreal_le_minus_iff) }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1230
  moreover
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1231
  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
  1232
    using assms by (auto intro!: suminf_le_pos simp: field_simps)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1233
  then have "suminf (\<lambda>i. f i - g i) \<noteq> \<infinity>" using fin by auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1234
  ultimately show ?thesis using assms `\<And>i. 0 \<le> f i`
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1235
    apply simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1236
    by (subst (1 2 3) suminf_extreal)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1237
       (auto intro!: suminf_diff[symmetric] summable_extreal)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1238
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1239
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1240
lemma suminf_extreal_PInf[simp]:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1241
  "(\<Sum>x. \<infinity>) = \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1242
proof -
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1243
  have "(\<Sum>i<Suc 0. \<infinity>) \<le> (\<Sum>x. \<infinity>)" by (rule suminf_upper) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1244
  then show ?thesis by simp
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1245
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1246
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1247
lemma summable_real_of_extreal:
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1248
  assumes f: "\<And>i. 0 \<le> f i" and fin: "(\<Sum>i. f i) \<noteq> \<infinity>"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1249
  shows "summable (\<lambda>i. real (f i))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1250
proof (rule summable_def[THEN iffD2])
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1251
  have "0 \<le> (\<Sum>i. f i)" using assms by (auto intro: suminf_0_le)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1252
  with fin obtain r where r: "extreal r = (\<Sum>i. f i)" by (cases "(\<Sum>i. f i)") auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1253
  { fix i have "f i \<noteq> \<infinity>" using f by (intro suminf_PInfty[OF _ fin]) auto
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1254
    then have "\<bar>f i\<bar> \<noteq> \<infinity>" using f[of i] by auto }
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1255
  note fin = this
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1256
  have "(\<lambda>i. extreal (real (f i))) sums (\<Sum>i. extreal (real (f i)))"
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1257
    using f by (auto intro!: summable_extreal_pos summable_sums simp: extreal_le_real_iff zero_extreal_def)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1258
  also have "\<dots> = extreal r" using fin r by (auto simp: extreal_real)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1259
  finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_extreal)
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1260
qed
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1261
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
diff changeset
  1262
end