equal
deleted
inserted
replaced
42 emeasure M (\<Union>i. A i) - emeasure N (\<Union>i. A i) " |
42 emeasure M (\<Union>i. A i) - emeasure N (\<Union>i. A i) " |
43 by (simp add: suminf) |
43 by (simp add: suminf) |
44 qed |
44 qed |
45 qed fact |
45 qed fact |
46 |
46 |
47 text {*An equivalent characterization of sigma-finite spaces is the existence of integrable |
47 text \<open>An equivalent characterization of sigma-finite spaces is the existence of integrable |
48 positive functions (or, still equivalently, the existence of a probability measure which is in |
48 positive functions (or, still equivalently, the existence of a probability measure which is in |
49 the same measure class as the original measure).*} |
49 the same measure class as the original measure).\<close> |
50 |
50 |
51 lemma (in sigma_finite_measure) obtain_positive_integrable_function: |
51 lemma (in sigma_finite_measure) obtain_positive_integrable_function: |
52 obtains f::"'a \<Rightarrow> real" where |
52 obtains f::"'a \<Rightarrow> real" where |
53 "f \<in> borel_measurable M" |
53 "f \<in> borel_measurable M" |
54 "\<And>x. f x > 0" |
54 "\<And>x. f x > 0" |
67 apply (rule suminf_le) using * power_half_series summable_def by (auto simp add: indicator_def divide_simps) |
67 apply (rule suminf_le) using * power_half_series summable_def by (auto simp add: indicator_def divide_simps) |
68 then have g_le_1: "g x \<le> 1" for x using power_half_series sums_unique by fastforce |
68 then have g_le_1: "g x \<le> 1" for x using power_half_series sums_unique by fastforce |
69 |
69 |
70 have g_pos: "g x > 0" if "x \<in> space M" for x |
70 have g_pos: "g x > 0" if "x \<in> space M" for x |
71 unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto) |
71 unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto) |
72 obtain i where "x \<in> A i" using `(\<Union>i. A i) = space M` `x \<in> space M` by auto |
72 obtain i where "x \<in> A i" using \<open>(\<Union>i. A i) = space M\<close> \<open>x \<in> space M\<close> by auto |
73 then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))" |
73 then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))" |
74 unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"] |
74 unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"] |
75 by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power) |
75 by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power) |
76 then show "\<exists>i. 0 < (1 / 2) ^ i * indicator (A i) x / (2 + 2 * Sigma_Algebra.measure M (A i))" |
76 then show "\<exists>i. 0 < (1 / 2) ^ i * indicator (A i) x / (2 + 2 * Sigma_Algebra.measure M (A i))" |
77 by auto |
77 by auto |
79 |
79 |
80 have "integrable M g" |
80 have "integrable M g" |
81 unfolding g_def proof (rule integrable_suminf) |
81 unfolding g_def proof (rule integrable_suminf) |
82 fix n |
82 fix n |
83 show "integrable M (\<lambda>x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))" |
83 show "integrable M (\<lambda>x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))" |
84 using `emeasure M (A n) \<noteq> \<infinity>` |
84 using \<open>emeasure M (A n) \<noteq> \<infinity>\<close> |
85 by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum) |
85 by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum) |
86 next |
86 next |
87 show "AE x in M. summable (\<lambda>n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))" |
87 show "AE x in M. summable (\<lambda>n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))" |
88 using * by auto |
88 using * by auto |
89 show "summable (\<lambda>n. (\<integral>x. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))) \<partial>M))" |
89 show "summable (\<lambda>n. (\<integral>x. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))) \<partial>M))" |
95 define f where "f = (\<lambda>x. if x \<in> space M then g x else 1)" |
95 define f where "f = (\<lambda>x. if x \<in> space M then g x else 1)" |
96 have "f x > 0" for x unfolding f_def using g_pos by auto |
96 have "f x > 0" for x unfolding f_def using g_pos by auto |
97 moreover have "f x \<le> 1" for x unfolding f_def using g_le_1 by auto |
97 moreover have "f x \<le> 1" for x unfolding f_def using g_le_1 by auto |
98 moreover have [measurable]: "f \<in> borel_measurable M" unfolding f_def by auto |
98 moreover have [measurable]: "f \<in> borel_measurable M" unfolding f_def by auto |
99 moreover have "integrable M f" |
99 moreover have "integrable M f" |
100 apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using `integrable M g` by auto |
100 apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using \<open>integrable M g\<close> by auto |
101 ultimately show "(\<And>f. f \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 < f x) \<Longrightarrow> (\<And>x. f x \<le> 1) \<Longrightarrow> integrable M f \<Longrightarrow> thesis) \<Longrightarrow> thesis" |
101 ultimately show "(\<And>f. f \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 < f x) \<Longrightarrow> (\<And>x. f x \<le> 1) \<Longrightarrow> integrable M f \<Longrightarrow> thesis) \<Longrightarrow> thesis" |
102 by (meson that) |
102 by (meson that) |
103 qed |
103 qed |
104 |
104 |
105 lemma (in sigma_finite_measure) Ex_finite_integrable_function: |
105 lemma (in sigma_finite_measure) Ex_finite_integrable_function: |
312 with f_less_N pos_A have "0 < b" "b \<noteq> top" |
312 with f_less_N pos_A have "0 < b" "b \<noteq> top" |
313 by (auto intro!: diff_gr0_ennreal simp: zero_less_iff_neq_zero diff_eq_0_iff_ennreal ennreal_divide_eq_top_iff) |
313 by (auto intro!: diff_gr0_ennreal simp: zero_less_iff_neq_zero diff_eq_0_iff_ennreal ennreal_divide_eq_top_iff) |
314 |
314 |
315 let ?f = "\<lambda>x. f x + b" |
315 let ?f = "\<lambda>x. f x + b" |
316 have "nn_integral M f \<noteq> top" |
316 have "nn_integral M f \<noteq> top" |
317 using `f \<in> G`[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong) |
317 using \<open>f \<in> G\<close>[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong) |
318 with \<open>b \<noteq> top\<close> interpret Mf: finite_measure "density M ?f" |
318 with \<open>b \<noteq> top\<close> interpret Mf: finite_measure "density M ?f" |
319 by (intro finite_measureI) |
319 by (intro finite_measureI) |
320 (auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff |
320 (auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff |
321 emeasure_density nn_integral_cmult_indicator nn_integral_add |
321 emeasure_density nn_integral_cmult_indicator nn_integral_add |
322 cong: nn_integral_cong) |
322 cong: nn_integral_cong) |