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