src/HOL/Probability/Lebesgue_Integration.thy
 changeset 56212 3253aaf73a01 parent 56193 c726ecfb22b6 child 56213 e5720d3c18f0
```     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 18 21:02:33 2014 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 18 22:11:46 2014 +0100
1.3 @@ -946,18 +946,18 @@
1.4
1.5    have "integral\<^sup>S M u = (SUP i. integral\<^sup>S M (?uB i))"
1.6      unfolding simple_integral_indicator[OF B `simple_function M u`]
1.7 -  proof (subst SUPR_ereal_setsum, safe)
1.8 +  proof (subst SUP_ereal_setsum, safe)
1.9      fix x n assume "x \<in> space M"
1.10      with u_range show "incseq (\<lambda>i. u x * (emeasure M) (?B' (u x) i))" "\<And>i. 0 \<le> u x * (emeasure M) (?B' (u x) i)"
1.11        using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff)
1.12    next
1.13      show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"
1.14        using measure_conv u_range B_u unfolding simple_integral_def
1.15 -      by (auto intro!: setsum_cong SUPR_ereal_cmult[symmetric])
1.16 +      by (auto intro!: setsum_cong SUP_ereal_cmult [symmetric])
1.17    qed
1.18    moreover
1.19    have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"
1.20 -    apply (subst SUPR_ereal_cmult[symmetric])
1.21 +    apply (subst SUP_ereal_cmult [symmetric])
1.22    proof (safe intro!: SUP_mono bexI)
1.23      fix i
1.24      have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
1.25 @@ -1120,8 +1120,8 @@
1.26            by auto }
1.27        then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
1.28          using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
1.29 -        by (subst SUPR_ereal_cmult[symmetric, OF u(6) `0 \<le> a`])
1.31 +        by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
1.34      then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
1.35        unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2)
1.36 @@ -1132,8 +1132,8 @@
1.37    finally have "(\<integral>\<^sup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^sup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+x. max 0 (g x) \<partial>M)"
1.38      unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
1.39      unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
1.40 -    apply (subst SUPR_ereal_cmult[symmetric, OF pos(1) `0 \<le> a`])
1.41 -    apply (subst SUPR_ereal_add[symmetric, OF inc not_MInf]) .
1.42 +    apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
1.43 +    apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
1.44    then show ?thesis by (simp add: positive_integral_max_0)
1.45  qed
1.46
1.47 @@ -1277,14 +1277,14 @@
1.48    have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x"
1.49      using assms by (auto simp: AE_all_countable)
1.50    have "(\<Sum>i. integral\<^sup>P M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>P M (f i))"
1.51 -    using positive_integral_positive by (rule suminf_ereal_eq_SUPR)
1.52 +    using positive_integral_positive by (rule suminf_ereal_eq_SUP)
1.53    also have "\<dots> = (SUP n. \<integral>\<^sup>+x. (\<Sum>i<n. f i x) \<partial>M)"
1.54      unfolding positive_integral_setsum[OF f] ..
1.55    also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
1.56      by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
1.57         (elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3)
1.58    also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
1.59 -    by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUPR)
1.60 +    by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
1.61    finally show ?thesis by simp
1.62  qed
1.63
1.64 @@ -1297,11 +1297,11 @@
1.65    have pos: "AE x in M. \<forall>i. 0 \<le> u i x" using u by (auto simp: AE_all_countable)
1.66    have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) =
1.67      (SUP n. \<integral>\<^sup>+ x. (INF i:{n..}. u i x) \<partial>M)"
1.68 -    unfolding liminf_SUPR_INFI using pos u
1.69 +    unfolding liminf_SUP_INF using pos u
1.70      by (intro positive_integral_monotone_convergence_SUP_AE)
1.71         (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
1.72    also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
1.73 -    unfolding liminf_SUPR_INFI
1.74 +    unfolding liminf_SUP_INF
1.75      by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
1.76    finally show ?thesis .
1.77  qed
1.78 @@ -2749,7 +2749,7 @@
1.79  next
1.80    case (seq U)
1.81    from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
1.82 -    by eventually_elim (simp add: SUPR_ereal_cmult seq)
1.83 +    by eventually_elim (simp add: SUP_ereal_cmult seq)
1.84    from seq f show ?case