Quelle Product_PMF.thy Sprache: Isabelle

(*
  File:    Product_PMF.thy
  Authors: Manuel Eberl, Max W. Haslbeck
*)
section \<open>Indexed products of PMFs\<close>
theory Product_PMF
  imports Probability_Mass_Function Independent_Family
begin

text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
no_notation Infinite_Sum.abs_summable_on (infixr \<open>abs'_summable'_on\<close> 46)

subsection \<open>Preliminaries\<close>

lemma pmf_expectation_eq_infsetsum: "measure_pmf.expectation p f = infsetsum (\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 \ B) = measure_pmf.prob M A * measure_pmf.prob N B"
proof -
  have "measure_pmf.prob (pair_pmf M N) (A \ B) = (\\<^sub>a(a, b)\A \ B. pmf M a * pmf N b)"
    by (auto intro!: infsetsum_cong simp add: measure_pmf_conv_infsetsum pmf_pair)
  also have "\ = 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 \ 'b \ ('a \ 'b pmf) \ ('a \ '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.._. 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. \x. x \ A \ f x = dflt}"
  define B where "B = (\x. set_pmf (p x))"

  have neutral_left: "(\xa\A. pmf (p xa) (f xa)) = 0"
    if "f \ PiE A B - (\f. restrict f A) ` S" for f
  proof -
    have "restrict (\x. if x \ A then f x else dflt) A \ (\f. restrict f A) ` S"
      by (intro imageI) (auto simp: S_def)
    also have "restrict (\x. if x \ 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: "(\xa\A. pmf (p xa) (f xa)) = 0"
    if "f \ (\f. restrict f A) ` S - PiE A B" for f
  proof -
    from that obtain f' where f': "f = restrict f' A" "f' \ S" by auto
    moreover from this and that have "restrict f' A \ PiE A B" by simp
    then obtain x where "x \ 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 "(\f. \x\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 \ (\f. \x\A. pmf (p x) (f x)) abs_summable_on (\f. restrict f A) ` S"
    by (intro abs_summable_on_cong_neutral neutral_left neutral_right) auto
  also have "\ \ (\f. \x\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 "\ \ (\f. if \x. x \ A \ f x = dflt then \x\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 = (\x\A. 1::real)" by simp
  also have "(\x\A. 1) = (\x\A. \\<^sub>ay\B x. pmf (p x) y)"
    unfolding B_def by (subst infsetsum_pmf_eq_1) auto
  also have "(\x\A. \\<^sub>ay\B x. pmf (p x) y) = (\\<^sub>af\Pi\<^sub>E A B. \x\A. pmf (p x) (f x))"
    by (intro infsetsum_prod_PiE [symmetric] A) (auto simp: B_def)
  also have "\ = (\\<^sub>af\(\f. restrict f A) ` S. \x\A. pmf (p x) (f x))" using A
    by (intro infsetsum_cong_neutral neutral_left neutral_right refl)
  also have "\ = (\\<^sub>af\S. \x\A. pmf (p x) (restrict f A x))"
    by (rule infsetsum_reindex) (force simp: inj_on_def fun_eq_iff S_def)
  also have "\ = (\\<^sub>af\S. \x\A. pmf (p x) (f x))"
    by (intro infsetsum_cong) (auto simp: S_def)
  also have "\ = (\\<^sub>af. if \x. x \ A \ f x = dflt then \x\A. pmf (p x) (f x) else 0)"
    by (intro infsetsum_cong_neutral) (auto simp: S_def)
  also have "ennreal \ = (\\<^sup>+f. ennreal (if \x. x \ A \ 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 Pi_pmf_cong:
  assumes "A = A'" "dflt = dflt'" "\x. x \ A \ f x = f' x"
  shows   "Pi_pmf A dflt f = Pi_pmf A' dflt' f'"
proof -
  have "(\fa. if \x. x \ A \ fa x = dflt then \x\A. pmf (f x) (fa x) else 0) =
        (\<lambda>f. if \<forall>x. x \<notin> A' \<longrightarrow> f x = dflt' then \<Prod>x\<in>A'. pmf (f' x) (f x) else 0)"
    using assms by (intro ext) (auto intro!: prod.cong)
  thus ?thesis
    by (simp only: Pi_pmf_def)
qed

lemma pmf_Pi':
  assumes "finite A" "\x. x \ A \ f x = dflt"
  shows   "pmf (Pi_pmf A dflt p) f = (\x\A. pmf (p x) (f x))"
  using assms by (subst pmf_Pi) auto

lemma pmf_Pi_outside:
  assumes "finite A" "\x. x \ A \ f x \ 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 (\_. dflt)"
  by (intro pmf_eqI, subst pmf_Pi) (auto simp: indicator_def)

lemma set_Pi_pmf_subset: "finite A \ set_pmf (Pi_pmf A dflt p) \ {f. \x. x \ A \ f x = dflt}"
  by (auto simp: set_pmf_eq pmf_Pi)

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. \x. (x \ A \ f x \ B x) \ (x \ A \ f x = dflt)}"

lemma restrict_PiE_dflt: "(\h. restrict h A) ` PiE_dflt A dflt B = PiE A B"
proof (intro equalityI subsetI)
  fix h assume "h \ (\h. restrict h A) ` PiE_dflt A dflt B"
  thus "h \ PiE A B"
    by (auto simp: PiE_dflt_def)
next
  fix h assume h: "h \ PiE A B"
  hence "restrict (\x. if x \ A then h x else dflt) A \ (\h. restrict h A) ` PiE_dflt A dflt B"
    by (intro imageI) (auto simp: PiE_def extensional_def PiE_dflt_def)
  also have "restrict (\x. if x \ A then h x else dflt) A = h"
    using h by (auto simp: fun_eq_iff)
  finally show "h \ (\h. restrict h A) ` PiE_dflt A dflt B" .
qed

lemma dflt_image_PiE: "(\h x. if x \ 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 \ ?f ` ?X"
  thus "h \ ?Y"
    by (auto simp: PiE_dflt_def PiE_def)
next
  fix h assume h: "h \ ?Y"
  hence "?f (restrict h A) \ ?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 \ ?f ` ?X" .
qed

lemma finite_PiE_dflt [intro]:
  assumes "finite A" "\x. x \ A \ finite (B x)"
  shows   "finite (PiE_dflt A d B)"
proof -
  have "PiE_dflt A d B = (\f x. if x \ A then f x else d) ` PiE A B"
    by (rule dflt_image_PiE [symmetric])
  also have "finite \"
    by (intro finite_imageI finite_PiE assms)
  finally show ?thesis .
qed

lemma card_PiE_dflt:
  assumes "finite A" "\x. x \ A \ finite (B x)"
  shows   "card (PiE_dflt A d B) = (\x\A. card (B x))"
proof -
  from assms have "(\x\A. card (B x)) = card (PiE A B)"
    by (intro card_PiE [symmetric]) auto
  also have "PiE A B = (\f. restrict f A) ` PiE_dflt A d B"
    by (rule restrict_PiE_dflt [symmetric])
  also have "card \ = 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 = {} \ (\x\A. B x = {})"
  by (simp add: dflt_image_PiE [symmetric] PiE_eq_empty_iff)

lemma set_Pi_pmf_subset':
  assumes "finite A"
  shows   "set_pmf (Pi_pmf A dflt p) \ PiE_dflt A dflt (set_pmf \ p)"
  using assms by (auto simp: set_pmf_eq pmf_Pi PiE_dflt_def)

lemma set_Pi_pmf:
  assumes "finite A"
  shows   "set_pmf (Pi_pmf A dflt p) = PiE_dflt A dflt (set_pmf \ p)"
proof (rule equalityI)
  show "PiE_dflt A dflt (set_pmf \ p) \ set_pmf (Pi_pmf A dflt p)"
  proof safe
    fix f assume f: "f \ PiE_dflt A dflt (set_pmf \ p)"
    hence "pmf (Pi_pmf A dflt p) f = (\x\A. pmf (p x) (f x))"
      using assms by (auto simp: pmf_Pi PiE_dflt_def)
    also have "\ > 0"
      using f by (intro prod_pos) (auto simp: PiE_dflt_def set_pmf_eq)
    finally show "f \ set_pmf (Pi_pmf A dflt p)"
      by (auto simp: set_pmf_eq)
  qed
qed (use set_Pi_pmf_subset'[OF assms, of dflt p] in auto)

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 "\ = (\\<^sub>ah\PiE_dflt A dflt B. \x\A. pmf (p x) (h x))"
    by (intro infsetsum_cong, subst pmf_Pi') (auto simp: PiE_dflt_def)
  also have "\ = (\\<^sub>ah\(\h. restrict h A) ` PiE_dflt A dflt B. \x\A. pmf (p x) (h x))"
    by (subst infsetsum_reindex) (force simp: inj_on_def PiE_dflt_def fun_eq_iff)+
  also have "(\h. restrict h A) ` PiE_dflt A dflt B = PiE A B"
    by (rule restrict_PiE_dflt)
  also have "(\\<^sub>ah\PiE A B. \x\A. pmf (p x) (h x)) = (\\<^sub>ah\PiE A B'. \x\A. pmf (p x) (h x))"
    by (intro infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq)
  also have "(\\<^sub>ah\PiE A B'. \x\A. pmf (p x) (h x)) = (\x\A. infsetsum (pmf (p x)) (B' x))"
    by (intro infsetsum_prod_PiE) (auto simp: B'_def)
  also have "\ = (\x\A. infsetsum (pmf (p x)) (B x))"
    by (intro prod.cong infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq)
  also have "\ = (\x\A. measure_pmf.prob (p x) (B x))"
    by (subst measure_pmf_conv_infsetsum) (rule refl)
  finally show ?thesis .
qed

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 "\ = ?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 (\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 "\x\-A. f x \ d")
    case False
    define B where "B = (\x. set_pmf (p x))"
    have [simp]: "countable (B x)" for x by (auto simp: B_def)

    {
      fix x :: 'a
      have "(\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) \ 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 "(\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 = (\\<^sub>ag. pmf (Pi_pmf A d' p) g * (\x\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 "\ = (\\<^sub>ag\PiE_dflt A d' B.
                      pmf (Pi_pmf A d' p) g * (\x\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 "\ = (\\<^sub>ag\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 "\ = (\\<^sub>ag\(\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 "(\g. restrict g A) ` PiE_dflt A d' B = PiE A B"
      by (rule restrict_PiE_dflt)
    also have "(\\<^sub>ag\\. (\x\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 "\ = (\x\A. \\<^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 "\ = 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) (\x. pmf (Pi_pmf A d (\xa. q xa (x xa))) f)"
      using assms by (simp add: pmf_bind)
    also have "\ = measure_pmf.expectation (Pi_pmf A d' p) (\x. 0)"
      using assms True by (intro Bochner_Integration.integral_cong pmf_Pi_outside) auto
    also have "\ = pmf ?lhs f"
      using assms True by (subst pmf_Pi_outside) auto
    finally show ?thesis ..
  qed
qed

lemma Pi_pmf_return_pmf [simp]:
  assumes "finite A"
  shows   "Pi_pmf A dflt (\x. return_pmf (f x)) = return_pmf (\x. if x \ A then f x else dflt)"
  using assms by (intro pmf_eqI) (auto simp: pmf_Pi simp: indicator_def split: if_splits)

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' (\x. map_pmf f (g x)) = map_pmf (\h. f \ h) (Pi_pmf A dflt g)"
proof -
  have "Pi_pmf A dflt' (\x. map_pmf f (g x)) =
          Pi_pmf A dflt' (\x. g x \ (\x. return_pmf (f x)))"
    using assms by (simp add: map_pmf_def Pi_pmf_bind)
  also have "\ = Pi_pmf A dflt g \ (\h. return_pmf (\x. if x \ A then f (h x) else dflt'))"
   by (subst Pi_pmf_bind[where d' = dflt]) auto
  also have "\ = map_pmf (\h. f \ 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 (\f x. if x \ 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 = "(\f x. if x \ A then f x else dflt') -` {f} \ PiE_dflt A dflt (\_. UNIV)"
  show ?case
  proof (cases "\x\-A. f x \ dflt'")
    case False
    let ?f' = "\x. if x \ 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 "\ = 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) \ = 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" "\x. x \ A \ h x \ B"
  shows "Pi_pmf A dflt (\_. f) = map_pmf (\g. g \ h) (Pi_pmf B dflt (\_. 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 "\a. a \ A \ 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 \ 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 (\_. f)) ((\g. g \ h) -` {g})"
      unfolding pmf_map by simp
    also have "\ = measure_pmf.prob (Pi_pmf B dflt (\_. 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 "\ = pmf (Pi_pmf B dflt (\_. f)) (\x. if x \ B then g (h' x) else dflt)"
    proof -
      have "(if h x \ B then g (h' (h x)) else dflt) = g x" for x
        using h' assms True by (cases "x \ A") (auto simp add: bij_betwE)
      then have "(\g. g \ h) -` {g} \ PiE_dflt B dflt (\_. 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 "\ = pmf (Pi_pmf A dflt (\_. 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 (\_. f))) ((\g. g \ h) -` {g})"
      using assms by (auto simp add: measure_pmf_conv_infsetsum pmf_map)
    also have "\ = infsetsum (\_. 0) ((\g x. g (h x)) -` {g})"
      using B False assms by (intro infsetsum_cong pmf_Pi_outside) fastforce+
    also have "\ = 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" "\x. x \ A \ finite (B x)" "\x. x \ A \ B x \ {}"
  shows   "Pi_pmf A d (\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 "\x. x \ A \ f x \ 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 \ 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 = (\x\A. pmf (pmf_of_set (B x)) (f x))"
      using assms by (subst pmf_Pi') auto
    also have "\ = (\x\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 "\ = (\x\A. indicator (B x) (f x)) / real (\x\A. card (B x))"
      by (subst prod_dividef) simp_all
    also have "(\x\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 "(\x\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 / \ = 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 \ A"
  shows   "Pi_pmf (insert x A) dflt p = map_pmf (\(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 (\(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 "((\(y, f). f(x := y)) -` {f}) = (\y'. {(f x, f(x := y'))})"
    by (auto simp: fun_upd_def fun_eq_iff)
  also have "measure_pmf.prob ?M \ = 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 "\ = 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 "\ = pmf (Pi_pmf (insert x A) dflt p) f"
  proof (cases "\y. y \ insert x A \ 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 "(\xa\A. pmf (p xa) ((f(x := dflt)) xa)) = (\xa\A. pmf (p xa) (f xa))"
      using assms by (intro prod.cong) auto
    also have "pmf (p x) (f x) * \ = 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 "\ = pmf (map_pmf (\(y, f). f(x := y)) ?M) f" ..
qed

lemma Pi_pmf_insert':
  assumes "finite A"  "x \ 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 (\a b. if b = x then a else dflt) (p x)"
proof -
  have "Pi_pmf {x} dflt p = map_pmf (fun_upd (\_. dflt) x) (p x)"
    by (subst Pi_pmf_insert) (simp_all add: pair_return_pmf2 pmf.map_comp o_def)
  also have "fun_upd (\_. dflt) x = (\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 (\f. f x) (Pi_pmf A dflt p) = (if x \ A then p x else return_pmf dflt)"
proof (cases "x \ 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 (\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 (\f. f x) (Pi_pmf A dflt p) = map_pmf (\_. 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 \ B = {}"
  shows   "Pi_pmf (A \ 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 "\ = do {v \ p x; (f, g) \ ?q A; return_pmf ((?h A (f,g))(x := v))}"
    by (intro bind_pmf_cong refl) (auto simp: fun_eq_iff)
  also have "\ = do {v \ p x; f \ 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 "\ = do {v \ p x; f \ Pi_pmf (A \ 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 "\ = Pi_pmf (insert x (A \ 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 \ B) = insert x A \ 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' \ A"
  shows   "Pi_pmf A' dflt p = map_pmf (\f x. if x \ 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' \ (A - A')"
    by blast
  also have "Pi_pmf \ dflt p = map_pmf (\(f,g) x. if x \ A' then f x else g x) ?P"
    using assms by (intro Pi_pmf_union) auto
  also have "map_pmf (\f x. if x \ A' then f x else dflt) \ = 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 "\ = Pi_pmf A' dflt p"
    by (simp add: map_fst_pair_pmf)
  finally show ?thesis ..
qed

lemma Pi_pmf_subset':
  fixes f :: "'a \ 'b pmf"
  assumes "finite A" "B \ A" "\x. x \ A - B \ f x = return_pmf dflt"
  shows "Pi_pmf A dflt f = Pi_pmf B dflt f"
proof -
  have "Pi_pmf (B \ (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 (\_. return_pmf dflt)"
    using assms by (intro Pi_pmf_cong) auto
  also have "\ = return_pmf (\_. dflt)"
    using assms by simp
  also have "map_pmf (\(f, g) x. if x \ 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 "\ = Pi_pmf B dflt f"
    using assms by (intro Pi_pmf_default_swap) (auto dest: finite_subset)
  also have "B \ (A - B) = A"
    using assms by auto
  finally show ?thesis .
qed

lemma Pi_pmf_if_set:
  assumes "finite A"
  shows "Pi_pmf A dflt (\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 (\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 "\ = Pi_pmf {x\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 (\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 (\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 "\ = Pi_pmf {x\A. \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 (\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 "\ = map_pmf (\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>Additional properties\<close>

lemma nn_integral_prod_Pi_pmf:
  assumes "finite A"
  shows   "nn_integral (Pi_pmf A dflt p) (\y. \x\A. f x (y x)) = (\x\A. nn_integral (p x) (f x))"
  using assms
proof (induction rule: finite_induct)
  case (insert x A)
  have "nn_integral (Pi_pmf (insert x A) dflt p) (\y. \z\insert x A. f z (y z)) =
          (\<integral>\<^sup>+a. \<integral>\<^sup>+b. f x a * (\<Prod>z\<in>A. f z (if z = x then a else b z)) \<partial>Pi_pmf A dflt p \<partial>p x)"
    using insert by (auto simp: Pi_pmf_insert case_prod_unfold nn_integral_pair_pmf' cong: if_cong)
  also have "(\a b. \z\A. f z (if z = x then a else b z)) = (\a b. \z\A. f z (b z))"
    by (intro ext prod.cong) (use insert.hyps in auto)
  also have "(\\<^sup>+a. \\<^sup>+b. f x a * (\z\A. f z (b z)) \Pi_pmf A dflt p \p x) =
             (\<integral>\<^sup>+y. f x y \<partial>(p x)) * (\<integral>\<^sup>+y. (\<Prod>z\<in>A. f z (y z)) \<partial>(Pi_pmf A dflt p))"
    by (simp add: nn_integral_multc nn_integral_cmult)
  also have "(\\<^sup>+y. (\z\A. f z (y z)) \(Pi_pmf A dflt p)) = (\x\A. nn_integral (p x) (f x))"
    by (rule insert.IH)
  also have "(\\<^sup>+y. f x y \(p x)) * \ = (\x\insert x A. nn_integral (p x) (f x))"
    using insert.hyps by simp
  finally show ?case .
qed auto

lemma integrable_prod_Pi_pmf:
  fixes f :: "'a \ 'b \ 'c :: {real_normed_field, second_countable_topology, banach}"
  assumes "finite A" and "\x. x \ A \ integrable (measure_pmf (p x)) (f x)"
  shows   "integrable (measure_pmf (Pi_pmf A dflt p)) (\h. \x\A. f x (h x))"
proof (intro integrableI_bounded)
  have "(\\<^sup>+ x. ennreal (norm (\xa\A. f xa (x xa))) \measure_pmf (Pi_pmf A dflt p)) =
        (\<integral>\<^sup>+ x. (\<Prod>y\<in>A. ennreal (norm (f y (x y)))) \<partial>measure_pmf (Pi_pmf A dflt p))"
    by (simp flip: prod_norm prod_ennreal)
  also have "\ = (\x\A. \\<^sup>+ a. ennreal (norm (f x a)) \measure_pmf (p x))"
    by (intro nn_integral_prod_Pi_pmf) fact
  also have "(\\<^sup>+a. ennreal (norm (f i a)) \measure_pmf (p i)) \ top" if i: "i \ A" for i
    using assms(2)[OF i] by (simp add: integrable_iff_bounded)
  hence "(\x\A. \\<^sup>+ a. ennreal (norm (f x a)) \measure_pmf (p x)) \ top"
    by (subst ennreal_prod_eq_top) auto
  finally show "(\\<^sup>+ x. ennreal (norm (\xa\A. f xa (x xa))) \measure_pmf (Pi_pmf A dflt p)) < \"
    by (simp add: top.not_eq_extremum)
qed auto

lemma expectation_prod_Pi_pmf:
  fixes f :: "_ \ _ \ real"
  assumes "finite A"
  assumes "\x. x \ A \ integrable (measure_pmf (p x)) (f x)"
  assumes "\x y. x \ A \ y \ set_pmf (p x) \ f x y \ 0"
  shows   "measure_pmf.expectation (Pi_pmf A dflt p) (\y. \x\A. f x (y x)) =
             (\<Prod>x\<in>A. measure_pmf.expectation (p x) (\<lambda>v. f x v))"
proof -
  have nonneg: "measure_pmf.expectation (p x) (f x) \ 0" if "x \ A" for x
    using that by (intro Bochner_Integration.integral_nonneg_AE AE_pmfI assms)
  have nonneg': "0 \ measure_pmf.expectation (Pi_pmf A dflt p) (\y. \x\A. f x (y x))"
    by (intro Bochner_Integration.integral_nonneg_AE AE_pmfI assms prod_nonneg)
       (use assms in \<open>auto simp: set_Pi_pmf PiE_dflt_def\<close>)

  have "ennreal (measure_pmf.expectation (Pi_pmf A dflt p) (\y. \x\A. f x (y x))) =
          nn_integral (Pi_pmf A dflt p) (\<lambda>y. ennreal (\<Prod>x\<in>A. f x (y x)))" using assms
    by (intro nn_integral_eq_integral [symmetric] assms integrable_prod_Pi_pmf)
       (auto simp: AE_measure_pmf_iff set_Pi_pmf PiE_dflt_def prod_nonneg)
  also have "\ = nn_integral (Pi_pmf A dflt p) (\y. (\x\A. ennreal (f x (y x))))"
    by (intro nn_integral_cong_AE AE_pmfI prod_ennreal [symmetric])
       (use assms(1) in \<open>auto simp: set_Pi_pmf PiE_dflt_def intro!: assms(3)\<close>)
  also have "\ = (\x\A. \\<^sup>+ a. ennreal (f x a) \measure_pmf (p x))"
    by (rule nn_integral_prod_Pi_pmf) fact+
  also have "\ = (\x\A. ennreal (measure_pmf.expectation (p x) (f x)))"
    by (intro prod.cong nn_integral_eq_integral assms AE_pmfI) auto
  also have "\ = ennreal (\x\A. measure_pmf.expectation (p x) (f x))"
    by (intro prod_ennreal nonneg)
  finally show ?thesis
    using nonneg nonneg' by (subst (asm) ennreal_inj) (auto intro!: prod_nonneg)
qed

lemma indep_vars_Pi_pmf:
  assumes fin: "finite I"
  shows   "prob_space.indep_vars (measure_pmf (Pi_pmf I dflt p))
             (\<lambda>_. count_space UNIV) (\<lambda>x f. f x) I"
proof (cases "I = {}")
  case True
  show ?thesis
    by (subst prob_space.indep_vars_def [OF measure_pmf.prob_space_axioms],
        subst prob_space.indep_sets_def [OF measure_pmf.prob_space_axioms]) (simp_all add: True)
next
  case [simp]: False
  show ?thesis
  proof (subst prob_space.indep_vars_iff_distr_eq_PiM')
    show "distr (measure_pmf (Pi_pmf I dflt p)) (Pi\<^sub>M I (\i. count_space UNIV)) (\x. restrict x I) =
          Pi\<^sub>M I (\<lambda>i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\<lambda>f. f i))"
    proof (rule product_sigma_finite.PiM_eqI, goal_cases)
      case 1
      interpret product_prob_space "\i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\f. f i)"
        by (intro product_prob_spaceI prob_space.prob_space_distr measure_pmf.prob_space_axioms)
           simp_all
      show ?case by unfold_locales
    next
      case 3
      have "sets (Pi\<^sub>M I (\i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\f. f i))) =
            sets (Pi\<^sub>M I (\<lambda>_. count_space UNIV))"
        by (intro sets_PiM_cong) simp_all
      thus ?case by simp
    next
      case (4 A)
      have "Pi\<^sub>E I A \ sets (Pi\<^sub>M I (\i. count_space UNIV))"
        using 4 by (intro sets_PiM_I_finite fin) auto
      hence "emeasure (distr (measure_pmf (Pi_pmf I dflt p)) (Pi\<^sub>M I (\i. count_space UNIV))
              (\<lambda>x. restrict x I)) (Pi\<^sub>E I A) =
             emeasure (measure_pmf (Pi_pmf I dflt p)) ((\<lambda>x. restrict x I) -` Pi\<^sub>E I A)"
        using 4 by (subst emeasure_distr) (auto simp: space_PiM)
      also have "\ = emeasure (measure_pmf (Pi_pmf I dflt p)) (PiE_dflt I dflt A)"
        by (intro emeasure_eq_AE AE_pmfI) (auto simp: PiE_dflt_def set_Pi_pmf fin)
      also have "\ = (\i\I. emeasure (measure_pmf (p i)) (A i))"
        by (simp add: measure_pmf.emeasure_eq_measure measure_Pi_pmf_PiE_dflt fin prod_ennreal)
      also have "\ = (\i\I. emeasure (measure_pmf (map_pmf (\f. f i) (Pi_pmf I dflt p))) (A i))"
        by (intro prod.cong refl, subst Pi_pmf_component) (auto simp: fin)
      finally show ?case
        by (simp add: map_pmf_rep_eq)
    qed fact+
  qed (simp_all add: measure_pmf.prob_space_axioms)
qed

lemma
  fixes h :: "'a :: comm_monoid_add \ 'b::{banach, second_countable_topology}"
  assumes fin: "finite I"
  assumes integrable: "\i. i \ I \ integrable (measure_pmf (D i)) h"
  shows   integrable_sum_Pi_pmf: "integrable (Pi_pmf I dflt D) (\g. \i\I. h (g i))"
    and   expectation_sum_Pi_pmf:
            "measure_pmf.expectation (Pi_pmf I dflt D) (\g. \i\I. h (g i)) =
             (\<Sum>i\<in>I. measure_pmf.expectation (D i) h)"
proof -
  have integrable': "integrable (Pi_pmf I dflt D) (\g. h (g i))" if i: "i \ I" for i
  proof -
    have "integrable (D i) h"
      using i by (rule assms)
    also have "D i = map_pmf (\g. g i) (Pi_pmf I dflt D)"
      by (subst Pi_pmf_component) (use fin i in auto)
    finally show "integrable (measure_pmf (Pi_pmf I dflt D)) (\x. h (x i))"
      by simp
  qed
  thus "integrable (Pi_pmf I dflt D) (\g. \i\I. h (g i))"
    by (intro Bochner_Integration.integrable_sum)

  have "measure_pmf.expectation (Pi_pmf I dflt D) (\x. \i\I. h (x i)) =
               (\<Sum>i\<in>I. measure_pmf.expectation (map_pmf (\<lambda>x. x i) (Pi_pmf I dflt D)) h)"
    using integrable' by (subst Bochner_Integration.integral_sum) auto
  also have "\ = (\i\I. measure_pmf.expectation (D i) h)"
    by (intro sum.cong refl, subst Pi_pmf_component) (use fin in auto)
  finally show "measure_pmf.expectation (Pi_pmf I dflt D) (\g. \i\I. h (g i)) =
                  (\<Sum>i\<in>I. measure_pmf.expectation (D i) h)" .
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 (\b. {x\A. b x}) (Pi_pmf A P (\_. bernoulli_pmf (1/2))) = pmf_of_set (Pow A)"
proof -
  have "Pi_pmf A P (\_. bernoulli_pmf (1/2)) = pmf_of_set (PiE_dflt A P (\x. UNIV))"
    using assms by (simp add: bernoulli_pmf_half_conv_pmf_of_set Pi_pmf_of_set)
  also have "map_pmf (\b. {x\A. b x}) \ = pmf_of_set (Pow A)"
  proof -
    have "bij_betw (\b. {x \ A. b x}) (PiE_dflt A P (\_. UNIV)) (Pow A)"
      by (rule bij_betwI[of _ _ _ "\B b. if b \ A then b \ 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 \ {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 "\ = ?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 \ 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 "\ = 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\A. f y} = card ((if b then {x} else {}) \ {y\A. f y})"
        using insert.hyps by auto
      also have "(if b then {x} else {}) \ {y\A. f y} = {y\insert x A. (f(x := b)) y}"
        using insert.hyps by auto
      finally show ?case by simp
    qed
    also have "\ = map_pmf (\f. card {y\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

quality99%

¤ Dauer der Verarbeitung: 0.46 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.