src/HOL/Probability/Probability_Mass_Function.thy
changeset 64267 b9a1486e79be
parent 64008 17a20ca86d62
child 64634 5bd30359e46e
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -205,13 +205,13 @@
     1.4    using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure pmf_nonneg measure_nonneg)
     1.5  
     1.6  lemma emeasure_measure_pmf_finite: "finite S \<Longrightarrow> emeasure (measure_pmf M) S = (\<Sum>s\<in>S. pmf M s)"
     1.7 -  by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single pmf_nonneg)
     1.8 +  by (subst emeasure_eq_sum_singleton) (auto simp: emeasure_pmf_single pmf_nonneg)
     1.9  
    1.10 -lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S"
    1.11 +lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = sum (pmf M) S"
    1.12    using emeasure_measure_pmf_finite[of S M]
    1.13 -  by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg setsum_nonneg pmf_nonneg)
    1.14 +  by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg sum_nonneg pmf_nonneg)
    1.15  
    1.16 -lemma setsum_pmf_eq_1:
    1.17 +lemma sum_pmf_eq_1:
    1.18    assumes "finite A" "set_pmf p \<subseteq> A"
    1.19    shows   "(\<Sum>x\<in>A. pmf p x) = 1"
    1.20  proof -
    1.21 @@ -575,7 +575,7 @@
    1.22    apply (subst integral_measure_pmf_real[where A="{b}"])
    1.23    apply (auto simp: indicator_eq_0_iff)
    1.24    apply (subst integral_measure_pmf_real[where A="{a}"])
    1.25 -  apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg)
    1.26 +  apply (auto simp: indicator_eq_0_iff sum_nonneg_eq_0_iff pmf_nonneg)
    1.27    done
    1.28  
    1.29  lemma set_pair_pmf[simp]: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
    1.30 @@ -752,7 +752,7 @@
    1.31    unfolding measure_pmf_eq_density
    1.32    apply (simp add: integral_density)
    1.33    apply (subst lebesgue_integral_count_space_finite_support)
    1.34 -  apply (auto intro!: finite_subset[OF _ \<open>finite A\<close>] setsum.mono_neutral_left simp: pmf_eq_0_set_pmf)
    1.35 +  apply (auto intro!: finite_subset[OF _ \<open>finite A\<close>] sum.mono_neutral_left simp: pmf_eq_0_set_pmf)
    1.36    done
    1.37  
    1.38  lemma continuous_on_LINT_pmf: -- \<open>This is dominated convergence!?\<close>
    1.39 @@ -764,7 +764,7 @@
    1.40    assume "finite M" with f show ?thesis
    1.41      using integral_measure_pmf[OF \<open>finite M\<close>]
    1.42      by (subst integral_measure_pmf[OF \<open>finite M\<close>])
    1.43 -       (auto intro!: continuous_on_setsum continuous_on_scaleR continuous_on_const)
    1.44 +       (auto intro!: continuous_on_sum continuous_on_scaleR continuous_on_const)
    1.45  next
    1.46    assume "infinite M"
    1.47    let ?f = "\<lambda>i x. pmf (map_pmf (to_nat_on M) M) i *\<^sub>R f (from_nat_into M i) x"
    1.48 @@ -772,7 +772,7 @@
    1.49    show ?thesis
    1.50    proof (rule uniform_limit_theorem)
    1.51      show "\<forall>\<^sub>F n in sequentially. continuous_on A (\<lambda>a. \<Sum>i<n. ?f i a)"
    1.52 -      by (intro always_eventually allI continuous_on_setsum continuous_on_scaleR continuous_on_const f
    1.53 +      by (intro always_eventually allI continuous_on_sum continuous_on_scaleR continuous_on_const f
    1.54                  from_nat_into set_pmf_not_empty)
    1.55      show "uniform_limit A (\<lambda>n a. \<Sum>i<n. ?f i a) (\<lambda>a. LINT i|M. f i a) sequentially"
    1.56      proof (subst uniform_limit_cong[where g="\<lambda>n a. \<Sum>i<n. ?f i a"])
    1.57 @@ -1677,8 +1677,8 @@
    1.58    show "(\<integral>\<^sup>+ x. ennreal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"
    1.59      using M_not_empty
    1.60      by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size
    1.61 -                  setsum_divide_distrib[symmetric])
    1.62 -       (auto simp: size_multiset_overloaded_eq intro!: setsum.cong)
    1.63 +                  sum_divide_distrib[symmetric])
    1.64 +       (auto simp: size_multiset_overloaded_eq intro!: sum.cong)
    1.65  qed simp
    1.66  
    1.67  lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M"
    1.68 @@ -1712,17 +1712,17 @@
    1.69  lemma emeasure_pmf_of_set_space[simp]: "emeasure pmf_of_set S = 1"
    1.70    by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
    1.71  
    1.72 -lemma nn_integral_pmf_of_set: "nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S"
    1.73 +lemma nn_integral_pmf_of_set: "nn_integral (measure_pmf pmf_of_set) f = sum f S / card S"
    1.74    by (subst nn_integral_measure_pmf_finite)
    1.75 -     (simp_all add: setsum_distrib_right[symmetric] card_gt_0_iff S_not_empty S_finite divide_ennreal_def
    1.76 +     (simp_all add: sum_distrib_right[symmetric] card_gt_0_iff S_not_empty S_finite divide_ennreal_def
    1.77                  divide_ennreal[symmetric] ennreal_of_nat_eq_real_of_nat[symmetric] ennreal_times_divide)
    1.78  
    1.79 -lemma integral_pmf_of_set: "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S"
    1.80 -  by (subst integral_measure_pmf[of S]) (auto simp: S_finite setsum_divide_distrib)
    1.81 +lemma integral_pmf_of_set: "integral\<^sup>L (measure_pmf pmf_of_set) f = sum f S / card S"
    1.82 +  by (subst integral_measure_pmf[of S]) (auto simp: S_finite sum_divide_distrib)
    1.83  
    1.84  lemma emeasure_pmf_of_set: "emeasure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
    1.85    by (subst nn_integral_indicator[symmetric], simp)
    1.86 -     (simp add: S_finite S_not_empty card_gt_0_iff indicator_def setsum.If_cases divide_ennreal
    1.87 +     (simp add: S_finite S_not_empty card_gt_0_iff indicator_def sum.If_cases divide_ennreal
    1.88                  ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set)
    1.89  
    1.90  lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
    1.91 @@ -1752,8 +1752,8 @@
    1.92    with assms have "ennreal ?lhs = ennreal ?rhs"
    1.93      by (subst ennreal_pmf_bind)
    1.94         (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric]
    1.95 -        setsum_nonneg ennreal_of_nat_eq_real_of_nat)
    1.96 -  thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: setsum_nonneg divide_nonneg_nonneg)
    1.97 +        sum_nonneg ennreal_of_nat_eq_real_of_nat)
    1.98 +  thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: sum_nonneg divide_nonneg_nonneg)
    1.99  qed
   1.100  
   1.101  lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
   1.102 @@ -1801,12 +1801,12 @@
   1.103    also from assms
   1.104      have "indicator (\<Union>x\<in>A. f x) x / real \<dots> =
   1.105                indicator (\<Union>x\<in>A. f x) x / (n * real (card A))"
   1.106 -      by (simp add: setsum_divide_distrib [symmetric] mult_ac)
   1.107 +      by (simp add: sum_divide_distrib [symmetric] mult_ac)
   1.108    also from assms have "indicator (\<Union>x\<in>A. f x) x = (\<Sum>y\<in>A. indicator (f y) x)"
   1.109      by (intro indicator_UN_disjoint) simp_all
   1.110    also from assms have "ereal ((\<Sum>y\<in>A. indicator (f y) x) / (real n * real (card A))) =
   1.111                            ereal (pmf ?rhs x)"
   1.112 -    by (subst pmf_bind_pmf_of_set) (simp_all add: setsum_divide_distrib)
   1.113 +    by (subst pmf_bind_pmf_of_set) (simp_all add: sum_divide_distrib)
   1.114    finally show "pmf ?lhs x = pmf ?rhs x" by simp
   1.115  qed
   1.116  
   1.117 @@ -2043,32 +2043,32 @@
   1.118      by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list Int_def)
   1.119    also from assms
   1.120      have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
   1.121 -    by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
   1.122 +    by (subst sum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
   1.123    also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
   1.124        indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
   1.125 -    using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
   1.126 +    using assms by (intro ennreal_cong sum.cong) (auto simp: pmf_pmf_of_list)
   1.127    also have "?S = (\<Sum>x\<in>set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)"
   1.128 -    using assms by (intro setsum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto
   1.129 +    using assms by (intro sum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto
   1.130    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
   1.131 -    using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
   1.132 +    using assms by (intro sum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
   1.133    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
   1.134                        sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
   1.135      using assms by (simp add: pmf_pmf_of_list)
   1.136    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). sum_list (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
   1.137 -    by (intro setsum.cong) (auto simp: indicator_def)
   1.138 +    by (intro sum.cong) (auto simp: indicator_def)
   1.139    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
   1.140                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
   1.141 -    by (intro setsum.cong refl, subst sum_list_map_filter', subst sum_list_setsum_nth) simp
   1.142 +    by (intro sum.cong refl, subst sum_list_map_filter', subst sum_list_sum_nth) simp
   1.143    also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
   1.144                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
   1.145 -    by (rule setsum.commute)
   1.146 +    by (rule sum.commute)
   1.147    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
   1.148                       (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
   1.149 -    by (auto intro!: setsum.cong setsum.neutral)
   1.150 +    by (auto intro!: sum.cong sum.neutral)
   1.151    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
   1.152 -    by (intro setsum.cong refl) (simp_all add: setsum.delta)
   1.153 +    by (intro sum.cong refl) (simp_all add: sum.delta)
   1.154    also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
   1.155 -    by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all
   1.156 +    by (subst sum_list_map_filter', subst sum_list_sum_nth) simp_all
   1.157    finally show ?thesis .
   1.158  qed
   1.159