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.30 -           (auto intro!: SUPR_ereal_add
    1.31 +        by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
    1.32 +           (auto intro!: SUP_ereal_add
    1.33                   simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) }
    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
    1.85      apply (simp add: positive_integral_monotone_convergence_SUP)
    1.86      apply (subst positive_integral_cong_AE[OF eq])