# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1568720164 -3600
# Node ID 47258727fa42f4b562b7e7be68f067fe310f49dc
# Parent  99e24569cc1f3ac0ef00a04dc5539c179d8724dc
A few new theorems, tidying up and deletion of obsolete material

diff -r 99e24569cc1f -r 47258727fa42 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Sep 16 23:51:24 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Sep 17 12:36:04 2019 +0100
@@ -1108,6 +1108,48 @@
   shows "\<lbrakk>f absolutely_integrable_on S; {a..b} \<subseteq> S\<rbrakk> \<Longrightarrow> f absolutely_integrable_on {a..b}"
   using absolutely_integrable_on_subcbox by fastforce
 
+lemma integrable_subinterval:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "integrable (lebesgue_on {a..b}) f"
+    and "{c..d} \<subseteq> {a..b}"
+  shows "integrable (lebesgue_on {c..d}) f"
+proof (rule absolutely_integrable_imp_integrable)
+  show "f absolutely_integrable_on {c..d}"
+  proof -
+    have "f integrable_on {c..d}"
+      using assms integrable_on_lebesgue_on integrable_on_subinterval by fastforce
+    moreover have "(\<lambda>x. norm (f x)) integrable_on {c..d}"
+    proof (rule integrable_on_subinterval)
+      show "(\<lambda>x. norm (f x)) integrable_on {a..b}"
+        by (simp add: assms integrable_on_lebesgue_on)
+    qed (use assms in auto)
+    ultimately show ?thesis
+      by (auto simp: absolutely_integrable_on_def)
+  qed
+qed auto
+
+lemma indefinite_integral_continuous_real:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "integrable (lebesgue_on {a..b}) f"
+  shows "continuous_on {a..b} (\<lambda>x. integral\<^sup>L (lebesgue_on {a..x}) f)"
+proof -
+  have "f integrable_on {a..b}"
+    by (simp add: assms integrable_on_lebesgue_on)
+  then have "continuous_on {a..b} (\<lambda>x. integral {a..x} f)"
+    using indefinite_integral_continuous_1 by blast
+  moreover have "integral\<^sup>L (lebesgue_on {a..x}) f = integral {a..x} f" if "a \<le> x" "x \<le> b" for x
+  proof -
+    have "{a..x} \<subseteq> {a..b}"
+      using that by auto
+    then have "integrable (lebesgue_on {a..x}) f"
+      using integrable_subinterval assms by blast
+    then show "integral\<^sup>L (lebesgue_on {a..x}) f = integral {a..x} f"
+      by (simp add: lebesgue_integral_eq_integral)
+  qed
+  ultimately show ?thesis
+    by (metis (no_types, lifting) atLeastAtMost_iff continuous_on_cong)
+qed
+
 lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
   by (subst absolutely_integrable_on_iff_nonneg[symmetric])
      (simp_all add: lmeasurable_iff_integrable set_integrable_def)
@@ -3132,21 +3174,8 @@
   qed
 qed
 
-
 subsection\<open>Lemmas about absolute integrability\<close>
 
-text\<open>FIXME Redundant!\<close>
-lemma absolutely_integrable_add[intro]:
-  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on s"
-  by (rule set_integral_add)
-
-text\<open>FIXME Redundant!\<close>
-lemma absolutely_integrable_diff[intro]:
-  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) absolutely_integrable_on s"
-  by (rule set_integral_diff)
-
 lemma absolutely_integrable_linear:
   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
     and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
@@ -3375,8 +3404,8 @@
   qed
   moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
                  absolutely_integrable_on S"
-    apply (intro absolutely_integrable_add absolutely_integrable_scaleR_left assms)
-    using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]]
+    apply (intro set_integral_add absolutely_integrable_scaleR_left assms)
+    using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
     apply (simp add: algebra_simps)
     done
   ultimately show ?thesis by metis
@@ -3410,8 +3439,8 @@
   qed
   moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
                  absolutely_integrable_on S"
-    apply (intro absolutely_integrable_add absolutely_integrable_diff absolutely_integrable_scaleR_left assms)
-    using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]]
+    apply (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
+    using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
     apply (simp add: algebra_simps)
     done
   ultimately show ?thesis by metis
@@ -3450,7 +3479,7 @@
   shows "f absolutely_integrable_on A"
 proof -
   have "(\<lambda>x. g x - (g x - f x)) absolutely_integrable_on A"
-    apply (rule absolutely_integrable_diff [OF g nonnegative_absolutely_integrable])
+    apply (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
     using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
     by (simp add: comp inner_diff_left)
   then show ?thesis
@@ -3464,7 +3493,7 @@
   shows "g absolutely_integrable_on A"
 proof -
   have "(\<lambda>x. f x + (g x - f x)) absolutely_integrable_on A"
-    apply (rule absolutely_integrable_add [OF f nonnegative_absolutely_integrable])
+    apply (rule set_integral_add [OF f nonnegative_absolutely_integrable])
     using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
     by (simp add: comp inner_diff_left)
   then show ?thesis
@@ -4495,6 +4524,22 @@
     by (auto simp: has_bochner_integral_restrict_space)
 qed
 
+lemma has_bochner_integral_reflect_real[simp]:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  shows "has_bochner_integral (lebesgue_on {-b..-a}) (\<lambda>x. f(-x)) i \<longleftrightarrow> has_bochner_integral (lebesgue_on {a..b}) f i"
+  by (auto simp: dest: has_bochner_integral_reflect_real_lemma)
+
+lemma integrable_reflect_real[simp]:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  shows "integrable (lebesgue_on {-b..-a}) (\<lambda>x. f(-x)) \<longleftrightarrow> integrable (lebesgue_on {a..b}) f"
+  by (metis has_bochner_integral_iff has_bochner_integral_reflect_real)
+
+lemma integral_reflect_real[simp]:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  shows "integral\<^sup>L (lebesgue_on {-b .. -a}) (\<lambda>x. f(-x)) = integral\<^sup>L (lebesgue_on {a..b::real}) f"
+  using has_bochner_integral_reflect_real [of b a f]
+  by (metis has_bochner_integral_iff not_integrable_integral_eq)
+
 subsection\<open>More results on integrability\<close>
 
 lemma integrable_on_all_intervals_UNIV:
@@ -4790,9 +4835,9 @@
        "(\<lambda>x. if x \<in> T then f x else 0) absolutely_integrable_on UNIV"
     using S T absolutely_integrable_restrict_UNIV by blast+
   then have "(\<lambda>x. (if x \<in> S then f x else 0) + (if x \<in> T then f x else 0)) absolutely_integrable_on UNIV"
-    by (rule absolutely_integrable_add)
+    by (rule set_integral_add)
   then have "(\<lambda>x. ((if x \<in> S then f x else 0) + (if x \<in> T then f x else 0)) - (if x \<in> ?ST then f x else 0)) absolutely_integrable_on UNIV"
-    using Int by (rule absolutely_integrable_diff)
+    using Int by (rule set_integral_diff)
   then have "(\<lambda>x. if x \<in> S \<union> T then f x else 0) absolutely_integrable_on UNIV"
     by (rule absolutely_integrable_spike) (auto intro: empty_imp_negligible)
   then show ?thesis
diff -r 99e24569cc1f -r 47258727fa42 src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Mon Sep 16 23:51:24 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Tue Sep 17 12:36:04 2019 +0100
@@ -860,32 +860,6 @@
   qed (auto simp: conF)
 qed
 
-
-lemma measurable_on_preimage_lemma0:
-  fixes f :: "'a::euclidean_space \<Rightarrow> real"
-  assumes "m \<in> \<int>" and f: "m / 2^n \<le> (f x)" "(f x) < (m+1) / 2^n" and m: "\<bar>m\<bar> \<le> 2^(2 * n)"
-  shows "(\<Sum>k\<in>{k \<in> \<int>. \<bar>k\<bar> \<le> 2^(2 * n)}.
-             (k / 2^n) * indicator {y. k / 2^n \<le> f y \<and> f y < (k+1) / 2^n} x)
-       = (m / 2^n)"  (is "?lhs = ?rhs")
-proof -
-  have "?lhs = (\<Sum>k\<in>{m}. (k / 2^n) * indicator {y. k / 2^n \<le> f y \<and> f y < (k+1) / 2^n} x)"
-  proof (intro sum.mono_neutral_right ballI)
-    show "finite {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2^(2 * n)}"
-      using finite_abs_int_segment by blast
-    show "(i / 2^n) * indicat_real {y. i / 2^n \<le> f y \<and> f y < (i+1) / 2^n} x = 0"
-      if "i \<in> {N \<in> \<int>. \<bar>N\<bar> \<le> 2^(2 * n)} - {m}" for i
-      using f m \<open>m \<in> \<int>\<close> that Ints_eq_abs_less1 [of i m]
-      by (auto simp: indicator_def divide_simps)
-  qed (auto simp: assms)
-  also have "\<dots> = ?rhs"
-    using assms by (auto simp: indicator_def)
-  finally show ?thesis .
-qed
-
-(*see HOL Light's lebesgue_measurable BUT OUR lmeasurable IS NOT THE SAME. It's more like "sets lebesgue"
- `lebesgue_measurable s <=> (indicator s) measurable_on (:real^N)`;;
-*)
-
 proposition indicator_measurable_on:
   assumes "S \<in> sets lebesgue"
   shows "indicat_real S measurable_on UNIV"
@@ -1615,6 +1589,7 @@
 qed
 
 subsection \<open>Measurability on generalisations of the binary product\<close>
+
 lemma measurable_on_bilinear:
   fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
   assumes h: "bilinear h" and f: "f measurable_on S" and g: "g measurable_on S"
@@ -1663,4 +1638,72 @@
   shows "(\<lambda>x. f x * g x) absolutely_integrable_on S"
   using absolutely_integrable_bounded_measurable_product bilinear_times assms by blast
 
+
+lemma borel_measurable_AE:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "f \<in> borel_measurable lebesgue" and ae: "AE x in lebesgue. f x = g x"
+  shows "g \<in> borel_measurable lebesgue"
+proof -
+  obtain N where N: "N \<in> null_sets lebesgue" "\<And>x. x \<notin> N \<Longrightarrow> f x = g x"
+    using ae unfolding completion.AE_iff_null_sets by auto
+  have "f measurable_on UNIV"
+    by (simp add: assms lebesgue_measurable_imp_measurable_on)
+  then have "g measurable_on UNIV"
+    by (metis Diff_iff N measurable_on_spike negligible_iff_null_sets)
+  then show ?thesis
+    using measurable_on_imp_borel_measurable_lebesgue_UNIV by blast
+qed
+
+lemma has_bochner_integral_combine:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "a \<le> c" "c \<le> b"
+    and ac: "has_bochner_integral (lebesgue_on {a..c}) f i"
+    and cb: "has_bochner_integral (lebesgue_on {c..b}) f j"
+  shows "has_bochner_integral (lebesgue_on {a..b}) f(i + j)"
+proof -
+  have i: "has_bochner_integral lebesgue (\<lambda>x. indicator {a..c} x *\<^sub>R f x) i"
+   and j: "has_bochner_integral lebesgue (\<lambda>x. indicator {c..b} x *\<^sub>R f x) j"
+    using assms  by (auto simp: has_bochner_integral_restrict_space)
+  have AE: "AE x in lebesgue. indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x"
+  proof (rule AE_I')
+    have eq: "indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x" if "x \<noteq> c" for x
+      using assms that by (auto simp: indicator_def)
+    then show "{x \<in> space lebesgue. indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x \<noteq> indicat_real {a..b} x *\<^sub>R f x} \<subseteq> {c}"
+      by auto
+  qed auto
+  have "has_bochner_integral lebesgue (\<lambda>x. indicator {a..b} x *\<^sub>R f x) (i + j)"
+  proof (rule has_bochner_integralI_AE [OF has_bochner_integral_add [OF i j] _ AE])
+    have eq: "indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x" if "x \<noteq> c" for x
+      using assms that by (auto simp: indicator_def)
+    show "(\<lambda>x. indicat_real {a..b} x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+    proof (rule borel_measurable_AE [OF borel_measurable_add AE])
+      show "(\<lambda>x. indicator {a..c} x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+           "(\<lambda>x. indicator {c..b} x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+        using i j by auto
+    qed
+  qed
+  then show ?thesis
+    by (simp add: has_bochner_integral_restrict_space)
+qed
+
+lemma integrable_combine:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "integrable (lebesgue_on {a..c}) f" "integrable (lebesgue_on {c..b}) f"
+    and "a \<le> c" "c \<le> b"
+  shows "integrable (lebesgue_on {a..b}) f"
+  using assms has_bochner_integral_combine has_bochner_integral_iff by blast
+
+lemma integral_combine:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes f: "integrable (lebesgue_on {a..b}) f" and "a \<le> c" "c \<le> b"
+  shows "integral\<^sup>L (lebesgue_on {a..b}) f = integral\<^sup>L (lebesgue_on {a..c}) f + integral\<^sup>L (lebesgue_on {c..b}) f"
+proof -
+  have i: "has_bochner_integral (lebesgue_on {a..c}) f(integral\<^sup>L (lebesgue_on {a..c}) f)"
+    using integrable_subinterval \<open>c \<le> b\<close> f has_bochner_integral_iff by fastforce
+  have j: "has_bochner_integral (lebesgue_on {c..b}) f(integral\<^sup>L (lebesgue_on {c..b}) f)"
+    using integrable_subinterval \<open>a \<le> c\<close> f has_bochner_integral_iff by fastforce
+  show ?thesis
+    by (meson \<open>a \<le> c\<close> \<open>c \<le> b\<close> has_bochner_integral_combine has_bochner_integral_iff i j)
+qed
+
 end
diff -r 99e24569cc1f -r 47258727fa42 src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Mon Sep 16 23:51:24 2019 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy	Tue Sep 17 12:36:04 2019 +0100
@@ -1757,13 +1757,11 @@
             have I_int [simp]: "?I \<inter> box a b = ?I"
               using 1 by (simp add: Int_absorb2)
             have int_fI: "f integrable_on ?I"
-              apply (rule integrable_subinterval [OF int_f order_refl])
-              using "*" box_subset_cbox by blast
+              by (metis I_int inf_le2 int_f)
             then have "(\<lambda>x. f x \<bullet> j) integrable_on ?I"
               by (simp add: integrable_component)
             moreover have "g integrable_on ?I"
-              apply (rule integrable_subinterval [OF int_gab])
-              using "*" box_subset_cbox by blast
+              by (metis I_int inf.orderI int_gab integrable_on_open_interval integrable_on_subcbox)
             moreover
             have "\<bar>integral ?I (\<lambda>x. f x \<bullet> j)\<bar> \<le> norm (integral ?I f)"
               by (simp add: Basis_le_norm int_fI \<open>j \<in> Basis\<close>)
@@ -1837,13 +1835,11 @@
             have I_int [simp]: "?I \<inter> box a b = ?I"
               using 1 by (simp add: Int_absorb2)
             have int_fI: "f integrable_on ?I"
-              apply (rule integrable_subinterval [OF int_f order_refl])
-              using "*" box_subset_cbox by blast
+              by (simp add: inf.orderI int_f)
             then have "(\<lambda>x. f x \<bullet> j) integrable_on ?I"
               by (simp add: integrable_component)
             moreover have "g integrable_on ?I"
-              apply (rule integrable_subinterval [OF int_gab])
-              using "*" box_subset_cbox by blast
+              by (metis I_int inf.orderI int_gab integrable_on_open_interval integrable_on_subcbox)
             moreover
             have "\<bar>integral ?I (\<lambda>x. f x \<bullet> j)\<bar> \<le> norm (integral ?I f)"
               by (simp add: Basis_le_norm int_fI \<open>j \<in> Basis\<close>)
@@ -2268,6 +2264,5 @@
     using second_mean_value_theorem_full [where g=g, OF assms]
     by (metis (full_types) integral_unique)
 
-
 end
 
diff -r 99e24569cc1f -r 47258727fa42 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Mon Sep 16 23:51:24 2019 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Tue Sep 17 12:36:04 2019 +0100
@@ -173,12 +173,30 @@
   unfolding set_integrable_def
   using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
+lemma set_integrable_mult_right_iff [simp]:
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  assumes "a \<noteq> 0"
+  shows "set_integrable M A (\<lambda>t. a * f t) \<longleftrightarrow> set_integrable M A f"
+proof
+  assume "set_integrable M A (\<lambda>t. a * f t)"
+  then have "set_integrable M A (\<lambda>t. 1/a * (a * f t))"
+    using set_integrable_mult_right by blast
+  then show "set_integrable M A f"
+    using assms by auto
+qed auto
+
 lemma set_integrable_mult_left [simp, intro]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
   unfolding set_integrable_def
   using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
+lemma set_integrable_mult_left_iff [simp]:
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  assumes "a \<noteq> 0"
+  shows "set_integrable M A (\<lambda>t. f t * a) \<longleftrightarrow> set_integrable M A f"
+  using assms by (subst set_integrable_mult_right_iff [symmetric]) (auto simp: mult.commute)
+
 lemma set_integrable_divide [simp, intro]:
   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
@@ -192,6 +210,12 @@
     unfolding set_integrable_def .
 qed
 
+lemma set_integrable_mult_divide_iff [simp]:
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  assumes "a \<noteq> 0"
+  shows "set_integrable M A (\<lambda>t. f t / a) \<longleftrightarrow> set_integrable M A f"
+  by (simp add: divide_inverse assms)
+
 lemma set_integral_add [simp, intro]:
   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "set_integrable M A f" "set_integrable M A g"
@@ -205,8 +229,6 @@
     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
   using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
 
-(* question: why do we have this for negation, but multiplication by a constant
-   requires an integrability assumption? *)
 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
   unfolding set_integrable_def set_lebesgue_integral_def
   by (subst integral_minus[symmetric]) simp_all