changeset 43923 ab93d0190a5d parent 43920 cedb5cb948fd child 44568 e6f291cb5810
1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Jul 19 14:37:49 2011 +0200
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Jul 19 14:38:29 2011 +0200
1.3 @@ -951,15 +951,15 @@
1.4    proof (rule AE_I')
1.5      { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
1.6          and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
1.7 -      let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
1.8 +      let "?A i" = "Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
1.9        have "(\<Union>i. ?A i) \<in> null_sets"
1.10        proof (rule null_sets_UN)
1.11 -        fix i have "?A i \<in> sets M"
1.12 +        fix i ::nat have "?A i \<in> sets M"
1.13            using borel Q0(1) by auto
1.14 -        have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. of_nat i * indicator (?A i) x \<partial>M)"
1.15 +        have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. (i::ereal) * indicator (?A i) x \<partial>M)"
1.16            unfolding eq[OF `?A i \<in> sets M`]
1.17            by (auto intro!: positive_integral_mono simp: indicator_def)
1.18 -        also have "\<dots> = of_nat i * \<mu> (?A i)"
1.19 +        also have "\<dots> = i * \<mu> (?A i)"
1.20            using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
1.21          also have "\<dots> < \<infinity>"
1.22            using `?A i \<in> sets M`[THEN finite_measure] by auto
1.23 @@ -1067,7 +1067,7 @@
1.24    interpret \<nu>: measure_space ?N
1.25      where "borel_measurable ?N = borel_measurable M" and "measure ?N = \<nu>"
1.26      and "sets ?N = sets M" and "space ?N = space M" using \<nu> by (auto simp: measurable_def)
1.27 -  def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. of_nat (Suc n)}) \<inter> space M"
1.28 +  def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ereal(of_nat (Suc n))}) \<inter> space M"
1.29    { fix i j have "A i \<inter> Q j \<in> sets M"
1.30      unfolding A_def using f Q
1.31      apply (rule_tac Int)
1.32 @@ -1095,7 +1095,7 @@
1.33          case PInf with x show ?thesis unfolding A_def by (auto intro: exI[of _ 0])
1.34        next
1.35          case (real r)
1.36 -        with less_PInf_Ex_of_nat[of "f x"] obtain n where "f x < of_nat n" by (auto simp: real_eq_of_nat)
1.37 +        with less_PInf_Ex_of_nat[of "f x"] obtain n :: nat where "f x < n" by (auto simp: real_eq_of_nat)
1.38          then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"])
1.39        next
1.40          case MInf with x show ?thesis
1.41 @@ -1115,9 +1115,9 @@
1.42      next
1.43        case (Suc n)
1.44        then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
1.45 -        (\<integral>\<^isup>+x. of_nat (Suc n) * indicator (Q j) x \<partial>M)"
1.46 +        (\<integral>\<^isup>+x. (Suc n :: ereal) * indicator (Q j) x \<partial>M)"
1.47          by (auto intro!: positive_integral_mono simp: indicator_def A_def)
1.48 -      also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
1.49 +      also have "\<dots> = Suc n * \<mu> (Q j)"
1.50          using Q by (auto intro!: positive_integral_cmult_indicator)
1.51        also have "\<dots> < \<infinity>"
1.52          using Q by (auto simp: real_eq_of_nat[symmetric])