equal
deleted
inserted
replaced
57 using K J by simp |
57 using K J by simp |
58 also have "\<dots> = (\<integral>\<^sup>+ x. emeasure (Pi\<^sub>M (K - J) M) (?M x) \<partial>Pi\<^sub>M J M)" |
58 also have "\<dots> = (\<integral>\<^sup>+ x. emeasure (Pi\<^sub>M (K - J) M) (?M x) \<partial>Pi\<^sub>M J M)" |
59 using K J by (subst emeasure_fold_integral) auto |
59 using K J by (subst emeasure_fold_integral) auto |
60 also have "\<dots> = (\<integral>\<^sup>+ y. \<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^sub>M I M)) \<partial>Pi\<^sub>M J M)" |
60 also have "\<dots> = (\<integral>\<^sup>+ y. \<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^sub>M I M)) \<partial>Pi\<^sub>M J M)" |
61 (is "_ = (\<integral>\<^sup>+x. \<mu>G (?MZ x) \<partial>Pi\<^sub>M J M)") |
61 (is "_ = (\<integral>\<^sup>+x. \<mu>G (?MZ x) \<partial>Pi\<^sub>M J M)") |
62 proof (intro positive_integral_cong) |
62 proof (intro nn_integral_cong) |
63 fix x assume x: "x \<in> space (Pi\<^sub>M J M)" |
63 fix x assume x: "x \<in> space (Pi\<^sub>M J M)" |
64 with K merge_in_G(2)[OF this] |
64 with K merge_in_G(2)[OF this] |
65 show "emeasure (Pi\<^sub>M (K - J) M) (?M x) = \<mu>G (?MZ x)" |
65 show "emeasure (Pi\<^sub>M (K - J) M) (?M x) = \<mu>G (?MZ x)" |
66 unfolding `Z = emb I K X` merge_in_G(1)[OF x] by (subst mu_G_eq) auto |
66 unfolding `Z = emb I K X` merge_in_G(1)[OF x] by (subst mu_G_eq) auto |
67 qed |
67 qed |
139 proof (intro INF_greatest) |
139 proof (intro INF_greatest) |
140 fix n |
140 fix n |
141 have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto |
141 have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto |
142 also have "\<dots> \<le> (\<integral>\<^sup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^sub>M J' M)" |
142 also have "\<dots> \<le> (\<integral>\<^sup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^sub>M J' M)" |
143 unfolding fold(2)[OF J' `Z n \<in> ?G`] |
143 unfolding fold(2)[OF J' `Z n \<in> ?G`] |
144 proof (intro positive_integral_mono) |
144 proof (intro nn_integral_mono) |
145 fix x assume x: "x \<in> space (Pi\<^sub>M J' M)" |
145 fix x assume x: "x \<in> space (Pi\<^sub>M J' M)" |
146 then have "?q n x \<le> 1 + 0" |
146 then have "?q n x \<le> 1 + 0" |
147 using J' Z fold(3) Z_sets by auto |
147 using J' Z fold(3) Z_sets by auto |
148 also have "\<dots> \<le> 1 + ?a / 2^(k+1)" |
148 also have "\<dots> \<le> 1 + ?a / 2^(k+1)" |
149 using `0 < ?a` by (intro add_mono) auto |
149 using `0 < ?a` by (intro add_mono) auto |
151 with x show "?q n x \<le> indicator (?Q n) x + ?a / 2^(k+1)" |
151 with x show "?q n x \<le> indicator (?Q n) x + ?a / 2^(k+1)" |
152 by (auto split: split_indicator simp del: power_Suc) |
152 by (auto split: split_indicator simp del: power_Suc) |
153 qed |
153 qed |
154 also have "\<dots> = emeasure (Pi\<^sub>M J' M) (?Q n) + ?a / 2^(k+1)" |
154 also have "\<dots> = emeasure (Pi\<^sub>M J' M) (?Q n) + ?a / 2^(k+1)" |
155 using `0 \<le> ?a` Q_sets J'.emeasure_space_1 |
155 using `0 \<le> ?a` Q_sets J'.emeasure_space_1 |
156 by (subst positive_integral_add) auto |
156 by (subst nn_integral_add) auto |
157 finally show "?a / 2^(k+1) \<le> emeasure (Pi\<^sub>M J' M) (?Q n)" using `?a \<le> 1` |
157 finally show "?a / 2^(k+1) \<le> emeasure (Pi\<^sub>M J' M) (?Q n)" using `?a \<le> 1` |
158 by (cases rule: ereal2_cases[of ?a "emeasure (Pi\<^sub>M J' M) (?Q n)"]) |
158 by (cases rule: ereal2_cases[of ?a "emeasure (Pi\<^sub>M J' M) (?Q n)"]) |
159 (auto simp: field_simps) |
159 (auto simp: field_simps) |
160 qed |
160 qed |
161 also have "\<dots> = emeasure (Pi\<^sub>M J' M) (\<Inter>n. ?Q n)" |
161 also have "\<dots> = emeasure (Pi\<^sub>M J' M) (\<Inter>n. ?Q n)" |