equal
deleted
inserted
replaced
1289 have "\<bar>q 0\<bar> \<le> \<bar>q 0 - q y\<bar> + \<bar>q y\<bar>" by auto |
1289 have "\<bar>q 0\<bar> \<le> \<bar>q 0 - q y\<bar> + \<bar>q y\<bar>" by auto |
1290 also have "... < e + \<bar>q y\<bar>" using d(2) that by force |
1290 also have "... < e + \<bar>q y\<bar>" using d(2) that by force |
1291 finally have "\<bar>q y\<bar> > \<bar>q 0\<bar> - e" by auto |
1291 finally have "\<bar>q y\<bar> > \<bar>q 0\<bar> - e" by auto |
1292 then show ?thesis unfolding e_def by simp |
1292 then show ?thesis unfolding e_def by simp |
1293 qed |
1293 qed |
1294 have "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} \<le> emeasure M ({x \<in> space M. 1 \<le> ennreal(1/e) * \<bar>q(X x)\<bar>} \<inter> space M)" |
1294 have "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} \<le> emeasure M ({x \<in> space M. 1 \<le> ennreal(1/e) * \<bar>q(X x)\<bar>})" |
1295 by (rule emeasure_mono, auto simp add: * \<open>e>0\<close> less_imp_le ennreal_mult''[symmetric]) |
1295 by (rule emeasure_mono, auto simp add: * \<open>e>0\<close> less_imp_le ennreal_mult''[symmetric]) |
1296 also have "... \<le> (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) * indicator (space M) x \<partial>M)" |
1296 also have "... \<le> (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) * indicator (space M) x \<partial>M)" |
1297 by (rule nn_integral_Markov_inequality, auto) |
1297 by (rule nn_integral_Markov_inequality, auto) |
1298 also have "... = (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) \<partial>M)" by auto |
1298 also have "... = (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) \<partial>M)" by auto |
1299 also have "... = (1/e) * ennreal(\<integral>x. \<bar>q(X x)\<bar> \<partial>M)" |
1299 also have "... = (1/e) * ennreal(\<integral>x. \<bar>q(X x)\<bar> \<partial>M)" |
1302 by (simp add: ennreal_mult_less_top) |
1302 by (simp add: ennreal_mult_less_top) |
1303 finally have A: "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} < \<infinity>" by simp |
1303 finally have A: "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} < \<infinity>" by simp |
1304 |
1304 |
1305 have "{x \<in> space M. \<bar>X x\<bar> \<ge> d} = {x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M" |
1305 have "{x \<in> space M. \<bar>X x\<bar> \<ge> d} = {x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M" |
1306 by (auto simp add: \<open>d>0\<close> ennreal_mult''[symmetric]) |
1306 by (auto simp add: \<open>d>0\<close> ennreal_mult''[symmetric]) |
1307 then have "emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d} = emeasure M ({x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M)" |
1307 then have "emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d} = emeasure M ({x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>})" |
1308 by auto |
1308 by auto |
1309 also have "... \<le> (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) * indicator (space M) x \<partial>M)" |
1309 also have "... \<le> (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) * indicator (space M) x \<partial>M)" |
1310 by (rule nn_integral_Markov_inequality, auto) |
1310 by (rule nn_integral_Markov_inequality, auto) |
1311 also have "... = (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) \<partial>M)" by auto |
1311 also have "... = (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) \<partial>M)" by auto |
1312 also have "... = (1/d) * ennreal(\<integral>x. \<bar>X x\<bar> \<partial>M)" |
1312 also have "... = (1/d) * ennreal(\<integral>x. \<bar>X x\<bar> \<partial>M)" |