equal
deleted
inserted
replaced
1965 |
1965 |
1966 lemma measure_spmf_of_set: |
1966 lemma measure_spmf_of_set: |
1967 "measure (measure_spmf (spmf_of_set S)) A = card (S \<inter> A) / card S" |
1967 "measure (measure_spmf (spmf_of_set S)) A = card (S \<inter> A) / card S" |
1968 by(auto simp add: measure_spmf_spmf_of_set measure_pmf_of_set) |
1968 by(auto simp add: measure_spmf_spmf_of_set measure_pmf_of_set) |
1969 |
1969 |
1970 lemma nn_integral_spmf_of_set: "nn_integral (measure_spmf (spmf_of_set A)) f = setsum f A / card A" |
1970 lemma nn_integral_spmf_of_set: "nn_integral (measure_spmf (spmf_of_set A)) f = sum f A / card A" |
1971 by(cases "finite A")(auto simp add: spmf_of_set_def nn_integral_pmf_of_set card_gt_0_iff simp del: spmf_of_pmf_pmf_of_set) |
1971 by(cases "finite A")(auto simp add: spmf_of_set_def nn_integral_pmf_of_set card_gt_0_iff simp del: spmf_of_pmf_pmf_of_set) |
1972 |
1972 |
1973 lemma integral_spmf_of_set: "integral\<^sup>L (measure_spmf (spmf_of_set A)) f = setsum f A / card A" |
1973 lemma integral_spmf_of_set: "integral\<^sup>L (measure_spmf (spmf_of_set A)) f = sum f A / card A" |
1974 by(clarsimp simp add: spmf_of_set_def integral_pmf_of_set card_gt_0_iff simp del: spmf_of_pmf_pmf_of_set) |
1974 by(clarsimp simp add: spmf_of_set_def integral_pmf_of_set card_gt_0_iff simp del: spmf_of_pmf_pmf_of_set) |
1975 |
1975 |
1976 notepad begin \<comment> \<open>@{const pmf_of_set} is not fully parametric.\<close> |
1976 notepad begin \<comment> \<open>@{const pmf_of_set} is not fully parametric.\<close> |
1977 define R :: "nat \<Rightarrow> nat \<Rightarrow> bool" where "R x y \<longleftrightarrow> (x \<noteq> 0 \<longrightarrow> y = 0)" for x y |
1977 define R :: "nat \<Rightarrow> nat \<Rightarrow> bool" where "R x y \<longleftrightarrow> (x \<noteq> 0 \<longrightarrow> y = 0)" for x y |
1978 define A :: "nat set" where "A = {0, 1}" |
1978 define A :: "nat set" where "A = {0, 1}" |