(* Title: HOL/Analysis/Equivalence_Measurable_On_Borel
Author: LC Paulson (some material ported from HOL Light)
*)
section\<open>Equivalence Between Classical Borel Measurability and HOL Light's\<close>
theory Equivalence_Measurable_On_Borel
imports Equivalence_Lebesgue_Henstock_Integration Improper_Integral Continuous_Extension
begin
(*Borrowed from Ergodic_Theory/SG_Library_Complement*)
abbreviation sym_diff :: "'a set \ 'a set \ 'a set" where
"sym_diff A B \ ((A - B) \ (B-A))"
subsection\<open>Austin's Lemma\<close>
lemma Austin_Lemma:
fixes \<D> :: "'a::euclidean_space set set"
assumes "finite \" and \: "\D. D \ \ \ \k a b. D = cbox a b \ (\i \ Basis. b\i - a\i = k)"
obtains \<C> where "\<C> \<subseteq> \<D>" "pairwise disjnt \<C>"
"measure lebesgue (\\) \ measure lebesgue (\\) / 3 ^ (DIM('a))"
using assms
proof (induction "card \" arbitrary: \ thesis rule: less_induct)
case less
show ?case
proof (cases "\ = {}")
case True
then show thesis
using less by auto
next
case False
then have "Max (Sigma_Algebra.measure lebesgue ` \) \ Sigma_Algebra.measure lebesgue ` \"
using Max_in finite_imageI \<open>finite \<D>\<close> by blast
then obtain D where "D \ \" and "measure lebesgue D = Max (measure lebesgue ` \)"
by auto
then have D: "\C. C \ \ \ measure lebesgue C \ measure lebesgue D"
by (simp add: \<open>finite \<D>\<close>)
let ?\<E> = "{C. C \<in> \<D> - {D} \<and> disjnt C D}"
obtain \<D>' where \<D>'sub: "\<D>' \<subseteq> ?\<E>" and \<D>'dis: "pairwise disjnt \<D>'"
and \<D>'m: "measure lebesgue (\<Union>\<D>') \<ge> measure lebesgue (\<Union>?\<E>) / 3 ^ (DIM('a))"
proof (rule less.hyps)
have *: "?\ \ \"
using \<open>D \<in> \<D>\<close> by auto
then show "card ?\ < card \" "finite ?\"
by (auto simp: \<open>finite \<D>\<close> psubset_card_mono)
show "\k a b. D = cbox a b \ (\i\Basis. b \ i - a \ i = k)" if "D \ ?\" for D
using less.prems(3) that by auto
qed
then have [simp]: "\\' - D = \\'"
by (auto simp: disjnt_iff)
show ?thesis
proof (rule less.prems)
show "insert D \' \ \"
using \<D>'sub \<open>D \<in> \<D>\<close> by blast
show "disjoint (insert D \')"
using \<D>'dis \<D>'sub by (fastforce simp add: pairwise_def disjnt_sym)
obtain a3 b3 where m3: "content (cbox a3 b3) = 3 ^ DIM('a) * measure lebesgue D"
and sub3: "\C. \C \ \; \ disjnt C D\ \ C \ cbox a3 b3"
proof -
obtain k a b where ab: "D = cbox a b" and k: "\i. i \ Basis \ b\i - a\i = k"
using less.prems \<open>D \<in> \<D>\<close> by meson
then have eqk: "\i. i \ Basis \ a \ i \ b \ i \ k \ 0"
by force
show thesis
proof
let ?a = "(a + b) /\<^sub>R 2 - (3/2) *\<^sub>R (b - a)"
let ?b = "(a + b) /\<^sub>R 2 + (3/2) *\<^sub>R (b - a)"
have eq: "(\i\Basis. b \ i * 3 - a \ i * 3) = (\i\Basis. b \ i - a \ i) * 3 ^ DIM('a)"
by (simp add: comm_monoid_mult_class.prod.distrib flip: left_diff_distrib inner_diff_left)
show "content (cbox ?a ?b) = 3 ^ DIM('a) * measure lebesgue D"
by (simp add: content_cbox_if box_eq_empty algebra_simps eq ab k)
show "C \ cbox ?a ?b" if "C \ \" and CD: "\ disjnt C D" for C
proof -
obtain k' a' b' where ab': "C = cbox a' b'" and k': "\i. i \ Basis \ b'\i - a'\i = k'"
using less.prems \<open>C \<in> \<D>\<close> by meson
then have eqk': "\i. i \ Basis \ a' \ i \ b' \ i \ k' \ 0"
by force
show ?thesis
proof (clarsimp simp add: disjoint_interval disjnt_def ab ab' not_less subset_box algebra_simps)
show "a \ i * 2 \ a' \ i + b \ i \ a \ i + b' \ i \ b \ i * 2"
if * [rule_format]: "\j\Basis. a' \ j \ b' \ j" and "i \ Basis" for i
proof -
have "a' \ i \ b' \ i \ a \ i \ b \ i \ a \ i \ b' \ i \ a' \ i \ b \ i"
using \<open>i \<in> Basis\<close> CD by (simp_all add: disjoint_interval disjnt_def ab ab' not_less)
then show ?thesis
using D [OF \<open>C \<in> \<D>\<close>] \<open>i \<in> Basis\<close>
apply (simp add: ab ab' k k' eqk eqk' content_cbox_cases)
using k k' by fastforce
qed
qed
qed
qed
qed
have \<D>lm: "\<And>D. D \<in> \<D> \<Longrightarrow> D \<in> lmeasurable"
using less.prems(3) by blast
have "measure lebesgue (\\) \ measure lebesgue (cbox a3 b3 \ (\\ - cbox a3 b3))"
proof (rule measure_mono_fmeasurable)
show "\\ \ sets lebesgue"
using \<D>lm \<open>finite \<D>\<close> by blast
show "cbox a3 b3 \ (\\ - cbox a3 b3) \ lmeasurable"
by (simp add: \<D>lm fmeasurable.Un fmeasurable.finite_Union less.prems(2) subset_eq)
qed auto
also have "\ = content (cbox a3 b3) + measure lebesgue (\\ - cbox a3 b3)"
by (simp add: \<D>lm fmeasurable.finite_Union less.prems(2) measure_Un2 subsetI)
also have "\ \ (measure lebesgue D + measure lebesgue (\\')) * 3 ^ DIM('a)"
proof -
have "(\\ - cbox a3 b3) \ \?\"
using sub3 by fastforce
then have "measure lebesgue (\\ - cbox a3 b3) \ measure lebesgue (\?\)"
proof (rule measure_mono_fmeasurable)
show "\ \ - cbox a3 b3 \ sets lebesgue"
by (simp add: \<D>lm fmeasurableD less.prems(2) sets.Diff sets.finite_Union subsetI)
show "\ {C \ \ - {D}. disjnt C D} \ lmeasurable"
using \<D>lm less.prems(2) by auto
qed
then have "measure lebesgue (\\ - cbox a3 b3) / 3 ^ DIM('a) \ measure lebesgue (\ \')"
using \<D>'m by (simp add: field_split_simps)
then show ?thesis
by (simp add: m3 field_simps)
qed
also have "\ \ measure lebesgue (\(insert D \')) * 3 ^ DIM('a)"
proof (simp add: \<D>lm \<open>D \<in> \<D>\<close>)
show "measure lebesgue D + measure lebesgue (\\') \ measure lebesgue (D \ \ \')"
proof (subst measure_Un2)
show "\ \' \ lmeasurable"
by (meson \<D>lm \<open>insert D \<D>' \<subseteq> \<D>\<close> fmeasurable.finite_Union less.prems(2) finite_subset subset_eq subset_insertI)
show "measure lebesgue D + measure lebesgue (\ \') \ measure lebesgue D + measure lebesgue (\ \' - D)"
using \<open>insert D \<D>' \<subseteq> \<D>\<close> infinite_super less.prems(2) by force
qed (simp add: \<D>lm \<open>D \<in> \<D>\<close>)
qed
finally show "measure lebesgue (\\) / 3 ^ DIM('a) \ measure lebesgue (\(insert D \'))"
by (simp add: field_split_simps)
qed
qed
qed
subsection\<open>A differentiability-like property of the indefinite integral. \<close>
proposition integrable_ccontinuous_explicit:
fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
assumes "\a b::'a. f integrable_on cbox a b"
obtains N where
"negligible N"
"\x e. \x \ N; 0 < e\ \
\<exists>d>0. \<forall>h. 0 < h \<and> h < d \<longrightarrow>
norm(integral (cbox x (x + h *\<^sub>R One)) f /\<^sub>R h ^ DIM('a) - f x) < e"
proof -
define BOX where "BOX \ \h. \x::'a. cbox x (x + h *\<^sub>R One)"
define BOX2 where "BOX2 \ \h. \x::'a. cbox (x - h *\<^sub>R One) (x + h *\<^sub>R One)"
define i where "i \ \h x. integral (BOX h x) f /\<^sub>R h ^ DIM('a)"
define \<Psi> where "\<Psi> \<equiv> \<lambda>x r. \<forall>d>0. \<exists>h. 0 < h \<and> h < d \<and> r \<le> norm(i h x - f x)"
let ?N = "{x. \e>0. \ x e}"
have "\N. negligible N \ (\x e. x \ N \ 0 < e \ \ \ x e)"
proof (rule exI ; intro conjI allI impI)
let ?M = "\n. {x. \ x (inverse(real n + 1))}"
have "negligible ({x. \ x \} \ cbox a b)"
if "\ > 0" for a b \
proof (cases "negligible(cbox a b)")
case True
then show ?thesis
by (simp add: negligible_Int)
next
case False
then have "box a b \ {}"
by (simp add: negligible_interval)
then have ab: "\i. i \ Basis \ a\i < b\i"
by (simp add: box_ne_empty)
show ?thesis
unfolding negligible_outer_le
proof (intro allI impI)
fix e::real
let ?ee = "(e * \) / 2 / 6 ^ (DIM('a))"
assume "e > 0"
then have gt0: "?ee > 0"
using \<open>\<mu> > 0\<close> by auto
have f': "f integrable_on cbox (a - One) (b + One)"
using assms by blast
obtain \<gamma> where "gauge \<gamma>"
and \<gamma>: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox (a - One) (b + One)); \<gamma> fine p\<rbrakk>
\<Longrightarrow> (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < ?ee"
using Henstock_lemma [OF f' gt0] that by auto
let ?E = "{x. x \ cbox a b \ \ x \}"
have "\h>0. BOX h x \ \ x \
BOX h x \<subseteq> cbox (a - One) (b + One) \<and> \<mu> \<le> norm (i h x - f x)"
if "x \ cbox a b" "\ x \" for x
proof -
obtain d where "d > 0" and d: "ball x d \ \ x"
using gaugeD [OF \<open>gauge \<gamma>\<close>, of x] openE by blast
then obtain h where "0 < h" "h < 1" and hless: "h < d / real DIM('a)"
and mule: "\ \ norm (i h x - f x)"
using \<open>\<Psi> x \<mu>\<close> [unfolded \<Psi>_def, rule_format, of "min 1 (d / DIM('a))"]
by auto
show ?thesis
proof (intro exI conjI)
show "0 < h" "\ \ norm (i h x - f x)" by fact+
have "BOX h x \ ball x d"
proof (clarsimp simp: BOX_def mem_box dist_norm algebra_simps)
fix y
assume "\i\Basis. x \ i \ y \ i \ y \ i \ h + x \ i"
then have lt: "\(x - y) \ i\ < d / real DIM('a)" if "i \ Basis" for i
using hless that by (force simp: inner_diff_left)
have "norm (x - y) \ (\i\Basis. \(x - y) \ i\)"
using norm_le_l1 by blast
also have "\ < d"
using sum_bounded_above_strict [of Basis "\i. \(x - y) \ i\" "d / DIM('a)", OF lt]
by auto
finally show "norm (x - y) < d" .
qed
with d show "BOX h x \ \ x"
by blast
show "BOX h x \ cbox (a - One) (b + One)"
using that \<open>h < 1\<close>
by (force simp: BOX_def mem_box algebra_simps intro: subset_box_imp)
qed
qed
then obtain \<eta> where h0: "\<And>x. x \<in> ?E \<Longrightarrow> \<eta> x > 0"
and BOX_\<gamma>: "\<And>x. x \<in> ?E \<Longrightarrow> BOX (\<eta> x) x \<subseteq> \<gamma> x"
and "\x. x \ ?E \ BOX (\ x) x \ cbox (a - One) (b + One) \ \ \ norm (i (\ x) x - f x)"
by simp metis
then have BOX_cbox: "\x. x \ ?E \ BOX (\ x) x \ cbox (a - One) (b + One)"
and \<mu>_le: "\<And>x. x \<in> ?E \<Longrightarrow> \<mu> \<le> norm (i (\<eta> x) x - f x)"
by blast+
define \<gamma>' where "\<gamma>' \<equiv> \<lambda>x. if x \<in> cbox a b \<and> \<Psi> x \<mu> then ball x (\<eta> x) else \<gamma> x"
have "gauge \'"
using \<open>gauge \<gamma>\<close> by (auto simp: h0 gauge_def \<gamma>'_def)
obtain \<D> where "countable \<D>"
and \<D>: "\<Union>\<D> \<subseteq> cbox a b"
"\K. K \ \ \ interior K \ {} \ (\c d. K = cbox c d)"
and Dcovered: "\K. K \ \ \ \x. x \ cbox a b \ \ x \ \ x \ K \ K \ \' x"
and subUD: "?E \ \\"
by (rule covering_lemma [of ?E a b \<gamma>']) (simp_all add: Bex_def \<open>box a b \<noteq> {}\<close> \<open>gauge \<gamma>'\<close>)
then have "\ \ sets lebesgue"
by fastforce
show "\T. {x. \ x \} \ cbox a b \ T \ T \ lmeasurable \ measure lebesgue T \ e"
proof (intro exI conjI)
show "{x. \ x \} \ cbox a b \ \\"
apply auto
using subUD by auto
have mUE: "measure lebesgue (\ \) \ measure lebesgue (cbox a b)"
if "\ \ \" "finite \" for \
proof (rule measure_mono_fmeasurable)
show "\ \ \ cbox a b"
using \<D>(1) that(1) by blast
show "\ \ \ sets lebesgue"
by (metis \<D>(2) fmeasurable.finite_Union fmeasurableD lmeasurable_cbox subset_eq that)
qed auto
then show "\\ \ lmeasurable"
by (metis \<D>(2) \<open>countable \<D>\<close> fmeasurable_Union_bound lmeasurable_cbox)
then have leab: "measure lebesgue (\\) \ measure lebesgue (cbox a b)"
by (meson \<D>(1) fmeasurableD lmeasurable_cbox measure_mono_fmeasurable)
obtain \<F> where "\<F> \<subseteq> \<D>" "finite \<F>"
and \<F>: "measure lebesgue (\<Union>\<D>) \<le> 2 * measure lebesgue (\<Union>\<F>)"
proof (cases "measure lebesgue (\\) = 0")
case True
then show ?thesis
by (force intro: that [where \<F> = "{}"])
next
case False
obtain \<F> where "\<F> \<subseteq> \<D>" "finite \<F>"
and \<F>: "measure lebesgue (\<Union>\<D>)/2 < measure lebesgue (\<Union>\<F>)"
proof (rule measure_countable_Union_approachable [of \<D> "measure lebesgue (\<Union>\<D>) / 2" "content (cbox a b)"])
show "countable \"
by fact
show "0 < measure lebesgue (\ \) / 2"
using False by (simp add: zero_less_measure_iff)
show Dlm: "D \ lmeasurable" if "D \ \" for D
using \<D>(2) that by blast
show "measure lebesgue (\ \) \ content (cbox a b)"
if "\ \ \" "finite \" for \
proof -
have "measure lebesgue (\ \) \ measure lebesgue (\\)"
proof (rule measure_mono_fmeasurable)
show "\ \ \ \ \"
by (simp add: Sup_subset_mono \<open>\<F> \<subseteq> \<D>\<close>)
show "\ \ \ sets lebesgue"
by (meson Dlm fmeasurableD sets.finite_Union subset_eq that)
show "\ \ \ lmeasurable"
by fact
qed
also have "\ \ measure lebesgue (cbox a b)"
proof (rule measure_mono_fmeasurable)
show "\ \ \ sets lebesgue"
by (simp add: \<open>\<Union> \<D> \<in> lmeasurable\<close> fmeasurableD)
qed (auto simp:\<D>(1))
finally show ?thesis
by simp
qed
qed auto
then show ?thesis
using that by auto
qed
obtain tag where tag_in_E: "\D. D \ \ \ tag D \ ?E"
and tag_in_self: "\D. D \ \ \ tag D \ D"
and tag_sub: "\D. D \ \ \ D \ \' (tag D)"
using Dcovered by simp metis
then have sub_ball_tag: "\D. D \ \ \ D \ ball (tag D) (\ (tag D))"
by (simp add: \<gamma>'_def)
define \<Phi> where "\<Phi> \<equiv> \<lambda>D. BOX (\<eta>(tag D)) (tag D)"
define \<Phi>2 where "\<Phi>2 \<equiv> \<lambda>D. BOX2 (\<eta>(tag D)) (tag D)"
obtain \<C> where "\<C> \<subseteq> \<Phi>2 ` \<F>" "pairwise disjnt \<C>"
"measure lebesgue (\\) \ measure lebesgue (\(\2`\)) / 3 ^ (DIM('a))"
proof (rule Austin_Lemma)
show "finite (\2`\)"
using \<open>finite \<F>\<close> by blast
have "\k a b. \2 D = cbox a b \ (\i\Basis. b \ i - a \ i = k)" if "D \ \" for D
apply (rule_tac x="2 * \(tag D)" in exI)
apply (rule_tac x="tag D - \(tag D) *\<^sub>R One" in exI)
apply (rule_tac x="tag D + \(tag D) *\<^sub>R One" in exI)
using that
apply (auto simp: \<Phi>2_def BOX2_def algebra_simps)
done
then show "\D. D \ \2 ` \ \ \k a b. D = cbox a b \ (\i\Basis. b \ i - a \ i = k)"
by blast
qed auto
then obtain \<G> where "\<G> \<subseteq> \<F>" and disj: "pairwise disjnt (\<Phi>2 ` \<G>)"
and "measure lebesgue (\(\2 ` \)) \ measure lebesgue (\(\2`\)) / 3 ^ (DIM('a))"
unfolding \<Phi>2_def subset_image_iff
by (meson empty_subsetI equals0D pairwise_imageI)
moreover
have "measure lebesgue (\(\2 ` \)) * 3 ^ DIM('a) \ e/2"
proof -
have "finite \"
using \<open>finite \<F>\<close> \<open>\<G> \<subseteq> \<F>\<close> infinite_super by blast
have BOX2_m: "\x. x \ tag ` \ \ BOX2 (\ x) x \ lmeasurable"
by (auto simp: BOX2_def)
have BOX_m: "\x. x \ tag ` \ \ BOX (\ x) x \ lmeasurable"
by (auto simp: BOX_def)
have BOX_sub: "BOX (\ x) x \ BOX2 (\ x) x" for x
by (auto simp: BOX_def BOX2_def subset_box algebra_simps)
have DISJ2: "BOX2 (\ (tag X)) (tag X) \ BOX2 (\ (tag Y)) (tag Y) = {}"
if "X \ \" "Y \ \" "tag X \ tag Y" for X Y
proof -
obtain i where i: "i \ Basis" "tag X \ i \ tag Y \ i"
using \<open>tag X \<noteq> tag Y\<close> by (auto simp: euclidean_eq_iff [of "tag X"])
have XY: "X \ \" "Y \ \"
using \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> that by auto
then have "0 \ \ (tag X)" "0 \ \ (tag Y)"
by (meson h0 le_cases not_le tag_in_E)+
with XY i have "BOX2 (\ (tag X)) (tag X) \ BOX2 (\ (tag Y)) (tag Y)"
unfolding eq_iff
by (fastforce simp add: BOX2_def subset_box algebra_simps)
then show ?thesis
using disj that by (auto simp: pairwise_def disjnt_def \<Phi>2_def)
qed
then have BOX2_disj: "pairwise (\x y. negligible (BOX2 (\ x) x \ BOX2 (\ y) y)) (tag ` \)"
by (simp add: pairwise_imageI)
then have BOX_disj: "pairwise (\x y. negligible (BOX (\ x) x \ BOX (\ y) y)) (tag ` \)"
proof (rule pairwise_mono)
show "negligible (BOX (\ x) x \ BOX (\ y) y)"
if "negligible (BOX2 (\ x) x \ BOX2 (\ y) y)" for x y
by (metis (no_types, hide_lams) that Int_mono negligible_subset BOX_sub)
qed auto
have eq: "\box. (\D. box (\ (tag D)) (tag D)) ` \ = (\t. box (\ t) t) ` tag ` \"
by (simp add: image_comp)
have "measure lebesgue (BOX2 (\ t) t) * 3 ^ DIM('a)
= measure lebesgue (BOX (\<eta> t) t) * (2*3) ^ DIM('a)"
if "t \ tag ` \" for t
proof -
have "content (cbox (t - \ t *\<^sub>R One) (t + \ t *\<^sub>R One))
= content (cbox t (t + \<eta> t *\<^sub>R One)) * 2 ^ DIM('a)"
using that by (simp add: algebra_simps content_cbox_if box_eq_empty)
then show ?thesis
by (simp add: BOX2_def BOX_def flip: power_mult_distrib)
qed
then have "measure lebesgue (\(\2 ` \)) * 3 ^ DIM('a) = measure lebesgue (\(\ ` \)) * 6 ^ DIM('a)"
unfolding \<Phi>_def \<Phi>2_def eq
by (simp add: measure_negligible_finite_Union_image
\<open>finite \<G>\<close> BOX2_m BOX_m BOX2_disj BOX_disj sum_distrib_right
del: UN_simps)
also have "\ \ e/2"
proof -
have "\ * measure lebesgue (\D\\. \ D) \ \ * (\D \ \`\. measure lebesgue D)"
using \<open>\<mu> > 0\<close> \<open>finite \<G>\<close> by (force simp: BOX_m \<Phi>_def fmeasurableD intro: measure_Union_le)
also have "\ = (\D \ \`\. measure lebesgue D * \)"
by (metis mult.commute sum_distrib_right)
also have "\ \ (\(x, K) \ (\D. (tag D, \ D)) ` \. norm (content K *\<^sub>R f x - integral K f))"
proof (rule sum_le_included; clarify?)
fix D
assume "D \ \"
then have "\ (tag D) > 0"
using \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> h0 tag_in_E by auto
then have m_\<Phi>: "measure lebesgue (\<Phi> D) > 0"
by (simp add: \<Phi>_def BOX_def algebra_simps)
have "\ \ norm (i (\(tag D)) (tag D) - f(tag D))"
using \<mu>_le \<open>D \<in> \<G>\<close> \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> tag_in_E by auto
also have "\ = norm ((content (\ D) *\<^sub>R f(tag D) - integral (\ D) f) /\<^sub>R measure lebesgue (\ D))"
using m_\<Phi>
unfolding i_def \<Phi>_def BOX_def
by (simp add: algebra_simps content_cbox_plus norm_minus_commute)
finally have "measure lebesgue (\ D) * \ \ norm (content (\ D) *\<^sub>R f(tag D) - integral (\ D) f)"
using m_\<Phi> by simp (simp add: field_simps)
then show "\y\(\D. (tag D, \ D)) ` \.
snd y = \<Phi> D \<and> measure lebesgue (\<Phi> D) * \<mu> \<le> (case y of (x, k) \<Rightarrow> norm (content k *\<^sub>R f x - integral k f))"
using \<open>D \<in> \<G>\<close> by auto
qed (use \<open>finite \<G>\<close> in auto)
also have "\ < ?ee"
proof (rule \<gamma>)
show "(\D. (tag D, \ D)) ` \ tagged_partial_division_of cbox (a - One) (b + One)"
unfolding tagged_partial_division_of_def
proof (intro conjI allI impI ; clarify ?)
show "tag D \ \ D"
if "D \ \" for D
using that \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> h0 tag_in_E
by (auto simp: \<Phi>_def BOX_def mem_box algebra_simps eucl_less_le_not_le in_mono)
show "y \ cbox (a - One) (b + One)" if "D \ \" "y \ \ D" for D y
using that BOX_cbox \<Phi>_def \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> tag_in_E by blast
show "tag D = tag E \ \ D = \ E"
if "D \ \" "E \ \" and ne: "interior (\ D) \ interior (\ E) \ {}" for D E
proof -
have "BOX2 (\ (tag D)) (tag D) \ BOX2 (\ (tag E)) (tag E) = {} \ tag E = tag D"
using DISJ2 \<open>D \<in> \<G>\<close> \<open>E \<in> \<G>\<close> by force
then have "BOX (\ (tag D)) (tag D) \ BOX (\ (tag E)) (tag E) = {} \ tag E = tag D"
using BOX_sub by blast
then show "tag D = tag E \ \ D = \ E"
by (metis \<Phi>_def interior_Int interior_empty ne)
qed
qed (use \<open>finite \<G>\<close> \<Phi>_def BOX_def in auto)
show "\ fine (\D. (tag D, \ D)) ` \"
unfolding fine_def \<Phi>_def using BOX_\<gamma> \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> tag_in_E by blast
qed
finally show ?thesis
using \<open>\<mu> > 0\<close> by (auto simp: field_split_simps)
qed
finally show ?thesis .
qed
moreover
have "measure lebesgue (\\) \ measure lebesgue (\(\2`\))"
proof (rule measure_mono_fmeasurable)
have "D \ ball (tag D) (\(tag D))" if "D \ \" for D
using \<open>\<F> \<subseteq> \<D>\<close> sub_ball_tag that by blast
moreover have "ball (tag D) (\(tag D)) \ BOX2 (\ (tag D)) (tag D)" if "D \ \" for D
proof (clarsimp simp: \<Phi>2_def BOX2_def mem_box algebra_simps dist_norm)
fix x and i::'a
assume "norm (tag D - x) < \ (tag D)" and "i \ Basis"
then have "\tag D \ i - x \ i\ \ \ (tag D)"
by (metis eucl_less_le_not_le inner_commute inner_diff_right norm_bound_Basis_le)
then show "tag D \ i \ x \ i + \ (tag D) \ x \ i \ \ (tag D) + tag D \ i"
by (simp add: abs_diff_le_iff)
qed
ultimately show "\\ \ \(\2`\)"
by (force simp: \<Phi>2_def)
show "\\ \ sets lebesgue"
using \<open>finite \<F>\<close> \<open>\<D> \<subseteq> sets lebesgue\<close> \<open>\<F> \<subseteq> \<D>\<close> by blast
show "\(\2`\) \ lmeasurable"
unfolding \<Phi>2_def BOX2_def using \<open>finite \<F>\<close> by blast
qed
ultimately
have "measure lebesgue (\\) \ e/2"
by (auto simp: field_split_simps)
then show "measure lebesgue (\\) \ e"
using \<F> by linarith
qed
qed
qed
then have "\j. negligible {x. \ x (inverse(real j + 1))}"
using negligible_on_intervals
by (metis (full_types) inverse_positive_iff_positive le_add_same_cancel1 linorder_not_le nat_le_real_less not_add_less1 of_nat_0)
then have "negligible ?M"
by auto
moreover have "?N \ ?M"
proof (clarsimp simp: dist_norm)
fix y e
assume "0 < e"
and ye [rule_format]: "\ y e"
then obtain k where k: "0 < k" "inverse (real k + 1) < e"
by (metis One_nat_def add.commute less_add_same_cancel2 less_imp_inverse_less less_trans neq0_conv of_nat_1 of_nat_Suc reals_Archimedean zero_less_one)
with ye show "\n. \ y (inverse (real n + 1))"
apply (rule_tac x=k in exI)
unfolding \<Psi>_def
by (force intro: less_le_trans)
qed
ultimately show "negligible ?N"
by (blast intro: negligible_subset)
show "\ \ x e" if "x \ ?N \ 0 < e" for x e
using that by blast
qed
with that show ?thesis
unfolding i_def BOX_def \<Psi>_def by (fastforce simp add: not_le)
qed
subsection\<open>HOL Light measurability\<close>
definition measurable_on :: "('a::euclidean_space \ 'b::real_normed_vector) \ 'a set \ bool"
(infixr "measurable'_on" 46)
where "f measurable_on S \
\<exists>N g. negligible N \<and>
(\<forall>n. continuous_on UNIV (g n)) \<and>
(\<forall>x. x \<notin> N \<longrightarrow> (\<lambda>n. g n x) \<longlonglongrightarrow> (if x \<in> S then f x else 0))"
lemma measurable_on_UNIV:
"(\x. if x \ S then f x else 0) measurable_on UNIV \ f measurable_on S"
by (auto simp: measurable_on_def)
lemma measurable_on_spike_set:
assumes f: "f measurable_on S" and neg: "negligible ((S - T) \ (T - S))"
shows "f measurable_on T"
proof -
obtain N and F
where N: "negligible N"
and conF: "\n. continuous_on UNIV (F n)"
and tendsF: "\x. x \ N \ (\n. F n x) \ (if x \ S then f x else 0)"
using f by (auto simp: measurable_on_def)
show ?thesis
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "continuous_on UNIV (\x. F n x)" for n
by (intro conF continuous_intros)
show "negligible (N \ (S - T) \ (T - S))"
by (metis (full_types) N neg negligible_Un_eq)
show "(\n. F n x) \ (if x \ T then f x else 0)"
if "x \ (N \ (S - T) \ (T - S))" for x
using that tendsF [of x] by auto
qed
qed
text\<open> Various common equivalent forms of function measurability. \<close>
lemma measurable_on_0 [simp]: "(\x. 0) measurable_on S"
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "(\n. 0) \ (if x \ S then 0::'b else 0)" for x
by force
qed auto
lemma measurable_on_scaleR_const:
assumes f: "f measurable_on S"
shows "(\x. c *\<^sub>R f x) measurable_on S"
proof -
obtain NF and F
where NF: "negligible NF"
and conF: "\n. continuous_on UNIV (F n)"
and tendsF: "\x. x \ NF \ (\n. F n x) \ (if x \ S then f x else 0)"
using f by (auto simp: measurable_on_def)
show ?thesis
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "continuous_on UNIV (\x. c *\<^sub>R F n x)" for n
by (intro conF continuous_intros)
show "(\n. c *\<^sub>R F n x) \ (if x \ S then c *\<^sub>R f x else 0)"
if "x \ NF" for x
using tendsto_scaleR [OF tendsto_const tendsF, of x] that by auto
qed (auto simp: NF)
qed
lemma measurable_on_cmul:
fixes c :: real
assumes "f measurable_on S"
shows "(\x. c * f x) measurable_on S"
using measurable_on_scaleR_const [OF assms] by simp
lemma measurable_on_cdivide:
fixes c :: real
assumes "f measurable_on S"
shows "(\x. f x / c) measurable_on S"
proof (cases "c=0")
case False
then show ?thesis
using measurable_on_cmul [of f S "1/c"]
by (simp add: assms)
qed auto
lemma measurable_on_minus:
"f measurable_on S \ (\x. -(f x)) measurable_on S"
using measurable_on_scaleR_const [of f S "-1"] by auto
lemma continuous_imp_measurable_on:
"continuous_on UNIV f \ f measurable_on UNIV"
unfolding measurable_on_def
apply (rule_tac x="{}" in exI)
apply (rule_tac x="\n. f" in exI, auto)
done
proposition integrable_subintervals_imp_measurable:
fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
assumes "\a b. f integrable_on cbox a b"
shows "f measurable_on UNIV"
proof -
define BOX where "BOX \ \h. \x::'a. cbox x (x + h *\<^sub>R One)"
define i where "i \ \h x. integral (BOX h x) f /\<^sub>R h ^ DIM('a)"
obtain N where "negligible N"
and k: "\x e. \x \ N; 0 < e\
\<Longrightarrow> \<exists>d>0. \<forall>h. 0 < h \<and> h < d \<longrightarrow>
norm (integral (cbox x (x + h *\<^sub>R One)) f /\<^sub>R h ^ DIM('a) - f x) < e"
using integrable_ccontinuous_explicit assms by blast
show ?thesis
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "continuous_on UNIV ((\n x. i (inverse(Suc n)) x) n)" for n
proof (clarsimp simp: continuous_on_iff)
show "\d>0. \x'. dist x' x < d \ dist (i (inverse (1 + real n)) x') (i (inverse (1 + real n)) x) < e"
if "0 < e"
for x e
proof -
let ?e = "e / (1 + real n) ^ DIM('a)"
have "?e > 0"
using \<open>e > 0\<close> by auto
moreover have "x \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One)"
by (simp add: mem_box inner_diff_left inner_left_distrib)
moreover have "x + One /\<^sub>R real (Suc n) \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One)"
by (auto simp: mem_box inner_diff_left inner_left_distrib field_simps)
ultimately obtain \<delta> where "\<delta> > 0"
and \<delta>: "\<And>c' d'. \<lbrakk>c' \<in> cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One);
d' \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One);
norm(c' - x) \ \; norm(d' - (x + One /\<^sub>R Suc n)) \ \\
\<Longrightarrow> norm(integral(cbox c' d') f - integral(cbox x (x + One /\<^sub>R Suc n)) f) < ?e"
by (blast intro: indefinite_integral_continuous [of f _ _ x] assms)
show ?thesis
proof (intro exI impI conjI allI)
show "min \ 1 > 0"
using \<open>\<delta> > 0\<close> by auto
show "dist (i (inverse (1 + real n)) y) (i (inverse (1 + real n)) x) < e"
if "dist y x < min \ 1" for y
proof -
have no: "norm (y - x) < 1"
using that by (auto simp: dist_norm)
have le1: "inverse (1 + real n) \ 1"
by (auto simp: field_split_simps)
have "norm (integral (cbox y (y + One /\<^sub>R real (Suc n))) f
- integral (cbox x (x + One /\<^sub>R real (Suc n))) f)
< e / (1 + real n) ^ DIM('a)"
proof (rule \<delta>)
show "y \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One)"
using no by (auto simp: mem_box algebra_simps dest: Basis_le_norm [of _ "y-x"])
show "y + One /\<^sub>R real (Suc n) \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One)"
proof (simp add: dist_norm mem_box algebra_simps, intro ballI conjI)
fix i::'a
assume "i \ Basis"
then have 1: "\y \ i - x \ i\ < 1"
by (metis inner_commute inner_diff_right no norm_bound_Basis_lt)
moreover have "\ < (2 + inverse (1 + real n))" "1 \ 2 - inverse (1 + real n)"
by (auto simp: field_simps)
ultimately show "x \ i \ y \ i + (2 + inverse (1 + real n))"
"y \ i + inverse (1 + real n) \ x \ i + 2"
by linarith+
qed
show "norm (y - x) \ \" "norm (y + One /\<^sub>R real (Suc n) - (x + One /\<^sub>R real (Suc n))) \ \"
using that by (auto simp: dist_norm)
qed
then show ?thesis
using that by (simp add: dist_norm i_def BOX_def flip: scaleR_diff_right) (simp add: field_simps)
qed
qed
qed
qed
show "negligible N"
by (simp add: \<open>negligible N\<close>)
show "(\n. i (inverse (Suc n)) x) \ (if x \ UNIV then f x else 0)"
if "x \ N" for x
unfolding lim_sequentially
proof clarsimp
show "\no. \n\no. dist (i (inverse (1 + real n)) x) (f x) < e"
if "0 < e" for e
proof -
obtain d where "d > 0"
and d: "\h. \0 < h; h < d\ \
norm (integral (cbox x (x + h *\<^sub>R One)) f /\<^sub>R h ^ DIM('a) - f x) < e"
using k [of x e] \<open>x \<notin> N\<close> \<open>0 < e\<close> by blast
then obtain M where M: "M \ 0" "0 < inverse (real M)" "inverse (real M) < d"
using real_arch_invD by auto
show ?thesis
proof (intro exI allI impI)
show "dist (i (inverse (1 + real n)) x) (f x) < e"
if "M \ n" for n
proof -
have *: "0 < inverse (1 + real n)" "inverse (1 + real n) \ inverse M"
using that \<open>M \<noteq> 0\<close> by auto
show ?thesis
using that M
apply (simp add: i_def BOX_def dist_norm)
apply (blast intro: le_less_trans * d)
done
qed
qed
qed
qed
qed
qed
subsection\<open>Composing continuous and measurable functions; a few variants\<close>
lemma measurable_on_compose_continuous:
assumes f: "f measurable_on UNIV" and g: "continuous_on UNIV g"
shows "(g \ f) measurable_on UNIV"
proof -
obtain N and F
where "negligible N"
and conF: "\n. continuous_on UNIV (F n)"
and tendsF: "\x. x \ N \ (\n. F n x) \ f x"
using f by (auto simp: measurable_on_def)
show ?thesis
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "negligible N"
by fact
show "continuous_on UNIV (g \ (F n))" for n
using conF continuous_on_compose continuous_on_subset g by blast
show "(\n. (g \ F n) x) \ (if x \ UNIV then (g \ f) x else 0)"
if "x \ N" for x :: 'a
using that g tendsF by (auto simp: continuous_on_def intro: tendsto_compose)
qed
qed
lemma measurable_on_compose_continuous_0:
assumes f: "f measurable_on S" and g: "continuous_on UNIV g" and "g 0 = 0"
shows "(g \ f) measurable_on S"
proof -
have f': "(\x. if x \ S then f x else 0) measurable_on UNIV"
using f measurable_on_UNIV by blast
show ?thesis
using measurable_on_compose_continuous [OF f' g]
by (simp add: measurable_on_UNIV o_def if_distrib \<open>g 0 = 0\<close> cong: if_cong)
qed
lemma measurable_on_compose_continuous_box:
assumes fm: "f measurable_on UNIV" and fab: "\x. f x \ box a b"
and contg: "continuous_on (box a b) g"
shows "(g \ f) measurable_on UNIV"
proof -
have "\\. (\n. continuous_on UNIV (\ n)) \ (\x. x \ N \ (\n. \ n x) \ g (f x))"
if "negligible N"
and conth [rule_format]: "\n. continuous_on UNIV (\x. h n x)"
and tends [rule_format]: "\x. x \ N \ (\n. h n x) \ f x"
for N and h :: "nat \ 'a \ 'b"
proof -
define \<theta> where "\<theta> \<equiv> \<lambda>n x. (\<Sum>i\<in>Basis. (max (a\<bullet>i + (b\<bullet>i - a\<bullet>i) / real (n+2))
(min ((h n x)\<bullet>i)
(b\<bullet>i - (b\<bullet>i - a\<bullet>i) / real (n+2)))) *\<^sub>R i)"
have aibi: "\i. i \ Basis \ a \ i < b \ i"
using box_ne_empty(2) fab by auto
then have *: "\i n. i \ Basis \ a \ i + real n * (a \ i) < b \ i + real n * (b \ i)"
by (meson add_mono_thms_linordered_field(3) less_eq_real_def mult_left_mono of_nat_0_le_iff)
show ?thesis
proof (intro exI conjI allI impI)
show "continuous_on UNIV (g \ (\ n))" for n :: nat
unfolding \<theta>_def
apply (intro continuous_on_compose2 [OF contg] continuous_intros conth)
apply (auto simp: aibi * mem_box less_max_iff_disj min_less_iff_disj field_split_simps)
done
show "(\n. (g \ \ n) x) \ g (f x)"
if "x \ N" for x
unfolding o_def
proof (rule isCont_tendsto_compose [where g=g])
show "isCont g (f x)"
using contg fab continuous_on_eq_continuous_at by blast
have "(\n. \ n x) \ (\i\Basis. max (a \ i) (min (f x \ i) (b \ i)) *\<^sub>R i)"
unfolding \<theta>_def
proof (intro tendsto_intros \<open>x \<notin> N\<close> tends)
fix i::'b
assume "i \ Basis"
have a: "(\n. a \ i + (b \ i - a \ i) / real n) \ a\i + 0"
by (intro tendsto_add lim_const_over_n tendsto_const)
show "(\n. a \ i + (b \ i - a \ i) / real (n + 2)) \ a \ i"
using LIMSEQ_ignore_initial_segment [where k=2, OF a] by simp
have b: "(\n. b\i - (b \ i - a \ i) / (real n)) \ b\i - 0"
by (intro tendsto_diff lim_const_over_n tendsto_const)
show "(\n. b \ i - (b \ i - a \ i) / real (n + 2)) \ b \ i"
using LIMSEQ_ignore_initial_segment [where k=2, OF b] by simp
qed
also have "(\i\Basis. max (a \ i) (min (f x \ i) (b \ i)) *\<^sub>R i) = (\i\Basis. (f x \ i) *\<^sub>R i)"
apply (rule sum.cong)
using fab
apply auto
apply (intro order_antisym)
apply (auto simp: mem_box)
using less_imp_le apply blast
by (metis (full_types) linear max_less_iff_conj min.bounded_iff not_le)
also have "\ = f x"
using euclidean_representation by blast
finally show "(\n. \ n x) \ f x" .
qed
qed
qed
then show ?thesis
using fm by (auto simp: measurable_on_def)
qed
lemma measurable_on_Pair:
assumes f: "f measurable_on S" and g: "g measurable_on S"
shows "(\x. (f x, g x)) measurable_on S"
proof -
obtain NF and F
where NF: "negligible NF"
and conF: "\n. continuous_on UNIV (F n)"
and tendsF: "\x. x \ NF \ (\n. F n x) \ (if x \ S then f x else 0)"
using f by (auto simp: measurable_on_def)
obtain NG and G
where NG: "negligible NG"
and conG: "\n. continuous_on UNIV (G n)"
and tendsG: "\x. x \ NG \ (\n. G n x) \ (if x \ S then g x else 0)"
using g by (auto simp: measurable_on_def)
show ?thesis
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "negligible (NF \ NG)"
by (simp add: NF NG)
show "continuous_on UNIV (\x. (F n x, G n x))" for n
using conF conG continuous_on_Pair by blast
show "(\n. (F n x, G n x)) \ (if x \ S then (f x, g x) else 0)"
if "x \ NF \ NG" for x
using tendsto_Pair [OF tendsF tendsG, of x x] that unfolding zero_prod_def
by (simp add: split: if_split_asm)
qed
qed
lemma measurable_on_combine:
assumes f: "f measurable_on S" and g: "g measurable_on S"
and h: "continuous_on UNIV (\x. h (fst x) (snd x))" and "h 0 0 = 0"
shows "(\x. h (f x) (g x)) measurable_on S"
proof -
have *: "(\x. h (f x) (g x)) = (\x. h (fst x) (snd x)) \ (\x. (f x, g x))"
by auto
show ?thesis
unfolding * by (auto simp: measurable_on_compose_continuous_0 measurable_on_Pair assms)
qed
lemma measurable_on_add:
assumes f: "f measurable_on S" and g: "g measurable_on S"
shows "(\x. f x + g x) measurable_on S"
by (intro continuous_intros measurable_on_combine [OF assms]) auto
lemma measurable_on_diff:
assumes f: "f measurable_on S" and g: "g measurable_on S"
shows "(\x. f x - g x) measurable_on S"
by (intro continuous_intros measurable_on_combine [OF assms]) auto
lemma measurable_on_scaleR:
assumes f: "f measurable_on S" and g: "g measurable_on S"
shows "(\x. f x *\<^sub>R g x) measurable_on S"
by (intro continuous_intros measurable_on_combine [OF assms]) auto
lemma measurable_on_sum:
assumes "finite I" "\i. i \ I \ f i measurable_on S"
shows "(\x. sum (\i. f i x) I) measurable_on S"
using assms by (induction I) (auto simp: measurable_on_add)
lemma measurable_on_spike:
assumes f: "f measurable_on T" and "negligible S" and gf: "\x. x \ T - S \ g x = f x"
shows "g measurable_on T"
proof -
obtain NF and F
where NF: "negligible NF"
and conF: "\n. continuous_on UNIV (F n)"
and tendsF: "\x. x \ NF \ (\n. F n x) \ (if x \ T then f x else 0)"
using f by (auto simp: measurable_on_def)
show ?thesis
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "negligible (NF \ S)"
by (simp add: NF \<open>negligible S\<close>)
show "\x. x \ NF \ S \ (\n. F n x) \ (if x \ T then g x else 0)"
by (metis (full_types) Diff_iff Un_iff gf tendsF)
qed (auto simp: conF)
qed
proposition indicator_measurable_on:
assumes "S \ sets lebesgue"
shows "indicat_real S measurable_on UNIV"
proof -
{ fix n::nat
let ?\<epsilon> = "(1::real) / (2 * 2^n)"
have \<epsilon>: "?\<epsilon> > 0"
by auto
obtain T where "closed T" "T \ S" "S-T \ lmeasurable" and ST: "emeasure lebesgue (S - T) < ?\"
by (meson \<epsilon> assms sets_lebesgue_inner_closed)
obtain U where "open U" "S \ U" "(U - S) \ lmeasurable" and US: "emeasure lebesgue (U - S) < ?\"
by (meson \<epsilon> assms sets_lebesgue_outer_open)
have eq: "-T \ U = (S-T) \ (U - S)"
using \<open>T \<subseteq> S\<close> \<open>S \<subseteq> U\<close> by auto
have "emeasure lebesgue ((S-T) \ (U - S)) \ emeasure lebesgue (S - T) + emeasure lebesgue (U - S)"
using \<open>S - T \<in> lmeasurable\<close> \<open>U - S \<in> lmeasurable\<close> emeasure_subadditive by blast
also have "\ < ?\ + ?\"
using ST US add_mono_ennreal by metis
finally have le: "emeasure lebesgue (-T \ U) < ennreal (1 / 2^n)"
by (simp add: eq)
have 1: "continuous_on (T \ -U) (indicat_real S)"
unfolding indicator_def
proof (rule continuous_on_cases [OF \<open>closed T\<close>])
show "closed (- U)"
using \<open>open U\<close> by blast
show "continuous_on T (\x. 1::real)" "continuous_on (- U) (\x. 0::real)"
by (auto simp: continuous_on)
show "\x. x \ T \ x \ S \ x \ - U \ x \ S \ (1::real) = 0"
using \<open>T \<subseteq> S\<close> \<open>S \<subseteq> U\<close> by auto
qed
have 2: "closedin (top_of_set UNIV) (T \ -U)"
using \<open>closed T\<close> \<open>open U\<close> by auto
obtain g where "continuous_on UNIV g" "\x. x \ T \ -U \ g x = indicat_real S x" "\x. norm(g x) \ 1"
by (rule Tietze [OF 1 2, of 1]) auto
with le have "\g E. continuous_on UNIV g \ (\x \ -E. g x = indicat_real S x) \
(\<forall>x. norm(g x) \<le> 1) \<and> E \<in> sets lebesgue \<and> emeasure lebesgue E < ennreal (1 / 2^n)"
apply (rule_tac x=g in exI)
apply (rule_tac x="-T \ U" in exI)
using \<open>S - T \<in> lmeasurable\<close> \<open>U - S \<in> lmeasurable\<close> eq by auto
}
then obtain g E where cont: "\n. continuous_on UNIV (g n)"
and geq: "\n x. x \ - E n \ g n x = indicat_real S x"
and ng1: "\n x. norm(g n x) \ 1"
and Eset: "\n. E n \ sets lebesgue"
and Em: "\n. emeasure lebesgue (E n) < ennreal (1 / 2^n)"
by metis
have null: "limsup E \ null_sets lebesgue"
proof (rule borel_cantelli_limsup1 [OF Eset])
show "emeasure lebesgue (E n) < \" for n
by (metis Em infinity_ennreal_def order.asym top.not_eq_extremum)
show "summable (\n. measure lebesgue (E n))"
proof (rule summable_comparison_test' [OF summable_geometric, of "1/2" 0])
show "norm (measure lebesgue (E n)) \ (1/2) ^ n" for n
using Em [of n] by (simp add: measure_def enn2real_leI power_one_over)
qed auto
qed
have tends: "(\n. g n x) \ indicat_real S x" if "x \ limsup E" for x
proof -
have "\\<^sub>F n in sequentially. x \ - E n"
using that by (simp add: mem_limsup_iff not_frequently)
then show ?thesis
unfolding tendsto_iff dist_real_def
by (simp add: eventually_mono geq)
qed
show ?thesis
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "negligible (limsup E)"
using negligible_iff_null_sets null by blast
show "continuous_on UNIV (g n)" for n
using cont by blast
qed (use tends in auto)
qed
lemma measurable_on_restrict:
assumes f: "f measurable_on UNIV" and S: "S \ sets lebesgue"
shows "(\x. if x \ S then f x else 0) measurable_on UNIV"
proof -
have "indicat_real S measurable_on UNIV"
by (simp add: S indicator_measurable_on)
then show ?thesis
using measurable_on_scaleR [OF _ f, of "indicat_real S"]
by (simp add: indicator_scaleR_eq_if)
qed
lemma measurable_on_const_UNIV: "(\x. k) measurable_on UNIV"
by (simp add: continuous_imp_measurable_on)
lemma measurable_on_const [simp]: "S \ sets lebesgue \ (\x. k) measurable_on S"
using measurable_on_UNIV measurable_on_const_UNIV measurable_on_restrict by blast
lemma simple_function_indicator_representation_real:
fixes f ::"'a \ real"
assumes f: "simple_function M f" and x: "x \ space M" and nn: "\x. f x \ 0"
shows "f x = (\y \ f ` space M. y * indicator (f -` {y} \ space M) x)"
proof -
have f': "simple_function M (ennreal \ f)"
by (simp add: f)
have *: "f x =
enn2real
(\<Sum>y\<in> ennreal ` f ` space M.
y * indicator ((ennreal \<circ> f) -` {y} \<inter> space M) x)"
using arg_cong [OF simple_function_indicator_representation [OF f' x], of enn2real, simplified nn o_def] nn
unfolding o_def image_comp
by (metis enn2real_ennreal)
have "enn2real (\y\ennreal ` f ` space M. if ennreal (f x) = y \ x \ space M then y else 0)
= sum (enn2real \<circ> (\<lambda>y. if ennreal (f x) = y \<and> x \<in> space M then y else 0))
(ennreal ` f ` space M)"
by (rule enn2real_sum) auto
also have "\ = sum (enn2real \ (\y. if ennreal (f x) = y \ x \ space M then y else 0) \ ennreal)
(f ` space M)"
by (rule sum.reindex) (use nn in \<open>auto simp: inj_on_def intro: sum.cong\<close>)
also have "\ = (\y\f ` space M. if f x = y \ x \ space M then y else 0)"
using nn
by (auto simp: inj_on_def intro: sum.cong)
finally show ?thesis
by (subst *) (simp add: enn2real_sum indicator_def if_distrib cong: if_cong)
qed
lemma\<^marker>\<open>tag important\<close> simple_function_induct_real
[consumes 1, case_names cong set mult add, induct set: simple_function]:
fixes u :: "'a \ real"
assumes u: "simple_function M u"
assumes cong: "\f g. simple_function M f \ simple_function M g \ (AE x in M. f x = g x) \ P f \ P g"
assumes set: "\A. A \ sets M \ P (indicator A)"
assumes mult: "\u c. P u \ P (\x. c * u x)"
assumes add: "\u v. P u \ P v \ P (\x. u x + v x)"
and nn: "\x. u x \ 0"
shows "P u"
proof (rule cong)
from AE_space show "AE x in M. (\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x"
proof eventually_elim
fix x assume x: "x \ space M"
from simple_function_indicator_representation_real[OF u x] nn
show "(\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x"
by metis
qed
next
from u have "finite (u ` space M)"
unfolding simple_function_def by auto
then show "P (\x. \y\u ` space M. y * indicator (u -` {y} \ space M) x)"
proof induct
case empty
then show ?case
using set[of "{}"] by (simp add: indicator_def[abs_def])
next
case (insert a F)
have eq: "\ {y. u x = y \ (y = a \ y \ F) \ x \ space M}
= (if u x = a \<and> x \<in> space M then a else 0) + \<Sum> {y. u x = y \<and> y \<in> F \<and> x \<in> space M}" for x
proof (cases "x \ space M")
case True
have *: "{y. u x = y \ (y = a \ y \ F)} = {y. u x = a \ y = a} \ {y. u x = y \ y \ F}"
by auto
show ?thesis
using insert by (simp add: * True)
qed auto
have a: "P (\x. a * indicator (u -` {a} \ space M) x)"
proof (intro mult set)
show "u -` {a} \ space M \ sets M"
using u by auto
qed
show ?case
using nn insert a
by (simp add: eq indicator_times_eq_if [where f = "\x. a"] add)
qed
next
show "simple_function M (\x. (\y\u ` space M. y * indicator (u -` {y} \ space M) x))"
apply (subst simple_function_cong)
apply (rule simple_function_indicator_representation_real[symmetric])
apply (auto intro: u nn)
done
qed fact
proposition simple_function_measurable_on_UNIV:
fixes f :: "'a::euclidean_space \ real"
assumes f: "simple_function lebesgue f" and nn: "\x. f x \ 0"
shows "f measurable_on UNIV"
using f
proof (induction f)
case (cong f g)
then obtain N where "negligible N" "{x. g x \ f x} \ N"
by (auto simp: eventually_ae_filter_negligible eq_commute)
then show ?case
by (blast intro: measurable_on_spike cong)
next
case (set S)
then show ?case
by (simp add: indicator_measurable_on)
next
case (mult u c)
then show ?case
by (simp add: measurable_on_cmul)
case (add u v)
then show ?case
by (simp add: measurable_on_add)
qed (auto simp: nn)
lemma simple_function_lebesgue_if:
fixes f :: "'a::euclidean_space \ real"
assumes f: "simple_function lebesgue f" and S: "S \ sets lebesgue"
shows "simple_function lebesgue (\x. if x \ S then f x else 0)"
proof -
have ffin: "finite (range f)" and fsets: "\x. f -` {f x} \ sets lebesgue"
using f by (auto simp: simple_function_def)
have "finite (f ` S)"
by (meson finite_subset subset_image_iff ffin top_greatest)
moreover have "finite ((\x. 0::real) ` T)" for T :: "'a set"
by (auto simp: image_def)
moreover have if_sets: "(\x. if x \ S then f x else 0) -` {f a} \ sets lebesgue" for a
proof -
have *: "(\x. if x \ S then f x else 0) -` {f a}
= (if f a = 0 then -S \<union> f -` {f a} else (f -` {f a}) \<inter> S)"
by (auto simp: split: if_split_asm)
show ?thesis
unfolding * by (metis Compl_in_sets_lebesgue S sets.Int sets.Un fsets)
qed
moreover have "(\x. if x \ S then f x else 0) -` {0} \ sets lebesgue"
proof (cases "0 \ range f")
case True
then show ?thesis
by (metis (no_types, lifting) if_sets rangeE)
next
case False
then have "(\x. if x \ S then f x else 0) -` {0} = -S"
by auto
then show ?thesis
by (simp add: Compl_in_sets_lebesgue S)
qed
ultimately show ?thesis
by (auto simp: simple_function_def)
qed
corollary simple_function_measurable_on:
fixes f :: "'a::euclidean_space \ real"
assumes f: "simple_function lebesgue f" and nn: "\x. f x \ 0" and S: "S \ sets lebesgue"
shows "f measurable_on S"
by (simp add: measurable_on_UNIV [symmetric, of f] S f simple_function_lebesgue_if nn simple_function_measurable_on_UNIV)
lemma
fixes f :: "'a::euclidean_space \ 'b::ordered_euclidean_space"
assumes f: "f measurable_on S" and g: "g measurable_on S"
shows measurable_on_sup: "(\x. sup (f x) (g x)) measurable_on S"
and measurable_on_inf: "(\x. inf (f x) (g x)) measurable_on S"
proof -
obtain NF and F
where NF: "negligible NF"
and conF: "\n. continuous_on UNIV (F n)"
and tendsF: "\x. x \ NF \ (\n. F n x) \ (if x \ S then f x else 0)"
using f by (auto simp: measurable_on_def)
obtain NG and G
where NG: "negligible NG"
and conG: "\n. continuous_on UNIV (G n)"
and tendsG: "\x. x \ NG \ (\n. G n x) \ (if x \ S then g x else 0)"
using g by (auto simp: measurable_on_def)
show "(\x. sup (f x) (g x)) measurable_on S"
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "continuous_on UNIV (\x. sup (F n x) (G n x))" for n
unfolding sup_max eucl_sup by (intro conF conG continuous_intros)
show "(\n. sup (F n x) (G n x)) \ (if x \ S then sup (f x) (g x) else 0)"
if "x \ NF \ NG" for x
using tendsto_sup [OF tendsF tendsG, of x x] that by auto
qed (simp add: NF NG)
show "(\x. inf (f x) (g x)) measurable_on S"
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "continuous_on UNIV (\x. inf (F n x) (G n x))" for n
unfolding inf_min eucl_inf by (intro conF conG continuous_intros)
show "(\n. inf (F n x) (G n x)) \ (if x \ S then inf (f x) (g x) else 0)"
if "x \ NF \ NG" for x
using tendsto_inf [OF tendsF tendsG, of x x] that by auto
qed (simp add: NF NG)
qed
proposition measurable_on_componentwise_UNIV:
"f measurable_on UNIV \ (\i\Basis. (\x. (f x \ i) *\<^sub>R i) measurable_on UNIV)"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
show ?rhs
proof
fix i::'b
assume "i \ Basis"
have cont: "continuous_on UNIV (\x. (x \ i) *\<^sub>R i)"
by (intro continuous_intros)
show "(\x. (f x \ i) *\<^sub>R i) measurable_on UNIV"
using measurable_on_compose_continuous [OF L cont]
by (simp add: o_def)
qed
next
assume ?rhs
then have "\N g. negligible N \
(\<forall>n. continuous_on UNIV (g n)) \<and>
(\<forall>x. x \<notin> N \<longrightarrow> (\<lambda>n. g n x) \<longlonglongrightarrow> (f x \<bullet> i) *\<^sub>R i)"
if "i \ Basis" for i
by (simp add: measurable_on_def that)
then obtain N g where N: "\i. i \ Basis \ negligible (N i)"
and cont: "\i n. i \ Basis \ continuous_on UNIV (g i n)"
and tends: "\i x. \i \ Basis; x \ N i\ \ (\n. g i n x) \ (f x \ i) *\<^sub>R i"
by metis
show ?lhs
unfolding measurable_on_def
proof (intro exI conjI allI impI)
show "negligible (\i \ Basis. N i)"
using N eucl.finite_Basis by blast
show "continuous_on UNIV (\x. (\i\Basis. g i n x))" for n
by (intro continuous_intros cont)
next
fix x
assume "x \ (\i \ Basis. N i)"
then have "\i. i \ Basis \ x \ N i"
by auto
then have "(\n. (\i\Basis. g i n x)) \ (\i\Basis. (f x \ i) *\<^sub>R i)"
by (intro tends tendsto_intros)
then show "(\n. (\i\Basis. g i n x)) \ (if x \ UNIV then f x else 0)"
by (simp add: euclidean_representation)
qed
qed
corollary measurable_on_componentwise:
"f measurable_on S \ (\i\Basis. (\x. (f x \ i) *\<^sub>R i) measurable_on S)"
apply (subst measurable_on_UNIV [symmetric])
apply (subst measurable_on_componentwise_UNIV)
apply (simp add: measurable_on_UNIV if_distrib [of "\x. inner x _"] if_distrib [of "\x. scaleR x _"] cong: if_cong)
done
(*FIXME: avoid duplication of proofs WRT borel_measurable_implies_simple_function_sequence*)
lemma\<^marker>\<open>tag important\<close> borel_measurable_implies_simple_function_sequence_real:
fixes u :: "'a \ real"
assumes u[measurable]: "u \ borel_measurable M" and nn: "\x. u x \ 0"
shows "\f. incseq f \ (\i. simple_function M (f i)) \ (\x. bdd_above (range (\i. f i x))) \
(\<forall>i x. 0 \<le> f i x) \<and> u = (SUP i. f i)"
proof -
define f where [abs_def]:
"f i x = real_of_int (floor ((min i (u x)) * 2^i)) / 2^i" for i x
have [simp]: "0 \ f i x" for i x
by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg nn)
have *: "2^n * real_of_int x = real_of_int (2^n * x)" for n x
by simp
have "real_of_int \real i * 2 ^ i\ = real_of_int \i * 2 ^ i\" for i
by (intro arg_cong[where f=real_of_int]) simp
then have [simp]: "real_of_int \real i * 2 ^ i\ = i * 2 ^ i" for i
unfolding floor_of_nat by simp
have bdd: "bdd_above (range (\i. f i x))" for x
by (rule bdd_aboveI [where M = "u x"]) (auto simp: f_def field_simps min_def)
have "incseq f"
proof (intro monoI le_funI)
fix m n :: nat and x assume "m \ n"
moreover
{ fix d :: nat
have "\2^d::real\ * \2^m * (min (of_nat m) (u x))\ \ \2^d * (2^m * (min (of_nat m) (u x)))\"
by (rule le_mult_floor) (auto simp: nn)
also have "\ \ \2^d * (2^m * (min (of_nat d + of_nat m) (u x)))\"
by (intro floor_mono mult_mono min.mono)
(auto simp: nn min_less_iff_disj of_nat_less_top)
finally have "f m x \ f(m + d) x"
unfolding f_def
by (auto simp: field_simps power_add * simp del: of_int_mult) }
ultimately show "f m x \ f n x"
by (auto simp: le_iff_add)
qed
then have inc_f: "incseq (\i. f i x)" for x
by (auto simp: incseq_def le_fun_def)
moreover
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.56 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
