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 (fA)"

   115 proof -

   116   have "(inv f) (Inf (fA)) \<le> Inf ((inv f)(fA))"

   117     using mono_Inf[OF mono_inv[OF assms], of "fA"] by simp

   118   then have "Inf (fA) \<le> f (Inf ((inv f)(fA)))"

   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> gA. 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 (gA))"

  1986     by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw)

  1987   also have "... = (\<integral>\<^sup>+y \<in> gA. 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> gA. 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
`