equal
deleted
inserted
replaced
388 by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq) |
388 by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq) |
389 have 3: "\<And>u v. set_integrable lborel {u..v} (\<lambda>x. cmod (1 - char M' x))" |
389 have 3: "\<And>u v. set_integrable lborel {u..v} (\<lambda>x. cmod (1 - char M' x))" |
390 by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on |
390 by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on |
391 continuous_intros ballI M'.isCont_char continuous_intros) |
391 continuous_intros ballI M'.isCont_char continuous_intros) |
392 have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)" |
392 have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)" |
393 using integral_norm_bound[OF 2] by simp |
393 using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp |
394 also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4" |
394 also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4" |
395 apply (rule integral_mono [OF 3]) |
395 apply (rule integral_mono [OF 3]) |
396 apply (simp add: emeasure_lborel_Icc_eq) |
396 apply (simp add: emeasure_lborel_Icc_eq) |
397 apply (case_tac "x \<in> {-d/2..d/2}") |
397 apply (case_tac "x \<in> {-d/2..d/2}") |
398 apply auto |
398 apply auto |