equal
deleted
inserted
replaced
139 qed |
139 qed |
140 |
140 |
141 lemma subprob_space_null_measure_iff: |
141 lemma subprob_space_null_measure_iff: |
142 "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}" |
142 "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}" |
143 by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty) |
143 by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty) |
|
144 |
|
145 lemma subprob_space_restrict_space: |
|
146 assumes M: "subprob_space M" |
|
147 and A: "A \<inter> space M \<in> sets M" "A \<inter> space M \<noteq> {}" |
|
148 shows "subprob_space (restrict_space M A)" |
|
149 proof(rule subprob_spaceI) |
|
150 have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \<inter> space M)" |
|
151 using A by(simp add: emeasure_restrict_space space_restrict_space) |
|
152 also have "\<dots> \<le> 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M) |
|
153 finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \<le> 1" . |
|
154 next |
|
155 show "space (restrict_space M A) \<noteq> {}" |
|
156 using A by(simp add: space_restrict_space) |
|
157 qed |
144 |
158 |
145 definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where |
159 definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where |
146 "subprob_algebra K = |
160 "subprob_algebra K = |
147 (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)" |
161 (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)" |
148 |
162 |