Theory Dependent_Product

theory Dependent_Product
  imports "HOL-Probability.Probability"
begin

text ‹The following lemma was reproduced from \cite[Lemma \emph{measure\_pmf\_prob\_dependent\_product\_bound\_eq}]{Approximate_Model_Counting-AFP}
The AFP imports \verb|Monad_Normalisation.Monad_Normalisation| which alters some Isabelle syntax, which we want to avoid by copy pasting the lemmas here›

lemma measure_pmf_prob_dependent_product_bound_eq:
  assumes "countable A" "⋀i. countable (B i)"
  assumes "⋀a. a ∈ A ⟹ measure_pmf.prob N (B a) = r"
  shows "measure_pmf.prob (pair_pmf M N) (Sigma A B) = measure_pmf.prob M A * r"
    (is "?L = ?R")
proof -
  have "?L =
    (∑⇩a(a, b) ∈ Sigma A B. pmf M a * pmf N b)"
    by (auto intro!: infsetsum_cong simp add: measure_pmf_conv_infsetsum pmf_pair)

  also have "… = (∑⇩aa∈A. ∑⇩ab∈B a. pmf M a * pmf N b)"
    apply (subst infsetsum_Sigma)
      using assms abs_summable_on_cong[of _ "pmf (pair_pmf M N)" "λuub. pmf M (fst uub) * pmf N (snd uub)"] pmf_pair[of M N]
      by (fastforce simp: case_prod_beta)+

  also have "… = (∑⇩aa∈A. pmf M a * (measure_pmf.prob N (B a)))"
    by (simp add: infsetsum_cmult_right measure_pmf_conv_infsetsum pmf_abs_summable)

  also have "… = (∑⇩aa∈A. pmf M a * r)"
    using assms(3) by fastforce

  also have "… = ?R"
    by (simp add: infsetsum_cmult_left pmf_abs_summable measure_pmf_conv_infsetsum)

  finally show ?thesis .
qed

text ‹The following lemma was reproduced from \cite[Lemma \emph{measure\_pmf\_prob\_dependent\_product\_bound\_eq'}]{Approximate_Model_Counting-AFP}
The AFP imports \verb|Monad_Normalisation.Monad_Normalisation| which alters some Isabelle syntax, which we want to avoid by copy pasting the lemmas here›

lemma measure_pmf_prob_dependent_product_bound_eq':
  ― ‹N is the pmf we want to fix depending on values from M›
  assumes "⋀a. a ∈ A ∩ set_pmf M ⟹ measure_pmf.prob N (B a) = r"
  shows "measure_pmf.prob (pair_pmf M N) (Sigma A B) = measure_pmf.prob M A * r"
    (is "?L = ?R")
proof -
  have "Sigma A B ∩ (set_pmf M × set_pmf N) =
    Sigma (A ∩ set_pmf M) (λi. B i ∩ set_pmf N)"
    by auto

  then have "?L =
    measure_pmf.prob (pair_pmf M N) (Sigma (A ∩ set_pmf M) (λi. B i ∩ set_pmf N))"
    by (metis measure_Int_set_pmf set_pair_pmf)

  also have "… = measure_pmf.prob M (A ∩ set_pmf M) * r"
    by (fastforce intro: measure_pmf_prob_dependent_product_bound_eq simp: assms measure_Int_set_pmf)

  also have "… = ?R" by (simp add: measure_Int_set_pmf)

  finally show ?thesis .
qed

end