equal
deleted
inserted
replaced
55 let ?B = "\<lambda>i. 2^Suc i * emeasure M (A i)" |
55 let ?B = "\<lambda>i. 2^Suc i * emeasure M (A i)" |
56 have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)" |
56 have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)" |
57 proof |
57 proof |
58 fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)" |
58 fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)" |
59 using measure[of i] emeasure_nonneg[of M "A i"] |
59 using measure[of i] emeasure_nonneg[of M "A i"] |
60 by (auto intro!: ereal_dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff) |
60 by (auto intro!: dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff) |
61 qed |
61 qed |
62 from choice[OF this] obtain n where n: "\<And>i. 0 < n i" |
62 from choice[OF this] obtain n where n: "\<And>i. 0 < n i" |
63 "\<And>i. n i < inverse (2^Suc i * emeasure M (A i))" by auto |
63 "\<And>i. n i < inverse (2^Suc i * emeasure M (A i))" by auto |
64 { fix i have "0 \<le> n i" using n(1)[of i] by auto } note pos = this |
64 { fix i have "0 \<le> n i" using n(1)[of i] by auto } note pos = this |
65 let ?h = "\<lambda>x. \<Sum>i. n i * indicator (A i) x" |
65 let ?h = "\<lambda>x. \<Sum>i. n i * indicator (A i) x" |