272 using subs generator.additive_increasing[OF positive_mu_G additive_mu_G] |
272 using subs generator.additive_increasing[OF positive_mu_G additive_mu_G] |
273 unfolding increasing_def by auto |
273 unfolding increasing_def by auto |
274 also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using \<open>Z _ \<in> generator\<close> \<open>Z' _ \<in> generator\<close> |
274 also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using \<open>Z _ \<in> generator\<close> \<open>Z' _ \<in> generator\<close> |
275 by (intro generator.subadditive[OF positive_mu_G additive_mu_G]) auto |
275 by (intro generator.subadditive[OF positive_mu_G additive_mu_G]) auto |
276 also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. 2 powr -real i * ?a)" |
276 also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. 2 powr -real i * ?a)" |
277 proof (rule setsum_mono) |
277 proof (rule sum_mono) |
278 fix i assume "i \<in> {1..n}" hence "i \<le> n" by simp |
278 fix i assume "i \<in> {1..n}" hence "i \<le> n" by simp |
279 have "\<mu>G (Z i - Z' i) = \<mu>G (prod_emb I (\<lambda>_. borel) (J i) (B i - K i))" |
279 have "\<mu>G (Z i - Z' i) = \<mu>G (prod_emb I (\<lambda>_. borel) (J i) (B i - K i))" |
280 unfolding Z'_def Z_def by simp |
280 unfolding Z'_def Z_def by simp |
281 also have "\<dots> = P (J i) (B i - K i)" |
281 also have "\<dots> = P (J i) (B i - K i)" |
282 using J K_sets by (subst mu_G_spec) auto |
282 using J K_sets by (subst mu_G_spec) auto |
288 compact_imp_closed[OF \<open>compact (K' _)\<close>] space_PiM PiE_def) |
288 compact_imp_closed[OF \<open>compact (K' _)\<close>] space_PiM PiE_def) |
289 also have "\<dots> \<le> ennreal (2 powr - real i) * ?a" using K'(1)[of i] . |
289 also have "\<dots> \<le> ennreal (2 powr - real i) * ?a" using K'(1)[of i] . |
290 finally show "\<mu>G (Z i - Z' i) \<le> (2 powr - real i) * ?a" . |
290 finally show "\<mu>G (Z i - Z' i) \<le> (2 powr - real i) * ?a" . |
291 qed |
291 qed |
292 also have "\<dots> = ennreal ((\<Sum> i\<in>{1..n}. (2 powr -enn2real i)) * enn2real ?a)" |
292 also have "\<dots> = ennreal ((\<Sum> i\<in>{1..n}. (2 powr -enn2real i)) * enn2real ?a)" |
293 using r by (simp add: setsum_distrib_right ennreal_mult[symmetric]) |
293 using r by (simp add: sum_distrib_right ennreal_mult[symmetric]) |
294 also have "\<dots> < ennreal (1 * enn2real ?a)" |
294 also have "\<dots> < ennreal (1 * enn2real ?a)" |
295 proof (intro ennreal_lessI mult_strict_right_mono) |
295 proof (intro ennreal_lessI mult_strict_right_mono) |
296 have "(\<Sum>i = 1..n. 2 powr - real i) = (\<Sum>i = 1..<Suc n. (1/2) ^ i)" |
296 have "(\<Sum>i = 1..n. 2 powr - real i) = (\<Sum>i = 1..<Suc n. (1/2) ^ i)" |
297 by (rule setsum.cong) (auto simp: powr_realpow powr_divide power_divide powr_minus_divide) |
297 by (rule sum.cong) (auto simp: powr_realpow powr_divide power_divide powr_minus_divide) |
298 also have "{1..<Suc n} = {..<Suc n} - {0}" by auto |
298 also have "{1..<Suc n} = {..<Suc n} - {0}" by auto |
299 also have "setsum (op ^ (1 / 2::real)) ({..<Suc n} - {0}) = |
299 also have "sum (op ^ (1 / 2::real)) ({..<Suc n} - {0}) = |
300 setsum (op ^ (1 / 2)) ({..<Suc n}) - 1" by (auto simp: setsum_diff1) |
300 sum (op ^ (1 / 2)) ({..<Suc n}) - 1" by (auto simp: sum_diff1) |
301 also have "\<dots> < 1" by (subst geometric_sum) auto |
301 also have "\<dots> < 1" by (subst geometric_sum) auto |
302 finally show "(\<Sum>i = 1..n. 2 powr - enn2real i) < 1" by simp |
302 finally show "(\<Sum>i = 1..n. 2 powr - enn2real i) < 1" by simp |
303 qed (auto simp: r enn2real_positive_iff) |
303 qed (auto simp: r enn2real_positive_iff) |
304 also have "\<dots> = ?a" by (auto simp: r) |
304 also have "\<dots> = ?a" by (auto simp: r) |
305 also have "\<dots> \<le> \<mu>G (Z n)" |
305 also have "\<dots> \<le> \<mu>G (Z n)" |