Theory HOL-Probability.Product_PMF

(*
  File:    Product_PMF.thy
  Authors: Manuel Eberl, Max W. Haslbeck
*)
section ‹Indexed products of PMFs›
theory Product_PMF
  imports Probability_Mass_Function Independent_Family
begin

text ‹Conflicting notation from theoryHOL-Analysis.Infinite_Sum
no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)

subsection ‹Preliminaries›

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) = (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 ‹Definition›

text ‹
  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 termA :: 'a set and a function termf :: 'a  'b pmf
  that maps each element from termA to a PMF and defines the product measure
  $\bigotimes_{i\in A} f(i)$ , which is represented as a typ('a  'b) pmf.

  Note that unlike @{const PiM}, this only works for ‹finite› index sets. It could
  be extended to countable sets and beyond, but the construction becomes somewhat more involved.
›
definition Pi_pmf :: "'a set  'b  ('a  'b pmf)  ('a  'b) pmf" where
  "Pi_pmf A dflt p =
     embed_pmf (λf. if (x. x  A  f x = dflt) then xA. pmf (p x) (f x) else 0)"

text ‹
  A technical subtlety that needs to be addressed is this: Intuitively, the functions in the
  support of a product distribution have domain A›. However, since HOL is a total logic, these
  functions must still return ‹some› value for inputs outside A›. 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 termdflt :: 'b that is returned
  in these cases.

  As one possible application, one could model the result of n› different independent coin
  tosses as @{term "Pi_pmf {0..<n} False (λ_. bernoulli_pmf (1 / 2))"}. This returns a function
  of type typnat  bool that maps every natural number below n› to the result of the
  corresponding coin toss, and every other natural number to termFalse.
›

lemma pmf_Pi:
  assumes A: "finite A"
  shows   "pmf (Pi_pmf A dflt p) f =
             (if (x. x  A  f x = dflt) then xA. 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: "(xaA. 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: "(xaA. 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. xA. 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. xA. 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. xA. 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 xA. 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:  .

  have "1 = (xA. 1::real)" by simp
  also have "(xA. 1) = (xA. ayB x. pmf (p x) y)"
    unfolding B_def by (subst infsetsum_pmf_eq_1) auto
  also have "(xA. ayB x. pmf (p x) y) = (afPiE A B. xA. pmf (p x) (f x))"
    by (intro infsetsum_prod_PiE [symmetric] A) (auto simp: B_def)
  also have " = (af(λf. restrict f A) ` S. xA. pmf (p x) (f x))" using A
    by (intro infsetsum_cong_neutral neutral_left neutral_right refl)
  also have " = (afS. xA. pmf (p x) (restrict f A x))"
    by (rule infsetsum_reindex) (force simp: inj_on_def fun_eq_iff S_def)
  also have " = (afS. xA. pmf (p x) (f x))"
    by (intro infsetsum_cong) (auto simp: S_def)
  also have " = (af. if x. x  A  f x = dflt then xA. pmf (p x) (f x) else 0)"
    by (intro infsetsum_cong_neutral) (auto simp: S_def)
  also have "ennreal  = (+f. ennreal (if x. x  A  f x = dflt
                             then xA. pmf (p x) (f x) else 0) 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 xA. pmf (f x) (fa x) else 0) =
        (λf. if x. x  A'  f x = dflt' then xA'. 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 = (xA. 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 ‹Dependent product sets with a default›

text ‹
  The following describes a dependent product of sets where the functions are required to return
  the default value termdflt outside their domain, in analogy to @{const PiE}, which uses
  @{const undefined}.
›
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) = (xA. card (B x))"
proof -
  from assms have "(xA. 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 = {}  (xA. 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 = (xA. 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 ‹
  The probability of an independent combination of events is precisely the product
  of the probabilities of each individual event.
›
lemma measure_Pi_pmf_PiE_dflt:
  assumes [simp]: "finite A"
  shows   "measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B) =
             (xA. measure_pmf.prob (p x) (B x))"
proof -
  define B' where "B' = (λx. B x  set_pmf (p x))"
  have "measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B) =
          (ahPiE_dflt A dflt B. pmf (Pi_pmf A dflt p) h)"
    by (rule measure_pmf_conv_infsetsum)
  also have " = (ahPiE_dflt A dflt B. xA. pmf (p x) (h x))"
    by (intro infsetsum_cong, subst pmf_Pi') (auto simp: PiE_dflt_def)
  also have " = (ah(λh. restrict h A) ` PiE_dflt A dflt B. xA. 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 "(ahPiE A B. xA. pmf (p x) (h x)) = (ahPiE A B'. xA. pmf (p x) (h x))"
    by (intro infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq)
  also have "(ahPiE A B'. xA. pmf (p x) (h x)) = (xA. infsetsum (pmf (p x)) (B' x))"
    by (intro infsetsum_prod_PiE) (auto simp: B'_def)
  also have " = (xA. infsetsum (pmf (p x)) (B x))"
    by (intro prod.cong infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq)
  also have " = (xA. 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) =
             (xA. 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 ‹Common PMF operations on products›

text @{const Pi_pmf} distributes over the `bind' operation in the Giry monad:
›
lemma Pi_pmf_bind:
  assumes "finite A"
  shows   "Pi_pmf A d (λx. bind_pmf (p x) (q x)) =
             do {f  Pi_pmf A d' p; Pi_pmf A d (λ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 = (ag. pmf (Pi_pmf A d' p) g * (xA. 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 " = (agPiE_dflt A d' B.
                      pmf (Pi_pmf A d' p) g * (xA. 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 " = (agPiE_dflt A d' B.
                      (xA. 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 " = (ag(λg. restrict g A) ` PiE_dflt A d' B.
                      (xA. 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 "(ag. (xA. pmf (p x) (g x) * pmf (q x (g x)) (f x))) =
                 (xA. aaB x. pmf (p x) a * pmf (q x a) (f x))"
      using assms summable by (subst infsetsum_prod_PiE) simp_all
    also have " = (xA. 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 ‹
  Analogously any componentwise mapping can be pulled outside the product:
›
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 ‹
  We can exchange the default value in a product of PMFs like this:
›
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 ‹
  The following rule allows reindexing the product:
›
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  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))
                                (((λg. g  h) -` {g})  PiE_dflt B dflt (λ_. 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) =
            {(λx. if x  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 ‹
  A product of uniform random choices is again a uniform distribution.
›
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 = (xA. pmf (pmf_of_set (B x)) (f x))"
      using assms by (subst pmf_Pi') auto
    also have " = (xA. 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 " = (xA. indicator (B x) (f x)) / real (xA. card (B x))"
      by (subst prod_dividef) simp_all
    also have "(xA. 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 "(xA. 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 ‹Merging and splitting PMF products›

text ‹
  The following lemma shows that we can add a single PMF to a product:
›
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 ((λ(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) * (xaA. pmf (p xa) ((f(x := dflt)) xa))"
      by (subst pmf_Pi') auto
    also have "(xaA. pmf (p xa) ((f(x := dflt)) xa)) = (xaA. 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  p x; f  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 ‹
  Projecting a product of PMFs onto a component yields the expected result:
›
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 ‹
  We can take merge two PMF products on disjoint sets like this:
›
lemma Pi_pmf_union:
  assumes "finite A" "finite B" "A  B = {}"
  shows   "Pi_pmf (A  B) dflt p =
             map_pmf (λ(f,g) x. if x  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  p x; (f, g)  pair_pmf (Pi_pmf A dflt p) (Pi_pmf B dflt p);
              return_pmf (λy. if y  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 ‹
  We can also project a product to a subset of the indices by mapping all the other
  indices to the default value:
›
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 (λ(f, g) x. if x  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 (λ_. dflt))) =
             map_pmf (λf x. if x  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 {xA. b x} dflt f"
proof -
  have "Pi_pmf A dflt (λx. if b x then f x else return_pmf dflt) =
          Pi_pmf {xA. b x} dflt (λx. if b x then f x else return_pmf dflt)"
    using assms by (intro Pi_pmf_subset') auto
  also have " = Pi_pmf {xA. 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 {xA. ¬b x} dflt f"
proof -
  have "Pi_pmf A dflt (λx. if b x then return_pmf dflt else  f x) =
          Pi_pmf {xA. ¬b x} dflt (λx. if b x then return_pmf dflt else  f x)"
    using assms by (intro Pi_pmf_subset') auto
  also have " = Pi_pmf {xA. ¬b x} dflt f"
    by (intro Pi_pmf_cong) auto
  finally show ?thesis .
qed

text ‹
  Lastly, we can delete a single component from a product:
›
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 (λf xa. if xa  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 ‹Additional properties›

lemma nn_integral_prod_Pi_pmf:
  assumes "finite A"
  shows   "nn_integral (Pi_pmf A dflt p) (λy. xA. f x (y x)) = (xA. 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. zinsert x A. f z (y z)) =
          (+a. +b. f x a * (zA. f z (if z = x then a else b z)) Pi_pmf A dflt p p x)"
    using insert by (auto simp: Pi_pmf_insert case_prod_unfold nn_integral_pair_pmf' cong: if_cong)
  also have "(λa b. zA. f z (if z = x then a else b z)) = (λa b. zA. f z (b z))"
    by (intro ext prod.cong) (use insert.hyps in auto)
  also have "(+a. +b. f x a * (zA. f z (b z)) Pi_pmf A dflt p p x) =
             (+y. f x y (p x)) * (+y. (zA. f z (y z)) (Pi_pmf A dflt p))"
    by (simp add: nn_integral_multc nn_integral_cmult)
  also have "(+y. (zA. f z (y z)) (Pi_pmf A dflt p)) = (xA. nn_integral (p x) (f x))"
    by (rule insert.IH)
  also have "(+y. f x y (p x)) *  = (xinsert 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. xA. f x (h x))"
proof (intro integrableI_bounded)
  have "(+ x. ennreal (norm (xaA. f xa (x xa))) measure_pmf (Pi_pmf A dflt p)) =
        (+ x. (yA. ennreal (norm (f y (x y)))) measure_pmf (Pi_pmf A dflt p))"
    by (simp flip: prod_norm prod_ennreal)
  also have " = (xA. + a. ennreal (norm (f x a)) measure_pmf (p x))"
    by (intro nn_integral_prod_Pi_pmf) fact
  also have "(+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 "(xA. + a. ennreal (norm (f x a)) measure_pmf (p x))  top"
    by (subst ennreal_prod_eq_top) auto
  finally show "(+ x. ennreal (norm (xaA. 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. xA. f x (y x)) =
             (xA. measure_pmf.expectation (p x) (λ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. xA. f x (y x))"
    by (intro Bochner_Integration.integral_nonneg_AE AE_pmfI assms prod_nonneg)
       (use assms in auto simp: set_Pi_pmf PiE_dflt_def)

  have "ennreal (measure_pmf.expectation (Pi_pmf A dflt p) (λy. xA. f x (y x))) =
          nn_integral (Pi_pmf A dflt p) (λy. ennreal (xA. 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. (xA. ennreal (f x (y x))))"
    by (intro nn_integral_cong_AE AE_pmfI prod_ennreal [symmetric])
       (use assms(1) in auto simp: set_Pi_pmf PiE_dflt_def intro!: assms(3))
  also have " = (xA. + a. ennreal (f x a) measure_pmf (p x))"
    by (rule nn_integral_prod_Pi_pmf) fact+
  also have " = (xA. ennreal (measure_pmf.expectation (p x) (f x)))"
    by (intro prod.cong nn_integral_eq_integral assms AE_pmfI) auto
  also have " = ennreal (xA. 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))
             (λ_. count_space UNIV) (λ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)) (PiM I (λi. count_space UNIV)) (λx. restrict x I) =
          PiM I (λi. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (λ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 (PiM I (λi. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (λf. f i))) =
            sets (PiM I (λ_. count_space UNIV))"
        by (intro sets_PiM_cong) simp_all
      thus ?case by simp
    next
      case (4 A)
      have "PiE I A  sets (PiM 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)) (PiM I (λi. count_space UNIV))
              (λx. restrict x I)) (PiE I A) =
             emeasure (measure_pmf (Pi_pmf I dflt p)) ((λx. restrict x I) -` PiE 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 " = (iI. 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 " = (iI. 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. iI. h (g i))"
    and   expectation_sum_Pi_pmf:
            "measure_pmf.expectation (Pi_pmf I dflt D) (λg. iI. h (g i)) =
             (iI. 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. iI. h (g i))"
    by (intro Bochner_Integration.integrable_sum)

  have "measure_pmf.expectation (Pi_pmf I dflt D) (λx. iI. h (x i)) =
               (iI. measure_pmf.expectation (map_pmf (λx. x i) (Pi_pmf I dflt D)) h)"
    using integrable' by (subst Bochner_Integration.integral_sum) auto
  also have " = (iI. 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. iI. h (g i)) =
                  (iI. measure_pmf.expectation (D i) h)" .
qed


subsection ‹Applications›

text ‹
  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.
›
lemma pmf_of_set_Pow_conv_bernoulli:
  assumes "finite (A :: 'a set)"
  shows "map_pmf (λb. {xA. 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. {xA. 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 ‹
  A binomial distribution can be seen as the number of successes in n› independent coin tosses.
›
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 (λf. card {xA. f x}) (Pi_pmf A dflt (λ_. 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  bernoulli_pmf p;
                                     f  Pi_pmf A dflt (λ_. bernoulli_pmf p);
                                     return_pmf ((if b then 1 else 0) + card {y  A. f y})
                                   }"
      using p by (simp add: binomial_pmf_Suc insert.IH bind_map_pmf)
    also have " = do {
                      b  bernoulli_pmf p;
                      f  Pi_pmf A dflt (λ_. bernoulli_pmf p);
                      return_pmf (card {y  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 {yA. f y} = card ((if b then {x} else {})  {yA. f y})"
        using insert.hyps by auto
      also have "(if b then {x} else {})  {yA. f y} = {yinsert x A. (f(x := b)) y}"
        using insert.hyps by auto
      finally show ?case by simp
    qed
    also have " = map_pmf (λf. card {yinsert x A. f y})
                      (Pi_pmf (insert x A) dflt (λ_. 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