src/HOL/Probability/Infinite_Product_Measure.thy
changeset 43920 cedb5cb948fd
parent 43679 052eaf7509cf
child 44928 7ef6505bde7f
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Jul 19 14:35:44 2011 +0200
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Jul 19 14:36:12 2011 +0200
     1.3 @@ -563,7 +563,7 @@
     1.4              using `0 \<le> ?a` Q_sets J'.measure_space_1
     1.5              by (subst J'.positive_integral_add) auto
     1.6            finally show "?a / 2^(k+1) \<le> measure (Pi\<^isub>M J' M) (?Q n)" using `?a \<le> 1`
     1.7 -            by (cases rule: extreal2_cases[of ?a "measure (Pi\<^isub>M J' M) (?Q n)"])
     1.8 +            by (cases rule: ereal2_cases[of ?a "measure (Pi\<^isub>M J' M) (?Q n)"])
     1.9                 (auto simp: field_simps)
    1.10          qed
    1.11          also have "\<dots> = measure (Pi\<^isub>M J' M) (\<Inter>n. ?Q n)"
    1.12 @@ -712,7 +712,7 @@
    1.13        with `(\<Inter>i. A i) = {}` show False by auto
    1.14      qed
    1.15      ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
    1.16 -      using LIMSEQ_extreal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp
    1.17 +      using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp
    1.18    qed
    1.19  qed
    1.20  
    1.21 @@ -812,7 +812,7 @@
    1.22    using assms
    1.23    unfolding \<mu>'_def M.\<mu>'_def
    1.24    by (subst measure_times[OF assms])
    1.25 -     (auto simp: finite_measure_eq M.finite_measure_eq setprod_extreal)
    1.26 +     (auto simp: finite_measure_eq M.finite_measure_eq setprod_ereal)
    1.27  
    1.28  lemma (in product_prob_space) finite_measure_infprod_emb_Pi:
    1.29    assumes J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> X j \<in> sets (M j)"