equal
deleted
inserted
replaced
1159 assumes "f \<in> borel_measurable M" "0 \<le> c" |
1159 assumes "f \<in> borel_measurable M" "0 \<le> c" |
1160 shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c" |
1160 shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c" |
1161 unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp |
1161 unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp |
1162 |
1162 |
1163 lemma nn_integral_divide: |
1163 lemma nn_integral_divide: |
1164 "0 < c \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+x. f x / c \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M) / c" |
1164 "\<lbrakk> 0 \<le> c; f \<in> borel_measurable M \<rbrakk> \<Longrightarrow> (\<integral>\<^sup>+ x. f x / c \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M) / c" |
1165 unfolding divide_ereal_def |
1165 by(simp add: divide_ereal_def nn_integral_multc inverse_ereal_ge0I) |
1166 apply (rule nn_integral_multc) |
|
1167 apply assumption |
|
1168 apply (cases c) |
|
1169 apply auto |
|
1170 done |
|
1171 |
1166 |
1172 lemma nn_integral_indicator[simp]: |
1167 lemma nn_integral_indicator[simp]: |
1173 "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A" |
1168 "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A" |
1174 by (subst nn_integral_eq_simple_integral) |
1169 by (subst nn_integral_eq_simple_integral) |
1175 (auto simp: simple_integral_indicator) |
1170 (auto simp: simple_integral_indicator) |