equal
deleted
inserted
replaced
1953 then show ?thesis |
1953 then show ?thesis |
1954 unfolding nn_integral_def_finite SUP_def by simp |
1954 unfolding nn_integral_def_finite SUP_def by simp |
1955 qed |
1955 qed |
1956 |
1956 |
1957 lemma nn_integral_count_space_indicator: |
1957 lemma nn_integral_count_space_indicator: |
1958 assumes "NO_MATCH (X::'a set) (UNIV::'a set)" |
1958 assumes "NO_MATCH (UNIV::'a set) (X::'a set)" |
1959 shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)" |
1959 shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)" |
1960 by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space) |
1960 by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space) |
1961 |
1961 |
1962 lemma nn_integral_count_space_eq: |
1962 lemma nn_integral_count_space_eq: |
1963 "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow> |
1963 "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow> |