equal
deleted
inserted
replaced
854 using bnd by (auto intro!: mult_mono simp: from_nat_into set_pmf_not_empty) |
854 using bnd by (auto intro!: mult_mono simp: from_nat_into set_pmf_not_empty) |
855 next |
855 next |
856 have "integrable (map_pmf (to_nat_on M) M) (\<lambda>n. B)" |
856 have "integrable (map_pmf (to_nat_on M) M) (\<lambda>n. B)" |
857 by auto |
857 by auto |
858 then show "summable (\<lambda>n. pmf (map_pmf (to_nat_on (set_pmf M)) M) n * B)" |
858 then show "summable (\<lambda>n. pmf (map_pmf (to_nat_on (set_pmf M)) M) n * B)" |
859 by (simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_rabs_cancel) |
859 by (fastforce simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_mult2) |
860 qed |
860 qed |
861 qed simp |
861 qed simp |
862 qed simp |
862 qed simp |
863 qed |
863 qed |
864 |
864 |