2858 |
2858 |
2859 lemma simple_function_point_measure[simp]: |
2859 lemma simple_function_point_measure[simp]: |
2860 "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)" |
2860 "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)" |
2861 by (simp add: point_measure_def) |
2861 by (simp add: point_measure_def) |
2862 |
2862 |
2863 declare [[simproc del: finite_Collect]] |
|
2864 lemma emeasure_point_measure: |
2863 lemma emeasure_point_measure: |
2865 assumes A: "finite {a\<in>X. 0 < f a}" "X \<subseteq> A" |
2864 assumes A: "finite {a\<in>X. 0 < f a}" "X \<subseteq> A" |
2866 shows "emeasure (point_measure A f) X = (\<Sum>a|a\<in>X \<and> 0 < f a. f a)" |
2865 shows "emeasure (point_measure A f) X = (\<Sum>a|a\<in>X \<and> 0 < f a. f a)" |
2867 proof - |
2866 proof - |
2868 have "{a. (a \<in> X \<longrightarrow> a \<in> A \<and> 0 < f a) \<and> a \<in> X} = {a\<in>X. 0 < f a}" |
2867 have "{a. (a \<in> X \<longrightarrow> a \<in> A \<and> 0 < f a) \<and> a \<in> X} = {a\<in>X. 0 < f a}" |
2869 using `X \<subseteq> A` by auto |
2868 using `X \<subseteq> A` by auto |
2870 with A show ?thesis |
2869 with A show ?thesis |
2871 by (simp add: emeasure_density positive_integral_count_space ereal_zero_le_0_iff |
2870 by (simp add: emeasure_density positive_integral_count_space ereal_zero_le_0_iff |
2872 point_measure_def indicator_def) |
2871 point_measure_def indicator_def) |
2873 qed |
2872 qed |
2874 declare [[simproc add: finite_Collect]] |
|
2875 |
2873 |
2876 lemma emeasure_point_measure_finite: |
2874 lemma emeasure_point_measure_finite: |
2877 "finite A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)" |
2875 "finite A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)" |
2878 by (subst emeasure_point_measure) (auto dest: finite_subset intro!: setsum_mono_zero_left simp: less_le) |
2876 by (subst emeasure_point_measure) (auto dest: finite_subset intro!: setsum_mono_zero_left simp: less_le) |
2879 |
2877 |