# HG changeset patch # User hoelzl # Date 1401458190 -7200 # Node ID f174712d0a843ca25c6ffc20443dea152443f963 # Parent 653e56c6c963b096c294f90421a839dd8f77db0a better support for restrict_space diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Fri May 30 18:13:40 2014 +0200 +++ b/src/HOL/Probability/Bochner_Integration.thy Fri May 30 15:56:30 2014 +0200 @@ -856,6 +856,32 @@ by (rule has_bochner_integral_eq) qed +lemma simple_bochner_integrable_restrict_space: + fixes f :: "_ \ 'b::real_normed_vector" + assumes \: "\ \ space M \ sets M" + shows "simple_bochner_integrable (restrict_space M \) f \ + simple_bochner_integrable M (\x. indicator \ x *\<^sub>R f x)" + by (simp add: simple_bochner_integrable.simps space_restrict_space + simple_function_restrict_space[OF \] emeasure_restrict_space[OF \] Collect_restrict + indicator_eq_0_iff conj_ac) + +lemma simple_bochner_integral_restrict_space: + fixes f :: "_ \ 'b::real_normed_vector" + assumes \: "\ \ space M \ sets M" + assumes f: "simple_bochner_integrable (restrict_space M \) f" + shows "simple_bochner_integral (restrict_space M \) f = + simple_bochner_integral M (\x. indicator \ x *\<^sub>R f x)" +proof - + have "finite ((\x. indicator \ x *\<^sub>R f x)`space M)" + using f simple_bochner_integrable_restrict_space[OF \, of f] + by (simp add: simple_bochner_integrable.simps simple_function_def) + then show ?thesis + by (auto simp: space_restrict_space measure_restrict_space[OF \(1)] le_infI2 + simple_bochner_integral_def Collect_restrict + split: split_indicator split_indicator_asm + intro!: setsum_mono_zero_cong_left arg_cong2[where f=measure]) +qed + inductive integrable for M f where "has_bochner_integral M f x \ integrable M f" @@ -1251,14 +1277,14 @@ by (simp add: integrable_iff_bounded borel_measurable_indicator_iff ereal_indicator nn_integral_indicator' cong: conj_cong) -lemma integral_dominated_convergence: +lemma fixes f :: "'a \ 'b::{banach, second_countable_topology}" and w :: "'a \ real" assumes "f \ borel_measurable M" "\i. s i \ borel_measurable M" "integrable M w" assumes lim: "AE x in M. (\i. s i x) ----> f x" assumes bound: "\i. AE x in M. norm (s i x) \ w x" - shows "integrable M f" - and "\i. integrable M (s i)" - and "(\i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f" + shows integrable_dominated_convergence: "integrable M f" + and integrable_dominated_convergence2: "\i. integrable M (s i)" + and integral_dominated_convergence: "(\i. integral\<^sup>L M (s i)) ----> integral\<^sup>L M f" proof - have "AE x in M. 0 \ w x" using bound[of 0] by eventually_elim (auto intro: norm_ge_zero order_trans) @@ -1421,13 +1447,14 @@ finally show "norm (\i (\i. norm (f i x))" by simp qed - note int = integral_dominated_convergence(1,3)[OF _ _ 1 2 3] + note ibl = integrable_dominated_convergence[OF _ _ 1 2 3] + note int = integral_dominated_convergence[OF _ _ 1 2 3] show "integrable M ?S" - by (rule int) measurable + by (rule ibl) measurable show "?f sums ?x" unfolding sums_def - using int(2) by (simp add: integrable) + using int by (simp add: integrable) then show "?x = suminf ?f" "summable ?f" unfolding sums_iff by auto qed @@ -1600,6 +1627,49 @@ by simp qed +subsection {* Restricted measure spaces *} + +lemma integrable_restrict_space: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + assumes \[simp]: "\ \ space M \ sets M" + shows "integrable (restrict_space M \) f \ integrable M (\x. indicator \ x *\<^sub>R f x)" + unfolding integrable_iff_bounded + borel_measurable_restrict_space_iff[OF \] + nn_integral_restrict_space[OF \] + by (simp add: ac_simps ereal_indicator times_ereal.simps(1)[symmetric] del: times_ereal.simps) + +lemma integral_restrict_space: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + assumes \[simp]: "\ \ space M \ sets M" + shows "integral\<^sup>L (restrict_space M \) f = integral\<^sup>L M (\x. indicator \ x *\<^sub>R f x)" +proof (rule integral_eq_cases) + assume "integrable (restrict_space M \) f" + then show ?thesis + proof induct + case (base A c) then show ?case + by (simp add: indicator_inter_arith[symmetric] sets_restrict_space_iff + emeasure_restrict_space Int_absorb1 measure_restrict_space) + next + case (add g f) then show ?case + by (simp add: scaleR_add_right integrable_restrict_space) + next + case (lim f s) + show ?case + proof (rule LIMSEQ_unique) + show "(\i. integral\<^sup>L (restrict_space M \) (s i)) ----> integral\<^sup>L (restrict_space M \) f" + using lim by (intro integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) simp_all + + show "(\i. integral\<^sup>L (restrict_space M \) (s i)) ----> (\ x. indicator \ x *\<^sub>R f x \M)" + unfolding lim + using lim + by (intro integral_dominated_convergence[where w="\x. 2 * norm (indicator \ x *\<^sub>R f x)"]) + (auto simp add: space_restrict_space integrable_restrict_space + simp del: norm_scaleR + split: split_indicator) + qed + qed +qed (simp add: integrable_restrict_space) + subsection {* Measure spaces with an associated density *} lemma integrable_density: @@ -1653,7 +1723,7 @@ show ?case proof (rule LIMSEQ_unique) show "(\i. integral\<^sup>L M (\x. g x *\<^sub>R s i x)) ----> integral\<^sup>L M (\x. g x *\<^sub>R f x)" - proof (rule integral_dominated_convergence(3)) + proof (rule integral_dominated_convergence) show "integrable M (\x. 2 * norm (g x *\<^sub>R f x))" by (intro integrable_mult_right integrable_norm integrable_density[THEN iffD1] lim g) auto show "AE x in M. (\i. g x *\<^sub>R s i x) ----> g x *\<^sub>R f x" @@ -1663,7 +1733,7 @@ qed auto show "(\i. integral\<^sup>L M (\x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f" unfolding lim(2)[symmetric] - by (rule integral_dominated_convergence(3)[where w="\x. 2 * norm (f x)"]) + by (rule integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) (insert lim(3-5), auto) qed qed @@ -1732,7 +1802,7 @@ show ?case proof (rule LIMSEQ_unique) show "(\i. integral\<^sup>L M (\x. s i (g x))) ----> integral\<^sup>L M (\x. f (g x))" - proof (rule integral_dominated_convergence(3)) + proof (rule integral_dominated_convergence) show "integrable M (\x. 2 * norm (f (g x)))" using lim by (auto simp: integrable_distr_eq) show "AE x in M. (\i. s i (g x)) ----> f (g x)" @@ -1742,7 +1812,7 @@ qed auto show "(\i. integral\<^sup>L M (\x. s i (g x))) ----> integral\<^sup>L (distr M N g) f" unfolding lim(2)[symmetric] - by (rule integral_dominated_convergence(3)[where w="\x. 2 * norm (f x)"]) + by (rule integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) (insert lim(3-5), auto) qed qed diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Fri May 30 18:13:40 2014 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Fri May 30 15:56:30 2014 +0200 @@ -119,6 +119,52 @@ shows "f \ borel_measurable M" using assms unfolding measurable_def by auto +lemma borel_measurable_restrict_space_iff_ereal: + fixes f :: "'a \ ereal" + assumes \[measurable, simp]: "\ \ space M \ sets M" + shows "f \ borel_measurable (restrict_space M \) \ + (\x. f x * indicator \ x) \ borel_measurable M" +proof - + { fix X :: "ereal set" assume "X \ sets borel" + have 1: "(\x. f x * indicator \ x) -` X \ space M = + (if 0 \ X then (f -` X \ (\ \ space M)) \ (space M - (\ \ space M)) else f -` X \ (\ \ space M))" + by (auto split: split_if_asm simp: indicator_def) + have *: "f -` X \ (\ \ space M) = + (f -` X \ (\ \ space M) \ (space M - \ \ space M)) - (space M - \ \ space M)" + by auto + have "f -` X \ (\ \ space M) \ (space M - \ \ space M) \ sets M + \ f -` X \ (\ \ space M) \ sets M" + by (subst *) auto + note this 1 } + note 1 = this(1) and 2 = this(2) + + from 2 show ?thesis + by (auto simp add: measurable_def space_restrict_space sets_restrict_space_iff intro: 1 \) +qed + +lemma borel_measurable_restrict_space_iff: + fixes f :: "'a \ 'b::real_normed_vector" + assumes \[measurable, simp]: "\ \ space M \ sets M" + shows "f \ borel_measurable (restrict_space M \) \ + (\x. indicator \ x *\<^sub>R f x) \ borel_measurable M" +proof - + { fix X :: "'b set" assume "X \ sets borel" + have 1: "(\x. indicator \ x *\<^sub>R f x) -` X \ space M = + (if 0 \ X then (f -` X \ (\ \ space M)) \ (space M - (\ \ space M)) else f -` X \ (\ \ space M))" + by (auto split: split_if_asm simp: indicator_def) + have *: "f -` X \ (\ \ space M) = + (f -` X \ (\ \ space M) \ (space M - \ \ space M)) - (space M - \ \ space M)" + by auto + have "f -` X \ (\ \ space M) \ (space M - \ \ space M) \ sets M + \ f -` X \ (\ \ space M) \ sets M" + by (subst *) auto + note this 1 } + note 1 = this(1) and 2 = this(2) + + from 2 show ?thesis + by (auto simp add: measurable_def space_restrict_space sets_restrict_space_iff intro: 1 \) +qed + lemma borel_measurable_continuous_on1: fixes f :: "'a::topological_space \ 'b::topological_space" assumes "continuous_on UNIV f" diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Fri May 30 18:13:40 2014 +0200 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri May 30 15:56:30 2014 +0200 @@ -740,7 +740,7 @@ show "\x\UNIV. (\k. s k x) ----> f x" using lim by auto show "(\k. integral\<^sup>L lebesgue (s k)) ----> integral\<^sup>L lebesgue f" - using lim by (intro integral_dominated_convergence(3)[where w="\x. 2 * norm (f x)"]) auto + using lim by (intro integral_dominated_convergence[where w="\x. 2 * norm (f x)"]) auto qed qed diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Fri May 30 18:13:40 2014 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Fri May 30 15:56:30 2014 +0200 @@ -1693,6 +1693,29 @@ by (simp add: emeasure_notin_sets) qed +lemma measure_restrict_space: + assumes "\ \ space M \ sets M" "A \ \" + shows "measure (restrict_space M \) A = measure M A" + using emeasure_restrict_space[OF assms] by (simp add: measure_def) + +lemma AE_restrict_space_iff: + assumes "\ \ space M \ sets M" + shows "(AE x in restrict_space M \. P x) \ (AE x in M. x \ \ \ P x)" +proof - + have ex_cong: "\P Q f. (\x. P x \ Q x) \ (\x. Q x \ P (f x)) \ (\x. P x) \ (\x. Q x)" + by auto + { fix X assume X: "X \ sets M" "emeasure M X = 0" + then have "emeasure M (\ \ space M \ X) \ emeasure M X" + by (intro emeasure_mono) auto + then have "emeasure M (\ \ space M \ X) = 0" + using X by (auto intro!: antisym) } + with assms show ?thesis + unfolding eventually_ae_filter + by (auto simp add: space_restrict_space null_sets_def sets_restrict_space_iff + emeasure_restrict_space cong: conj_cong + intro!: ex_cong[where f="\X. (\ \ space M) \ X"]) +qed + lemma restrict_restrict_space: assumes "A \ space M \ sets M" "B \ space M \ sets M" shows "restrict_space (restrict_space M A) B = restrict_space M (A \ B)" (is "?l = ?r") @@ -1718,5 +1741,18 @@ by (cases "finite X") (auto simp add: emeasure_restrict_space) qed +lemma restrict_distr: + assumes [measurable]: "f \ measurable M N" + assumes [simp]: "\ \ space N \ sets N" and restrict: "f \ space M \ \" + shows "restrict_space (distr M N f) \ = distr M (restrict_space N \) f" + (is "?l = ?r") +proof (rule measure_eqI) + fix A assume "A \ sets (restrict_space (distr M N f) \)" + with restrict show "emeasure ?l A = emeasure ?r A" + by (subst emeasure_distr) + (auto simp: sets_restrict_space_iff emeasure_restrict_space emeasure_distr + intro!: measurable_restrict_space2) +qed (simp add: sets_restrict_space) + end diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri May 30 18:13:40 2014 +0200 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri May 30 15:56:30 2014 +0200 @@ -1733,32 +1733,102 @@ subsubsection {* Measures with Restricted Space *} +lemma simple_function_iff_borel_measurable: + fixes f :: "'a \ 'x::{t2_space}" + shows "simple_function M f \ finite (f ` space M) \ f \ borel_measurable M" + by (metis borel_measurable_simple_function simple_functionD(1) simple_function_borel_measurable) + +lemma simple_function_restrict_space_ereal: + fixes f :: "'a \ ereal" + assumes "\ \ space M \ sets M" + shows "simple_function (restrict_space M \) f \ simple_function M (\x. f x * indicator \ x)" +proof - + { assume "finite (f ` space (restrict_space M \))" + then have "finite (f ` space (restrict_space M \) \ {0})" by simp + then have "finite ((\x. f x * indicator \ x) ` space M)" + by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) } + moreover + { assume "finite ((\x. f x * indicator \ x) ` space M)" + then have "finite (f ` space (restrict_space M \))" + by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) } + ultimately show ?thesis + unfolding simple_function_iff_borel_measurable + borel_measurable_restrict_space_iff_ereal[OF assms] + by auto +qed + +lemma simple_function_restrict_space: + fixes f :: "'a \ 'b::real_normed_vector" + assumes "\ \ space M \ sets M" + shows "simple_function (restrict_space M \) f \ simple_function M (\x. indicator \ x *\<^sub>R f x)" +proof - + { assume "finite (f ` space (restrict_space M \))" + then have "finite (f ` space (restrict_space M \) \ {0})" by simp + then have "finite ((\x. indicator \ x *\<^sub>R f x) ` space M)" + by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) } + moreover + { assume "finite ((\x. indicator \ x *\<^sub>R f x) ` space M)" + then have "finite (f ` space (restrict_space M \))" + by (rule rev_finite_subset) (auto split: split_indicator simp: space_restrict_space) } + ultimately show ?thesis + unfolding simple_function_iff_borel_measurable + borel_measurable_restrict_space_iff[OF assms] + by auto +qed + + +lemma split_indicator_asm: "P (indicator Q x) = (\ (x \ Q \ \ P 1 \ x \ Q \ \ P 0))" + by (auto split: split_indicator) + +lemma simple_integral_restrict_space: + assumes \: "\ \ space M \ sets M" "simple_function (restrict_space M \) f" + shows "simple_integral (restrict_space M \) f = simple_integral M (\x. f x * indicator \ x)" + using simple_function_restrict_space_ereal[THEN iffD1, OF \, THEN simple_functionD(1)] + by (auto simp add: space_restrict_space emeasure_restrict_space[OF \(1)] le_infI2 simple_integral_def + split: split_indicator split_indicator_asm + intro!: setsum_mono_zero_cong_left ereal_left_mult_cong arg_cong2[where f=emeasure]) + +lemma one_not_less_zero[simp]: "\ 1 < (0::ereal)" + by (simp add: zero_ereal_def one_ereal_def) + lemma nn_integral_restrict_space: - assumes \: "\ \ sets M" and f: "f \ borel_measurable M" "\x. 0 \ f x" "\x. x \ space M - \ \ f x = 0" - shows "nn_integral (restrict_space M \) f = nn_integral M f" -using f proof (induct rule: borel_measurable_induct) - case (cong f g) then show ?case - using nn_integral_cong[of M f g] nn_integral_cong[of "restrict_space M \" f g] - sets.sets_into_space[OF `\ \ sets M`] - by (simp add: subset_eq space_restrict_space) -next - case (set A) - then have "A \ \" - unfolding indicator_eq_0_iff by (auto dest: sets.sets_into_space) - with set `\ \ sets M` sets.sets_into_space[OF `\ \ sets M`] show ?case - by (subst nn_integral_indicator') - (auto simp add: sets_restrict_space_iff space_restrict_space - emeasure_restrict_space Int_absorb2 - dest: sets.sets_into_space) -next - case (mult f c) then show ?case - by (cases "c = 0") (simp_all add: measurable_restrict_space1 \ nn_integral_cmult) -next - case (add f g) then show ?case - by (simp add: measurable_restrict_space1 \ nn_integral_add ereal_add_nonneg_eq_0_iff) -next - case (seq F) then show ?case - by (auto simp add: SUP_eq_iff measurable_restrict_space1 \ nn_integral_monotone_convergence_SUP) + assumes \[simp]: "\ \ space M \ sets M" + shows "nn_integral (restrict_space M \) f = nn_integral M (\x. f x * indicator \ x)" +proof - + let ?R = "restrict_space M \" and ?X = "\M f. {s. simple_function M s \ s \ max 0 \ f \ range s \ {0 ..< \}}" + have "integral\<^sup>S ?R ` ?X ?R f = integral\<^sup>S M ` ?X M (\x. f x * indicator \ x)" + proof (safe intro!: image_eqI) + fix s assume s: "simple_function ?R s" "s \ max 0 \ f" "range s \ {0..<\}" + from s show "integral\<^sup>S (restrict_space M \) s = integral\<^sup>S M (\x. s x * indicator \ x)" + by (intro simple_integral_restrict_space) auto + from s show "simple_function M (\x. s x * indicator \ x)" + by (simp add: simple_function_restrict_space_ereal) + from s show "(\x. s x * indicator \ x) \ max 0 \ (\x. f x * indicator \ x)" + "\x. s x * indicator \ x \ {0..<\}" + by (auto split: split_indicator simp: le_fun_def image_subset_iff) + next + fix s assume s: "simple_function M s" "s \ max 0 \ (\x. f x * indicator \ x)" "range s \ {0..<\}" + then have "simple_function M (\x. s x * indicator (\ \ space M) x)" (is ?s') + by (intro simple_function_mult simple_function_indicator) auto + also have "?s' \ simple_function M (\x. s x * indicator \ x)" + by (rule simple_function_cong) (auto split: split_indicator) + finally show sf: "simple_function (restrict_space M \) s" + by (simp add: simple_function_restrict_space_ereal) + + from s have s_eq: "s = (\x. s x * indicator \ x)" + by (auto simp add: fun_eq_iff le_fun_def image_subset_iff + split: split_indicator split_indicator_asm + intro: antisym) + + show "integral\<^sup>S M s = integral\<^sup>S (restrict_space M \) s" + by (subst s_eq) (rule simple_integral_restrict_space[symmetric, OF \ sf]) + show "\x. s x \ {0..<\}" + using s by (auto simp: image_subset_iff) + from s show "s \ max 0 \ f" + by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm) + qed + then show ?thesis + unfolding nn_integral_def_finite SUP_def by simp qed subsubsection {* Measure spaces with an associated density *} diff -r 653e56c6c963 -r f174712d0a84 src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Fri May 30 18:13:40 2014 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Fri May 30 15:56:30 2014 +0200 @@ -2351,9 +2351,9 @@ qed lemma measurable_restrict_space2: - "\ \ sets N \ f \ space M \ \ \ f \ measurable M N \ + "\ \ space N \ sets N \ f \ space M \ \ \ f \ measurable M N \ f \ measurable M (restrict_space N \)" - by (simp add: measurable_def space_restrict_space sets_restrict_space_iff) + by (simp add: measurable_def space_restrict_space sets_restrict_space_iff Pi_Int[symmetric]) end