equal
deleted
inserted
replaced
1401 using AE_iff_null[OF sets] u by auto |
1401 using AE_iff_null[OF sets] u by auto |
1402 also have "\<dots> \<longleftrightarrow> (AE x in M. u x \<le> 0)" by (auto split: split_max) |
1402 also have "\<dots> \<longleftrightarrow> (AE x in M. u x \<le> 0)" by (auto split: split_max) |
1403 finally show ?thesis . |
1403 finally show ?thesis . |
1404 qed |
1404 qed |
1405 |
1405 |
|
1406 lemma AE_iff_positive_integral: |
|
1407 "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> integral\<^isup>P M (indicator {x. \<not> P x}) = 0" |
|
1408 by (subst positive_integral_0_iff_AE) |
|
1409 (auto simp: one_ereal_def zero_ereal_def sets_Collect_neg indicator_def[abs_def] measurable_If) |
|
1410 |
1406 lemma positive_integral_const_If: |
1411 lemma positive_integral_const_If: |
1407 "(\<integral>\<^isup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)" |
1412 "(\<integral>\<^isup>+x. a \<partial>M) = (if 0 \<le> a then a * (emeasure M) (space M) else 0)" |
1408 by (auto intro!: positive_integral_0_iff_AE[THEN iffD2]) |
1413 by (auto intro!: positive_integral_0_iff_AE[THEN iffD2]) |
1409 |
1414 |
1410 lemma positive_integral_subalgebra: |
1415 lemma positive_integral_subalgebra: |