diff -r 4c53227f4b73 -r 3d894e1cfc75 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Sep 11 20:48:10 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 12 14:51:45 2019 +0100
@@ -462,8 +462,232 @@
   using integral_restrict_Int [of S UNIV f] assms
   by (simp add: lebesgue_on_UNIV_eq)
 
+lemma integrable_lebesgue_on_empty [iff]:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{second_countable_topology,banach}"
+  shows "integrable (lebesgue_on {}) f"
+  by (simp add: integrable_restrict_space)
 
-text\<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
+lemma integral_lebesgue_on_empty [simp]:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{second_countable_topology,banach}"
+  shows "integral\<^sup>L (lebesgue_on {}) f = 0"
+  by (simp add: Bochner_Integration.integral_empty)
+lemma has_bochner_integral_restrict_space:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
+  shows "has_bochner_integral (restrict_space M \<Omega>) f i
+     \<longleftrightarrow> has_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) i"
+  by (simp add: integrable_restrict_space [OF assms] integral_restrict_space [OF assms] has_bochner_integral_iff)
+
+lemma integrable_restrict_UNIV:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes S: "S \<in> sets lebesgue"
+  shows  "integrable lebesgue (\<lambda>x. if x \<in> S then f x else 0) \<longleftrightarrow> integrable (lebesgue_on S) f"
+  using has_bochner_integral_restrict_space [of S lebesgue f] assms
+  by (simp add: integrable.simps indicator_scaleR_eq_if)
+
+lemma integral_mono_lebesgue_on_AE:
+  fixes f::"_ \<Rightarrow> real"
+  assumes f: "integrable (lebesgue_on T) f"
+    and gf: "AE x in (lebesgue_on S). g x \<le> f x"
+    and f0: "AE x in (lebesgue_on T). 0 \<le> f x"
+    and "S \<subseteq> T" and S: "S \<in> sets lebesgue" and T: "T \<in> sets lebesgue"
+  shows "(\<integral>x. g x \<partial>(lebesgue_on S)) \<le> (\<integral>x. f x \<partial>(lebesgue_on T))"
+proof -
+  have "(\<integral>x. g x \<partial>(lebesgue_on S)) = (\<integral>x. (if x \<in> S then g x else 0) \<partial>lebesgue)"
+    by (simp add: Lebesgue_Measure.integral_restrict_UNIV S)
+  also have "\<dots> \<le> (\<integral>x. (if x \<in> T then f x else 0) \<partial>lebesgue)"
+  proof (rule Bochner_Integration.integral_mono_AE')
+    show "integrable lebesgue (\<lambda>x. if x \<in> T then f x else 0)"
+      by (simp add: integrable_restrict_UNIV T f)
+    show "AE x in lebesgue. (if x \<in> S then g x else 0) \<le> (if x \<in> T then f x else 0)"
+      using assms by (auto simp: AE_restrict_space_iff)
+    show "AE x in lebesgue. 0 \<le> (if x \<in> T then f x else 0)"
+      using f0 by (simp add: AE_restrict_space_iff T)
+  qed
+  also have "\<dots> = (\<integral>x. f x \<partial>(lebesgue_on T))"
+    using Lebesgue_Measure.integral_restrict_UNIV T by blast
+  finally show ?thesis .
+qed
+
+
+subsection \<open>Borel measurability\<close>
+
+lemma borel_measurable_if_I:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "f \<in> borel_measurable (lebesgue_on S)" and S: "S \<in> sets lebesgue"
+  shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
+proof -
+  have eq: "{x. x \<notin> S} \<union> {x. f x \<in> Y} = {x. x \<notin> S} \<union> {x. f x \<in> Y} \<inter> S" for Y
+    by blast
+  show ?thesis
+  using f S
+  apply (simp add: vimage_def in_borel_measurable_borel Ball_def)
+  apply (elim all_forward imp_forward asm_rl)
+  apply (simp only: Collect_conj_eq Collect_disj_eq imp_conv_disj eq)
+  apply (auto simp: Compl_eq [symmetric] Compl_in_sets_lebesgue sets_restrict_space_iff)
+  done
+qed
+
+lemma borel_measurable_if_D:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
+  shows "f \<in> borel_measurable (lebesgue_on S)"
+  using assms
+  apply (simp add: in_borel_measurable_borel Ball_def)
+  apply (elim all_forward imp_forward asm_rl)
+  apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
+  done
+
+lemma borel_measurable_if:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "S \<in> sets lebesgue"
+  shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
+  using assms borel_measurable_if_D borel_measurable_if_I by blast
+
+lemma borel_measurable_vimage_halfspace_component_lt:
+     "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+      (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i < a} \<in> sets (lebesgue_on S))"
+  apply (rule trans [OF borel_measurable_iff_halfspace_less])
+  apply (fastforce simp add: space_restrict_space)
+  done
+
+lemma borel_measurable_vimage_halfspace_component_ge:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<ge> a} \<in> sets (lebesgue_on S))"
+  apply (rule trans [OF borel_measurable_iff_halfspace_ge])
+  apply (fastforce simp add: space_restrict_space)
+  done
+
+lemma borel_measurable_vimage_halfspace_component_gt:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i > a} \<in> sets (lebesgue_on S))"
+  apply (rule trans [OF borel_measurable_iff_halfspace_greater])
+  apply (fastforce simp add: space_restrict_space)
+  done
+
+lemma borel_measurable_vimage_halfspace_component_le:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<le> a} \<in> sets (lebesgue_on S))"
+  apply (rule trans [OF borel_measurable_iff_halfspace_le])
+  apply (fastforce simp add: space_restrict_space)
+  done
+
+lemma
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows borel_measurable_vimage_open_interval:
+         "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S))" (is ?thesis1)
+   and borel_measurable_vimage_open:
+         "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>T. open T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))" (is ?thesis2)
+proof -
+  have "{x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" if "f \<in> borel_measurable (lebesgue_on S)" for a b
+  proof -
+    have "S = S \<inter> space lebesgue"
+      by simp
+    then have "S \<inter> (f -` box a b) \<in> sets (lebesgue_on S)"
+      by (metis (no_types) box_borel in_borel_measurable_borel inf_sup_aci(1) space_restrict_space that)
+    then show ?thesis
+      by (simp add: Collect_conj_eq vimage_def)
+  qed
+  moreover
+  have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
+       if T: "\<And>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" "open T" for T
+  proof -
+    obtain \<D> where "countable \<D>" and \<D>: "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = T"
+      using open_countable_Union_open_box that \<open>open T\<close> by metis
+    then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
+      by blast
+    have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
+      using that T \<D> by blast
+    then show ?thesis
+      by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
+  qed
+  moreover
+  have eq: "{x \<in> S. f x \<bullet> i < a} = {x \<in> S. f x \<in> {y. y \<bullet> i < a}}" for i a
+    by auto
+  have "f \<in> borel_measurable (lebesgue_on S)"
+    if "\<And>T. open T \<Longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
+    by (metis (no_types) eq borel_measurable_vimage_halfspace_component_lt open_halfspace_component_lt that)
+  ultimately show "?thesis1" "?thesis2"
+    by blast+
+qed
+
+lemma borel_measurable_vimage_closed:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>T. closed T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
+        (is "?lhs = ?rhs")
+proof -
+  have eq: "{x \<in> S. f x \<in> T} = S - {x \<in> S. f x \<in> (- T)}" for T
+    by auto
+  show ?thesis
+    apply (simp add: borel_measurable_vimage_open, safe)
+     apply (simp_all (no_asm) add: eq)
+     apply (intro sets.Diff sets_lebesgue_on_refl, force simp: closed_open)
+    apply (intro sets.Diff sets_lebesgue_on_refl, force simp: open_closed)
+    done
+qed
+
+lemma borel_measurable_vimage_closed_interval:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a b. {x \<in> S. f x \<in> cbox a b} \<in> sets (lebesgue_on S))"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using borel_measurable_vimage_closed by blast
+next
+  assume RHS: ?rhs
+  have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)" if "open T" for T
+  proof -
+    obtain \<D> where "countable \<D>" and \<D>: "\<D> \<subseteq> Pow T" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = T"
+      using open_countable_Union_open_cbox that \<open>open T\<close> by metis
+    then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
+      by blast
+    have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
+      using that \<D> by (metis RHS)
+    then show ?thesis
+      by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
+  qed
+  then show ?lhs
+    by (simp add: borel_measurable_vimage_open)
+qed
+
+lemma borel_measurable_UNIV_eq: "borel_measurable (lebesgue_on UNIV) = borel_measurable lebesgue"
+  by auto
+
+lemma borel_measurable_vimage_borel:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
+        (is "?lhs = ?rhs")
+proof
+  assume f: ?lhs
+  then show ?rhs
+    using measurable_sets [OF f]
+      by (simp add: Collect_conj_eq inf_sup_aci(1) space_restrict_space vimage_def)
+qed (simp add: borel_measurable_vimage_open_interval)
+
+lemma lebesgue_measurable_vimage_borel:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "f \<in> borel_measurable lebesgue" "T \<in> sets borel"
+  shows "{x. f x \<in> T} \<in> sets lebesgue"
+  using assms borel_measurable_vimage_borel [of f UNIV] by auto
+
+lemma borel_measurable_lebesgue_preimage_borel:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable lebesgue \<longleftrightarrow>
+         (\<forall>T. T \<in> sets borel \<longrightarrow> {x. f x \<in> T} \<in> sets lebesgue)"
+  apply (intro iffI allI impI lebesgue_measurable_vimage_borel)
+    apply (auto simp: in_borel_measurable_borel vimage_def)
+  done
+
+
+subsection \<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
 
 lemma continuous_imp_measurable_on_sets_lebesgue:
   assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue"