equal
deleted
inserted
replaced
495 using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) |
495 using s t by (auto intro: borel_measurable_simple_function elim: simple_bochner_integrable.cases) |
496 |
496 |
497 have "ennreal (norm (?s - ?t)) = norm (simple_bochner_integral M (\<lambda>x. s x - t x))" |
497 have "ennreal (norm (?s - ?t)) = norm (simple_bochner_integral M (\<lambda>x. s x - t x))" |
498 using s t by (subst simple_bochner_integral_diff) auto |
498 using s t by (subst simple_bochner_integral_diff) auto |
499 also have "\<dots> \<le> simple_bochner_integral M (\<lambda>x. norm (s x - t x))" |
499 also have "\<dots> \<le> simple_bochner_integral M (\<lambda>x. norm (s x - t x))" |
500 using simple_bochner_integrable_compose2[of "op -" M "s" "t"] s t |
500 using simple_bochner_integrable_compose2[of "(-)" M "s" "t"] s t |
501 by (auto intro!: simple_bochner_integral_norm_bound) |
501 by (auto intro!: simple_bochner_integral_norm_bound) |
502 also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)" |
502 also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)" |
503 using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t |
503 using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t |
504 by (auto intro!: simple_bochner_integral_eq_nn_integral) |
504 by (auto intro!: simple_bochner_integral_eq_nn_integral) |
505 also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \<partial>M)" |
505 also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \<partial>M)" |
1853 then have s'_eq_s: "\<And>i x. x \<in> space M \<Longrightarrow> s' i x = s i x" |
1853 then have s'_eq_s: "\<And>i x. x \<in> space M \<Longrightarrow> s' i x = s i x" |
1854 by simp |
1854 by simp |
1855 |
1855 |
1856 have sf[measurable]: "\<And>i. simple_function M (s' i)" |
1856 have sf[measurable]: "\<And>i. simple_function M (s' i)" |
1857 unfolding s'_def using s(1) |
1857 unfolding s'_def using s(1) |
1858 by (intro simple_function_compose2[where h="op *\<^sub>R"] simple_function_indicator) auto |
1858 by (intro simple_function_compose2[where h="( *\<^sub>R)"] simple_function_indicator) auto |
1859 |
1859 |
1860 { fix i |
1860 { fix i |
1861 have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} = |
1861 have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} = |
1862 (if z \<in> space M \<and> s' i z \<noteq> 0 then {s' i z} else {})" |
1862 (if z \<in> space M \<and> s' i z \<noteq> 0 then {s' i z} else {})" |
1863 by (auto simp add: s'_def split: split_indicator) |
1863 by (auto simp add: s'_def split: split_indicator) |
2280 assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
2280 assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" |
2281 and nn: "AE x in M. 0 \<le> g x" |
2281 and nn: "AE x in M. 0 \<le> g x" |
2282 shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)" |
2282 shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)" |
2283 unfolding integrable_iff_bounded using nn |
2283 unfolding integrable_iff_bounded using nn |
2284 apply (simp add: nn_integral_density less_top[symmetric]) |
2284 apply (simp add: nn_integral_density less_top[symmetric]) |
2285 apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE) |
2285 apply (intro arg_cong2[where f="(=)"] refl nn_integral_cong_AE) |
2286 apply (auto simp: ennreal_mult) |
2286 apply (auto simp: ennreal_mult) |
2287 done |
2287 done |
2288 |
2288 |
2289 lemma integral_density: |
2289 lemma integral_density: |
2290 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real" |
2290 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real" |