src/HOL/Probability/Radon_Nikodym.thy
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])