--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Sep 11 20:48:10 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Sep 12 14:51:45 2019 +0100
@@ -4226,13 +4226,6 @@
qed
-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_simple_function_limit:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
@@ -4298,174 +4291,6 @@
using borel_measurable_vimage_halfspace_component_lt by blast
qed
-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_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_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 \<open>Lebesgue sets and continuous images\<close>
proposition lebesgue_regular_inner: