src/HOL/Probability/Lebesgue_Integration.thy
 changeset 39910 10097e0a9dbd parent 39302 d7728f65b353 child 40786 0a54cfc9add3
```     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Oct 01 14:15:49 2010 +0200
1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Oct 01 16:05:25 2010 +0200
1.3 @@ -495,7 +495,7 @@
1.4
1.5  lemma (in measure_space) simple_function_partition:
1.6    assumes "simple_function f" and "simple_function g"
1.7 -  shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. contents (f`A) * \<mu> A)"
1.8 +  shows "simple_integral f = (\<Sum>A\<in>(\<lambda>x. f -` {f x} \<inter> g -` {g x} \<inter> space M) ` space M. the_elem (f`A) * \<mu> A)"
1.9      (is "_ = setsum _ (?p ` space M)")
1.10  proof-
1.11    let "?sub x" = "?p ` (f -` {x} \<inter> space M)"
1.12 @@ -530,18 +530,18 @@
1.13      unfolding simple_integral_def
1.14      by (subst setsum_Sigma[symmetric],
1.15         auto intro!: setsum_cong simp: setsum_right_distrib[symmetric])
1.16 -  also have "\<dots> = (\<Sum>A\<in>?p ` space M. contents (f`A) * \<mu> A)"
1.17 +  also have "\<dots> = (\<Sum>A\<in>?p ` space M. the_elem (f`A) * \<mu> A)"
1.18    proof -
1.19      have [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f ` ?p x = {f x}" by (auto intro!: imageI)
1.20 -    have "(\<lambda>A. (contents (f ` A), A)) ` ?p ` space M
1.21 +    have "(\<lambda>A. (the_elem (f ` A), A)) ` ?p ` space M
1.22        = (\<lambda>x. (f x, ?p x)) ` space M"
1.23      proof safe
1.24        fix x assume "x \<in> space M"
1.25 -      thus "(f x, ?p x) \<in> (\<lambda>A. (contents (f`A), A)) ` ?p ` space M"
1.26 +      thus "(f x, ?p x) \<in> (\<lambda>A. (the_elem (f`A), A)) ` ?p ` space M"
1.27          by (auto intro!: image_eqI[of _ _ "?p x"])
1.28      qed auto
1.29      thus ?thesis
1.30 -      apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (contents (f`A), A)"] inj_onI)
1.31 +      apply (auto intro!: setsum_reindex_cong[of "\<lambda>A. (the_elem (f`A), A)"] inj_onI)
1.32        apply (rule_tac x="xa" in image_eqI)
1.33        by simp_all
1.34    qed
1.35 @@ -602,7 +602,7 @@
1.36    fix x let ?S = "g -` {g x} \<inter> f -` {f x} \<inter> space M"
1.37    assume "x \<in> space M"
1.38    hence "f ` ?S = {f x}" "g ` ?S = {g x}" by auto
1.39 -  thus "contents (f`?S) * \<mu> ?S \<le> contents (g`?S) * \<mu> ?S"
1.40 +  thus "the_elem (f`?S) * \<mu> ?S \<le> the_elem (g`?S) * \<mu> ?S"
1.41      using mono[OF `x \<in> space M`] by (auto intro!: mult_right_mono)
1.42  qed
1.43
```