*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Pmf and measure*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 15 Oct 2019 10:10:02 +0200*Autocrypt*: addr=eberlm at in.tum.de; keydata= mQINBFnXYyYBEADCLx1xTJEx34IA2n1uH2xGOXNlYA5MRecNLArLyF1bOx5Gjex1ilmZJzj2 mhonPfwpP98QsQDL4N4Nbi+MFpBJGrDATN56GPBQh8a4ttndlp0+srOeNA4kLSE48gp4YdTX zUCXeutse3eHBRtBSqelCoU9VwFc0QmAyiHnnwVy4AgZwiMCbrSvgBSvx/gcyZhYYuOVekTg JN1aZCGpedpTwhH2f7XH8X1Bw4AhjexHPSRZYI+E7eek+QFJTdXndXApHWGQajswrFZQ5W5p q3zS2XAOSMZdquAu0XC7CZzJHV8xzoWQC9XLdV7DltOmASWrLMi2FUrNr/O/uPV08ZIzZxZX 9T+WynujrWwEZPwkcNFM1EUyxIMqaOvJNA5r1Is89SL4rArk8M3MzpF4xqVguAYFxSHyCpZ5 Ijjn1XrYgR/VCqTAhDNXSeOlomd6fFxdDmIo35g/GZZs7giQGi7XocnZegnleeHyJwZdPkie 7zz5cjvFuwrSTvEHybfMIA4pyC2XnVFpCS4y5sCOSemHNEbXQYwJqG1pIj+tH0ncF/O2e9x6 ygW4dKp43aY7E+CMHzQBEuZZo4JLDMmnoGuPPWrjFZA6EmJNIvHUf4uzzdiFJVEuRNqh82R6 HvDvxQkjhuRQvC8cP31pRbf51M8j5W77f0WZ/rFnkIx9hh53EQARAQABtB9NYW51ZWwgRWJl cmwgPGViZXJsbUBpbi50dW0uZGU+iQJUBBMBCAA+FiEEN1tratkE0f8X2q+Y59G0ZJvnKoQF AlnXY18CGwMFCQlmAYAFCwkIBwIGFQgJCgsCBBYCAwECHgECF4AACgkQ59G0ZJvnKoTDEA/+ KY5vnLMwy/WhMaV3r3sl8+L2r75zmIVvatyevVEnfLYunghOO6AurT9S5egwNqOGjuW2FXju NVukQ2/sFqjodUNBdkeMjCSgBG0puGEdTkf9JA2dWAs5cCzQRyFVzwYx9SuHO+gdpxliV/ba 6tHQewoV0BZNtgvu4dlLAaOQw5JPip38tEa0FdMCwpaoPtOTdhwCcDOTDf0sLivi5Eo7zTjP 8edhJoxa0UuWAMWTaPE8UlXSJqN/ufFS5MP1n1eCuSJOkM3ELewjmKddm4/TycxUtvrd4aHp jqJfbm5gh0Xj3l6K7clykqtvrnv5PSydaZvi/THwvlcqlRSekKfBlRYbZUykzZ8xryjNToh/ tbCv19vPlLDm1K2hPfljrMfr5PZj35Ca7v1o2WYQRlYFSIbmY5amUyptsUi1934clybq8lhg lwQCIO4w0gpcMEKyq1hZK4PNvpnac9IcW2G48vjoMCyEJpTrJLO23eEVYGqRBpJGl94b2H6A eWek1Z/3znr+ph0S4tddcfe1Tz5qCOeD5UI0BCMHYw+6uM4Q6NMVwXz1+czcgMJUzbT0FYti EqXMOnh/DC5C1evV1lcyHuI/jEOfpOMfgjKwN/bTQkmzXf3d/Cyf2h4+K4JKZUjT4Wteac+o 3tHLX/2MamTXcqsaU2vrMz+Q6OlDEwY4GXO5Ag0EWddjJgEQANO9foaUMRzjVeniynCTLul/ gDztIR3G9d0aYM4sQ2Sv1hV3xcV+EWyrEPmOjhOYfCEtzW4MBhAKvKFHGMyTz1fIFYvEeBFH AflFnpD5r69B38nv/TkDx2hcrY7ZJ98/2YkE2l5pz8aAU4B2NSgLwpr2eISpAMDZ+Y7Y+G1d n6g5tdlZTdPBSBXVIam1axbKJdRLlAdL4yZNRAqiVaC6kfwkB0O3+4Zhh6NbL8vEkKQB/tOv 6QkJZLBO7kNGtoJP5dc4UnlbSgu5Gq3csbbJsdFFdJETqSDgVrO/2gVxulQjmA6UCzYoXBcn fOioSJQ+4Zu76kBFPRotQ5goAA7JjtHWoLdZ7hTorBy4M5o02OqA9VayZsmiA060oINaS+Kp UQZEUq7i/G+Al5FNqcG8Gq5GBZSAuORYP2KGaAJcrv0tVDbF3BBEdtkPQeLBxb2mVqn8rLQI NDZUdzKr6S19qj2knJFA0dY/jceFSHG4EV8Fr0oEoAfD9opyaduGAJDmO/Zq4xOOJPvIYalB aekPxMbWNmrDmeuK7HQ1IqOx65EoNoOzqqYHnae21NyMSV+h3Wsqq7DJAWiDFqx/ebHpRS25 SyD5Pe89iaC9Cr9X2h3gK2dfgd3UpOTUjRJE1A82c1jEZCvSNDouFY6fiUgFycBrxKa5XzrC nWF7c8soh+YJABEBAAGJAjwEGAEIACYWIQQ3W2tq2QTR/xfar5jn0bRkm+cqhAUCWddjJgIb DAUJCWYBgAAKCRDn0bRkm+cqhIJFEACpRkf/NC+OeYyXmWUja0fVDKoTOmXcBVNdeptnz2Rr QrDZy8Di+DfWmz8VqEkI6PomAWjO3xDU/5yCs7A+gQrt8ioTPJbUCSQNRJGmFSEiLJ0/l9Sq iqjQsUjZbTNYAt2F/RDj7eQYh6c1smXpkbIyCQUfkOtafW9QFCnq06EPuuLOZeh35cphZ7W0 AcCrel2KLvX7PDNQxPmLuP/y2E787YySA/2f7dDjEgvrpNS9WOnWUekFSc3oWtN/dnmn0kXw AK6TYV1C9jUdGVQmjI8JcK4NUEJhVHV4N205EWivBU74L5QMXHHsA3YukYQTYXQOUWlP4x7G Jr4whSKeVh3xZpl2EvF/9Rp9rbwhqTxcBe/oAOeWR98puguCcKQkgANETArKLd3+e1KLeimT OMtgEA4srbuqBh7BtTcbdz4bbjIfKyYFxH/I9ZKpaO6J8DJxNJYQKZfpfs86tv9znfpYWJcB HeSN3ilKW0CBcboQ3Zcs0qycWYLHgMH7DNB49DTCfSMMKGLFmvarAtjkaX5NZraY32PgPvlT ZFTM2SHd14WlC8lwDQgEsYvcItKWped2+XRYfgxGX9SDWwAKr4q/yUAmBaXQyPf519IEcmNe qtIOXZlrjgSw1Kgk1JRlbFkMnlJ5EEkEdBsXP1RCQ8hkwYBzdZURPSeRM+CU2IKREg==*In-reply-to*: <CAGn19Sw=1nbj5a=1Ttha5GXVxnjo3R2RCEHika+x2V6s2hO8Mw@mail.gmail.com>*References*: <CAGn19Sw=1nbj5a=1Ttha5GXVxnjo3R2RCEHika+x2V6s2hO8Mw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.1.0

On 15/10/2019 05:40, Kawin Worrasangasilpa wrote: > 2) Following (1), are there any n-ary to combine n independent pmf's? Andreas already answered most things, but for an n-ary independent product of PMFs, the best way (in most cases) is to use the Pi_pmf that (I think) I sent you last year. I really should put this into the distribution at some point; I'm not sure why I haven't done that already. I probably forgot. Manuel

(* File: Pi_pmf.thy Authors: Manuel Eberl, Max W. Haslbeck *) section \<open>Indexed products of PMFs\<close> theory Pi_pmf imports "HOL-Probability.Probability" begin subsection \<open>Preliminaries\<close> lemma pmf_expectation_eq_infsetsum: "measure_pmf.expectation p f = infsetsum (\<lambda>x. pmf p x * f x) UNIV" unfolding infsetsum_def measure_pmf_eq_density by (subst integral_density) simp_all lemma measure_pmf_prob_product: assumes "countable A" "countable B" shows "measure_pmf.prob (pair_pmf M N) (A \<times> B) = measure_pmf.prob M A * measure_pmf.prob N B" proof - have "measure_pmf.prob (pair_pmf M N) (A \<times> B) = (\<Sum>\<^sub>a(a, b)\<in>A \<times> B. pmf M a * pmf N b)" by (auto intro!: infsetsum_cong simp add: measure_pmf_conv_infsetsum pmf_pair) also have "\<dots> = measure_pmf.prob M A * measure_pmf.prob N B" using assms by (subst infsetsum_product) (auto simp add: measure_pmf_conv_infsetsum) finally show ?thesis by simp qed subsection \<open>Definition\<close> text \<open> In analogy to @{const PiM}, we define an indexed product of PMFs. In the literature, this is typically called taking a vector of independent random variables. Note that the components do not have to be identically distributed. The operation takes an explicit index set \<^term>\<open>A :: 'a set\<close> and a function \<^term>\<open>f :: 'a \<Rightarrow> 'b pmf\<close> that maps each element from \<^term>\<open>A\<close> to a PMF and defines the product measure $\bigotimes_{i\in A} f(i)$ , which is represented as a \<^typ>\<open>('a \<Rightarrow> 'b) pmf\<close>. Note that unlike @{const PiM}, this only works for \<^emph>\<open>finite\<close> index sets. It could be extended to countable sets and beyond, but the construction becomes somewhat more involved. \<close> definition Pi_pmf :: "'a set \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b pmf) \<Rightarrow> ('a \<Rightarrow> 'b) pmf" where "Pi_pmf A dflt p = embed_pmf (\<lambda>f. if (\<forall>x. x \<notin> A \<longrightarrow> f x = dflt) then \<Prod>x\<in>A. pmf (p x) (f x) else 0)" text \<open> A technical subtlety that needs to be addressed is this: Intuitively, the functions in the support of a product distribution have domain \<open>A\<close>. However, since HOL is a total logic, these functions must still return \<^emph>\<open>some\<close> value for inputs outside \<open>A\<close>. The product measure @{const PiM} simply lets these functions return @{const undefined} in these cases. We chose a different solution here, which is to supply a default value \<^term>\<open>dflt :: 'b\<close> that is returned in these cases. As one possible application, one could model the result of \<open>n\<close> different independent coin tosses as @{term "Pi_pmf {0..<n} False (\<lambda>_. bernoulli_pmf (1 / 2))"}. This returns a function of type \<^typ>\<open>nat \<Rightarrow> bool\<close> that maps every natural number below \<open>n\<close> to the result of the corresponding coin toss, and every other natural number to \<^term>\<open>False\<close>. \<close> lemma pmf_Pi: assumes A: "finite A" shows "pmf (Pi_pmf A dflt p) f = (if (\<forall>x. x \<notin> A \<longrightarrow> f x = dflt) then \<Prod>x\<in>A. pmf (p x) (f x) else 0)" unfolding Pi_pmf_def proof (rule pmf_embed_pmf, goal_cases) case 2 define S where "S = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = dflt}" define B where "B = (\<lambda>x. set_pmf (p x))" have neutral_left: "(\<Prod>xa\<in>A. pmf (p xa) (f xa)) = 0" if "f \<in> PiE A B - (\<lambda>f. restrict f A) ` S" for f proof - have "restrict (\<lambda>x. if x \<in> A then f x else dflt) A \<in> (\<lambda>f. restrict f A) ` S" by (intro imageI) (auto simp: S_def) also have "restrict (\<lambda>x. if x \<in> A then f x else dflt) A = f" using that by (auto simp: PiE_def Pi_def extensional_def fun_eq_iff) finally show ?thesis using that by blast qed have neutral_right: "(\<Prod>xa\<in>A. pmf (p xa) (f xa)) = 0" if "f \<in> (\<lambda>f. restrict f A) ` S - PiE A B" for f proof - from that obtain f' where f': "f = restrict f' A" "f' \<in> S" by auto moreover from this and that have "restrict f' A \<notin> PiE A B" by simp then obtain x where "x \<in> A" "pmf (p x) (f' x) = 0" by (auto simp: B_def set_pmf_eq) with f' and A show ?thesis by auto qed have "(\<lambda>f. \<Prod>x\<in>A. pmf (p x) (f x)) abs_summable_on PiE A B" by (intro abs_summable_on_prod_PiE A) (auto simp: B_def) also have "?this \<longleftrightarrow> (\<lambda>f. \<Prod>x\<in>A. pmf (p x) (f x)) abs_summable_on (\<lambda>f. restrict f A) ` S" by (intro abs_summable_on_cong_neutral neutral_left neutral_right) auto also have "\<dots> \<longleftrightarrow> (\<lambda>f. \<Prod>x\<in>A. pmf (p x) (restrict f A x)) abs_summable_on S" by (rule abs_summable_on_reindex_iff [symmetric]) (force simp: inj_on_def fun_eq_iff S_def) also have "\<dots> \<longleftrightarrow> (\<lambda>f. if \<forall>x. x \<notin> A \<longrightarrow> f x = dflt then \<Prod>x\<in>A. pmf (p x) (f x) else 0) abs_summable_on UNIV" by (intro abs_summable_on_cong_neutral) (auto simp: S_def) finally have summable: \<dots> . have "1 = (\<Prod>x\<in>A. 1::real)" by simp also have "(\<Prod>x\<in>A. 1) = (\<Prod>x\<in>A. \<Sum>\<^sub>ay\<in>B x. pmf (p x) y)" unfolding B_def by (subst infsetsum_pmf_eq_1) auto also have "(\<Prod>x\<in>A. \<Sum>\<^sub>ay\<in>B x. pmf (p x) y) = (\<Sum>\<^sub>af\<in>Pi\<^sub>E A B. \<Prod>x\<in>A. pmf (p x) (f x))" by (intro infsetsum_prod_PiE [symmetric] A) (auto simp: B_def) also have "\<dots> = (\<Sum>\<^sub>af\<in>(\<lambda>f. restrict f A) ` S. \<Prod>x\<in>A. pmf (p x) (f x))" using A by (intro infsetsum_cong_neutral neutral_left neutral_right refl) also have "\<dots> = (\<Sum>\<^sub>af\<in>S. \<Prod>x\<in>A. pmf (p x) (restrict f A x))" by (rule infsetsum_reindex) (force simp: inj_on_def fun_eq_iff S_def) also have "\<dots> = (\<Sum>\<^sub>af\<in>S. \<Prod>x\<in>A. pmf (p x) (f x))" by (intro infsetsum_cong) (auto simp: S_def) also have "\<dots> = (\<Sum>\<^sub>af. if \<forall>x. x \<notin> A \<longrightarrow> f x = dflt then \<Prod>x\<in>A. pmf (p x) (f x) else 0)" by (intro infsetsum_cong_neutral) (auto simp: S_def) also have "ennreal \<dots> = (\<integral>\<^sup>+f. ennreal (if \<forall>x. x \<notin> A \<longrightarrow> f x = dflt then \<Prod>x\<in>A. pmf (p x) (f x) else 0) \<partial>count_space UNIV)" by (intro nn_integral_conv_infsetsum [symmetric] summable) (auto simp: prod_nonneg) finally show ?case by simp qed (auto simp: prod_nonneg) lemma pmf_Pi': assumes "finite A" "\<And>x. x \<notin> A \<Longrightarrow> f x = dflt" shows "pmf (Pi_pmf A dflt p) f = (\<Prod>x\<in>A. pmf (p x) (f x))" using assms by (subst pmf_Pi) auto lemma pmf_Pi_outside: assumes "finite A" "\<exists>x. x \<notin> A \<and> f x \<noteq> dflt" shows "pmf (Pi_pmf A dflt p) f = 0" using assms by (subst pmf_Pi) auto lemma pmf_Pi_empty [simp]: "Pi_pmf {} dflt p = return_pmf (\<lambda>_. dflt)" by (intro pmf_eqI, subst pmf_Pi) (auto simp: indicator_def) lemma set_Pi_pmf_subset: "finite A \<Longrightarrow> set_pmf (Pi_pmf A dflt p) \<subseteq> {f. \<forall>x. x \<notin> A \<longrightarrow> f x = dflt}" by (auto simp: set_pmf_eq pmf_Pi) lemma Pi_pmf_cong [cong]: assumes "A = A'" "dflt = dflt'" "\<And>x. x \<in> A \<Longrightarrow> f x = f' x" shows "Pi_pmf A dflt f = Pi_pmf A' dflt' f'" proof - have "(\<lambda>g. \<Prod>x\<in>A. pmf (f x) (g x)) = (\<lambda>g. \<Prod>x\<in>A. pmf (f' x) (g x))" by (intro ext prod.cong) (auto simp: assms) with assms show ?thesis by (simp add: Pi_pmf_def cong: if_cong) qed subsection \<open>Dependent product sets with a default\<close> text \<open> The following describes a dependent product of sets where the functions are required to return the default value \<^term>\<open>dflt\<close> outside their domain, in analogy to @{const PiE}, which uses @{const undefined}. \<close> definition PiE_dflt where "PiE_dflt A dflt B = {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B x) \<and> (x \<notin> A \<longrightarrow> f x = dflt)}" lemma restrict_PiE_dflt: "(\<lambda>h. restrict h A) ` PiE_dflt A dflt B = PiE A B" proof (intro equalityI subsetI) fix h assume "h \<in> (\<lambda>h. restrict h A) ` PiE_dflt A dflt B" thus "h \<in> PiE A B" by (auto simp: PiE_dflt_def) next fix h assume h: "h \<in> PiE A B" hence "restrict (\<lambda>x. if x \<in> A then h x else dflt) A \<in> (\<lambda>h. restrict h A) ` PiE_dflt A dflt B" by (intro imageI) (auto simp: PiE_def extensional_def PiE_dflt_def) also have "restrict (\<lambda>x. if x \<in> A then h x else dflt) A = h" using h by (auto simp: fun_eq_iff) finally show "h \<in> (\<lambda>h. restrict h A) ` PiE_dflt A dflt B" . qed lemma dflt_image_PiE: "(\<lambda>h x. if x \<in> A then h x else dflt) ` PiE A B = PiE_dflt A dflt B" (is "?f ` ?X = ?Y") proof (intro equalityI subsetI) fix h assume "h \<in> ?f ` ?X" thus "h \<in> ?Y" by (auto simp: PiE_dflt_def PiE_def) next fix h assume h: "h \<in> ?Y" hence "?f (restrict h A) \<in> ?f ` ?X" by (intro imageI) (auto simp: PiE_def extensional_def PiE_dflt_def) also have "?f (restrict h A) = h" using h by (auto simp: fun_eq_iff PiE_dflt_def) finally show "h \<in> ?f ` ?X" . qed lemma finite_PiE_dflt [intro]: assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (B x)" shows "finite (PiE_dflt A d B)" proof - have "PiE_dflt A d B = (\<lambda>f x. if x \<in> A then f x else d) ` PiE A B" by (rule dflt_image_PiE [symmetric]) also have "finite \<dots>" by (intro finite_imageI finite_PiE assms) finally show ?thesis . qed lemma card_PiE_dflt: assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (B x)" shows "card (PiE_dflt A d B) = (\<Prod>x\<in>A. card (B x))" proof - from assms have "(\<Prod>x\<in>A. card (B x)) = card (PiE A B)" by (intro card_PiE [symmetric]) auto also have "PiE A B = (\<lambda>f. restrict f A) ` PiE_dflt A d B" by (rule restrict_PiE_dflt [symmetric]) also have "card \<dots> = card (PiE_dflt A d B)" by (intro card_image) (force simp: inj_on_def restrict_def fun_eq_iff PiE_dflt_def) finally show ?thesis .. qed lemma PiE_dflt_empty_iff [simp]: "PiE_dflt A dflt B = {} \<longleftrightarrow> (\<exists>x\<in>A. B x = {})" by (simp add: dflt_image_PiE [symmetric] PiE_eq_empty_iff) text \<open> The probability of an independent combination of events is precisely the product of the probabilities of each individual event. \<close> lemma measure_Pi_pmf_PiE_dflt: assumes [simp]: "finite A" shows "measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B) = (\<Prod>x\<in>A. measure_pmf.prob (p x) (B x))" proof - define B' where "B' = (\<lambda>x. B x \<inter> set_pmf (p x))" have "measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B) = (\<Sum>\<^sub>ah\<in>PiE_dflt A dflt B. pmf (Pi_pmf A dflt p) h)" by (rule measure_pmf_conv_infsetsum) also have "\<dots> = (\<Sum>\<^sub>ah\<in>PiE_dflt A dflt B. \<Prod>x\<in>A. pmf (p x) (h x))" by (intro infsetsum_cong, subst pmf_Pi') (auto simp: PiE_dflt_def) also have "\<dots> = (\<Sum>\<^sub>ah\<in>(\<lambda>h. restrict h A) ` PiE_dflt A dflt B. \<Prod>x\<in>A. pmf (p x) (h x))" by (subst infsetsum_reindex) (force simp: inj_on_def PiE_dflt_def fun_eq_iff)+ also have "(\<lambda>h. restrict h A) ` PiE_dflt A dflt B = PiE A B" by (rule restrict_PiE_dflt) also have "(\<Sum>\<^sub>ah\<in>PiE A B. \<Prod>x\<in>A. pmf (p x) (h x)) = (\<Sum>\<^sub>ah\<in>PiE A B'. \<Prod>x\<in>A. pmf (p x) (h x))" by (intro infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq) also have "(\<Sum>\<^sub>ah\<in>PiE A B'. \<Prod>x\<in>A. pmf (p x) (h x)) = (\<Prod>x\<in>A. infsetsum (pmf (p x)) (B' x))" by (intro infsetsum_prod_PiE) (auto simp: B'_def) also have "\<dots> = (\<Prod>x\<in>A. infsetsum (pmf (p x)) (B x))" by (intro prod.cong infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq) also have "\<dots> = (\<Prod>x\<in>A. measure_pmf.prob (p x) (B x))" by (subst measure_pmf_conv_infsetsum) (rule refl) finally show ?thesis . qed lemma set_Pi_pmf_subset': assumes "finite A" shows "set_pmf (Pi_pmf A dflt p) \<subseteq> PiE_dflt A dflt (set_pmf \<circ> p)" using assms by (auto simp: set_pmf_eq pmf_Pi PiE_dflt_def) lemma Pi_pmf_return_pmf [simp]: assumes "finite A" shows "Pi_pmf A dflt (\<lambda>x. return_pmf (f x)) = return_pmf (\<lambda>x. if x \<in> A then f x else dflt)" proof - have "set_pmf (Pi_pmf A dflt (\<lambda>x. return_pmf (f x))) \<subseteq> PiE_dflt A dflt (set_pmf \<circ> (\<lambda>x. return_pmf (f x)))" by (intro set_Pi_pmf_subset' assms) also have "\<dots> \<subseteq> {\<lambda>x. if x \<in> A then f x else dflt}" by (auto simp: PiE_dflt_def) finally show ?thesis by (simp add: set_pmf_subset_singleton) qed lemma Pi_pmf_return_pmf' [simp]: assumes "finite A" shows "Pi_pmf A dflt (\<lambda>_. return_pmf dflt) = return_pmf (\<lambda>_. dflt)" using assms by simp lemma measure_Pi_pmf_Pi: fixes t::nat assumes [simp]: "finite A" shows "measure_pmf.prob (Pi_pmf A dflt p) (Pi A B) = (\<Prod>x\<in>A. measure_pmf.prob (p x) (B x))" (is "?lhs = ?rhs") proof - have "?lhs = measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B)" by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def PiE_def intro!: pmf_Pi_outside)+ also have "\<dots> = ?rhs" using assms by (simp add: measure_Pi_pmf_PiE_dflt) finally show ?thesis by simp qed subsection \<open>Common PMF operations on products\<close> text \<open> @{const Pi_pmf} distributes over the `bind' operation in the Giry monad: \<close> lemma Pi_pmf_bind: assumes "finite A" shows "Pi_pmf A d (\<lambda>x. bind_pmf (p x) (q x)) = do {f \<leftarrow> Pi_pmf A d' p; Pi_pmf A d (\<lambda>x. q x (f x))}" (is "?lhs = ?rhs") proof (rule pmf_eqI, goal_cases) case (1 f) show ?case proof (cases "\<exists>x\<in>-A. f x \<noteq> d") case False define B where "B = (\<lambda>x. set_pmf (p x))" have [simp]: "countable (B x)" for x by (auto simp: B_def) { fix x :: 'a have "(\<lambda>a. pmf (p x) a * 1) abs_summable_on B x" by (simp add: pmf_abs_summable) moreover have "norm (pmf (p x) a * 1) \<ge> norm (pmf (p x) a * pmf (q x a) (f x))" for a unfolding norm_mult by (intro mult_left_mono) (auto simp: pmf_le_1) ultimately have "(\<lambda>a. pmf (p x) a * pmf (q x a) (f x)) abs_summable_on B x" by (rule abs_summable_on_comparison_test) } note summable = this have "pmf ?rhs f = (\<Sum>\<^sub>ag. pmf (Pi_pmf A d' p) g * (\<Prod>x\<in>A. pmf (q x (g x)) (f x)))" by (subst pmf_bind, subst pmf_Pi') (insert assms False, simp_all add: pmf_expectation_eq_infsetsum) also have "\<dots> = (\<Sum>\<^sub>ag\<in>PiE_dflt A d' B. pmf (Pi_pmf A d' p) g * (\<Prod>x\<in>A. pmf (q x (g x)) (f x)))" unfolding B_def using assms by (intro infsetsum_cong_neutral) (auto simp: pmf_Pi PiE_dflt_def set_pmf_eq) also have "\<dots> = (\<Sum>\<^sub>ag\<in>PiE_dflt A d' B. (\<Prod>x\<in>A. pmf (p x) (g x) * pmf (q x (g x)) (f x)))" using assms by (intro infsetsum_cong) (auto simp: pmf_Pi PiE_dflt_def prod.distrib) also have "\<dots> = (\<Sum>\<^sub>ag\<in>(\<lambda>g. restrict g A) ` PiE_dflt A d' B. (\<Prod>x\<in>A. pmf (p x) (g x) * pmf (q x (g x)) (f x)))" by (subst infsetsum_reindex) (force simp: PiE_dflt_def inj_on_def fun_eq_iff)+ also have "(\<lambda>g. restrict g A) ` PiE_dflt A d' B = PiE A B" by (rule restrict_PiE_dflt) also have "(\<Sum>\<^sub>ag\<in>\<dots>. (\<Prod>x\<in>A. pmf (p x) (g x) * pmf (q x (g x)) (f x))) = (\<Prod>x\<in>A. \<Sum>\<^sub>aa\<in>B x. pmf (p x) a * pmf (q x a) (f x))" using assms summable by (subst infsetsum_prod_PiE) simp_all also have "\<dots> = (\<Prod>x\<in>A. \<Sum>\<^sub>aa. pmf (p x) a * pmf (q x a) (f x))" by (intro prod.cong infsetsum_cong_neutral) (auto simp: B_def set_pmf_eq) also have "\<dots> = pmf ?lhs f" using False assms by (subst pmf_Pi') (simp_all add: pmf_bind pmf_expectation_eq_infsetsum) finally show ?thesis .. next case True have "pmf ?rhs f = measure_pmf.expectation (Pi_pmf A d' p) (\<lambda>x. pmf (Pi_pmf A d (\<lambda>xa. q xa (x xa))) f)" using assms by (simp add: pmf_bind) also have "\<dots> = measure_pmf.expectation (Pi_pmf A d' p) (\<lambda>x. 0)" using assms True by (intro Bochner_Integration.integral_cong pmf_Pi_outside) auto also have "\<dots> = pmf ?lhs f" using assms True by (subst pmf_Pi_outside) auto finally show ?thesis .. qed qed text \<open> Analogously any componentwise mapping can be pulled outside the product: \<close> lemma Pi_pmf_map: assumes [simp]: "finite A" and "f dflt = dflt'" shows "Pi_pmf A dflt' (\<lambda>x. map_pmf f (g x)) = map_pmf (\<lambda>h. f \<circ> h) (Pi_pmf A dflt g)" proof - have "Pi_pmf A dflt' (\<lambda>x. map_pmf f (g x)) = Pi_pmf A dflt' (\<lambda>x. g x \<bind> (\<lambda>x. return_pmf (f x)))" using assms by (simp add: map_pmf_def Pi_pmf_bind) also have "\<dots> = Pi_pmf A dflt g \<bind> (\<lambda>h. return_pmf (\<lambda>x. if x \<in> A then f (h x) else dflt'))" by (subst Pi_pmf_bind[where d' = dflt]) auto also have "\<dots> = map_pmf (\<lambda>h. f \<circ> h) (Pi_pmf A dflt g)" unfolding map_pmf_def using set_Pi_pmf_subset'[of A dflt g] by (intro bind_pmf_cong refl arg_cong[of _ _ return_pmf]) (auto dest: simp: fun_eq_iff PiE_dflt_def assms(2)) finally show ?thesis . qed text \<open> We can exchange the default value in a product of PMFs like this: \<close> lemma Pi_pmf_default_swap: assumes "finite A" shows "map_pmf (\<lambda>f x. if x \<in> A then f x else dflt') (Pi_pmf A dflt p) = Pi_pmf A dflt' p" (is "?lhs = ?rhs") proof (rule pmf_eqI, goal_cases) case (1 f) let ?B = "(\<lambda>f x. if x \<in> A then f x else dflt') -` {f} \<inter> PiE_dflt A dflt (\<lambda>_. UNIV)" show ?case proof (cases "\<exists>x\<in>-A. f x \<noteq> dflt'") case False let ?f' = "\<lambda>x. if x \<in> A then f x else dflt" from False have "pmf ?lhs f = measure_pmf.prob (Pi_pmf A dflt p) ?B" using assms unfolding pmf_map by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) also from False have "?B = {?f'}" by (auto simp: fun_eq_iff PiE_dflt_def) also have "measure_pmf.prob (Pi_pmf A dflt p) {?f'} = pmf (Pi_pmf A dflt p) ?f'" by (simp add: measure_pmf_single) also have "\<dots> = pmf ?rhs f" using False assms by (subst (1 2) pmf_Pi) auto finally show ?thesis . next case True have "pmf ?lhs f = measure_pmf.prob (Pi_pmf A dflt p) ?B" using assms unfolding pmf_map by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) also from True have "?B = {}" by auto also have "measure_pmf.prob (Pi_pmf A dflt p) \<dots> = 0" by simp also have "0 = pmf ?rhs f" using True assms by (intro pmf_Pi_outside [symmetric]) auto finally show ?thesis . qed qed text \<open> The following rule allows reindexing the product: \<close> lemma Pi_pmf_bij_betw: assumes "finite A" "bij_betw h A B" "\<And>x. x \<notin> A \<Longrightarrow> h x \<notin> B" shows "Pi_pmf A dflt (\<lambda>_. f) = map_pmf (\<lambda>g. g \<circ> h) (Pi_pmf B dflt (\<lambda>_. f))" (is "?lhs = ?rhs") proof - have B: "finite B" using assms bij_betw_finite by auto have "pmf ?lhs g = pmf ?rhs g" for g proof (cases "\<forall>a. a \<notin> A \<longrightarrow> g a = dflt") case True define h' where "h' = the_inv_into A h" have h': "h' (h x) = x" if "x \<in> A" for x unfolding h'_def using that assms by (auto simp add: bij_betw_def the_inv_into_f_f) have h: "h (h' x) = x" if "x \<in> B" for x unfolding h'_def using that assms f_the_inv_into_f_bij_betw by fastforce have "pmf ?rhs g = measure_pmf.prob (Pi_pmf B dflt (\<lambda>_. f)) ((\<lambda>g. g \<circ> h) -` {g})" unfolding pmf_map by simp also have "\<dots> = measure_pmf.prob (Pi_pmf B dflt (\<lambda>_. f)) (((\<lambda>g. g \<circ> h) -` {g}) \<inter> PiE_dflt B dflt (\<lambda>_. UNIV))" using B by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) also have "\<dots> = pmf (Pi_pmf B dflt (\<lambda>_. f)) (\<lambda>x. if x \<in> B then g (h' x) else dflt)" proof - have "(if h x \<in> B then g (h' (h x)) else dflt) = g x" for x using h' assms True by (cases "x \<in> A") (auto simp add: bij_betwE) then have "(\<lambda>g. g \<circ> h) -` {g} \<inter> PiE_dflt B dflt (\<lambda>_. UNIV) = {(\<lambda>x. if x \<in> B then g (h' x) else dflt)}" using assms h' h True unfolding PiE_dflt_def by auto then show ?thesis by (simp add: measure_pmf_single) qed also have "\<dots> = pmf (Pi_pmf A dflt (\<lambda>_. f)) g" using B assms True h'_def by (auto simp add: pmf_Pi intro!: prod.reindex_bij_betw bij_betw_the_inv_into) finally show ?thesis by simp next case False have "pmf ?rhs g = infsetsum (pmf (Pi_pmf B dflt (\<lambda>_. f))) ((\<lambda>g. g \<circ> h) -` {g})" using assms by (auto simp add: measure_pmf_conv_infsetsum pmf_map) also have "\<dots> = infsetsum (\<lambda>_. 0) ((\<lambda>g x. g (h x)) -` {g})" using B False assms by (intro infsetsum_cong pmf_Pi_outside) fastforce+ also have "\<dots> = 0" by simp finally show ?thesis using assms False by (auto simp add: pmf_Pi pmf_map) qed then show ?thesis by (rule pmf_eqI) qed text \<open> A product of uniform random choices is again a uniform distribution. \<close> lemma Pi_pmf_of_set: assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (B x)" "\<And>x. x \<in> A \<Longrightarrow> B x \<noteq> {}" shows "Pi_pmf A d (\<lambda>x. pmf_of_set (B x)) = pmf_of_set (PiE_dflt A d B)" (is "?lhs = ?rhs") proof (rule pmf_eqI, goal_cases) case (1 f) show ?case proof (cases "\<exists>x. x \<notin> A \<and> f x \<noteq> d") case True hence "pmf ?lhs f = 0" using assms by (intro pmf_Pi_outside) (auto simp: PiE_dflt_def) also from True have "f \<notin> PiE_dflt A d B" by (auto simp: PiE_dflt_def) hence "0 = pmf ?rhs f" using assms by (subst pmf_of_set) auto finally show ?thesis . next case False hence "pmf ?lhs f = (\<Prod>x\<in>A. pmf (pmf_of_set (B x)) (f x))" using assms by (subst pmf_Pi') auto also have "\<dots> = (\<Prod>x\<in>A. indicator (B x) (f x) / real (card (B x)))" by (intro prod.cong refl, subst pmf_of_set) (use assms False in auto) also have "\<dots> = (\<Prod>x\<in>A. indicator (B x) (f x)) / real (\<Prod>x\<in>A. card (B x))" by (subst prod_dividef) simp_all also have "(\<Prod>x\<in>A. indicator (B x) (f x) :: real) = indicator (PiE_dflt A d B) f" using assms False by (auto simp: indicator_def PiE_dflt_def) also have "(\<Prod>x\<in>A. card (B x)) = card (PiE_dflt A d B)" using assms by (intro card_PiE_dflt [symmetric]) auto also have "indicator (PiE_dflt A d B) f / \<dots> = pmf ?rhs f" using assms by (intro pmf_of_set [symmetric]) auto finally show ?thesis . qed qed subsection \<open>Merging and splitting PMF products\<close> text \<open> The following lemma shows that we can add a single PMF to a product: \<close> lemma Pi_pmf_insert: assumes "finite A" "x \<notin> A" shows "Pi_pmf (insert x A) dflt p = map_pmf (\<lambda>(y,f). f(x:=y)) (pair_pmf (p x) (Pi_pmf A dflt p))" proof (intro pmf_eqI) fix f let ?M = "pair_pmf (p x) (Pi_pmf A dflt p)" have "pmf (map_pmf (\<lambda>(y, f). f(x := y)) ?M) f = measure_pmf.prob ?M ((\<lambda>(y, f). f(x := y)) -` {f})" by (subst pmf_map) auto also have "((\<lambda>(y, f). f(x := y)) -` {f}) = (\<Union>y'. {(f x, f(x := y'))})" by (auto simp: fun_upd_def fun_eq_iff) also have "measure_pmf.prob ?M \<dots> = measure_pmf.prob ?M {(f x, f(x := dflt))}" using assms by (intro measure_prob_cong_0) (auto simp: pmf_pair pmf_Pi split: if_splits) also have "\<dots> = pmf (p x) (f x) * pmf (Pi_pmf A dflt p) (f(x := dflt))" by (simp add: measure_pmf_single pmf_pair pmf_Pi) also have "\<dots> = pmf (Pi_pmf (insert x A) dflt p) f" proof (cases "\<forall>y. y \<notin> insert x A \<longrightarrow> f y = dflt") case True with assms have "pmf (p x) (f x) * pmf (Pi_pmf A dflt p) (f(x := dflt)) = pmf (p x) (f x) * (\<Prod>xa\<in>A. pmf (p xa) ((f(x := dflt)) xa))" by (subst pmf_Pi') auto also have "(\<Prod>xa\<in>A. pmf (p xa) ((f(x := dflt)) xa)) = (\<Prod>xa\<in>A. pmf (p xa) (f xa))" using assms by (intro prod.cong) auto also have "pmf (p x) (f x) * \<dots> = pmf (Pi_pmf (insert x A) dflt p) f" using assms True by (subst pmf_Pi') auto finally show ?thesis . qed (insert assms, auto simp: pmf_Pi) finally show "\<dots> = pmf (map_pmf (\<lambda>(y, f). f(x := y)) ?M) f" .. qed lemma Pi_pmf_insert': assumes "finite A" "x \<notin> A" shows "Pi_pmf (insert x A) dflt p = do {y \<leftarrow> p x; f \<leftarrow> Pi_pmf A dflt p; return_pmf (f(x := y))}" using assms by (subst Pi_pmf_insert) (auto simp add: map_pmf_def pair_pmf_def case_prod_beta' bind_return_pmf bind_assoc_pmf) lemma Pi_pmf_singleton: "Pi_pmf {x} dflt p = map_pmf (\<lambda>a b. if b = x then a else dflt) (p x)" proof - have "Pi_pmf {x} dflt p = map_pmf (fun_upd (\<lambda>_. dflt) x) (p x)" by (subst Pi_pmf_insert) (simp_all add: pair_return_pmf2 pmf.map_comp o_def) also have "fun_upd (\<lambda>_. dflt) x = (\<lambda>z y. if y = x then z else dflt)" by (simp add: fun_upd_def fun_eq_iff) finally show ?thesis . qed text \<open> Projecting a product of PMFs onto a component yields the expected result: \<close> lemma Pi_pmf_component: assumes "finite A" shows "map_pmf (\<lambda>f. f x) (Pi_pmf A dflt p) = (if x \<in> A then p x else return_pmf dflt)" proof (cases "x \<in> A") case True define A' where "A' = A - {x}" from assms and True have A': "A = insert x A'" by (auto simp: A'_def) from assms have "map_pmf (\<lambda>f. f x) (Pi_pmf A dflt p) = p x" unfolding A' by (subst Pi_pmf_insert) (auto simp: A'_def pmf.map_comp o_def case_prod_unfold map_fst_pair_pmf) with True show ?thesis by simp next case False have "map_pmf (\<lambda>f. f x) (Pi_pmf A dflt p) = map_pmf (\<lambda>_. dflt) (Pi_pmf A dflt p)" using assms False set_Pi_pmf_subset[of A dflt p] by (intro pmf.map_cong refl) (auto simp: set_pmf_eq pmf_Pi_outside) with False show ?thesis by simp qed text \<open> We can take merge two PMF products on disjoint sets like this: \<close> lemma Pi_pmf_union: assumes "finite A" "finite B" "A \<inter> B = {}" shows "Pi_pmf (A \<union> B) dflt p = map_pmf (\<lambda>(f,g) x. if x \<in> A then f x else g x) (pair_pmf (Pi_pmf A dflt p) (Pi_pmf B dflt p))" (is "_ = map_pmf (?h A) (?q A)") using assms(1,3) proof (induction rule: finite_induct) case (insert x A) have "map_pmf (?h (insert x A)) (?q (insert x A)) = do {v \<leftarrow> p x; (f, g) \<leftarrow> pair_pmf (Pi_pmf A dflt p) (Pi_pmf B dflt p); return_pmf (\<lambda>y. if y \<in> insert x A then (f(x := v)) y else g y)}" by (subst Pi_pmf_insert) (insert insert.hyps insert.prems, simp_all add: pair_pmf_def map_bind_pmf bind_map_pmf bind_assoc_pmf bind_return_pmf) also have "\<dots> = do {v \<leftarrow> p x; (f, g) \<leftarrow> ?q A; return_pmf ((?h A (f,g))(x := v))}" by (intro bind_pmf_cong refl) (auto simp: fun_eq_iff) also have "\<dots> = do {v \<leftarrow> p x; f \<leftarrow> map_pmf (?h A) (?q A); return_pmf (f(x := v))}" by (simp add: bind_map_pmf map_bind_pmf case_prod_unfold cong: if_cong) also have "\<dots> = do {v \<leftarrow> p x; f \<leftarrow> Pi_pmf (A \<union> B) dflt p; return_pmf (f(x := v))}" using insert.hyps and insert.prems by (intro bind_pmf_cong insert.IH [symmetric] refl) auto also have "\<dots> = Pi_pmf (insert x (A \<union> B)) dflt p" by (subst Pi_pmf_insert) (insert assms insert.hyps insert.prems, auto simp: pair_pmf_def map_bind_pmf) also have "insert x (A \<union> B) = insert x A \<union> B" by simp finally show ?case .. qed (simp_all add: case_prod_unfold map_snd_pair_pmf) text \<open> We can also project a product to a subset of the indices by mapping all the other indices to the default value: \<close> lemma Pi_pmf_subset: assumes "finite A" "A' \<subseteq> A" shows "Pi_pmf A' dflt p = map_pmf (\<lambda>f x. if x \<in> A' then f x else dflt) (Pi_pmf A dflt p)" proof - let ?P = "pair_pmf (Pi_pmf A' dflt p) (Pi_pmf (A - A') dflt p)" from assms have [simp]: "finite A'" by (blast dest: finite_subset) from assms have "A = A' \<union> (A - A')" by blast also have "Pi_pmf \<dots> dflt p = map_pmf (\<lambda>(f,g) x. if x \<in> A' then f x else g x) ?P" using assms by (intro Pi_pmf_union) auto also have "map_pmf (\<lambda>f x. if x \<in> A' then f x else dflt) \<dots> = map_pmf fst ?P" unfolding map_pmf_comp o_def case_prod_unfold using set_Pi_pmf_subset[of A' dflt p] by (intro map_pmf_cong refl) (auto simp: fun_eq_iff) also have "\<dots> = Pi_pmf A' dflt p" by (simp add: map_fst_pair_pmf) finally show ?thesis .. qed lemma Pi_pmf_subset': fixes f :: "'a \<Rightarrow> 'b pmf" assumes "finite A" "B \<subseteq> A" "\<And>x. x \<in> A - B \<Longrightarrow> f x = return_pmf dflt" shows "Pi_pmf A dflt f = Pi_pmf B dflt f" proof - have "Pi_pmf (B \<union> (A - B)) dflt f = map_pmf (\<lambda>(f, g) x. if x \<in> B then f x else g x) (pair_pmf (Pi_pmf B dflt f) (Pi_pmf (A - B) dflt f))" using assms by (intro Pi_pmf_union) (auto dest: finite_subset) also have "Pi_pmf (A - B) dflt f = Pi_pmf (A - B) dflt (\<lambda>_. return_pmf dflt)" using assms by (intro Pi_pmf_cong) auto also have "\<dots> = return_pmf (\<lambda>_. dflt)" using assms by simp also have "map_pmf (\<lambda>(f, g) x. if x \<in> B then f x else g x) (pair_pmf (Pi_pmf B dflt f) (return_pmf (\<lambda>_. dflt))) = map_pmf (\<lambda>f x. if x \<in> B then f x else dflt) (Pi_pmf B dflt f)" by (simp add: map_pmf_def pair_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') also have "\<dots> = Pi_pmf B dflt f" using assms by (intro Pi_pmf_default_swap) (auto dest: finite_subset) also have "B \<union> (A - B) = A" using assms by auto finally show ?thesis . qed lemma Pi_pmf_if_set: assumes "finite A" shows "Pi_pmf A dflt (\<lambda>x. if b x then f x else return_pmf dflt) = Pi_pmf {x\<in>A. b x} dflt f" proof - have "Pi_pmf A dflt (\<lambda>x. if b x then f x else return_pmf dflt) = Pi_pmf {x\<in>A. b x} dflt (\<lambda>x. if b x then f x else return_pmf dflt)" using assms by (intro Pi_pmf_subset') auto also have "\<dots> = Pi_pmf {x\<in>A. b x} dflt f" by (intro Pi_pmf_cong) auto finally show ?thesis . qed lemma Pi_pmf_if_set': assumes "finite A" shows "Pi_pmf A dflt (\<lambda>x. if b x then return_pmf dflt else f x) = Pi_pmf {x\<in>A. \<not>b x} dflt f" proof - have "Pi_pmf A dflt (\<lambda>x. if b x then return_pmf dflt else f x) = Pi_pmf {x\<in>A. \<not>b x} dflt (\<lambda>x. if b x then return_pmf dflt else f x)" using assms by (intro Pi_pmf_subset') auto also have "\<dots> = Pi_pmf {x\<in>A. \<not>b x} dflt f" by (intro Pi_pmf_cong) auto finally show ?thesis . qed text \<open> Lastly, we can delete a single component from a product: \<close> lemma Pi_pmf_remove: assumes "finite A" shows "Pi_pmf (A - {x}) dflt p = map_pmf (\<lambda>f. f(x := dflt)) (Pi_pmf A dflt p)" proof - have "Pi_pmf (A - {x}) dflt p = map_pmf (\<lambda>f xa. if xa \<in> A - {x} then f xa else dflt) (Pi_pmf A dflt p)" using assms by (intro Pi_pmf_subset) auto also have "\<dots> = map_pmf (\<lambda>f. f(x := dflt)) (Pi_pmf A dflt p)" using set_Pi_pmf_subset[of A dflt p] assms by (intro map_pmf_cong refl) (auto simp: fun_eq_iff) finally show ?thesis . qed subsection \<open>Applications\<close> text \<open> Choosing a subset of a set uniformly at random is equivalent to tossing a fair coin independently for each element and collecting all the elements that came up heads. \<close> lemma pmf_of_set_Pow_conv_bernoulli: assumes "finite (A :: 'a set)" shows "map_pmf (\<lambda>b. {x\<in>A. b x}) (Pi_pmf A P (\<lambda>_. bernoulli_pmf (1/2))) = pmf_of_set (Pow A)" proof - have "Pi_pmf A P (\<lambda>_. bernoulli_pmf (1/2)) = pmf_of_set (PiE_dflt A P (\<lambda>x. UNIV))" using assms by (simp add: bernoulli_pmf_half_conv_pmf_of_set Pi_pmf_of_set) also have "map_pmf (\<lambda>b. {x\<in>A. b x}) \<dots> = pmf_of_set (Pow A)" proof - have "bij_betw (\<lambda>b. {x \<in> A. b x}) (PiE_dflt A P (\<lambda>_. UNIV)) (Pow A)" by (rule bij_betwI[of _ _ _ "\<lambda>B b. if b \<in> A then b \<in> B else P"]) (auto simp add: PiE_dflt_def) then show ?thesis using assms by (intro map_pmf_of_set_bij_betw) auto qed finally show ?thesis by simp qed text \<open> A binomial distribution can be seen as the number of successes in \<open>n\<close> independent coin tosses. \<close> lemma binomial_pmf_altdef': fixes A :: "'a set" assumes "finite A" and "card A = n" and p: "p \<in> {0..1}" shows "binomial_pmf n p = map_pmf (\<lambda>f. card {x\<in>A. f x}) (Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p))" (is "?lhs = ?rhs") proof - from assms have "?lhs = binomial_pmf (card A) p" by simp also have "\<dots> = ?rhs" using assms(1) proof (induction rule: finite_induct) case empty with p show ?case by (simp add: binomial_pmf_0) next case (insert x A) from insert.hyps have "card (insert x A) = Suc (card A)" by simp also have "binomial_pmf \<dots> p = do { b \<leftarrow> bernoulli_pmf p; f \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p); return_pmf ((if b then 1 else 0) + card {y \<in> A. f y}) }" using p by (simp add: binomial_pmf_Suc insert.IH bind_map_pmf) also have "\<dots> = do { b \<leftarrow> bernoulli_pmf p; f \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p); return_pmf (card {y \<in> insert x A. (f(x := b)) y}) }" proof (intro bind_pmf_cong refl, goal_cases) case (1 b f) have "(if b then 1 else 0) + card {y\<in>A. f y} = card ((if b then {x} else {}) \<union> {y\<in>A. f y})" using insert.hyps by auto also have "(if b then {x} else {}) \<union> {y\<in>A. f y} = {y\<in>insert x A. (f(x := b)) y}" using insert.hyps by auto finally show ?case by simp qed also have "\<dots> = map_pmf (\<lambda>f. card {y\<in>insert x A. f y}) (Pi_pmf (insert x A) dflt (\<lambda>_. bernoulli_pmf p))" using insert.hyps by (subst Pi_pmf_insert) (simp_all add: pair_pmf_def map_bind_pmf) finally show ?case . qed finally show ?thesis . qed end

**References**:**[isabelle] Pmf and measure***From:*Kawin Worrasangasilpa

- Previous by Date: Re: [isabelle] Pmf and measure
- Next by Date: Re: [isabelle] Pmf and measure
- Previous by Thread: Re: [isabelle] Pmf and measure
- Next by Thread: Re: [isabelle] Pmf and measure
- Cl-isabelle-users October 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list