1102 qed auto |
1102 qed auto |
1103 finally show ?thesis . |
1103 finally show ?thesis . |
1104 qed |
1104 qed |
1105 |
1105 |
1106 lemma measurable_translation: |
1106 lemma measurable_translation: |
1107 "S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. a + x) ` S) \<in> lmeasurable" |
1107 "S \<in> lmeasurable \<Longrightarrow> ((+) a ` S) \<in> lmeasurable" |
1108 unfolding fmeasurable_def |
1108 using emeasure_lebesgue_affine [of 1 a S] |
1109 apply (auto intro: lebesgue_sets_translation) |
1109 apply (auto intro: lebesgue_sets_translation simp add: fmeasurable_def cong: image_cong_simp) |
1110 using emeasure_lebesgue_affine [of 1 a S] |
1110 apply (simp add: ac_simps) |
1111 by (auto simp: add.commute [of _ a]) |
1111 done |
|
1112 |
|
1113 lemma measurable_translation_subtract: |
|
1114 "S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. x - a) ` S) \<in> lmeasurable" |
|
1115 using measurable_translation [of S "- a"] by (simp cong: image_cong_simp) |
1112 |
1116 |
1113 lemma measure_translation: |
1117 lemma measure_translation: |
1114 "measure lebesgue ((\<lambda>x. a + x) ` S) = measure lebesgue S" |
1118 "measure lebesgue ((+) a ` S) = measure lebesgue S" |
1115 using measure_lebesgue_affine [of 1 a S] |
1119 using measure_lebesgue_affine [of 1 a S] by (simp add: ac_simps cong: image_cong_simp) |
1116 by (auto simp: add.commute [of _ a]) |
1120 |
|
1121 lemma measure_translation_subtract: |
|
1122 "measure lebesgue ((\<lambda>x. x - a) ` S) = measure lebesgue S" |
|
1123 using measure_translation [of "- a"] by (simp cong: image_cong_simp) |
|
1124 |
1117 |
1125 |
1118 subsection \<open>A nice lemma for negligibility proofs\<close> |
1126 subsection \<open>A nice lemma for negligibility proofs\<close> |
1119 |
1127 |
1120 lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top" |
1128 lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top" |
1121 by (metis summable_suminf_not_top) |
1129 by (metis summable_suminf_not_top) |