src/HOL/Analysis/Set_Integral.thy
author wenzelm
Tue Jan 17 13:59:10 2017 +0100 (2017-01-17)
changeset 64911 f0e07600de47
parent 64284 f3b905b2eee2
child 66164 2d79288b042c
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 (*  Title:      HOL/Analysis/Set_Integral.thy
     2     Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
     3     Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
     4 
     5 Notation and useful facts for working with integrals over a set.
     6 
     7 TODO: keep all these? Need unicode translations as well.
     8 *)
     9 
    10 theory Set_Integral
    11   imports Radon_Nikodym
    12 begin
    13 
    14 lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" (* COPIED FROM Permutations *)
    15   using surj_f_inv_f[of p] by (auto simp add: bij_def)
    16 
    17 subsection \<open>Fun.thy\<close>
    18 
    19 lemma inj_fn:
    20   fixes f::"'a \<Rightarrow> 'a"
    21   assumes "inj f"
    22   shows "inj (f^^n)"
    23 proof (induction n)
    24   case (Suc n)
    25   have "inj (f o (f^^n))"
    26     using inj_comp[OF assms Suc.IH] by simp
    27   then show "inj (f^^(Suc n))"
    28     by auto
    29 qed (auto)
    30 
    31 lemma surj_fn:
    32   fixes f::"'a \<Rightarrow> 'a"
    33   assumes "surj f"
    34   shows "surj (f^^n)"
    35 proof (induction n)
    36   case (Suc n)
    37   have "surj (f o (f^^n))"
    38     using assms Suc.IH by (simp add: comp_surj)
    39   then show "surj (f^^(Suc n))"
    40     by auto
    41 qed (auto)
    42 
    43 lemma bij_fn:
    44   fixes f::"'a \<Rightarrow> 'a"
    45   assumes "bij f"
    46   shows "bij (f^^n)"
    47 by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]])
    48 
    49 lemma inv_fn_o_fn_is_id:
    50   fixes f::"'a \<Rightarrow> 'a"
    51   assumes "bij f"
    52   shows "((inv f)^^n) o (f^^n) = (\<lambda>x. x)"
    53 proof -
    54   have "((inv f)^^n)((f^^n) x) = x" for x n
    55   proof (induction n)
    56     case (Suc n)
    57     have *: "(inv f) (f y) = y" for y
    58       by (simp add: assms bij_is_inj)
    59     have "(inv f ^^ Suc n) ((f ^^ Suc n) x) = (inv f^^n) (inv f (f ((f^^n) x)))"
    60       by (simp add: funpow_swap1)
    61     also have "... = (inv f^^n) ((f^^n) x)"
    62       using * by auto
    63     also have "... = x" using Suc.IH by auto
    64     finally show ?case by simp
    65   qed (auto)
    66   then show ?thesis unfolding o_def by blast
    67 qed
    68 
    69 lemma fn_o_inv_fn_is_id:
    70   fixes f::"'a \<Rightarrow> 'a"
    71   assumes "bij f"
    72   shows "(f^^n) o ((inv f)^^n) = (\<lambda>x. x)"
    73 proof -
    74   have "(f^^n) (((inv f)^^n) x) = x" for x n
    75   proof (induction n)
    76     case (Suc n)
    77     have *: "f(inv f y) = y" for y
    78       using assms by (meson bij_inv_eq_iff)
    79     have "(f ^^ Suc n) ((inv f ^^ Suc n) x) = (f^^n) (f (inv f ((inv f^^n) x)))"
    80       by (simp add: funpow_swap1)
    81     also have "... = (f^^n) ((inv f^^n) x)"
    82       using * by auto
    83     also have "... = x" using Suc.IH by auto
    84     finally show ?case by simp
    85   qed (auto)
    86   then show ?thesis unfolding o_def by blast
    87 qed
    88 
    89 lemma inv_fn:
    90   fixes f::"'a \<Rightarrow> 'a"
    91   assumes "bij f"
    92   shows "inv (f^^n) = ((inv f)^^n)"
    93 proof -
    94   have "inv (f^^n) x = ((inv f)^^n) x" for x
    95   apply (rule inv_into_f_eq, auto simp add: inj_fn[OF bij_is_inj[OF assms]])
    96   using fn_o_inv_fn_is_id[OF assms, of n] by (metis comp_apply)
    97   then show ?thesis by auto
    98 qed
    99 
   100 
   101 lemma mono_inv:
   102   fixes f::"'a::linorder \<Rightarrow> 'b::linorder"
   103   assumes "mono f" "bij f"
   104   shows "mono (inv f)"
   105 proof
   106   fix x y::'b assume "x \<le> y"
   107   then show "inv f x \<le> inv f y"
   108     by (metis (no_types, lifting) assms bij_is_surj eq_iff le_cases mono_def surj_f_inv_f)
   109 qed
   110 
   111 lemma mono_bij_Inf:
   112   fixes f :: "'a::complete_linorder \<Rightarrow> 'b::complete_linorder"
   113   assumes "mono f" "bij f"
   114   shows "f (Inf A) = Inf (f`A)"
   115 proof -
   116   have "(inv f) (Inf (f`A)) \<le> Inf ((inv f)`(f`A))"
   117     using mono_Inf[OF mono_inv[OF assms], of "f`A"] by simp
   118   then have "Inf (f`A) \<le> f (Inf ((inv f)`(f`A)))"
   119     by (metis (no_types, lifting) assms mono_def bij_inv_eq_iff)
   120   also have "... = f(Inf A)"
   121     using assms by (simp add: bij_is_inj)
   122   finally show ?thesis using mono_Inf[OF assms(1), of A] by auto
   123 qed
   124 
   125 
   126 lemma Inf_nat_def1:
   127   fixes K::"nat set"
   128   assumes "K \<noteq> {}"
   129   shows "Inf K \<in> K"
   130 by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)
   131 
   132 subsection \<open>Liminf-Limsup.thy\<close>
   133 
   134 lemma limsup_shift:
   135   "limsup (\<lambda>n. u (n+1)) = limsup u"
   136 proof -
   137   have "(SUP m:{n+1..}. u m) = (SUP m:{n..}. u (m + 1))" for n
   138     apply (rule SUP_eq) using Suc_le_D by auto
   139   then have a: "(INF n. SUP m:{n..}. u (m + 1)) = (INF n. (SUP m:{n+1..}. u m))" by auto
   140   have b: "(INF n. (SUP m:{n+1..}. u m)) = (INF n:{1..}. (SUP m:{n..}. u m))"
   141     apply (rule INF_eq) using Suc_le_D by auto
   142   have "(INF n:{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
   143     apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
   144   moreover have "decseq (\<lambda>n. (SUP m:{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
   145   ultimately have c: "(INF n:{1..}. (SUP m:{n..}. u m)) = (INF n. (SUP m:{n..}. u m))" by simp
   146   have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m:{n..}. u (m + 1))" using a b c by simp
   147   then show ?thesis by (auto cong: limsup_INF_SUP)
   148 qed
   149 
   150 lemma limsup_shift_k:
   151   "limsup (\<lambda>n. u (n+k)) = limsup u"
   152 proof (induction k)
   153   case (Suc k)
   154   have "limsup (\<lambda>n. u (n+k+1)) = limsup (\<lambda>n. u (n+k))" using limsup_shift[where ?u="\<lambda>n. u(n+k)"] by simp
   155   then show ?case using Suc.IH by simp
   156 qed (auto)
   157 
   158 lemma liminf_shift:
   159   "liminf (\<lambda>n. u (n+1)) = liminf u"
   160 proof -
   161   have "(INF m:{n+1..}. u m) = (INF m:{n..}. u (m + 1))" for n
   162     apply (rule INF_eq) using Suc_le_D by (auto)
   163   then have a: "(SUP n. INF m:{n..}. u (m + 1)) = (SUP n. (INF m:{n+1..}. u m))" by auto
   164   have b: "(SUP n. (INF m:{n+1..}. u m)) = (SUP n:{1..}. (INF m:{n..}. u m))"
   165     apply (rule SUP_eq) using Suc_le_D by (auto)
   166   have "(SUP n:{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
   167     apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
   168   moreover have "incseq (\<lambda>n. (INF m:{n..}. u m))" by (simp add: INF_superset_mono mono_def)
   169   ultimately have c: "(SUP n:{1..}. (INF m:{n..}. u m)) = (SUP n. (INF m:{n..}. u m))" by simp
   170   have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m:{n..}. u (m + 1))" using a b c by simp
   171   then show ?thesis by (auto cong: liminf_SUP_INF)
   172 qed
   173 
   174 lemma liminf_shift_k:
   175   "liminf (\<lambda>n. u (n+k)) = liminf u"
   176 proof (induction k)
   177   case (Suc k)
   178   have "liminf (\<lambda>n. u (n+k+1)) = liminf (\<lambda>n. u (n+k))" using liminf_shift[where ?u="\<lambda>n. u(n+k)"] by simp
   179   then show ?case using Suc.IH by simp
   180 qed (auto)
   181 
   182 lemma Limsup_obtain:
   183   fixes u::"_ \<Rightarrow> 'a :: complete_linorder"
   184   assumes "Limsup F u > c"
   185   shows "\<exists>i. u i > c"
   186 proof -
   187   have "(INF P:{P. eventually P F}. SUP x:{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
   188   then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
   189 qed
   190 
   191 text \<open>The next lemma is extremely useful, as it often makes it possible to reduce statements
   192 about limsups to statements about limits.\<close>
   193 
   194 lemma limsup_subseq_lim:
   195   fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   196   shows "\<exists>r. subseq r \<and> (u o r) \<longlonglongrightarrow> limsup u"
   197 proof (cases)
   198   assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<le> u p"
   199   then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<le> u (r n)) \<and> r n < r (Suc n)"
   200     by (intro dependent_nat_choice) (auto simp: conj_commute)
   201   then obtain r where "subseq r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
   202     by (auto simp: subseq_Suc_iff)
   203   define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
   204   have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
   205   then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
   206   then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
   207   have "\<And>n. umax(r n) = u(r n)" unfolding umax_def using mono
   208     by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
   209   then have "umax o r = u o r" unfolding o_def by simp
   210   then have "(u o r) \<longlonglongrightarrow> limsup u" using * by simp
   211   then show ?thesis using \<open>subseq r\<close> by blast
   212 next
   213   assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<le> u p))"
   214   then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p < u m" by (force simp: not_le le_less)
   215   have "\<exists>r. \<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))"
   216   proof (rule dependent_nat_choice)
   217     fix x assume "N < x"
   218     then have a: "finite {N<..x}" "{N<..x} \<noteq> {}" by simp_all
   219     have "Max {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Max_in) using a by (auto)
   220     then obtain p where "p \<in> {N<..x}" and upmax: "u p = Max{u i |i. i \<in> {N<..x}}" by auto
   221     define U where "U = {m. m > p \<and> u p < u m}"
   222     have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
   223     define y where "y = Inf U"
   224     then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
   225     have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<le> u p"
   226     proof -
   227       fix i assume "i \<in> {N<..x}"
   228       then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
   229       then show "u i \<le> u p" using upmax by simp
   230     qed
   231     moreover have "u p < u y" using \<open>y \<in> U\<close> U_def by auto
   232     ultimately have "y \<notin> {N<..x}" using not_le by blast
   233     moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
   234     ultimately have "y > x" by auto
   235 
   236     have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<le> u y"
   237     proof -
   238       fix i assume "i \<in> {N<..y}" show "u i \<le> u y"
   239       proof (cases)
   240         assume "i = y"
   241         then show ?thesis by simp
   242       next
   243         assume "\<not>(i=y)"
   244         then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
   245         have "u i \<le> u p"
   246         proof (cases)
   247           assume "i \<le> x"
   248           then have "i \<in> {N<..x}" using i by simp
   249           then show ?thesis using a by simp
   250         next
   251           assume "\<not>(i \<le> x)"
   252           then have "i > x" by simp
   253           then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
   254           have "i < Inf U" using i y_def by simp
   255           then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
   256           then show ?thesis using U_def * by auto
   257         qed
   258         then show "u i \<le> u y" using \<open>u p < u y\<close> by auto
   259       qed
   260     qed
   261     then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
   262     then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" by auto
   263   qed (auto)
   264   then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))" by auto
   265   have "subseq r" using r by (auto simp: subseq_Suc_iff)
   266   have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
   267   then have "(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
   268   then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
   269   moreover have "limsup (u o r) \<le> limsup u" using \<open>subseq r\<close> by (simp add: limsup_subseq_mono)
   270   ultimately have "(SUP n. (u o r) n) \<le> limsup u" by simp
   271 
   272   {
   273     fix i assume i: "i \<in> {N<..}"
   274     obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
   275     then have "i \<in> {N<..r(Suc n)}" using i by simp
   276     then have "u i \<le> u (r(Suc n))" using r by simp
   277     then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
   278   }
   279   then have "(SUP i:{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
   280   then have "limsup u \<le> (SUP n. (u o r) n)" unfolding Limsup_def
   281     by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   282   then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
   283   then have "(u o r) \<longlonglongrightarrow> limsup u" using \<open>(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)\<close> by simp
   284   then show ?thesis using \<open>subseq r\<close> by auto
   285 qed
   286 
   287 lemma liminf_subseq_lim:
   288   fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   289   shows "\<exists>r. subseq r \<and> (u o r) \<longlonglongrightarrow> liminf u"
   290 proof (cases)
   291   assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<ge> u p"
   292   then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<ge> u (r n)) \<and> r n < r (Suc n)"
   293     by (intro dependent_nat_choice) (auto simp: conj_commute)
   294   then obtain r where "subseq r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
   295     by (auto simp: subseq_Suc_iff)
   296   define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
   297   have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
   298   then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
   299   then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
   300   have "\<And>n. umin(r n) = u(r n)" unfolding umin_def using mono
   301     by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
   302   then have "umin o r = u o r" unfolding o_def by simp
   303   then have "(u o r) \<longlonglongrightarrow> liminf u" using * by simp
   304   then show ?thesis using \<open>subseq r\<close> by blast
   305 next
   306   assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<ge> u p))"
   307   then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p > u m" by (force simp: not_le le_less)
   308   have "\<exists>r. \<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))"
   309   proof (rule dependent_nat_choice)
   310     fix x assume "N < x"
   311     then have a: "finite {N<..x}" "{N<..x} \<noteq> {}" by simp_all
   312     have "Min {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Min_in) using a by (auto)
   313     then obtain p where "p \<in> {N<..x}" and upmin: "u p = Min{u i |i. i \<in> {N<..x}}" by auto
   314     define U where "U = {m. m > p \<and> u p > u m}"
   315     have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
   316     define y where "y = Inf U"
   317     then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
   318     have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<ge> u p"
   319     proof -
   320       fix i assume "i \<in> {N<..x}"
   321       then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
   322       then show "u i \<ge> u p" using upmin by simp
   323     qed
   324     moreover have "u p > u y" using \<open>y \<in> U\<close> U_def by auto
   325     ultimately have "y \<notin> {N<..x}" using not_le by blast
   326     moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
   327     ultimately have "y > x" by auto
   328 
   329     have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<ge> u y"
   330     proof -
   331       fix i assume "i \<in> {N<..y}" show "u i \<ge> u y"
   332       proof (cases)
   333         assume "i = y"
   334         then show ?thesis by simp
   335       next
   336         assume "\<not>(i=y)"
   337         then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
   338         have "u i \<ge> u p"
   339         proof (cases)
   340           assume "i \<le> x"
   341           then have "i \<in> {N<..x}" using i by simp
   342           then show ?thesis using a by simp
   343         next
   344           assume "\<not>(i \<le> x)"
   345           then have "i > x" by simp
   346           then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
   347           have "i < Inf U" using i y_def by simp
   348           then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
   349           then show ?thesis using U_def * by auto
   350         qed
   351         then show "u i \<ge> u y" using \<open>u p > u y\<close> by auto
   352       qed
   353     qed
   354     then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
   355     then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" by auto
   356   qed (auto)
   357   then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
   358   have "subseq r" using r by (auto simp: subseq_Suc_iff)
   359   have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
   360   then have "(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)" using LIMSEQ_INF by blast
   361   then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
   362   moreover have "liminf (u o r) \<ge> liminf u" using \<open>subseq r\<close> by (simp add: liminf_subseq_mono)
   363   ultimately have "(INF n. (u o r) n) \<ge> liminf u" by simp
   364 
   365   {
   366     fix i assume i: "i \<in> {N<..}"
   367     obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
   368     then have "i \<in> {N<..r(Suc n)}" using i by simp
   369     then have "u i \<ge> u (r(Suc n))" using r by simp
   370     then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
   371   }
   372   then have "(INF i:{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
   373   then have "liminf u \<ge> (INF n. (u o r) n)" unfolding Liminf_def
   374     by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   375   then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
   376   then have "(u o r) \<longlonglongrightarrow> liminf u" using \<open>(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)\<close> by simp
   377   then show ?thesis using \<open>subseq r\<close> by auto
   378 qed
   379 
   380 
   381 subsection \<open>Extended-Real.thy\<close>
   382 
   383 text\<open>The proof of this one is copied from \verb+ereal_add_mono+.\<close>
   384 lemma ereal_add_strict_mono2:
   385   fixes a b c d :: ereal
   386   assumes "a < b"
   387     and "c < d"
   388   shows "a + c < b + d"
   389 using assms
   390 apply (cases a)
   391 apply (cases rule: ereal3_cases[of b c d], auto)
   392 apply (cases rule: ereal3_cases[of b c d], auto)
   393 done
   394 
   395 text \<open>The next ones are analogues of \verb+mult_mono+ and \verb+mult_mono'+ in ereal.\<close>
   396 
   397 lemma ereal_mult_mono:
   398   fixes a b c d::ereal
   399   assumes "b \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d"
   400   shows "a * c \<le> b * d"
   401 by (metis ereal_mult_right_mono mult.commute order_trans assms)
   402 
   403 lemma ereal_mult_mono':
   404   fixes a b c d::ereal
   405   assumes "a \<ge> 0" "c \<ge> 0" "a \<le> b" "c \<le> d"
   406   shows "a * c \<le> b * d"
   407 by (metis ereal_mult_right_mono mult.commute order_trans assms)
   408 
   409 lemma ereal_mult_mono_strict:
   410   fixes a b c d::ereal
   411   assumes "b > 0" "c > 0" "a < b" "c < d"
   412   shows "a * c < b * d"
   413 proof -
   414   have "c < \<infinity>" using \<open>c < d\<close> by auto
   415   then have "a * c < b * c" by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute)
   416   moreover have "b * c \<le> b * d" using assms(2) assms(4) by (simp add: assms(1) ereal_mult_left_mono less_imp_le)
   417   ultimately show ?thesis by simp
   418 qed
   419 
   420 lemma ereal_mult_mono_strict':
   421   fixes a b c d::ereal
   422   assumes "a > 0" "c > 0" "a < b" "c < d"
   423   shows "a * c < b * d"
   424 apply (rule ereal_mult_mono_strict, auto simp add: assms) using assms by auto
   425 
   426 lemma ereal_abs_add:
   427   fixes a b::ereal
   428   shows "abs(a+b) \<le> abs a + abs b"
   429 by (cases rule: ereal2_cases[of a b]) (auto)
   430 
   431 lemma ereal_abs_diff:
   432   fixes a b::ereal
   433   shows "abs(a-b) \<le> abs a + abs b"
   434 by (cases rule: ereal2_cases[of a b]) (auto)
   435 
   436 lemma sum_constant_ereal:
   437   fixes a::ereal
   438   shows "(\<Sum>i\<in>I. a) = a * card I"
   439 apply (cases "finite I", induct set: finite, simp_all)
   440 apply (cases a, auto, metis (no_types, hide_lams) add.commute mult.commute semiring_normalization_rules(3))
   441 done
   442 
   443 lemma real_lim_then_eventually_real:
   444   assumes "(u \<longlongrightarrow> ereal l) F"
   445   shows "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F"
   446 proof -
   447   have "ereal l \<in> {-\<infinity><..<(\<infinity>::ereal)}" by simp
   448   moreover have "open {-\<infinity><..<(\<infinity>::ereal)}" by simp
   449   ultimately have "eventually (\<lambda>n. u n \<in> {-\<infinity><..<(\<infinity>::ereal)}) F" using assms tendsto_def by blast
   450   moreover have "\<And>x. x \<in> {-\<infinity><..<(\<infinity>::ereal)} \<Longrightarrow> x = ereal(real_of_ereal x)" using ereal_real by auto
   451   ultimately show ?thesis by (metis (mono_tags, lifting) eventually_mono)
   452 qed
   453 
   454 lemma ereal_Inf_cmult:
   455   assumes "c>(0::real)"
   456   shows "Inf {ereal c * x |x. P x} = ereal c * Inf {x. P x}"
   457 proof -
   458   have "(\<lambda>x::ereal. c * x) (Inf {x::ereal. P x}) = Inf ((\<lambda>x::ereal. c * x)`{x::ereal. P x})"
   459     apply (rule mono_bij_Inf)
   460     apply (simp add: assms ereal_mult_left_mono less_imp_le mono_def)
   461     apply (rule bij_betw_byWitness[of _ "\<lambda>x. (x::ereal) / c"], auto simp add: assms ereal_mult_divide)
   462     using assms ereal_divide_eq apply auto
   463     done
   464   then show ?thesis by (simp only: setcompr_eq_image[symmetric])
   465 qed
   466 
   467 
   468 subsubsection \<open>Continuity of addition\<close>
   469 
   470 text \<open>The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
   471 in \verb+tendsto_add_ereal_general+ which essentially says that the addition
   472 is continuous on ereal times ereal, except at $(-\infty, \infty)$ and $(\infty, -\infty)$.
   473 It is much more convenient in many situations, see for instance the proof of
   474 \verb+tendsto_sum_ereal+ below.\<close>
   475 
   476 lemma tendsto_add_ereal_PInf:
   477   fixes y :: ereal
   478   assumes y: "y \<noteq> -\<infinity>"
   479   assumes f: "(f \<longlongrightarrow> \<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   480   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> \<infinity>) F"
   481 proof -
   482   have "\<exists>C. eventually (\<lambda>x. g x > ereal C) F"
   483   proof (cases y)
   484     case (real r)
   485     have "y > y-1" using y real by (simp add: ereal_between(1))
   486     then have "eventually (\<lambda>x. g x > y - 1) F" using g y order_tendsto_iff by auto
   487     moreover have "y-1 = ereal(real_of_ereal(y-1))"
   488       by (metis real ereal_eq_1(1) ereal_minus(1) real_of_ereal.simps(1))
   489     ultimately have "eventually (\<lambda>x. g x > ereal(real_of_ereal(y - 1))) F" by simp
   490     then show ?thesis by auto
   491   next
   492     case (PInf)
   493     have "eventually (\<lambda>x. g x > ereal 0) F" using g PInf by (simp add: tendsto_PInfty)
   494     then show ?thesis by auto
   495   qed (simp add: y)
   496   then obtain C::real where ge: "eventually (\<lambda>x. g x > ereal C) F" by auto
   497 
   498   {
   499     fix M::real
   500     have "eventually (\<lambda>x. f x > ereal(M - C)) F" using f by (simp add: tendsto_PInfty)
   501     then have "eventually (\<lambda>x. (f x > ereal (M-C)) \<and> (g x > ereal C)) F"
   502       by (auto simp add: ge eventually_conj_iff)
   503     moreover have "\<And>x. ((f x > ereal (M-C)) \<and> (g x > ereal C)) \<Longrightarrow> (f x + g x > ereal M)"
   504       using ereal_add_strict_mono2 by fastforce
   505     ultimately have "eventually (\<lambda>x. f x + g x > ereal M) F" using eventually_mono by force
   506   }
   507   then show ?thesis by (simp add: tendsto_PInfty)
   508 qed
   509 
   510 text\<open>One would like to deduce the next lemma from the previous one, but the fact
   511 that $-(x+y)$ is in general different from $(-x) + (-y)$ in ereal creates difficulties,
   512 so it is more efficient to copy the previous proof.\<close>
   513 
   514 lemma tendsto_add_ereal_MInf:
   515   fixes y :: ereal
   516   assumes y: "y \<noteq> \<infinity>"
   517   assumes f: "(f \<longlongrightarrow> -\<infinity>) F" and g: "(g \<longlongrightarrow> y) F"
   518   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> -\<infinity>) F"
   519 proof -
   520   have "\<exists>C. eventually (\<lambda>x. g x < ereal C) F"
   521   proof (cases y)
   522     case (real r)
   523     have "y < y+1" using y real by (simp add: ereal_between(1))
   524     then have "eventually (\<lambda>x. g x < y + 1) F" using g y order_tendsto_iff by force
   525     moreover have "y+1 = ereal(real_of_ereal (y+1))" by (simp add: real)
   526     ultimately have "eventually (\<lambda>x. g x < ereal(real_of_ereal(y + 1))) F" by simp
   527     then show ?thesis by auto
   528   next
   529     case (MInf)
   530     have "eventually (\<lambda>x. g x < ereal 0) F" using g MInf by (simp add: tendsto_MInfty)
   531     then show ?thesis by auto
   532   qed (simp add: y)
   533   then obtain C::real where ge: "eventually (\<lambda>x. g x < ereal C) F" by auto
   534 
   535   {
   536     fix M::real
   537     have "eventually (\<lambda>x. f x < ereal(M - C)) F" using f by (simp add: tendsto_MInfty)
   538     then have "eventually (\<lambda>x. (f x < ereal (M- C)) \<and> (g x < ereal C)) F"
   539       by (auto simp add: ge eventually_conj_iff)
   540     moreover have "\<And>x. ((f x < ereal (M-C)) \<and> (g x < ereal C)) \<Longrightarrow> (f x + g x < ereal M)"
   541       using ereal_add_strict_mono2 by fastforce
   542     ultimately have "eventually (\<lambda>x. f x + g x < ereal M) F" using eventually_mono by force
   543   }
   544   then show ?thesis by (simp add: tendsto_MInfty)
   545 qed
   546 
   547 lemma tendsto_add_ereal_general1:
   548   fixes x y :: ereal
   549   assumes y: "\<bar>y\<bar> \<noteq> \<infinity>"
   550   assumes f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   551   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   552 proof (cases x)
   553   case (real r)
   554   have a: "\<bar>x\<bar> \<noteq> \<infinity>" by (simp add: real)
   555   show ?thesis by (rule tendsto_add_ereal[OF a, OF y, OF f, OF g])
   556 next
   557   case PInf
   558   then show ?thesis using tendsto_add_ereal_PInf assms by force
   559 next
   560   case MInf
   561   then show ?thesis using tendsto_add_ereal_MInf assms
   562     by (metis abs_ereal.simps(3) ereal_MInfty_eq_plus)
   563 qed
   564 
   565 lemma tendsto_add_ereal_general2:
   566   fixes x y :: ereal
   567   assumes x: "\<bar>x\<bar> \<noteq> \<infinity>"
   568       and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   569   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   570 proof -
   571   have "((\<lambda>x. g x + f x) \<longlongrightarrow> x + y) F"
   572     using tendsto_add_ereal_general1[OF x, OF g, OF f] add.commute[of "y", of "x"] by simp
   573   moreover have "\<And>x. g x + f x = f x + g x" using add.commute by auto
   574   ultimately show ?thesis by simp
   575 qed
   576 
   577 text \<open>The next lemma says that the addition is continuous on ereal, except at
   578 the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$.\<close>
   579 
   580 lemma tendsto_add_ereal_general [tendsto_intros]:
   581   fixes x y :: ereal
   582   assumes "\<not>((x=\<infinity> \<and> y=-\<infinity>) \<or> (x=-\<infinity> \<and> y=\<infinity>))"
   583       and f: "(f \<longlongrightarrow> x) F" and g: "(g \<longlongrightarrow> y) F"
   584   shows "((\<lambda>x. f x + g x) \<longlongrightarrow> x + y) F"
   585 proof (cases x)
   586   case (real r)
   587   show ?thesis
   588     apply (rule tendsto_add_ereal_general2) using real assms by auto
   589 next
   590   case (PInf)
   591   then have "y \<noteq> -\<infinity>" using assms by simp
   592   then show ?thesis using tendsto_add_ereal_PInf PInf assms by auto
   593 next
   594   case (MInf)
   595   then have "y \<noteq> \<infinity>" using assms by simp
   596   then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
   597 qed
   598 
   599 subsubsection \<open>Continuity of multiplication\<close>
   600 
   601 text \<open>In the same way as for addition, we prove that the multiplication is continuous on
   602 ereal times ereal, except at $(\infty, 0)$ and $(-\infty, 0)$ and $(0, \infty)$ and $(0, -\infty)$,
   603 starting with specific situations.\<close>
   604 
   605 lemma tendsto_mult_real_ereal:
   606   assumes "(u \<longlongrightarrow> ereal l) F" "(v \<longlongrightarrow> ereal m) F"
   607   shows "((\<lambda>n. u n * v n) \<longlongrightarrow> ereal l * ereal m) F"
   608 proof -
   609   have ureal: "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) F" by (rule real_lim_then_eventually_real[OF assms(1)])
   610   then have "((\<lambda>n. ereal(real_of_ereal(u n))) \<longlongrightarrow> ereal l) F" using assms by auto
   611   then have limu: "((\<lambda>n. real_of_ereal(u n)) \<longlongrightarrow> l) F" by auto
   612   have vreal: "eventually (\<lambda>n. v n = ereal(real_of_ereal(v n))) F" by (rule real_lim_then_eventually_real[OF assms(2)])
   613   then have "((\<lambda>n. ereal(real_of_ereal(v n))) \<longlongrightarrow> ereal m) F" using assms by auto
   614   then have limv: "((\<lambda>n. real_of_ereal(v n)) \<longlongrightarrow> m) F" by auto
   615 
   616   {
   617     fix n assume "u n = ereal(real_of_ereal(u n))" "v n = ereal(real_of_ereal(v n))"
   618     then have "ereal(real_of_ereal(u n) * real_of_ereal(v n)) = u n * v n" by (metis times_ereal.simps(1))
   619   }
   620   then have *: "eventually (\<lambda>n. ereal(real_of_ereal(u n) * real_of_ereal(v n)) = u n * v n) F"
   621     using eventually_elim2[OF ureal vreal] by auto
   622 
   623   have "((\<lambda>n. real_of_ereal(u n) * real_of_ereal(v n)) \<longlongrightarrow> l * m) F" using tendsto_mult[OF limu limv] by auto
   624   then have "((\<lambda>n. ereal(real_of_ereal(u n)) * real_of_ereal(v n)) \<longlongrightarrow> ereal(l * m)) F" by auto
   625   then show ?thesis using * filterlim_cong by fastforce
   626 qed
   627 
   628 lemma tendsto_mult_ereal_PInf:
   629   fixes f g::"_ \<Rightarrow> ereal"
   630   assumes "(f \<longlongrightarrow> l) F" "l>0" "(g \<longlongrightarrow> \<infinity>) F"
   631   shows "((\<lambda>x. f x * g x) \<longlongrightarrow> \<infinity>) F"
   632 proof -
   633   obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast
   634   have *: "eventually (\<lambda>x. f x > a) F" using \<open>a < l\<close> assms(1) by (simp add: order_tendsto_iff)
   635   {
   636     fix K::real
   637     define M where "M = max K 1"
   638     then have "M > 0" by simp
   639     then have "ereal(M/a) > 0" using \<open>ereal a > 0\<close> by simp
   640     then have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > ereal a * ereal(M/a))"
   641       using ereal_mult_mono_strict'[where ?c = "M/a", OF \<open>0 < ereal a\<close>] by auto
   642     moreover have "ereal a * ereal(M/a) = M" using \<open>ereal a > 0\<close> by simp
   643     ultimately have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > M)" by simp
   644     moreover have "M \<ge> K" unfolding M_def by simp
   645     ultimately have Imp: "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > K)"
   646       using ereal_less_eq(3) le_less_trans by blast
   647 
   648     have "eventually (\<lambda>x. g x > M/a) F" using assms(3) by (simp add: tendsto_PInfty)
   649     then have "eventually (\<lambda>x. (f x > a) \<and> (g x > M/a)) F"
   650       using * by (auto simp add: eventually_conj_iff)
   651     then have "eventually (\<lambda>x. f x * g x > K) F" using eventually_mono Imp by force
   652   }
   653   then show ?thesis by (auto simp add: tendsto_PInfty)
   654 qed
   655 
   656 lemma tendsto_mult_ereal_pos:
   657   fixes f g::"_ \<Rightarrow> ereal"
   658   assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "l>0" "m>0"
   659   shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
   660 proof (cases)
   661   assume *: "l = \<infinity> \<or> m = \<infinity>"
   662   then show ?thesis
   663   proof (cases)
   664     assume "m = \<infinity>"
   665     then show ?thesis using tendsto_mult_ereal_PInf assms by auto
   666   next
   667     assume "\<not>(m = \<infinity>)"
   668     then have "l = \<infinity>" using * by simp
   669     then have "((\<lambda>x. g x * f x) \<longlongrightarrow> l * m) F" using tendsto_mult_ereal_PInf assms by auto
   670     moreover have "\<And>x. g x * f x = f x * g x" using mult.commute by auto
   671     ultimately show ?thesis by simp
   672   qed
   673 next
   674   assume "\<not>(l = \<infinity> \<or> m = \<infinity>)"
   675   then have "l < \<infinity>" "m < \<infinity>" by auto
   676   then obtain lr mr where "l = ereal lr" "m = ereal mr"
   677     using \<open>l>0\<close> \<open>m>0\<close> by (metis ereal_cases ereal_less(6) not_less_iff_gr_or_eq)
   678   then show ?thesis using tendsto_mult_real_ereal assms by auto
   679 qed
   680 
   681 text \<open>We reduce the general situation to the positive case by multiplying by suitable signs.
   682 Unfortunately, as ereal is not a ring, all the neat sign lemmas are not available there. We
   683 give the bare minimum we need.\<close>
   684 
   685 lemma ereal_sgn_abs:
   686   fixes l::ereal
   687   shows "sgn(l) * l = abs(l)"
   688 apply (cases l) by (auto simp add: sgn_if ereal_less_uminus_reorder)
   689 
   690 lemma sgn_squared_ereal:
   691   assumes "l \<noteq> (0::ereal)"
   692   shows "sgn(l) * sgn(l) = 1"
   693 apply (cases l) using assms by (auto simp add: one_ereal_def sgn_if)
   694 
   695 lemma tendsto_mult_ereal [tendsto_intros]:
   696   fixes f g::"_ \<Rightarrow> ereal"
   697   assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "\<not>((l=0 \<and> abs(m) = \<infinity>) \<or> (m=0 \<and> abs(l) = \<infinity>))"
   698   shows "((\<lambda>x. f x * g x) \<longlongrightarrow> l * m) F"
   699 proof (cases)
   700   assume "l=0 \<or> m=0"
   701   then have "abs(l) \<noteq> \<infinity>" "abs(m) \<noteq> \<infinity>" using assms(3) by auto
   702   then obtain lr mr where "l = ereal lr" "m = ereal mr" by auto
   703   then show ?thesis using tendsto_mult_real_ereal assms by auto
   704 next
   705   have sgn_finite: "\<And>a::ereal. abs(sgn a) \<noteq> \<infinity>"
   706     by (metis MInfty_neq_ereal(2) PInfty_neq_ereal(2) abs_eq_infinity_cases ereal_times(1) ereal_times(3) ereal_uminus_eq_reorder sgn_ereal.elims)
   707   then have sgn_finite2: "\<And>a b::ereal. abs(sgn a * sgn b) \<noteq> \<infinity>"
   708     by (metis abs_eq_infinity_cases abs_ereal.simps(2) abs_ereal.simps(3) ereal_mult_eq_MInfty ereal_mult_eq_PInfty)
   709   assume "\<not>(l=0 \<or> m=0)"
   710   then have "l \<noteq> 0" "m \<noteq> 0" by auto
   711   then have "abs(l) > 0" "abs(m) > 0"
   712     by (metis abs_ereal_ge0 abs_ereal_less0 abs_ereal_pos ereal_uminus_uminus ereal_uminus_zero less_le not_less)+
   713   then have "sgn(l) * l > 0" "sgn(m) * m > 0" using ereal_sgn_abs by auto
   714   moreover have "((\<lambda>x. sgn(l) * f x) \<longlongrightarrow> (sgn(l) * l)) F"
   715     by (rule tendsto_cmult_ereal, auto simp add: sgn_finite assms(1))
   716   moreover have "((\<lambda>x. sgn(m) * g x) \<longlongrightarrow> (sgn(m) * m)) F"
   717     by (rule tendsto_cmult_ereal, auto simp add: sgn_finite assms(2))
   718   ultimately have *: "((\<lambda>x. (sgn(l) * f x) * (sgn(m) * g x)) \<longlongrightarrow> (sgn(l) * l) * (sgn(m) * m)) F"
   719     using tendsto_mult_ereal_pos by force
   720   have "((\<lambda>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x))) \<longlongrightarrow> (sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m))) F"
   721     by (rule tendsto_cmult_ereal, auto simp add: sgn_finite2 *)
   722   moreover have "\<And>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x)) = f x * g x"
   723     by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
   724   moreover have "(sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m)) = l * m"
   725     by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
   726   ultimately show ?thesis by auto
   727 qed
   728 
   729 lemma tendsto_cmult_ereal_general [tendsto_intros]:
   730   fixes f::"_ \<Rightarrow> ereal" and c::ereal
   731   assumes "(f \<longlongrightarrow> l) F" "\<not> (l=0 \<and> abs(c) = \<infinity>)"
   732   shows "((\<lambda>x. c * f x) \<longlongrightarrow> c * l) F"
   733 by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
   734 
   735 
   736 subsubsection \<open>Continuity of division\<close>
   737 
   738 lemma tendsto_inverse_ereal_PInf:
   739   fixes u::"_ \<Rightarrow> ereal"
   740   assumes "(u \<longlongrightarrow> \<infinity>) F"
   741   shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 0) F"
   742 proof -
   743   {
   744     fix e::real assume "e>0"
   745     have "1/e < \<infinity>" by auto
   746     then have "eventually (\<lambda>n. u n > 1/e) F" using assms(1) by (simp add: tendsto_PInfty)
   747     moreover
   748     {
   749       fix z::ereal assume "z>1/e"
   750       then have "z>0" using \<open>e>0\<close> using less_le_trans not_le by fastforce
   751       then have "1/z \<ge> 0" by auto
   752       moreover have "1/z < e" using \<open>e>0\<close> \<open>z>1/e\<close>
   753         apply (cases z) apply auto
   754         by (metis (mono_tags, hide_lams) less_ereal.simps(2) less_ereal.simps(4) divide_less_eq ereal_divide_less_pos ereal_less(4)
   755             ereal_less_eq(4) less_le_trans mult_eq_0_iff not_le not_one_less_zero times_ereal.simps(1))
   756       ultimately have "1/z \<ge> 0" "1/z < e" by auto
   757     }
   758     ultimately have "eventually (\<lambda>n. 1/u n<e) F" "eventually (\<lambda>n. 1/u n\<ge>0) F" by (auto simp add: eventually_mono)
   759   } note * = this
   760   show ?thesis
   761   proof (subst order_tendsto_iff, auto)
   762     fix a::ereal assume "a<0"
   763     then show "eventually (\<lambda>n. 1/u n > a) F" using *(2) eventually_mono less_le_trans linordered_field_no_ub by fastforce
   764   next
   765     fix a::ereal assume "a>0"
   766     then obtain e::real where "e>0" "a>e" using ereal_dense2 ereal_less(2) by blast
   767     then have "eventually (\<lambda>n. 1/u n < e) F" using *(1) by auto
   768     then show "eventually (\<lambda>n. 1/u n < a) F" using \<open>a>e\<close> by (metis (mono_tags, lifting) eventually_mono less_trans)
   769   qed
   770 qed
   771 
   772 text \<open>The next lemma deserves to exist by itself, as it is so common and useful.\<close>
   773 
   774 lemma tendsto_inverse_real [tendsto_intros]:
   775   fixes u::"_ \<Rightarrow> real"
   776   shows "(u \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   777   using tendsto_inverse unfolding inverse_eq_divide .
   778 
   779 lemma tendsto_inverse_ereal [tendsto_intros]:
   780   fixes u::"_ \<Rightarrow> ereal"
   781   assumes "(u \<longlongrightarrow> l) F" "l \<noteq> 0"
   782   shows "((\<lambda>x. 1/ u x) \<longlongrightarrow> 1/l) F"
   783 proof (cases l)
   784   case (real r)
   785   then have "r \<noteq> 0" using assms(2) by auto
   786   then have "1/l = ereal(1/r)" using real by (simp add: one_ereal_def)
   787   define v where "v = (\<lambda>n. real_of_ereal(u n))"
   788   have ureal: "eventually (\<lambda>n. u n = ereal(v n)) F" unfolding v_def using real_lim_then_eventually_real assms(1) real by auto
   789   then have "((\<lambda>n. ereal(v n)) \<longlongrightarrow> ereal r) F" using assms real v_def by auto
   790   then have *: "((\<lambda>n. v n) \<longlongrightarrow> r) F" by auto
   791   then have "((\<lambda>n. 1/v n) \<longlongrightarrow> 1/r) F" using \<open>r \<noteq> 0\<close> tendsto_inverse_real by auto
   792   then have lim: "((\<lambda>n. ereal(1/v n)) \<longlongrightarrow> 1/l) F" using \<open>1/l = ereal(1/r)\<close> by auto
   793 
   794   have "r \<in> -{0}" "open (-{(0::real)})" using \<open>r \<noteq> 0\<close> by auto
   795   then have "eventually (\<lambda>n. v n \<in> -{0}) F" using * using topological_tendstoD by blast
   796   then have "eventually (\<lambda>n. v n \<noteq> 0) F" by auto
   797   moreover
   798   {
   799     fix n assume H: "v n \<noteq> 0" "u n = ereal(v n)"
   800     then have "ereal(1/v n) = 1/ereal(v n)" by (simp add: one_ereal_def)
   801     then have "ereal(1/v n) = 1/u n" using H(2) by simp
   802   }
   803   ultimately have "eventually (\<lambda>n. ereal(1/v n) = 1/u n) F" using ureal eventually_elim2 by force
   804   with Lim_transform_eventually[OF this lim] show ?thesis by simp
   805 next
   806   case (PInf)
   807   then have "1/l = 0" by auto
   808   then show ?thesis using tendsto_inverse_ereal_PInf assms PInf by auto
   809 next
   810   case (MInf)
   811   then have "1/l = 0" by auto
   812   have "1/z = -1/ -z" if "z < 0" for z::ereal
   813     apply (cases z) using divide_ereal_def \<open> z < 0 \<close> by auto
   814   moreover have "eventually (\<lambda>n. u n < 0) F" by (metis (no_types) MInf assms(1) tendsto_MInfty zero_ereal_def)
   815   ultimately have *: "eventually (\<lambda>n. -1/-u n = 1/u n) F" by (simp add: eventually_mono)
   816 
   817   define v where "v = (\<lambda>n. - u n)"
   818   have "(v \<longlongrightarrow> \<infinity>) F" unfolding v_def using MInf assms(1) tendsto_uminus_ereal by fastforce
   819   then have "((\<lambda>n. 1/v n) \<longlongrightarrow> 0) F" using tendsto_inverse_ereal_PInf by auto
   820   then have "((\<lambda>n. -1/v n) \<longlongrightarrow> 0) F" using tendsto_uminus_ereal by fastforce
   821   then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \<open> 1/l = 0 \<close> by auto
   822 qed
   823 
   824 lemma tendsto_divide_ereal [tendsto_intros]:
   825   fixes f g::"_ \<Rightarrow> ereal"
   826   assumes "(f \<longlongrightarrow> l) F" "(g \<longlongrightarrow> m) F" "m \<noteq> 0" "\<not>(abs(l) = \<infinity> \<and> abs(m) = \<infinity>)"
   827   shows "((\<lambda>x. f x / g x) \<longlongrightarrow> l / m) F"
   828 proof -
   829   define h where "h = (\<lambda>x. 1/ g x)"
   830   have *: "(h \<longlongrightarrow> 1/m) F" unfolding h_def using assms(2) assms(3) tendsto_inverse_ereal by auto
   831   have "((\<lambda>x. f x * h x) \<longlongrightarrow> l * (1/m)) F"
   832     apply (rule tendsto_mult_ereal[OF assms(1) *]) using assms(3) assms(4) by (auto simp add: divide_ereal_def)
   833   moreover have "f x * h x = f x / g x" for x unfolding h_def by (simp add: divide_ereal_def)
   834   moreover have "l * (1/m) = l/m" by (simp add: divide_ereal_def)
   835   ultimately show ?thesis unfolding h_def using Lim_transform_eventually by auto
   836 qed
   837 
   838 
   839 subsubsection \<open>Further limits\<close>
   840 
   841 lemma id_nat_ereal_tendsto_PInf [tendsto_intros]:
   842   "(\<lambda> n::nat. real n) \<longlonglongrightarrow> \<infinity>"
   843 by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top)
   844 
   845 lemma tendsto_at_top_pseudo_inverse [tendsto_intros]:
   846   fixes u::"nat \<Rightarrow> nat"
   847   assumes "LIM n sequentially. u n :> at_top"
   848   shows "LIM n sequentially. Inf {N. u N \<ge> n} :> at_top"
   849 proof -
   850   {
   851     fix C::nat
   852     define M where "M = Max {u n| n. n \<le> C}+1"
   853     {
   854       fix n assume "n \<ge> M"
   855       have "eventually (\<lambda>N. u N \<ge> n) sequentially" using assms
   856         by (simp add: filterlim_at_top)
   857       then have *: "{N. u N \<ge> n} \<noteq> {}" by force
   858 
   859       have "N > C" if "u N \<ge> n" for N
   860       proof (rule ccontr)
   861         assume "\<not>(N > C)"
   862         have "u N \<le> Max {u n| n. n \<le> C}"
   863           apply (rule Max_ge) using \<open>\<not>(N > C)\<close> by auto
   864         then show False using \<open>u N \<ge> n\<close> \<open>n \<ge> M\<close> unfolding M_def by auto
   865       qed
   866       then have **: "{N. u N \<ge> n} \<subseteq> {C..}" by fastforce
   867       have "Inf {N. u N \<ge> n} \<ge> C"
   868         by (metis "*" "**" Inf_nat_def1 atLeast_iff subset_eq)
   869     }
   870     then have "eventually (\<lambda>n. Inf {N. u N \<ge> n} \<ge> C) sequentially"
   871       using eventually_sequentially by auto
   872   }
   873   then show ?thesis using filterlim_at_top by auto
   874 qed
   875 
   876 lemma pseudo_inverse_finite_set:
   877   fixes u::"nat \<Rightarrow> nat"
   878   assumes "LIM n sequentially. u n :> at_top"
   879   shows "finite {N. u N \<le> n}"
   880 proof -
   881   fix n
   882   have "eventually (\<lambda>N. u N \<ge> n+1) sequentially" using assms
   883     by (simp add: filterlim_at_top)
   884   then obtain N1 where N1: "\<And>N. N \<ge> N1 \<Longrightarrow> u N \<ge> n + 1"
   885     using eventually_sequentially by auto
   886   have "{N. u N \<le> n} \<subseteq> {..<N1}"
   887     apply auto using N1 by (metis Suc_eq_plus1 not_less not_less_eq_eq)
   888   then show "finite {N. u N \<le> n}" by (simp add: finite_subset)
   889 qed
   890 
   891 lemma tendsto_at_top_pseudo_inverse2 [tendsto_intros]:
   892   fixes u::"nat \<Rightarrow> nat"
   893   assumes "LIM n sequentially. u n :> at_top"
   894   shows "LIM n sequentially. Max {N. u N \<le> n} :> at_top"
   895 proof -
   896   {
   897     fix N0::nat
   898     have "N0 \<le> Max {N. u N \<le> n}" if "n \<ge> u N0" for n
   899       apply (rule Max.coboundedI) using pseudo_inverse_finite_set[OF assms] that by auto
   900     then have "eventually (\<lambda>n. N0 \<le> Max {N. u N \<le> n}) sequentially"
   901       using eventually_sequentially by blast
   902   }
   903   then show ?thesis using filterlim_at_top by auto
   904 qed
   905 
   906 lemma ereal_truncation_top [tendsto_intros]:
   907   fixes x::ereal
   908   shows "(\<lambda>n::nat. min x n) \<longlonglongrightarrow> x"
   909 proof (cases x)
   910   case (real r)
   911   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   912   then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   913   then have "eventually (\<lambda>n. min x n = x) sequentially" using eventually_at_top_linorder by blast
   914   then show ?thesis by (simp add: Lim_eventually)
   915 next
   916   case (PInf)
   917   then have "min x n = n" for n::nat by (auto simp add: min_def)
   918   then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
   919 next
   920   case (MInf)
   921   then have "min x n = x" for n::nat by (auto simp add: min_def)
   922   then show ?thesis by auto
   923 qed
   924 
   925 lemma ereal_truncation_real_top [tendsto_intros]:
   926   fixes x::ereal
   927   assumes "x \<noteq> - \<infinity>"
   928   shows "(\<lambda>n::nat. real_of_ereal(min x n)) \<longlonglongrightarrow> x"
   929 proof (cases x)
   930   case (real r)
   931   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   932   then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   933   then have "real_of_ereal(min x n) = r" if "n \<ge> K" for n using real that by auto
   934   then have "eventually (\<lambda>n. real_of_ereal(min x n) = r) sequentially" using eventually_at_top_linorder by blast
   935   then have "(\<lambda>n. real_of_ereal(min x n)) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
   936   then show ?thesis using real by auto
   937 next
   938   case (PInf)
   939   then have "real_of_ereal(min x n) = n" for n::nat by (auto simp add: min_def)
   940   then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
   941 qed (simp add: assms)
   942 
   943 lemma ereal_truncation_bottom [tendsto_intros]:
   944   fixes x::ereal
   945   shows "(\<lambda>n::nat. max x (- real n)) \<longlonglongrightarrow> x"
   946 proof (cases x)
   947   case (real r)
   948   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   949   then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   950   then have "eventually (\<lambda>n. max x (-real n) = x) sequentially" using eventually_at_top_linorder by blast
   951   then show ?thesis by (simp add: Lim_eventually)
   952 next
   953   case (MInf)
   954   then have "max x (-real n) = (-1)* ereal(real n)" for n::nat by (auto simp add: max_def)
   955   moreover have "(\<lambda>n. (-1)* ereal(real n)) \<longlonglongrightarrow> -\<infinity>"
   956     using tendsto_cmult_ereal[of "-1", OF _ id_nat_ereal_tendsto_PInf] by (simp add: one_ereal_def)
   957   ultimately show ?thesis using MInf by auto
   958 next
   959   case (PInf)
   960   then have "max x (-real n) = x" for n::nat by (auto simp add: max_def)
   961   then show ?thesis by auto
   962 qed
   963 
   964 lemma ereal_truncation_real_bottom [tendsto_intros]:
   965   fixes x::ereal
   966   assumes "x \<noteq> \<infinity>"
   967   shows "(\<lambda>n::nat. real_of_ereal(max x (- real n))) \<longlonglongrightarrow> x"
   968 proof (cases x)
   969   case (real r)
   970   then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
   971   then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
   972   then have "real_of_ereal(max x (-real n)) = r" if "n \<ge> K" for n using real that by auto
   973   then have "eventually (\<lambda>n. real_of_ereal(max x (-real n)) = r) sequentially" using eventually_at_top_linorder by blast
   974   then have "(\<lambda>n. real_of_ereal(max x (-real n))) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
   975   then show ?thesis using real by auto
   976 next
   977   case (MInf)
   978   then have "real_of_ereal(max x (-real n)) = (-1)* ereal(real n)" for n::nat by (auto simp add: max_def)
   979   moreover have "(\<lambda>n. (-1)* ereal(real n)) \<longlonglongrightarrow> -\<infinity>"
   980     using tendsto_cmult_ereal[of "-1", OF _ id_nat_ereal_tendsto_PInf] by (simp add: one_ereal_def)
   981   ultimately show ?thesis using MInf by auto
   982 qed (simp add: assms)
   983 
   984 text \<open>the next one is copied from \verb+tendsto_sum+.\<close>
   985 lemma tendsto_sum_ereal [tendsto_intros]:
   986   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
   987   assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
   988           "\<And>i. abs(a i) \<noteq> \<infinity>"
   989   shows "((\<lambda>x. \<Sum>i\<in>S. f i x) \<longlongrightarrow> (\<Sum>i\<in>S. a i)) F"
   990 proof (cases "finite S")
   991   assume "finite S" then show ?thesis using assms
   992     by (induct, simp, simp add: tendsto_add_ereal_general2 assms)
   993 qed(simp)
   994 
   995 subsubsection \<open>Limsups and liminfs\<close>
   996 
   997 lemma limsup_finite_then_bounded:
   998   fixes u::"nat \<Rightarrow> real"
   999   assumes "limsup u < \<infinity>"
  1000   shows "\<exists>C. \<forall>n. u n \<le> C"
  1001 proof -
  1002   obtain C where C: "limsup u < C" "C < \<infinity>" using assms ereal_dense2 by blast
  1003   then have "C = ereal(real_of_ereal C)" using ereal_real by force
  1004   have "eventually (\<lambda>n. u n < C) sequentially" using C(1) unfolding Limsup_def
  1005     apply (auto simp add: INF_less_iff)
  1006     using SUP_lessD eventually_mono by fastforce
  1007   then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n < C" using eventually_sequentially by auto
  1008   define D where "D = max (real_of_ereal C) (Max {u n |n. n \<le> N})"
  1009   have "\<And>n. u n \<le> D"
  1010   proof -
  1011     fix n show "u n \<le> D"
  1012     proof (cases)
  1013       assume *: "n \<le> N"
  1014       have "u n \<le> Max {u n |n. n \<le> N}" by (rule Max_ge, auto simp add: *)
  1015       then show "u n \<le> D" unfolding D_def by linarith
  1016     next
  1017       assume "\<not>(n \<le> N)"
  1018       then have "n \<ge> N" by simp
  1019       then have "u n < C" using N by auto
  1020       then have "u n < real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
  1021       then show "u n \<le> D" unfolding D_def by linarith
  1022     qed
  1023   qed
  1024   then show ?thesis by blast
  1025 qed
  1026 
  1027 lemma liminf_finite_then_bounded_below:
  1028   fixes u::"nat \<Rightarrow> real"
  1029   assumes "liminf u > -\<infinity>"
  1030   shows "\<exists>C. \<forall>n. u n \<ge> C"
  1031 proof -
  1032   obtain C where C: "liminf u > C" "C > -\<infinity>" using assms using ereal_dense2 by blast
  1033   then have "C = ereal(real_of_ereal C)" using ereal_real by force
  1034   have "eventually (\<lambda>n. u n > C) sequentially" using C(1) unfolding Liminf_def
  1035     apply (auto simp add: less_SUP_iff)
  1036     using eventually_elim2 less_INF_D by fastforce
  1037   then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> u n > C" using eventually_sequentially by auto
  1038   define D where "D = min (real_of_ereal C) (Min {u n |n. n \<le> N})"
  1039   have "\<And>n. u n \<ge> D"
  1040   proof -
  1041     fix n show "u n \<ge> D"
  1042     proof (cases)
  1043       assume *: "n \<le> N"
  1044       have "u n \<ge> Min {u n |n. n \<le> N}" by (rule Min_le, auto simp add: *)
  1045       then show "u n \<ge> D" unfolding D_def by linarith
  1046     next
  1047       assume "\<not>(n \<le> N)"
  1048       then have "n \<ge> N" by simp
  1049       then have "u n > C" using N by auto
  1050       then have "u n > real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
  1051       then show "u n \<ge> D" unfolding D_def by linarith
  1052     qed
  1053   qed
  1054   then show ?thesis by blast
  1055 qed
  1056 
  1057 lemma liminf_upper_bound:
  1058   fixes u:: "nat \<Rightarrow> ereal"
  1059   assumes "liminf u < l"
  1060   shows "\<exists>N>k. u N < l"
  1061 by (metis assms gt_ex less_le_trans liminf_bounded_iff not_less)
  1062 
  1063 text \<open>The following statement about limsups is reduced to a statement about limits using
  1064 subsequences thanks to \verb+limsup_subseq_lim+. The statement for limits follows for instance from
  1065 \verb+tendsto_add_ereal_general+.\<close>
  1066 
  1067 lemma ereal_limsup_add_mono:
  1068   fixes u v::"nat \<Rightarrow> ereal"
  1069   shows "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
  1070 proof (cases)
  1071   assume "(limsup u = \<infinity>) \<or> (limsup v = \<infinity>)"
  1072   then have "limsup u + limsup v = \<infinity>" by simp
  1073   then show ?thesis by auto
  1074 next
  1075   assume "\<not>((limsup u = \<infinity>) \<or> (limsup v = \<infinity>))"
  1076   then have "limsup u < \<infinity>" "limsup v < \<infinity>" by auto
  1077 
  1078   define w where "w = (\<lambda>n. u n + v n)"
  1079   obtain r where r: "subseq r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  1080   obtain s where s: "subseq s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
  1081   obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  1082 
  1083   define a where "a = r o s o t"
  1084   have "subseq a" using r s t by (simp add: a_def subseq_o)
  1085   have l:"(w o a) \<longlonglongrightarrow> limsup w"
  1086          "(u o a) \<longlonglongrightarrow> limsup (u o r)"
  1087          "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
  1088   apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  1089   apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  1090   apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  1091   done
  1092 
  1093   have "limsup (u o r) \<le> limsup u" by (simp add: limsup_subseq_mono r(1))
  1094   then have a: "limsup (u o r) \<noteq> \<infinity>" using \<open>limsup u < \<infinity>\<close> by auto
  1095   have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
  1096   then have b: "limsup (v o r o s) \<noteq> \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
  1097 
  1098   have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)"
  1099     using l tendsto_add_ereal_general a b by fastforce
  1100   moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  1101   ultimately have "(w o a) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)" by simp
  1102   then have "limsup w = limsup (u o r) + limsup (v o r o s)" using l(1) LIMSEQ_unique by blast
  1103   then have "limsup w \<le> limsup u + limsup v"
  1104     using \<open>limsup (u o r) \<le> limsup u\<close> \<open>limsup (v o r o s) \<le> limsup v\<close> ereal_add_mono by simp
  1105   then show ?thesis unfolding w_def by simp
  1106 qed
  1107 
  1108 text \<open>There is an asymmetry between liminfs and limsups in ereal, as $\infty + (-\infty) = \infty$.
  1109 This explains why there are more assumptions in the next lemma dealing with liminfs that in the
  1110 previous one about limsups.\<close>
  1111 
  1112 lemma ereal_liminf_add_mono:
  1113   fixes u v::"nat \<Rightarrow> ereal"
  1114   assumes "\<not>((liminf u = \<infinity> \<and> liminf v = -\<infinity>) \<or> (liminf u = -\<infinity> \<and> liminf v = \<infinity>))"
  1115   shows "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
  1116 proof (cases)
  1117   assume "(liminf u = -\<infinity>) \<or> (liminf v = -\<infinity>)"
  1118   then have *: "liminf u + liminf v = -\<infinity>" using assms by auto
  1119   show ?thesis by (simp add: *)
  1120 next
  1121   assume "\<not>((liminf u = -\<infinity>) \<or> (liminf v = -\<infinity>))"
  1122   then have "liminf u > -\<infinity>" "liminf v > -\<infinity>" by auto
  1123 
  1124   define w where "w = (\<lambda>n. u n + v n)"
  1125   obtain r where r: "subseq r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  1126   obtain s where s: "subseq s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
  1127   obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> liminf (v o r o s)" using liminf_subseq_lim by auto
  1128 
  1129   define a where "a = r o s o t"
  1130   have "subseq a" using r s t by (simp add: a_def subseq_o)
  1131   have l:"(w o a) \<longlonglongrightarrow> liminf w"
  1132          "(u o a) \<longlonglongrightarrow> liminf (u o r)"
  1133          "(v o a) \<longlonglongrightarrow> liminf (v o r o s)"
  1134   apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  1135   apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  1136   apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  1137   done
  1138 
  1139   have "liminf (u o r) \<ge> liminf u" by (simp add: liminf_subseq_mono r(1))
  1140   then have a: "liminf (u o r) \<noteq> -\<infinity>" using \<open>liminf u > -\<infinity>\<close> by auto
  1141   have "liminf (v o r o s) \<ge> liminf v" by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) subseq_o)
  1142   then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using \<open>liminf v > -\<infinity>\<close> by auto
  1143 
  1144   have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)"
  1145     using l tendsto_add_ereal_general a b by fastforce
  1146   moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  1147   ultimately have "(w o a) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)" by simp
  1148   then have "liminf w = liminf (u o r) + liminf (v o r o s)" using l(1) LIMSEQ_unique by blast
  1149   then have "liminf w \<ge> liminf u + liminf v"
  1150     using \<open>liminf (u o r) \<ge> liminf u\<close> \<open>liminf (v o r o s) \<ge> liminf v\<close> ereal_add_mono by simp
  1151   then show ?thesis unfolding w_def by simp
  1152 qed
  1153 
  1154 lemma ereal_limsup_lim_add:
  1155   fixes u v::"nat \<Rightarrow> ereal"
  1156   assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
  1157   shows "limsup (\<lambda>n. u n + v n) = a + limsup v"
  1158 proof -
  1159   have "limsup u = a" using assms(1) using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  1160   have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
  1161   then have "limsup (\<lambda>n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  1162 
  1163   have "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
  1164     by (rule ereal_limsup_add_mono)
  1165   then have up: "limsup (\<lambda>n. u n + v n) \<le> a + limsup v" using \<open>limsup u = a\<close> by simp
  1166 
  1167   have a: "limsup (\<lambda>n. (u n + v n) + (-u n)) \<le> limsup (\<lambda>n. u n + v n) + limsup (\<lambda>n. -u n)"
  1168     by (rule ereal_limsup_add_mono)
  1169   have "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) sequentially" using assms
  1170     real_lim_then_eventually_real by auto
  1171   moreover have "\<And>x. x = ereal(real_of_ereal(x)) \<Longrightarrow> x + (-x) = 0"
  1172     by (metis plus_ereal.simps(1) right_minus uminus_ereal.simps(1) zero_ereal_def)
  1173   ultimately have "eventually (\<lambda>n. u n + (-u n) = 0) sequentially"
  1174     by (metis (mono_tags, lifting) eventually_mono)
  1175   moreover have "\<And>n. u n + (-u n) = 0 \<Longrightarrow> u n + v n + (-u n) = v n"
  1176     by (metis add.commute add.left_commute add.left_neutral)
  1177   ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
  1178     using eventually_mono by force
  1179   then have "limsup v = limsup (\<lambda>n. u n + v n + (-u n))" using Limsup_eq by force
  1180   then have "limsup v \<le> limsup (\<lambda>n. u n + v n) -a" using a \<open>limsup (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
  1181   then have "limsup (\<lambda>n. u n + v n) \<ge> a + limsup v" using assms(2) by (metis add.commute ereal_le_minus)
  1182   then show ?thesis using up by simp
  1183 qed
  1184 
  1185 lemma ereal_limsup_lim_mult:
  1186   fixes u v::"nat \<Rightarrow> ereal"
  1187   assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
  1188   shows "limsup (\<lambda>n. u n * v n) = a * limsup v"
  1189 proof -
  1190   define w where "w = (\<lambda>n. u n * v n)"
  1191   obtain r where r: "subseq r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
  1192   have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
  1193   with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * limsup v" using assms(2) assms(3) by auto
  1194   moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
  1195   ultimately have "(w o r) \<longlonglongrightarrow> a * limsup v" unfolding w_def by presburger
  1196   then have "limsup (w o r) = a * limsup v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  1197   then have I: "limsup w \<ge> a * limsup v" by (metis limsup_subseq_mono r(1))
  1198 
  1199   obtain s where s: "subseq s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  1200   have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
  1201   have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
  1202   moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
  1203   moreover have "(w o s) n / (u o s) n = (v o s) n" if "(u o s) n > 0" "(u o s) n < \<infinity>" for n
  1204     unfolding w_def using that by (auto simp add: ereal_divide_eq)
  1205   ultimately have "eventually (\<lambda>n. (w o s) n / (u o s) n = (v o s) n) sequentially" using eventually_elim2 by force
  1206   moreover have "(\<lambda>n. (w o s) n / (u o s) n) \<longlonglongrightarrow> (limsup w) / a"
  1207     apply (rule tendsto_divide_ereal[OF s(2) *]) using assms(2) assms(3) by auto
  1208   ultimately have "(v o s) \<longlonglongrightarrow> (limsup w) / a" using Lim_transform_eventually by fastforce
  1209   then have "limsup (v o s) = (limsup w) / a" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  1210   then have "limsup v \<ge> (limsup w) / a" by (metis limsup_subseq_mono s(1))
  1211   then have "a * limsup v \<ge> limsup w" using assms(2) assms(3) by (simp add: ereal_divide_le_pos)
  1212   then show ?thesis using I unfolding w_def by auto
  1213 qed
  1214 
  1215 lemma ereal_liminf_lim_mult:
  1216   fixes u v::"nat \<Rightarrow> ereal"
  1217   assumes "u \<longlonglongrightarrow> a" "a>0" "a \<noteq> \<infinity>"
  1218   shows "liminf (\<lambda>n. u n * v n) = a * liminf v"
  1219 proof -
  1220   define w where "w = (\<lambda>n. u n * v n)"
  1221   obtain r where r: "subseq r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
  1222   have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
  1223   with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * liminf v" using assms(2) assms(3) by auto
  1224   moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
  1225   ultimately have "(w o r) \<longlonglongrightarrow> a * liminf v" unfolding w_def by presburger
  1226   then have "liminf (w o r) = a * liminf v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  1227   then have I: "liminf w \<le> a * liminf v" by (metis liminf_subseq_mono r(1))
  1228 
  1229   obtain s where s: "subseq s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  1230   have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
  1231   have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
  1232   moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
  1233   moreover have "(w o s) n / (u o s) n = (v o s) n" if "(u o s) n > 0" "(u o s) n < \<infinity>" for n
  1234     unfolding w_def using that by (auto simp add: ereal_divide_eq)
  1235   ultimately have "eventually (\<lambda>n. (w o s) n / (u o s) n = (v o s) n) sequentially" using eventually_elim2 by force
  1236   moreover have "(\<lambda>n. (w o s) n / (u o s) n) \<longlonglongrightarrow> (liminf w) / a"
  1237     apply (rule tendsto_divide_ereal[OF s(2) *]) using assms(2) assms(3) by auto
  1238   ultimately have "(v o s) \<longlonglongrightarrow> (liminf w) / a" using Lim_transform_eventually by fastforce
  1239   then have "liminf (v o s) = (liminf w) / a" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  1240   then have "liminf v \<le> (liminf w) / a" by (metis liminf_subseq_mono s(1))
  1241   then have "a * liminf v \<le> liminf w" using assms(2) assms(3) by (simp add: ereal_le_divide_pos)
  1242   then show ?thesis using I unfolding w_def by auto
  1243 qed
  1244 
  1245 lemma ereal_liminf_lim_add:
  1246   fixes u v::"nat \<Rightarrow> ereal"
  1247   assumes "u \<longlonglongrightarrow> a" "abs(a) \<noteq> \<infinity>"
  1248   shows "liminf (\<lambda>n. u n + v n) = a + liminf v"
  1249 proof -
  1250   have "liminf u = a" using assms(1) tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  1251   then have *: "abs(liminf u) \<noteq> \<infinity>" using assms(2) by auto
  1252   have "(\<lambda>n. -u n) \<longlonglongrightarrow> -a" using assms(1) by auto
  1253   then have "liminf (\<lambda>n. -u n) = -a" using tendsto_iff_Liminf_eq_Limsup trivial_limit_at_top_linorder by blast
  1254   then have **: "abs(liminf (\<lambda>n. -u n)) \<noteq> \<infinity>" using assms(2) by auto
  1255 
  1256   have "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
  1257     apply (rule ereal_liminf_add_mono) using * by auto
  1258   then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using \<open>liminf u = a\<close> by simp
  1259 
  1260   have a: "liminf (\<lambda>n. (u n + v n) + (-u n)) \<ge> liminf (\<lambda>n. u n + v n) + liminf (\<lambda>n. -u n)"
  1261     apply (rule ereal_liminf_add_mono) using ** by auto
  1262   have "eventually (\<lambda>n. u n = ereal(real_of_ereal(u n))) sequentially" using assms
  1263     real_lim_then_eventually_real by auto
  1264   moreover have "\<And>x. x = ereal(real_of_ereal(x)) \<Longrightarrow> x + (-x) = 0"
  1265     by (metis plus_ereal.simps(1) right_minus uminus_ereal.simps(1) zero_ereal_def)
  1266   ultimately have "eventually (\<lambda>n. u n + (-u n) = 0) sequentially"
  1267     by (metis (mono_tags, lifting) eventually_mono)
  1268   moreover have "\<And>n. u n + (-u n) = 0 \<Longrightarrow> u n + v n + (-u n) = v n"
  1269     by (metis add.commute add.left_commute add.left_neutral)
  1270   ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
  1271     using eventually_mono by force
  1272   then have "liminf v = liminf (\<lambda>n. u n + v n + (-u n))" using Liminf_eq by force
  1273   then have "liminf v \<ge> liminf (\<lambda>n. u n + v n) -a" using a \<open>liminf (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
  1274   then have "liminf (\<lambda>n. u n + v n) \<le> a + liminf v" using assms(2) by (metis add.commute ereal_minus_le)
  1275   then show ?thesis using up by simp
  1276 qed
  1277 
  1278 lemma ereal_liminf_limsup_add:
  1279   fixes u v::"nat \<Rightarrow> ereal"
  1280   shows "liminf (\<lambda>n. u n + v n) \<le> liminf u + limsup v"
  1281 proof (cases)
  1282   assume "limsup v = \<infinity> \<or> liminf u = \<infinity>"
  1283   then show ?thesis by auto
  1284 next
  1285   assume "\<not>(limsup v = \<infinity> \<or> liminf u = \<infinity>)"
  1286   then have "limsup v < \<infinity>" "liminf u < \<infinity>" by auto
  1287 
  1288   define w where "w = (\<lambda>n. u n + v n)"
  1289   obtain r where r: "subseq r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
  1290   obtain s where s: "subseq s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
  1291   obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  1292 
  1293   define a where "a = r o s o t"
  1294   have "subseq a" using r s t by (simp add: a_def subseq_o)
  1295   have l:"(u o a) \<longlonglongrightarrow> liminf u"
  1296          "(w o a) \<longlonglongrightarrow> liminf (w o r)"
  1297          "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
  1298   apply (metis (no_types, lifting) r(2) s(1) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  1299   apply (metis (no_types, lifting) s(2) t(1) LIMSEQ_subseq_LIMSEQ a_def comp_assoc)
  1300   apply (metis (no_types, lifting) t(2) a_def comp_assoc)
  1301   done
  1302 
  1303   have "liminf (w o r) \<ge> liminf w" by (simp add: liminf_subseq_mono r(1))
  1304   have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
  1305   then have b: "limsup (v o r o s) < \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
  1306 
  1307   have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf u + limsup (v o r o s)"
  1308     apply (rule tendsto_add_ereal_general) using b \<open>liminf u < \<infinity>\<close> l(1) l(3) by force+
  1309   moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
  1310   ultimately have "(w o a) \<longlonglongrightarrow> liminf u + limsup (v o r o s)" by simp
  1311   then have "liminf (w o r) = liminf u + limsup (v o r o s)" using l(2) using LIMSEQ_unique by blast
  1312   then have "liminf w \<le> liminf u + limsup v"
  1313     using \<open>liminf (w o r) \<ge> liminf w\<close> \<open>limsup (v o r o s) \<le> limsup v\<close>
  1314     by (metis add_mono_thms_linordered_semiring(2) le_less_trans not_less)
  1315   then show ?thesis unfolding w_def by simp
  1316 qed
  1317 
  1318 lemma ereal_liminf_limsup_minus:
  1319   fixes u v::"nat \<Rightarrow> ereal"
  1320   shows "liminf (\<lambda>n. u n - v n) \<le> limsup u - limsup v"
  1321   unfolding minus_ereal_def
  1322   apply (subst add.commute)
  1323   apply (rule order_trans[OF ereal_liminf_limsup_add])
  1324   using ereal_Limsup_uminus[of sequentially "\<lambda>n. - v n"]
  1325   apply (simp add: add.commute)
  1326   done
  1327 
  1328 
  1329 lemma liminf_minus_ennreal:
  1330   fixes u v::"nat \<Rightarrow> ennreal"
  1331   shows "(\<And>n. v n \<le> u n) \<Longrightarrow> liminf (\<lambda>n. u n - v n) \<le> limsup u - limsup v"
  1332   unfolding liminf_SUP_INF limsup_INF_SUP
  1333   including ennreal.lifting
  1334 proof (transfer, clarsimp)
  1335   fix v u :: "nat \<Rightarrow> ereal" assume *: "\<forall>x. 0 \<le> v x" "\<forall>x. 0 \<le> u x" "\<And>n. v n \<le> u n"
  1336   moreover have "0 \<le> limsup u - limsup v"
  1337     using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp
  1338   moreover have "0 \<le> (SUPREMUM {x..} v)" for x
  1339     using * by (intro SUP_upper2[of x]) auto
  1340   moreover have "0 \<le> (SUPREMUM {x..} u)" for x
  1341     using * by (intro SUP_upper2[of x]) auto
  1342   ultimately show "(SUP n. INF n:{n..}. max 0 (u n - v n))
  1343             \<le> max 0 ((INF x. max 0 (SUPREMUM {x..} u)) - (INF x. max 0 (SUPREMUM {x..} v)))"
  1344     by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
  1345 qed
  1346 
  1347 (*
  1348     Notation
  1349 *)
  1350 
  1351 abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
  1352 
  1353 abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
  1354 
  1355 abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
  1356 
  1357 syntax
  1358 "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
  1359 ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
  1360 
  1361 translations
  1362 "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
  1363 
  1364 (*
  1365     Notation for integration wrt lebesgue measure on the reals:
  1366 
  1367       LBINT x. f
  1368       LBINT x : A. f
  1369 
  1370     TODO: keep all these? Need unicode.
  1371 *)
  1372 
  1373 syntax
  1374 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
  1375 ("(2LBINT _./ _)" [0,60] 60)
  1376 
  1377 syntax
  1378 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
  1379 ("(3LBINT _:_./ _)" [0,60,61] 60)
  1380 
  1381 (*
  1382     Basic properties
  1383 *)
  1384 
  1385 (*
  1386 lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
  1387   by (auto simp add: indicator_def)
  1388 *)
  1389 
  1390 lemma set_borel_measurable_sets:
  1391   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
  1392   assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
  1393   shows "f -` B \<inter> X \<in> sets M"
  1394 proof -
  1395   have "f \<in> borel_measurable (restrict_space M X)"
  1396     using assms by (subst borel_measurable_restrict_space_iff) auto
  1397   then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
  1398     by (rule measurable_sets) fact
  1399   with \<open>X \<in> sets M\<close> show ?thesis
  1400     by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
  1401 qed
  1402 
  1403 lemma set_lebesgue_integral_cong:
  1404   assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
  1405   shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
  1406   using assms by (auto intro!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
  1407 
  1408 lemma set_lebesgue_integral_cong_AE:
  1409   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1410   assumes "AE x \<in> A in M. f x = g x"
  1411   shows "LINT x:A|M. f x = LINT x:A|M. g x"
  1412 proof-
  1413   have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
  1414     using assms by auto
  1415   thus ?thesis by (intro integral_cong_AE) auto
  1416 qed
  1417 
  1418 lemma set_integrable_cong_AE:
  1419     "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
  1420     AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow>
  1421     set_integrable M A f = set_integrable M A g"
  1422   by (rule integrable_cong_AE) auto
  1423 
  1424 lemma set_integrable_subset:
  1425   fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1426   assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"
  1427   shows "set_integrable M B f"
  1428 proof -
  1429   have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
  1430     by (rule integrable_mult_indicator) fact+
  1431   with \<open>B \<subseteq> A\<close> show ?thesis
  1432     by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
  1433 qed
  1434 
  1435 (* TODO: integral_cmul_indicator should be named set_integral_const *)
  1436 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
  1437 
  1438 lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
  1439   by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
  1440 
  1441 lemma set_integral_mult_right [simp]:
  1442   fixes a :: "'a::{real_normed_field, second_countable_topology}"
  1443   shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
  1444   by (subst integral_mult_right_zero[symmetric]) auto
  1445 
  1446 lemma set_integral_mult_left [simp]:
  1447   fixes a :: "'a::{real_normed_field, second_countable_topology}"
  1448   shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
  1449   by (subst integral_mult_left_zero[symmetric]) auto
  1450 
  1451 lemma set_integral_divide_zero [simp]:
  1452   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
  1453   shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
  1454   by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
  1455      (auto split: split_indicator)
  1456 
  1457 lemma set_integrable_scaleR_right [simp, intro]:
  1458   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
  1459   unfolding scaleR_left_commute by (rule integrable_scaleR_right)
  1460 
  1461 lemma set_integrable_scaleR_left [simp, intro]:
  1462   fixes a :: "_ :: {banach, second_countable_topology}"
  1463   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
  1464   using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
  1465 
  1466 lemma set_integrable_mult_right [simp, intro]:
  1467   fixes a :: "'a::{real_normed_field, second_countable_topology}"
  1468   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
  1469   using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
  1470 
  1471 lemma set_integrable_mult_left [simp, intro]:
  1472   fixes a :: "'a::{real_normed_field, second_countable_topology}"
  1473   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
  1474   using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
  1475 
  1476 lemma set_integrable_divide [simp, intro]:
  1477   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
  1478   assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
  1479   shows "set_integrable M A (\<lambda>t. f t / a)"
  1480 proof -
  1481   have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
  1482     using assms by (rule integrable_divide_zero)
  1483   also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
  1484     by (auto split: split_indicator)
  1485   finally show ?thesis .
  1486 qed
  1487 
  1488 lemma set_integral_add [simp, intro]:
  1489   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1490   assumes "set_integrable M A f" "set_integrable M A g"
  1491   shows "set_integrable M A (\<lambda>x. f x + g x)"
  1492     and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
  1493   using assms by (simp_all add: scaleR_add_right)
  1494 
  1495 lemma set_integral_diff [simp, intro]:
  1496   assumes "set_integrable M A f" "set_integrable M A g"
  1497   shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
  1498     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
  1499   using assms by (simp_all add: scaleR_diff_right)
  1500 
  1501 (* question: why do we have this for negation, but multiplication by a constant
  1502    requires an integrability assumption? *)
  1503 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
  1504   by (subst integral_minus[symmetric]) simp_all
  1505 
  1506 lemma set_integral_complex_of_real:
  1507   "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
  1508   by (subst integral_complex_of_real[symmetric])
  1509      (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
  1510 
  1511 lemma set_integral_mono:
  1512   fixes f g :: "_ \<Rightarrow> real"
  1513   assumes "set_integrable M A f" "set_integrable M A g"
  1514     "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
  1515   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
  1516 using assms by (auto intro: integral_mono split: split_indicator)
  1517 
  1518 lemma set_integral_mono_AE:
  1519   fixes f g :: "_ \<Rightarrow> real"
  1520   assumes "set_integrable M A f" "set_integrable M A g"
  1521     "AE x \<in> A in M. f x \<le> g x"
  1522   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
  1523 using assms by (auto intro: integral_mono_AE split: split_indicator)
  1524 
  1525 lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
  1526   using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
  1527 
  1528 lemma set_integrable_abs_iff:
  1529   fixes f :: "_ \<Rightarrow> real"
  1530   shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
  1531   by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
  1532 
  1533 lemma set_integrable_abs_iff':
  1534   fixes f :: "_ \<Rightarrow> real"
  1535   shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
  1536     set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
  1537 by (intro set_integrable_abs_iff) auto
  1538 
  1539 lemma set_integrable_discrete_difference:
  1540   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1541   assumes "countable X"
  1542   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
  1543   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1544   shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
  1545 proof (rule integrable_discrete_difference[where X=X])
  1546   show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
  1547     using diff by (auto split: split_indicator)
  1548 qed fact+
  1549 
  1550 lemma set_integral_discrete_difference:
  1551   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  1552   assumes "countable X"
  1553   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
  1554   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
  1555   shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
  1556 proof (rule integral_discrete_difference[where X=X])
  1557   show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
  1558     using diff by (auto split: split_indicator)
  1559 qed fact+
  1560 
  1561 lemma set_integrable_Un:
  1562   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1563   assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
  1564     and [measurable]: "A \<in> sets M" "B \<in> sets M"
  1565   shows "set_integrable M (A \<union> B) f"
  1566 proof -
  1567   have "set_integrable M (A - B) f"
  1568     using f_A by (rule set_integrable_subset) auto
  1569   from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
  1570     by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
  1571 qed
  1572 
  1573 lemma set_integrable_UN:
  1574   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1575   assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
  1576     "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
  1577   shows "set_integrable M (\<Union>i\<in>I. A i) f"
  1578 using assms by (induct I) (auto intro!: set_integrable_Un)
  1579 
  1580 lemma set_integral_Un:
  1581   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1582   assumes "A \<inter> B = {}"
  1583   and "set_integrable M A f"
  1584   and "set_integrable M B f"
  1585   shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
  1586 by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
  1587       scaleR_add_left assms)
  1588 
  1589 lemma set_integral_cong_set:
  1590   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1591   assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
  1592     and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
  1593   shows "LINT x:B|M. f x = LINT x:A|M. f x"
  1594 proof (rule integral_cong_AE)
  1595   show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
  1596     using ae by (auto simp: subset_eq split: split_indicator)
  1597 qed fact+
  1598 
  1599 lemma set_borel_measurable_subset:
  1600   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1601   assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
  1602   shows "set_borel_measurable M B f"
  1603 proof -
  1604   have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
  1605     by measurable
  1606   also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
  1607     using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator)
  1608   finally show ?thesis .
  1609 qed
  1610 
  1611 lemma set_integral_Un_AE:
  1612   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1613   assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
  1614   and "set_integrable M A f"
  1615   and "set_integrable M B f"
  1616   shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
  1617 proof -
  1618   have f: "set_integrable M (A \<union> B) f"
  1619     by (intro set_integrable_Un assms)
  1620   then have f': "set_borel_measurable M (A \<union> B) f"
  1621     by (rule borel_measurable_integrable)
  1622   have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
  1623   proof (rule set_integral_cong_set)
  1624     show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
  1625       using ae by auto
  1626     show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
  1627       using f' by (rule set_borel_measurable_subset) auto
  1628   qed fact
  1629   also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)"
  1630     by (auto intro!: set_integral_Un set_integrable_subset[OF f])
  1631   also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
  1632     using ae
  1633     by (intro arg_cong2[where f="op+"] set_integral_cong_set)
  1634        (auto intro!: set_borel_measurable_subset[OF f'])
  1635   finally show ?thesis .
  1636 qed
  1637 
  1638 lemma set_integral_finite_Union:
  1639   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  1640   assumes "finite I" "disjoint_family_on A I"
  1641     and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
  1642   shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
  1643   using assms
  1644   apply induct
  1645   apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
  1646 by (subst set_integral_Un, auto intro: set_integrable_UN)
  1647 
  1648 (* TODO: find a better name? *)
  1649 lemma pos_integrable_to_top:
  1650   fixes l::real
  1651   assumes "\<And>i. A i \<in> sets M" "mono A"
  1652   assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
  1653   and intgbl: "\<And>i::nat. set_integrable M (A i) f"
  1654   and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
  1655   shows "set_integrable M (\<Union>i. A i) f"
  1656   apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
  1657   apply (rule intgbl)
  1658   prefer 3 apply (rule lim)
  1659   apply (rule AE_I2)
  1660   using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
  1661 proof (rule AE_I2)
  1662   { fix x assume "x \<in> space M"
  1663     show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
  1664     proof cases
  1665       assume "\<exists>i. x \<in> A i"
  1666       then guess i ..
  1667       then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
  1668         using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
  1669       show ?thesis
  1670         apply (intro Lim_eventually)
  1671         using *
  1672         apply eventually_elim
  1673         apply (auto split: split_indicator)
  1674         done
  1675     qed auto }
  1676   then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
  1677     apply (rule borel_measurable_LIMSEQ_real)
  1678     apply assumption
  1679     apply (intro borel_measurable_integrable intgbl)
  1680     done
  1681 qed
  1682 
  1683 (* Proof from Royden Real Analysis, p. 91. *)
  1684 lemma lebesgue_integral_countable_add:
  1685   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1686   assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
  1687     and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
  1688     and intgbl: "set_integrable M (\<Union>i. A i) f"
  1689   shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
  1690 proof (subst integral_suminf[symmetric])
  1691   show int_A: "\<And>i. set_integrable M (A i) f"
  1692     using intgbl by (rule set_integrable_subset) auto
  1693   { fix x assume "x \<in> space M"
  1694     have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
  1695       by (intro sums_scaleR_left indicator_sums) fact }
  1696   note sums = this
  1697 
  1698   have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
  1699     using int_A[THEN integrable_norm] by auto
  1700 
  1701   show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
  1702     using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
  1703 
  1704   show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
  1705   proof (rule summableI_nonneg_bounded)
  1706     fix n
  1707     show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
  1708       using norm_f by (auto intro!: integral_nonneg_AE)
  1709 
  1710     have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
  1711       (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
  1712       by (simp add: abs_mult)
  1713     also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
  1714       using norm_f
  1715       by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
  1716     also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
  1717       using intgbl[THEN integrable_norm]
  1718       by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
  1719          (auto split: split_indicator)
  1720     finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
  1721       set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
  1722       by simp
  1723   qed
  1724   show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
  1725     apply (rule Bochner_Integration.integral_cong[OF refl])
  1726     apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
  1727     using sums_unique[OF indicator_sums[OF disj]]
  1728     apply auto
  1729     done
  1730 qed
  1731 
  1732 lemma set_integral_cont_up:
  1733   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1734   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
  1735   and intgbl: "set_integrable M (\<Union>i. A i) f"
  1736   shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
  1737 proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
  1738   have int_A: "\<And>i. set_integrable M (A i) f"
  1739     using intgbl by (rule set_integrable_subset) auto
  1740   then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
  1741     "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
  1742     using intgbl integrable_norm[OF intgbl] by auto
  1743 
  1744   { fix x i assume "x \<in> A i"
  1745     with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
  1746       by (intro filterlim_cong refl)
  1747          (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
  1748   then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
  1749     by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
  1750 qed (auto split: split_indicator)
  1751 
  1752 (* Can the int0 hypothesis be dropped? *)
  1753 lemma set_integral_cont_down:
  1754   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
  1755   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
  1756   and int0: "set_integrable M (A 0) f"
  1757   shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
  1758 proof (rule integral_dominated_convergence)
  1759   have int_A: "\<And>i. set_integrable M (A i) f"
  1760     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
  1761   show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
  1762     using int0[THEN integrable_norm] by simp
  1763   have "set_integrable M (\<Inter>i. A i) f"
  1764     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
  1765   with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
  1766     by auto
  1767   show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
  1768     using A by (auto split: split_indicator simp: decseq_def)
  1769   { fix x i assume "x \<in> space M" "x \<notin> A i"
  1770     with A have "(\<lambda>i. indicator (A i) x::real) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<lambda>i. 0::real) \<longlonglongrightarrow> 0"
  1771       by (intro filterlim_cong refl)
  1772          (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
  1773   then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x *\<^sub>R f x"
  1774     by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
  1775 qed
  1776 
  1777 lemma set_integral_at_point:
  1778   fixes a :: real
  1779   assumes "set_integrable M {a} f"
  1780   and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
  1781   shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
  1782 proof-
  1783   have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
  1784     by (intro set_lebesgue_integral_cong) simp_all
  1785   then show ?thesis using assms by simp
  1786 qed
  1787 
  1788 
  1789 abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
  1790   "complex_integrable M f \<equiv> integrable M f"
  1791 
  1792 abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
  1793   "integral\<^sup>C M f == integral\<^sup>L M f"
  1794 
  1795 syntax
  1796   "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
  1797  ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
  1798 
  1799 translations
  1800   "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
  1801 
  1802 syntax
  1803   "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
  1804   ("(3CLINT _|_. _)" [0,110,60] 60)
  1805 
  1806 translations
  1807   "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
  1808 
  1809 lemma complex_integrable_cnj [simp]:
  1810   "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f"
  1811 proof
  1812   assume "complex_integrable M (\<lambda>x. cnj (f x))"
  1813   then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))"
  1814     by (rule integrable_cnj)
  1815   then show "complex_integrable M f"
  1816     by simp
  1817 qed simp
  1818 
  1819 lemma complex_of_real_integrable_eq:
  1820   "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f"
  1821 proof
  1822   assume "complex_integrable M (\<lambda>x. complex_of_real (f x))"
  1823   then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))"
  1824     by (rule integrable_Re)
  1825   then show "integrable M f"
  1826     by simp
  1827 qed simp
  1828 
  1829 
  1830 abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
  1831   "complex_set_integrable M A f \<equiv> set_integrable M A f"
  1832 
  1833 abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
  1834   "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
  1835 
  1836 syntax
  1837 "_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
  1838 ("(4CLINT _:_|_. _)" [0,60,110,61] 60)
  1839 
  1840 translations
  1841 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
  1842 
  1843 lemma set_borel_measurable_continuous:
  1844   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
  1845   assumes "S \<in> sets borel" "continuous_on S f"
  1846   shows "set_borel_measurable borel S f"
  1847 proof -
  1848   have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel"
  1849     by (intro assms borel_measurable_continuous_on_if continuous_on_const)
  1850   also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)"
  1851     by auto
  1852   finally show ?thesis .
  1853 qed
  1854 
  1855 lemma set_measurable_continuous_on_ivl:
  1856   assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
  1857   shows "set_borel_measurable borel {a..b} f"
  1858   by (rule set_borel_measurable_continuous[OF _ assms]) simp
  1859 
  1860 
  1861 text\<open>This notation is from Sébastien Gouëzel: His use is not directly in line with the
  1862 notations in this file, they are more in line with sum, and more readable he thinks.\<close>
  1863 
  1864 abbreviation "set_nn_integral M A f \<equiv> nn_integral M (\<lambda>x. f x * indicator A x)"
  1865 
  1866 syntax
  1867 "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
  1868 ("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
  1869 
  1870 "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
  1871 ("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
  1872 
  1873 translations
  1874 "\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
  1875 "\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
  1876 
  1877 lemma nn_integral_disjoint_pair:
  1878   assumes [measurable]: "f \<in> borel_measurable M"
  1879           "B \<in> sets M" "C \<in> sets M"
  1880           "B \<inter> C = {}"
  1881   shows "(\<integral>\<^sup>+x \<in> B \<union> C. f x \<partial>M) = (\<integral>\<^sup>+x \<in> B. f x \<partial>M) + (\<integral>\<^sup>+x \<in> C. f x \<partial>M)"
  1882 proof -
  1883   have mes: "\<And>D. D \<in> sets M \<Longrightarrow> (\<lambda>x. f x * indicator D x) \<in> borel_measurable M" by simp
  1884   have pos: "\<And>D. AE x in M. f x * indicator D x \<ge> 0" using assms(2) by auto
  1885   have "\<And>x. f x * indicator (B \<union> C) x = f x * indicator B x + f x * indicator C x" using assms(4)
  1886     by (auto split: split_indicator)
  1887   then have "(\<integral>\<^sup>+x. f x * indicator (B \<union> C) x \<partial>M) = (\<integral>\<^sup>+x. f x * indicator B x + f x * indicator C x \<partial>M)"
  1888     by simp
  1889   also have "... = (\<integral>\<^sup>+x. f x * indicator B x \<partial>M) + (\<integral>\<^sup>+x. f x * indicator C x \<partial>M)"
  1890     by (rule nn_integral_add) (auto simp add: assms mes pos)
  1891   finally show ?thesis by simp
  1892 qed
  1893 
  1894 lemma nn_integral_disjoint_pair_countspace:
  1895   assumes "B \<inter> C = {}"
  1896   shows "(\<integral>\<^sup>+x \<in> B \<union> C. f x \<partial>count_space UNIV) = (\<integral>\<^sup>+x \<in> B. f x \<partial>count_space UNIV) + (\<integral>\<^sup>+x \<in> C. f x \<partial>count_space UNIV)"
  1897 by (rule nn_integral_disjoint_pair) (simp_all add: assms)
  1898 
  1899 lemma nn_integral_null_delta:
  1900   assumes "A \<in> sets M" "B \<in> sets M"
  1901           "(A - B) \<union> (B - A) \<in> null_sets M"
  1902   shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> B. f x \<partial>M)"
  1903 proof (rule nn_integral_cong_AE, auto simp add: indicator_def)
  1904   have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
  1905     using assms(3) AE_not_in by blast
  1906   then show "AE a in M. a \<notin> A \<longrightarrow> a \<in> B \<longrightarrow> f a = 0"
  1907     by auto
  1908   show "AE x\<in>A in M. x \<notin> B \<longrightarrow> f x = 0"
  1909     using * by auto
  1910 qed
  1911 
  1912 lemma nn_integral_disjoint_family:
  1913   assumes [measurable]: "f \<in> borel_measurable M" "\<And>(n::nat). B n \<in> sets M"
  1914       and "disjoint_family B"
  1915   shows "(\<integral>\<^sup>+x \<in> (\<Union>n. B n). f x \<partial>M) = (\<Sum>n. (\<integral>\<^sup>+x \<in> B n. f x \<partial>M))"
  1916 proof -
  1917   have "(\<integral>\<^sup>+ x. (\<Sum>n. f x * indicator (B n) x) \<partial>M) = (\<Sum>n. (\<integral>\<^sup>+ x. f x * indicator (B n) x \<partial>M))"
  1918     by (rule nn_integral_suminf) simp
  1919   moreover have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (\<Union>n. B n) x" for x
  1920   proof (cases)
  1921     assume "x \<in> (\<Union>n. B n)"
  1922     then obtain n where "x \<in> B n" by blast
  1923     have a: "finite {n}" by simp
  1924     have "\<And>i. i \<noteq> n \<Longrightarrow> x \<notin> B i" using \<open>x \<in> B n\<close> assms(3) disjoint_family_on_def
  1925       by (metis IntI UNIV_I empty_iff)
  1926     then have "\<And>i. i \<notin> {n} \<Longrightarrow> indicator (B i) x = (0::ennreal)" using indicator_def by simp
  1927     then have b: "\<And>i. i \<notin> {n} \<Longrightarrow> f x * indicator (B i) x = (0::ennreal)" by simp
  1928 
  1929     define h where "h = (\<lambda>i. f x * indicator (B i) x)"
  1930     then have "\<And>i. i \<notin> {n} \<Longrightarrow> h i = 0" using b by simp
  1931     then have "(\<Sum>i. h i) = (\<Sum>i\<in>{n}. h i)"
  1932       by (metis sums_unique[OF sums_finite[OF a]])
  1933     then have "(\<Sum>i. h i) = h n" by simp
  1934     then have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (B n) x" using h_def by simp
  1935     then have "(\<Sum>n. f x * indicator (B n) x) = f x" using \<open>x \<in> B n\<close> indicator_def by simp
  1936     then show ?thesis using \<open>x \<in> (\<Union>n. B n)\<close> by auto
  1937   next
  1938     assume "x \<notin> (\<Union>n. B n)"
  1939     then have "\<And>n. f x * indicator (B n) x = 0" by simp
  1940     have "(\<Sum>n. f x * indicator (B n) x) = 0"
  1941       by (simp add: \<open>\<And>n. f x * indicator (B n) x = 0\<close>)
  1942     then show ?thesis using \<open>x \<notin> (\<Union>n. B n)\<close> by auto
  1943   qed
  1944   ultimately show ?thesis by simp
  1945 qed
  1946 
  1947 lemma nn_set_integral_add:
  1948   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1949           "A \<in> sets M"
  1950   shows "(\<integral>\<^sup>+x \<in> A. (f x + g x) \<partial>M) = (\<integral>\<^sup>+x \<in> A. f x \<partial>M) + (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
  1951 proof -
  1952   have "(\<integral>\<^sup>+x \<in> A. (f x + g x) \<partial>M) = (\<integral>\<^sup>+x. (f x * indicator A x + g x * indicator A x) \<partial>M)"
  1953     by (auto simp add: indicator_def intro!: nn_integral_cong)
  1954   also have "... = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + (\<integral>\<^sup>+x. g x * indicator A x \<partial>M)"
  1955     apply (rule nn_integral_add) using assms(1) assms(2) by auto
  1956   finally show ?thesis by simp
  1957 qed
  1958 
  1959 lemma nn_set_integral_cong:
  1960   assumes "AE x in M. f x = g x"
  1961   shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
  1962 apply (rule nn_integral_cong_AE) using assms(1) by auto
  1963 
  1964 lemma nn_set_integral_set_mono:
  1965   "A \<subseteq> B \<Longrightarrow> (\<integral>\<^sup>+ x \<in> A. f x \<partial>M) \<le> (\<integral>\<^sup>+ x \<in> B. f x \<partial>M)"
  1966 by (auto intro!: nn_integral_mono split: split_indicator)
  1967 
  1968 lemma nn_set_integral_mono:
  1969   assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  1970           "A \<in> sets M"
  1971       and "AE x\<in>A in M. f x \<le> g x"
  1972   shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) \<le> (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
  1973 by (auto intro!: nn_integral_mono_AE split: split_indicator simp: assms)
  1974 
  1975 lemma nn_set_integral_space [simp]:
  1976   shows "(\<integral>\<^sup>+ x \<in> space M. f x \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
  1977 by (metis (mono_tags, lifting) indicator_simps(1) mult.right_neutral nn_integral_cong)
  1978 
  1979 lemma nn_integral_count_compose_inj:
  1980   assumes "inj_on g A"
  1981   shows "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
  1982 proof -
  1983   have "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+x. f (g x) \<partial>count_space A)"
  1984     by (auto simp add: nn_integral_count_space_indicator[symmetric])
  1985   also have "... = (\<integral>\<^sup>+y. f y \<partial>count_space (g`A))"
  1986     by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw)
  1987   also have "... = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
  1988     by (auto simp add: nn_integral_count_space_indicator[symmetric])
  1989   finally show ?thesis by simp
  1990 qed
  1991 
  1992 lemma nn_integral_count_compose_bij:
  1993   assumes "bij_betw g A B"
  1994   shows "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> B. f y \<partial>count_space UNIV)"
  1995 proof -
  1996   have "inj_on g A" using assms bij_betw_def by auto
  1997   then have "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
  1998     by (rule nn_integral_count_compose_inj)
  1999   then show ?thesis using assms by (simp add: bij_betw_def)
  2000 qed
  2001 
  2002 lemma set_integral_null_delta:
  2003   fixes f::"_ \<Rightarrow> _ :: {banach, second_countable_topology}"
  2004   assumes [measurable]: "integrable M f" "A \<in> sets M" "B \<in> sets M"
  2005     and "(A - B) \<union> (B - A) \<in> null_sets M"
  2006   shows "(\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> B. f x \<partial>M)"
  2007 proof (rule set_integral_cong_set, auto)
  2008   have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
  2009     using assms(4) AE_not_in by blast
  2010   then show "AE x in M. (x \<in> B) = (x \<in> A)"
  2011     by auto
  2012 qed
  2013 
  2014 lemma set_integral_space:
  2015   assumes "integrable M f"
  2016   shows "(\<integral>x \<in> space M. f x \<partial>M) = (\<integral>x. f x \<partial>M)"
  2017 by (metis (mono_tags, lifting) indicator_simps(1) Bochner_Integration.integral_cong real_vector.scale_one)
  2018 
  2019 lemma null_if_pos_func_has_zero_nn_int:
  2020   fixes f::"'a \<Rightarrow> ennreal"
  2021   assumes [measurable]: "f \<in> borel_measurable M" "A \<in> sets M"
  2022     and "AE x\<in>A in M. f x > 0" "(\<integral>\<^sup>+x\<in>A. f x \<partial>M) = 0"
  2023   shows "A \<in> null_sets M"
  2024 proof -
  2025   have "AE x in M. f x * indicator A x = 0"
  2026     by (subst nn_integral_0_iff_AE[symmetric], auto simp add: assms(4))
  2027   then have "AE x\<in>A in M. False" using assms(3) by auto
  2028   then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
  2029 qed
  2030 
  2031 lemma null_if_pos_func_has_zero_int:
  2032   assumes [measurable]: "integrable M f" "A \<in> sets M"
  2033       and "AE x\<in>A in M. f x > 0" "(\<integral>x\<in>A. f x \<partial>M) = (0::real)"
  2034   shows "A \<in> null_sets M"
  2035 proof -
  2036   have "AE x in M. indicator A x * f x = 0"
  2037     apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
  2038     using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
  2039   then have "AE x\<in>A in M. f x = 0" by auto
  2040   then have "AE x\<in>A in M. False" using assms(3) by auto
  2041   then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
  2042 qed
  2043 
  2044 text\<open>The next lemma is a variant of \<open>density_unique\<close>. Note that it uses the notation
  2045 for nonnegative set integrals introduced earlier.\<close>
  2046 
  2047 lemma (in sigma_finite_measure) density_unique2:
  2048   assumes [measurable]: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
  2049   assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+ x \<in> A. f' x \<partial>M)"
  2050   shows "AE x in M. f x = f' x"
  2051 proof (rule density_unique)
  2052   show "density M f = density M f'"
  2053     by (intro measure_eqI) (auto simp: emeasure_density intro!: density_eq)
  2054 qed (auto simp add: assms)
  2055 
  2056 
  2057 text \<open>The next lemma implies the same statement for Banach-space valued functions
  2058 using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I
  2059 only formulate it for real-valued functions.\<close>
  2060 
  2061 lemma density_unique_real:
  2062   fixes f f'::"_ \<Rightarrow> real"
  2063   assumes [measurable]: "integrable M f" "integrable M f'"
  2064   assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M)"
  2065   shows "AE x in M. f x = f' x"
  2066 proof -
  2067   define A where "A = {x \<in> space M. f x < f' x}"
  2068   then have [measurable]: "A \<in> sets M" by simp
  2069   have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M) - (\<integral>x \<in> A. f x \<partial>M)"
  2070     using \<open>A \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
  2071   then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
  2072   then have "A \<in> null_sets M"
  2073     using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
  2074   then have "AE x in M. x \<notin> A" by (simp add: AE_not_in)
  2075   then have *: "AE x in M. f' x \<le> f x" unfolding A_def by auto
  2076 
  2077 
  2078   define B where "B = {x \<in> space M. f' x < f x}"
  2079   then have [measurable]: "B \<in> sets M" by simp
  2080   have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = (\<integral>x \<in> B. f x \<partial>M) - (\<integral>x \<in> B. f' x \<partial>M)"
  2081     using \<open>B \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
  2082   then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
  2083   then have "B \<in> null_sets M"
  2084     using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
  2085   then have "AE x in M. x \<notin> B" by (simp add: AE_not_in)
  2086   then have "AE x in M. f' x \<ge> f x" unfolding B_def by auto
  2087 
  2088   then show ?thesis using * by auto
  2089 qed
  2090 
  2091 text \<open>The next lemma shows that $L^1$ convergence of a sequence of functions follows from almost
  2092 everywhere convergence and the weaker condition of the convergence of the integrated norms (or even
  2093 just the nontrivial inequality about them). Useful in a lot of contexts! This statement (or its
  2094 variations) are known as Scheffe lemma.
  2095 
  2096 The formalization is more painful as one should jump back and forth between reals and ereals and justify
  2097 all the time positivity or integrability (thankfully, measurability is handled more or less automatically).\<close>
  2098 
  2099 lemma Scheffe_lemma1:
  2100   assumes "\<And>n. integrable M (F n)" "integrable M f"
  2101           "AE x in M. (\<lambda>n. F n x) \<longlonglongrightarrow> f x"
  2102           "limsup (\<lambda>n. \<integral>\<^sup>+ x. norm(F n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
  2103   shows "(\<lambda>n. \<integral>\<^sup>+ x. norm(F n x - f x) \<partial>M) \<longlonglongrightarrow> 0"
  2104 proof -
  2105   have [measurable]: "\<And>n. F n \<in> borel_measurable M" "f \<in> borel_measurable M"
  2106     using assms(1) assms(2) by simp_all
  2107   define G where "G = (\<lambda>n x. norm(f x) + norm(F n x) - norm(F n x - f x))"
  2108   have [measurable]: "\<And>n. G n \<in> borel_measurable M" unfolding G_def by simp
  2109   have G_pos[simp]: "\<And>n x. G n x \<ge> 0"
  2110     unfolding G_def by (metis ge_iff_diff_ge_0 norm_minus_commute norm_triangle_ineq4)
  2111   have finint: "(\<integral>\<^sup>+ x. norm(f x) \<partial>M) \<noteq> \<infinity>"
  2112     using has_bochner_integral_implies_finite_norm[OF has_bochner_integral_integrable[OF \<open>integrable M f\<close>]]
  2113     by simp
  2114   then have fin2: "2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M) \<noteq> \<infinity>"
  2115     by (auto simp: ennreal_mult_eq_top_iff)
  2116 
  2117   {
  2118     fix x assume *: "(\<lambda>n. F n x) \<longlonglongrightarrow> f x"
  2119     then have "(\<lambda>n. norm(F n x)) \<longlonglongrightarrow> norm(f x)" using tendsto_norm by blast
  2120     moreover have "(\<lambda>n. norm(F n x - f x)) \<longlonglongrightarrow> 0" using * Lim_null tendsto_norm_zero_iff by fastforce
  2121     ultimately have a: "(\<lambda>n. norm(F n x) - norm(F n x - f x)) \<longlonglongrightarrow> norm(f x)" using tendsto_diff by fastforce
  2122     have "(\<lambda>n. norm(f x) + (norm(F n x) - norm(F n x - f x))) \<longlonglongrightarrow> norm(f x) + norm(f x)"
  2123       by (rule tendsto_add) (auto simp add: a)
  2124     moreover have "\<And>n. G n x = norm(f x) + (norm(F n x) - norm(F n x - f x))" unfolding G_def by simp
  2125     ultimately have "(\<lambda>n. G n x) \<longlonglongrightarrow> 2 * norm(f x)" by simp
  2126     then have "(\<lambda>n. ennreal(G n x)) \<longlonglongrightarrow> ennreal(2 * norm(f x))" by simp
  2127     then have "liminf (\<lambda>n. ennreal(G n x)) = ennreal(2 * norm(f x))"
  2128       using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
  2129   }
  2130   then have "AE x in M. liminf (\<lambda>n. ennreal(G n x)) = ennreal(2 * norm(f x))" using assms(3) by auto
  2131   then have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. ennreal (G n x)) \<partial>M) = (\<integral>\<^sup>+ x. 2 * ennreal(norm(f x)) \<partial>M)"
  2132     by (simp add: nn_integral_cong_AE ennreal_mult)
  2133   also have "... = 2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M)" by (rule nn_integral_cmult) auto
  2134   finally have int_liminf: "(\<integral>\<^sup>+ x. liminf (\<lambda>n. ennreal (G n x)) \<partial>M) = 2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
  2135     by simp
  2136 
  2137   have "(\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) = (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(F n x) \<partial>M)" for n
  2138     by (rule nn_integral_add) (auto simp add: assms)
  2139   then have "limsup (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M)) =
  2140       limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(F n x) \<partial>M))"
  2141     by simp
  2142   also have "... = (\<integral>\<^sup>+x. norm(f x) \<partial>M) + limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x) \<partial>M))"
  2143     by (rule Limsup_const_add, auto simp add: finint)
  2144   also have "... \<le> (\<integral>\<^sup>+x. norm(f x) \<partial>M) + (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
  2145     using assms(4) by (simp add: add_left_mono)
  2146   also have "... = 2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
  2147     unfolding one_add_one[symmetric] distrib_right by simp
  2148   ultimately have a: "limsup (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M)) \<le>
  2149     2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)" by simp
  2150 
  2151   have le: "ennreal (norm (F n x - f x)) \<le> ennreal (norm (f x)) + ennreal (norm (F n x))" for n x
  2152     by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_plus[symmetric] ennreal_minus del: ennreal_plus)
  2153   then have le2: "(\<integral>\<^sup>+ x. ennreal (norm (F n x - f x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) + ennreal (norm (F n x)) \<partial>M)" for n
  2154     by (rule nn_integral_mono)
  2155 
  2156   have "2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M) = (\<integral>\<^sup>+ x. liminf (\<lambda>n. ennreal (G n x)) \<partial>M)"
  2157     by (simp add: int_liminf)
  2158   also have "\<dots> \<le> liminf (\<lambda>n. (\<integral>\<^sup>+x. G n x \<partial>M))"
  2159     by (rule nn_integral_liminf) auto
  2160   also have "liminf (\<lambda>n. (\<integral>\<^sup>+x. G n x \<partial>M)) =
  2161     liminf (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M))"
  2162   proof (intro arg_cong[where f=liminf] ext)
  2163     fix n
  2164     have "\<And>x. ennreal(G n x) = ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x))"
  2165       unfolding G_def by (simp add: ennreal_plus[symmetric] ennreal_minus del: ennreal_plus)
  2166     moreover have "(\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x)) \<partial>M)
  2167             = (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)"
  2168     proof (rule nn_integral_diff)
  2169       from le show "AE x in M. ennreal (norm (F n x - f x)) \<le> ennreal (norm (f x)) + ennreal (norm (F n x))"
  2170         by simp
  2171       from le2 have "(\<integral>\<^sup>+x. ennreal (norm (F n x - f x)) \<partial>M) < \<infinity>" using assms(1) assms(2)
  2172         by (metis has_bochner_integral_implies_finite_norm integrable.simps Bochner_Integration.integrable_diff)
  2173       then show "(\<integral>\<^sup>+x. ennreal (norm (F n x - f x)) \<partial>M) \<noteq> \<infinity>" by simp
  2174     qed (auto simp add: assms)
  2175     ultimately show "(\<integral>\<^sup>+x. G n x \<partial>M) = (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)"
  2176       by simp
  2177   qed
  2178   finally have "2 * (\<integral>\<^sup>+ x. norm(f x) \<partial>M) + limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)) \<le>
  2179     liminf (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)) +
  2180     limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M))"
  2181     by (intro add_mono) auto
  2182   also have "\<dots> \<le> (limsup (\<lambda>n. \<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - limsup (\<lambda>n. \<integral>\<^sup>+x. norm (F n x - f x) \<partial>M)) +
  2183     limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M))"
  2184     by (intro add_mono liminf_minus_ennreal le2) auto
  2185   also have "\<dots> = limsup (\<lambda>n. (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M))"
  2186     by (intro diff_add_cancel_ennreal Limsup_mono always_eventually allI le2)
  2187   also have "\<dots> \<le> 2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)"
  2188     by fact
  2189   finally have "limsup (\<lambda>n. (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)) = 0"
  2190     using fin2 by simp
  2191   then show ?thesis
  2192     by (rule tendsto_0_if_Limsup_eq_0_ennreal)
  2193 qed
  2194 
  2195 lemma Scheffe_lemma2:
  2196   fixes F::"nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  2197   assumes "\<And> n::nat. F n \<in> borel_measurable M" "integrable M f"
  2198           "AE x in M. (\<lambda>n. F n x) \<longlonglongrightarrow> f x"
  2199           "\<And>n. (\<integral>\<^sup>+ x. norm(F n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
  2200   shows "(\<lambda>n. \<integral>\<^sup>+ x. norm(F n x - f x) \<partial>M) \<longlonglongrightarrow> 0"
  2201 proof (rule Scheffe_lemma1)
  2202   fix n::nat
  2203   have "(\<integral>\<^sup>+ x. norm(f x) \<partial>M) < \<infinity>" using assms(2) by (metis has_bochner_integral_implies_finite_norm integrable.cases)
  2204   then have "(\<integral>\<^sup>+ x. norm(F n x) \<partial>M) < \<infinity>" using assms(4)[of n] by auto
  2205   then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n])
  2206 qed (auto simp add: assms Limsup_bounded)
  2207 
  2208 end