Quelle Probability_Mass_Function.thy Sprache: Isabelle

(*  Title:      HOL/Probability/Probability_Mass_Function.thy
    Author:     Johannes Hölzl, TU München
    Author:     Andreas Lochbihler, ETH Zurich
    Author:     Manuel Eberl, TU München
*)

section \<open> Probability mass function \<close>

theory Probability_Mass_Function
imports
  Giry_Monad
  "HOL-Library.Multiset"
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)

lemma AE_emeasure_singleton:
  assumes x: "emeasure M {x} \ 0" and ae: "AE x in M. P x" shows "P x"
proof -
  from x have x_M: "{x} \ sets M"
    by (auto intro: emeasure_notin_sets)
  from ae obtain N where N: "{x\space M. \ P x} \ N" "emeasure M N = 0" "N \ sets M"
    by (auto elim: AE_E)
  { assume "\ P x"
    with x_M[THEN sets.sets_into_space] N have "emeasure M {x} \ emeasure M N"
      by (intro emeasure_mono) auto
    with x N have False
      by (auto simp:) }
  then show "P x" by auto
qed

lemma AE_measure_singleton: "measure M {x} \ 0 \ AE x in M. P x \ P x"
  by (metis AE_emeasure_singleton measure_def emeasure_empty measure_empty)

lemma (in finite_measure) AE_support_countable:
  assumes [simp]: "sets M = UNIV"
  shows "(AE x in M. measure M {x} \ 0) \ (\S. countable S \ (AE x in M. x \ S))"
proof
  assume "\S. countable S \ (AE x in M. x \ S)"
  then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \ S"
    by auto
  then have "emeasure M (\x\{x\S. emeasure M {x} \ 0}. {x}) =
    (\<integral>\<^sup>+ x. emeasure M {x} * indicator {x\<in>S. emeasure M {x} \<noteq> 0} x \<partial>count_space UNIV)"
    by (subst emeasure_UN_countable)
       (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
  also have "\ = (\\<^sup>+ x. emeasure M {x} * indicator S x \count_space UNIV)"
    by (auto intro!: nn_integral_cong split: split_indicator)
  also have "\ = emeasure M (\x\S. {x})"
    by (subst emeasure_UN_countable)
       (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
  also have "\ = emeasure M (space M)"
    using ae by (intro emeasure_eq_AE) auto
  finally have "emeasure M {x \ space M. x\S \ emeasure M {x} \ 0} = emeasure M (space M)"
    by (simp add: emeasure_single_in_space cong: rev_conj_cong)
  with finite_measure_compl[of "{x \ space M. x\S \ emeasure M {x} \ 0}"]
  have "AE x in M. x \ S \ emeasure M {x} \ 0"
    by (intro AE_I[OF order_refl]) (auto simp: emeasure_eq_measure measure_nonneg set_diff_eq cong: conj_cong)
  then show "AE x in M. measure M {x} \ 0"
    by (auto simp: emeasure_eq_measure)
qed (auto intro!: exI[of _ "{x. measure M {x} \ 0}"] countable_support)

subsection \<open> PMF as measure \<close>

typedef 'a pmf = "{M :: 'a measure. prob_space M \<and> sets M = UNIV \<and> (AE x in M. measure M {x} \<noteq> 0)}"
  morphisms measure_pmf Abs_pmf
  by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
     (auto intro!: prob_space_uniform_measure AE_uniform_measureI)

declare [[coercion measure_pmf]]

lemma prob_space_measure_pmf: "prob_space (measure_pmf p)"
  using pmf.measure_pmf[of p] by auto

interpretation measure_pmf: prob_space "measure_pmf M" for M
  by (rule prob_space_measure_pmf)

interpretation measure_pmf: subprob_space "measure_pmf M" for M
  by (rule prob_space_imp_subprob_space) unfold_locales

lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"
  by unfold_locales

locale pmf_as_measure
begin

setup_lifting type_definition_pmf

end

context
begin

interpretation pmf_as_measure .

lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
  by transfer blast

lemma sets_measure_pmf_count_space[measurable_cong]:
  "sets (measure_pmf M) = sets (count_space UNIV)"
  by simp

lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
  using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp

lemma measure_pmf_UNIV [simp]: "measure (measure_pmf p) UNIV = 1"
using measure_pmf.prob_space[of p] by simp

lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \ space (subprob_algebra (count_space UNIV))"
  by (simp add: space_subprob_algebra subprob_space_measure_pmf)

lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \ space N"
  by (auto simp: measurable_def)

lemma measurable_pmf_measure2[simp]: "measurable N (M :: 'a pmf) = measurable N (count_space UNIV)"
  by (intro measurable_cong_sets) simp_all

lemma measurable_pair_restrict_pmf2:
  assumes "countable A"
  assumes [measurable]: "\y. y \ A \ (\x. f (x, y)) \ measurable M L"
  shows "f \ measurable (M \\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \ measurable ?M _")
proof -
  have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
    by (simp add: restrict_count_space)

  show ?thesis
    by (intro measurable_compose_countable'[where f="\a b. f (fst b, a)" and g=snd and I=A,
                                            unfolded prod.collapse] assms)
        measurable
qed

lemma measurable_pair_restrict_pmf1:
  assumes "countable A"
  assumes [measurable]: "\x. x \ A \ (\y. f (x, y)) \ measurable N L"
  shows "f \ measurable (restrict_space (measure_pmf M) A \\<^sub>M N) L"
proof -
  have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
    by (simp add: restrict_count_space)

  show ?thesis
    by (intro measurable_compose_countable'[where f="\a b. f (a, snd b)" and g=fst and I=A,
                                            unfolded prod.collapse] assms)
        measurable
qed

lift_definition pmf :: "'a pmf \ 'a \ real" is "\M x. measure M {x}" .

lift_definition set_pmf :: "'a pmf \ 'a set" is "\M. {x. measure M {x} \ 0}" .
declare [[coercion set_pmf]]

lemma AE_measure_pmf: "AE x in (M::'a pmf). x \ M"
  by transfer simp

lemma emeasure_pmf_single_eq_zero_iff:
  fixes M :: "'a pmf"
  shows "emeasure M {y} = 0 \ y \ M"
  unfolding set_pmf.rep_eq by (simp add: measure_pmf.emeasure_eq_measure)

lemma AE_measure_pmf_iff: "(AE x in measure_pmf M. P x) \ (\y\M. P y)"
  using AE_measure_singleton[of M] AE_measure_pmf[of M]
  by (auto simp: set_pmf.rep_eq)

lemma AE_pmfI: "(\y. y \ set_pmf M \ P y) \ almost_everywhere (measure_pmf M) P"
by(simp add: AE_measure_pmf_iff)

lemma countable_set_pmf [simp]: "countable (set_pmf p)"
  by transfer (metis prob_space.finite_measure finite_measure.countable_support)

lemma pmf_positive: "x \ set_pmf p \ 0 < pmf p x"
  by transfer (simp add: less_le)

lemma pmf_nonneg[simp]: "0 \ pmf p x"
  by transfer simp

lemma pmf_not_neg [simp]: "\pmf p x < 0"
  by (simp add: not_less pmf_nonneg)

lemma pmf_pos [simp]: "pmf p x \ 0 \ pmf p x > 0"
  using pmf_nonneg[of p x] by linarith

lemma pmf_le_1: "pmf p x \ 1"
  by (simp add: pmf.rep_eq)

lemma set_pmf_not_empty: "set_pmf M \ {}"
  using AE_measure_pmf[of M] by (intro notI) simp

lemma set_pmf_iff: "x \ set_pmf M \ pmf M x \ 0"
  by transfer simp

lemma pmf_positive_iff: "0 < pmf p x \ x \ set_pmf p"
  unfolding less_le by (simp add: set_pmf_iff)

lemma set_pmf_eq: "set_pmf M = {x. pmf M x \ 0}"
  by (auto simp: set_pmf_iff)

lemma set_pmf_eq': "set_pmf p = {x. pmf p x > 0}"
proof safe
  fix x assume "x \ set_pmf p"
  hence "pmf p x \ 0" by (auto simp: set_pmf_eq)
  with pmf_nonneg[of p x] show "pmf p x > 0" by simp
qed (auto simp: set_pmf_eq)

lemma emeasure_pmf_single:
  fixes M :: "'a pmf"
  shows "emeasure M {x} = pmf M x"
  by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])

lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x"
  using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure pmf_nonneg measure_nonneg)

lemma emeasure_measure_pmf_finite: "finite S \ emeasure (measure_pmf M) S = (\s\S. pmf M s)"
  by (subst emeasure_eq_sum_singleton) (auto simp: emeasure_pmf_single pmf_nonneg)

lemma measure_measure_pmf_finite: "finite S \ measure (measure_pmf M) S = sum (pmf M) S"
  using emeasure_measure_pmf_finite[of S M]
  by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg sum_nonneg pmf_nonneg)

lemma sum_pmf_eq_1:
  assumes "finite A" "set_pmf p \ A"
  shows   "(\x\A. pmf p x) = 1"
proof -
  have "(\x\A. pmf p x) = measure_pmf.prob p A"
    by (simp add: measure_measure_pmf_finite assms)
  also from assms have "\ = 1"
    by (subst measure_pmf.prob_eq_1) (auto simp: AE_measure_pmf_iff)
  finally show ?thesis .
qed

lemma nn_integral_measure_pmf_support:
  fixes f :: "'a \ ennreal"
  assumes f: "finite A" and nn: "\x. x \ A \ 0 \ f x" "\x. x \ set_pmf M \ x \ A \ f x = 0"
  shows "(\\<^sup>+x. f x \measure_pmf M) = (\x\A. f x * pmf M x)"
proof -
  have "(\\<^sup>+x. f x \M) = (\\<^sup>+x. f x * indicator A x \M)"
    using nn by (intro nn_integral_cong_AE) (auto simp: AE_measure_pmf_iff split: split_indicator)
  also have "\ = (\x\A. f x * emeasure M {x})"
    using assms by (intro nn_integral_indicator_finite) auto
  finally show ?thesis
    by (simp add: emeasure_measure_pmf_finite)
qed

lemma nn_integral_measure_pmf_finite:
  fixes f :: "'a \ ennreal"
  assumes f: "finite (set_pmf M)" and nn: "\x. x \ set_pmf M \ 0 \ f x"
  shows "(\\<^sup>+x. f x \measure_pmf M) = (\x\set_pmf M. f x * pmf M x)"
  using assms by (intro nn_integral_measure_pmf_support) auto

lemma integrable_measure_pmf_finite:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  shows "finite (set_pmf M) \ integrable M f"
  by (auto intro!: integrableI_bounded simp: nn_integral_measure_pmf_finite ennreal_mult_less_top)

lemma integral_measure_pmf_real:
  assumes [simp]: "finite A" and "\a. a \ set_pmf M \ f a \ 0 \ a \ A"
  shows "(\x. f x \measure_pmf M) = (\a\A. f a * pmf M a)"
proof -
  have "(\x. f x \measure_pmf M) = (\x. f x * indicator A x \measure_pmf M)"
    using assms(2) by (intro integral_cong_AE) (auto split: split_indicator simp: AE_measure_pmf_iff)
  also have "\ = (\a\A. f a * pmf M a)"
    by (subst integral_indicator_finite_real)
       (auto simp: measure_def emeasure_measure_pmf_finite pmf_nonneg)
  finally show ?thesis .
qed

lemma integrable_pmf: "integrable (count_space X) (pmf M)"
proof -
  have " (\\<^sup>+ x. pmf M x \count_space X) = (\\<^sup>+ x. pmf M x \count_space (M \ X))"
    by (auto simp add: nn_integral_count_space_indicator set_pmf_iff intro!: nn_integral_cong split: split_indicator)
  then have "integrable (count_space X) (pmf M) = integrable (count_space (M \ X)) (pmf M)"
    by (simp add: integrable_iff_bounded pmf_nonneg)
  then show ?thesis
    by (simp add: pmf.rep_eq measure_pmf.integrable_measure disjoint_family_on_def)
qed

lemma integral_pmf: "(\x. pmf M x \count_space X) = measure M X"
proof -
  have "(\x. pmf M x \count_space X) = (\\<^sup>+x. pmf M x \count_space X)"
    by (simp add: pmf_nonneg integrable_pmf nn_integral_eq_integral)
  also have "\ = (\\<^sup>+x. emeasure M {x} \count_space (X \ M))"
    by (auto intro!: nn_integral_cong_AE split: split_indicator
             simp: pmf.rep_eq measure_pmf.emeasure_eq_measure nn_integral_count_space_indicator
                   AE_count_space set_pmf_iff)
  also have "\ = emeasure M (X \ M)"
    by (rule emeasure_countable_singleton[symmetric]) (auto intro: countable_set_pmf)
  also have "\ = emeasure M X"
    by (auto intro!: emeasure_eq_AE simp: AE_measure_pmf_iff)
  finally show ?thesis
    by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg integral_nonneg pmf_nonneg)
qed

lemma integral_pmf_restrict:
  "(f::'a \ 'b::{banach, second_countable_topology}) \ borel_measurable (count_space UNIV) \
    (\<integral>x. f x \<partial>measure_pmf M) = (\<integral>x. f x \<partial>restrict_space M M)"
  by (auto intro!: integral_cong_AE simp add: integral_restrict_space AE_measure_pmf_iff)

lemma emeasure_pmf: "emeasure (M::'a pmf) M = 1"
proof -
  have "emeasure (M::'a pmf) M = emeasure (M::'a pmf) (space M)"
    by (intro emeasure_eq_AE) (simp_all add: AE_measure_pmf)
  then show ?thesis
    using measure_pmf.emeasure_space_1 by simp
qed

lemma emeasure_pmf_UNIV [simp]: "emeasure (measure_pmf M) UNIV = 1"
using measure_pmf.emeasure_space_1[of M] by simp

lemma in_null_sets_measure_pmfI:
  "A \ set_pmf p = {} \ A \ null_sets (measure_pmf p)"
using emeasure_eq_0_AE[where ?P="\x. x \ A" and M="measure_pmf p"]
by(auto simp add: null_sets_def AE_measure_pmf_iff)

lemma measure_subprob: "measure_pmf M \ space (subprob_algebra (count_space UNIV))"
  by (simp add: space_subprob_algebra subprob_space_measure_pmf)

subsection \<open> Monad Interpretation \<close>

lemma measurable_measure_pmf[measurable]:
  "(\x. measure_pmf (M x)) \ measurable (count_space UNIV) (subprob_algebra (count_space UNIV))"
  by (auto simp: space_subprob_algebra intro!: prob_space_imp_subprob_space) unfold_locales

lemma bind_measure_pmf_cong:
  assumes "\x. A x \ space (subprob_algebra N)" "\x. B x \ space (subprob_algebra N)"
  assumes "\i. i \ set_pmf x \ A i = B i"
  shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
proof (rule measure_eqI)
  show "sets (measure_pmf x \ A) = sets (measure_pmf x \ B)"
    using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
next
  fix X assume "X \ sets (measure_pmf x \ A)"
  then have X: "X \ sets N"
    using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
  show "emeasure (measure_pmf x \ A) X = emeasure (measure_pmf x \ B) X"
    using assms
    by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
       (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
qed

lift_definition bind_pmf :: "'a pmf \ ('a \ 'b pmf ) \ 'b pmf" is bind
proof (clarify, intro conjI)
  fix f :: "'a measure" and g :: "'a \ 'b measure"
  assume "prob_space f"
  then interpret f: prob_space f .
  assume "sets f = UNIV" and ae_f: "AE x in f. measure f {x} \ 0"
  then have s_f[simp]: "sets f = sets (count_space UNIV)"
    by simp
  assume g: "\x. prob_space (g x) \ sets (g x) = UNIV \ (AE y in g x. measure (g x) {y} \ 0)"
  then have g: "\x. prob_space (g x)" and s_g[simp]: "\x. sets (g x) = sets (count_space UNIV)"
    and ae_g: "\x. AE y in g x. measure (g x) {y} \ 0"
    by auto

  have [measurable]: "g \ measurable f (subprob_algebra (count_space UNIV))"
    by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g)

  show "prob_space (f \ g)"
    using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto
  then interpret fg: prob_space "f \ g" .
  show [simp]: "sets (f \ g) = UNIV"
    using sets_eq_imp_space_eq[OF s_f]
    by (subst sets_bind[where N="count_space UNIV"]) auto
  show "AE x in f \ g. measure (f \ g) {x} \ 0"
    apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"])
    using ae_f
    apply eventually_elim
    using ae_g
    apply eventually_elim
    apply (auto dest: AE_measure_singleton)
    done
qed

adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind_pmf

lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\\<^sup>+x. pmf (f x) i \measure_pmf N)"
  unfolding pmf.rep_eq bind_pmf.rep_eq
  by (auto simp: measure_pmf.measure_bind[where N="count_space UNIV"] measure_subprob measure_nonneg
           intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])

lemma pmf_bind: "pmf (bind_pmf N f) i = (\x. pmf (f x) i \measure_pmf N)"
  using ennreal_pmf_bind[of N f i]
  by (subst (asm) nn_integral_eq_integral)
     (auto simp: pmf_nonneg pmf_le_1 pmf_nonneg integral_nonneg
           intro!: nn_integral_eq_integral[symmetric] measure_pmf.integrable_const_bound[where B=1])

lemma bind_pmf_const[simp]: "bind_pmf M (\x. c) = c"
  by transfer (simp add: bind_const' prob_space_imp_subprob_space)

lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\M\set_pmf M. set_pmf (N M))"
proof -
  have "set_pmf (bind_pmf M N) = {x. ennreal (pmf (bind_pmf M N) x) \ 0}"
    by (simp add: set_pmf_eq pmf_nonneg)
  also have "\ = (\M\set_pmf M. set_pmf (N M))"
    unfolding ennreal_pmf_bind
    by (subst nn_integral_0_iff_AE) (auto simp: AE_measure_pmf_iff pmf_nonneg set_pmf_eq)
  finally show ?thesis .
qed

lemma bind_pmf_cong [fundef_cong]:
  assumes "p = q"
  shows "(\x. x \ set_pmf q \ f x = g x) \ bind_pmf p f = bind_pmf q g"
  unfolding \<open>p = q\<close>[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq
  by (auto simp: AE_measure_pmf_iff Pi_iff space_subprob_algebra subprob_space_measure_pmf
                 sets_bind[where N="count_space UNIV"] emeasure_bind[where N="count_space UNIV"]
           intro!: nn_integral_cong_AE measure_eqI)

lemma bind_pmf_cong_simp:
  "p = q \ (\x. x \ set_pmf q =simp=> f x = g x) \ bind_pmf p f = bind_pmf q g"
  by (simp add: simp_implies_def cong: bind_pmf_cong)

lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \ (\x. measure_pmf (f x)))"
  by transfer simp

lemma nn_integral_bind_pmf[simp]: "(\\<^sup>+x. f x \bind_pmf M N) = (\\<^sup>+x. \\<^sup>+y. f y \N x \M)"
  using measurable_measure_pmf[of N]
  unfolding measure_pmf_bind
  apply (intro nn_integral_bind[where B="count_space UNIV"])
  apply auto
  done

lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\\<^sup>+x. emeasure (N x) X \M)"
  using measurable_measure_pmf[of N]
  unfolding measure_pmf_bind
  by (subst emeasure_bind[where N="count_space UNIV"]) auto

lift_definition return_pmf :: "'a \ 'a pmf" is "return (count_space UNIV)"
  by (auto intro!: prob_space_return simp: AE_return measure_return)

lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x"
  by transfer
     (auto intro!: prob_space_imp_subprob_space bind_return[where N="count_space UNIV"]
           simp: space_subprob_algebra)

lemma set_return_pmf[simp]: "set_pmf (return_pmf x) = {x}"
  by transfer (auto simp add: measure_return split: split_indicator)

lemma bind_return_pmf': "bind_pmf N return_pmf = N"
proof (transfer, clarify)
  fix N :: "'a measure" assume "sets N = UNIV" then show "N \ return (count_space UNIV) = N"
    by (subst return_sets_cong[where N=N]) (simp_all add: bind_return')
qed

lemma bind_assoc_pmf: "bind_pmf (bind_pmf A B) C = bind_pmf A (\x. bind_pmf (B x) C)"
  by transfer
     (auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"]
           simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space)

definition "map_pmf f M = bind_pmf M (\x. return_pmf (f x))"

lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\x. map_pmf f (g x))"
  by (simp add: map_pmf_def bind_assoc_pmf)

lemma bind_map_pmf: "bind_pmf (map_pmf f M) g = bind_pmf M (\x. g (f x))"
  by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf)

lemma map_pmf_transfer[transfer_rule]:
  "rel_fun (=) (rel_fun cr_pmf cr_pmf) (\f M. distr M (count_space UNIV) f) map_pmf"
proof -
  have "rel_fun (=) (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf)
     (\<lambda>f M. M \<bind> (return (count_space UNIV) o f)) map_pmf"
    unfolding map_pmf_def[abs_def] comp_def by transfer_prover
  then show ?thesis
    by (force simp: rel_fun_def cr_pmf_def bind_return_distr)
qed

lemma map_pmf_rep_eq:
  "measure_pmf (map_pmf f M) = distr (measure_pmf M) (count_space UNIV) f"
  unfolding map_pmf_def bind_pmf.rep_eq comp_def return_pmf.rep_eq
  using bind_return_distr[of M f "count_space UNIV"] by (simp add: comp_def)

lemma map_pmf_id[simp]: "map_pmf id = id"
  by (rule, transfer) (auto simp: emeasure_distr measurable_def intro!: measure_eqI)

lemma map_pmf_ident[simp]: "map_pmf (\x. x) = (\x. x)"
  using map_pmf_id unfolding id_def .

lemma map_pmf_compose: "map_pmf (f \ g) = map_pmf f \ map_pmf g"
  by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def)

lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\x. f (g x)) M"
  using map_pmf_compose[of f g] by (simp add: comp_def)

lemma map_pmf_cong: "p = q \ (\x. x \ set_pmf q \ f x = g x) \ map_pmf f p = map_pmf g q"
  unfolding map_pmf_def by (rule bind_pmf_cong) auto

lemma pmf_set_map: "set_pmf \ map_pmf f = (`) f \ set_pmf"
  by (auto simp add: comp_def fun_eq_iff map_pmf_def)

lemma set_map_pmf[simp]: "set_pmf (map_pmf f M) = f`set_pmf M"
  using pmf_set_map[of f] by (auto simp: comp_def fun_eq_iff)

lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
  unfolding map_pmf_rep_eq by (subst emeasure_distr) auto

lemma measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f -` X)"
using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure measure_nonneg)

lemma nn_integral_map_pmf[simp]: "(\\<^sup>+x. f x \map_pmf g M) = (\\<^sup>+x. f (g x) \M)"
  unfolding map_pmf_rep_eq by (intro nn_integral_distr) auto

lemma ennreal_pmf_map: "pmf (map_pmf f p) x = (\\<^sup>+ y. indicator (f -` {x}) y \measure_pmf p)"
proof (transfer fixing: f x)
  fix p :: "'b measure"
  presume "prob_space p"
  then interpret prob_space p .
  presume "sets p = UNIV"
  then show "ennreal (measure (distr p (count_space UNIV) f) {x}) = integral\<^sup>N p (indicator (f -` {x}))"
    by(simp add: measure_distr measurable_def emeasure_eq_measure)
qed simp_all

lemma pmf_map: "pmf (map_pmf f p) x = measure p (f -` {x})"
proof (transfer fixing: f x)
  fix p :: "'b measure"
  presume "prob_space p"
  then interpret prob_space p .
  presume "sets p = UNIV"
  then show "measure (distr p (count_space UNIV) f) {x} = measure p (f -` {x})"
    by(simp add: measure_distr measurable_def emeasure_eq_measure)
qed simp_all

lemma nn_integral_pmf: "(\\<^sup>+ x. pmf p x \count_space A) = emeasure (measure_pmf p) A"
proof -
  have "(\\<^sup>+ x. pmf p x \count_space A) = (\\<^sup>+ x. pmf p x \count_space (A \ set_pmf p))"
    by(auto simp add: nn_integral_count_space_indicator indicator_def set_pmf_iff intro: nn_integral_cong)
  also have "\ = emeasure (measure_pmf p) (\x\A \ set_pmf p. {x})"
    by(subst emeasure_UN_countable)(auto simp add: emeasure_pmf_single disjoint_family_on_def)
  also have "\ = emeasure (measure_pmf p) ((\x\A \ set_pmf p. {x}) \ {x. x \ A \ x \ set_pmf p})"
    by(rule emeasure_Un_null_set[symmetric])(auto intro: in_null_sets_measure_pmfI)
  also have "\ = emeasure (measure_pmf p) A"
    by(auto intro: arg_cong2[where f=emeasure])
  finally show ?thesis .
qed

lemma integral_map_pmf[simp]:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  shows "integral\<^sup>L (map_pmf g p) f = integral\<^sup>L p (\x. f (g x))"
  by (simp add: integral_distr map_pmf_rep_eq)

lemma integrable_map_pmf_eq [simp]:
  fixes g :: "'a \ 'b::{banach, second_countable_topology}"
  shows "integrable (map_pmf f p) g \ integrable (measure_pmf p) (\x. g (f x))"
  by (subst map_pmf_rep_eq, subst integrable_distr_eq) auto

lemma integrable_map_pmf [intro]:
  fixes g :: "'a \ 'b::{banach, second_countable_topology}"
  shows "integrable (measure_pmf p) (\x. g (f x)) \ integrable (map_pmf f p) g"
  by (subst integrable_map_pmf_eq)

lemma pmf_abs_summable [intro]: "pmf p abs_summable_on A"
  by (rule abs_summable_on_subset[OF _ subset_UNIV])
     (auto simp:  abs_summable_on_def integrable_iff_bounded nn_integral_pmf)

lemma measure_pmf_conv_infsetsum: "measure (measure_pmf p) A = infsetsum (pmf p) A"
  unfolding infsetsum_def by (simp add: integral_eq_nn_integral nn_integral_pmf measure_def)

lemma infsetsum_pmf_eq_1:
  assumes "set_pmf p \ A"
  shows   "infsetsum (pmf p) A = 1"
proof -
  have "infsetsum (pmf p) A = lebesgue_integral (count_space UNIV) (pmf p)"
    using assms unfolding infsetsum_altdef set_lebesgue_integral_def
    by (intro Bochner_Integration.integral_cong) (auto simp: indicator_def set_pmf_eq)
  also have "\ = 1"
    by (subst integral_eq_nn_integral) (auto simp: nn_integral_pmf)
  finally show ?thesis .
qed

lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)"
  by transfer (simp add: distr_return)

lemma map_pmf_const[simp]: "map_pmf (\_. c) M = return_pmf c"
  by transfer (auto simp: prob_space.distr_const)

lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x"
  by transfer (simp add: measure_return)

lemma nn_integral_return_pmf[simp]: "0 \ f x \ (\\<^sup>+x. f x \return_pmf x) = f x"
  unfolding return_pmf.rep_eq by (intro nn_integral_return) auto

lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x"
  unfolding return_pmf.rep_eq by (intro emeasure_return) auto

lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x"
proof -
  have "ennreal (measure_pmf.prob (return_pmf x) A) =
          emeasure (measure_pmf (return_pmf x)) A"
    by (simp add: measure_pmf.emeasure_eq_measure)
  also have "\ = ennreal (indicator A x)" by (simp add: ennreal_indicator)
  finally show ?thesis by simp
qed

lemma return_pmf_inj[simp]: "return_pmf x = return_pmf y \ x = y"
  by (metis insertI1 set_return_pmf singletonD)

lemma map_pmf_eq_return_pmf_iff:
  "map_pmf f p = return_pmf x \ (\y \ set_pmf p. f y = x)"
proof
  assume "map_pmf f p = return_pmf x"
  then have "set_pmf (map_pmf f p) = set_pmf (return_pmf x)" by simp
  then show "\y \ set_pmf p. f y = x" by auto
next
  assume "\y \ set_pmf p. f y = x"
  then show "map_pmf f p = return_pmf x"
    unfolding map_pmf_const[symmetric, of _ p] by (intro map_pmf_cong) auto
qed

definition "pair_pmf A B = bind_pmf A (\x. bind_pmf B (\y. return_pmf (x, y)))"

lemma pmf_pair: "pmf (pair_pmf M N) (a, b) = pmf M a * pmf N b"
  unfolding pair_pmf_def pmf_bind pmf_return
  apply (subst integral_measure_pmf_real[where A="{b}"])
  apply (auto simp: indicator_eq_0_iff)
  apply (subst integral_measure_pmf_real[where A="{a}"])
  apply (auto simp: indicator_eq_0_iff sum_nonneg_eq_0_iff pmf_nonneg)
  done

lemma set_pair_pmf[simp]: "set_pmf (pair_pmf A B) = set_pmf A \ set_pmf B"
  unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto

lemma measure_pmf_in_subprob_space[measurable (raw)]:
  "measure_pmf M \ space (subprob_algebra (count_space UNIV))"
  by (simp add: space_subprob_algebra) intro_locales

lemma nn_integral_pair_pmf': "(\\<^sup>+x. f x \pair_pmf A B) = (\\<^sup>+a. \\<^sup>+b. f (a, b) \B \A)"
proof -
  have "(\\<^sup>+x. f x \pair_pmf A B) = (\\<^sup>+x. f x * indicator (A \ B) x \pair_pmf A B)"
    by (auto simp: AE_measure_pmf_iff intro!: nn_integral_cong_AE)
  also have "\ = (\\<^sup>+a. \\<^sup>+b. f (a, b) * indicator (A \ B) (a, b) \B \A)"
    by (simp add: pair_pmf_def)
  also have "\ = (\\<^sup>+a. \\<^sup>+b. f (a, b) \B \A)"
    by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
  finally show ?thesis .
qed

lemma bind_pair_pmf:
  assumes M[measurable]: "M \ measurable (count_space UNIV \\<^sub>M count_space UNIV) (subprob_algebra N)"
  shows "measure_pmf (pair_pmf A B) \ M = (measure_pmf A \ (\x. measure_pmf B \ (\y. M (x, y))))"
    (is "?L = ?R")
proof (rule measure_eqI)
  have M'[measurable]: "M \ measurable (pair_pmf A B) (subprob_algebra N)"
    using M[THEN measurable_space] by (simp_all add: space_pair_measure)

  note measurable_bind[where N="count_space UNIV", measurable]
  note measure_pmf_in_subprob_space[simp]

  have sets_eq_N: "sets ?L = N"
    by (subst sets_bind[OF sets_kernel[OF M']]) auto
  show "sets ?L = sets ?R"
    using measurable_space[OF M]
    by (simp add: sets_eq_N space_pair_measure space_subprob_algebra)
  fix X assume "X \ sets ?L"
  then have X[measurable]: "X \ sets N"
    unfolding sets_eq_N .
  then show "emeasure ?L X = emeasure ?R X"
    apply (simp add: emeasure_bind[OF _ M' X])
    apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
                     nn_integral_measure_pmf_finite)
    apply (subst emeasure_bind[OF _ _ X])
    apply measurable
    apply (subst emeasure_bind[OF _ _ X])
    apply measurable
    done
qed

lemma map_fst_pair_pmf: "map_pmf fst (pair_pmf A B) = A"
  by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf')

lemma map_snd_pair_pmf: "map_pmf snd (pair_pmf A B) = B"
  by (simp add: pair_pmf_def map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf')

lemma nn_integral_pmf':
  "inj_on f A \ (\\<^sup>+x. pmf p (f x) \count_space A) = emeasure p (f ` A)"
  by (subst nn_integral_bij_count_space[where g=f and B="f`A"])
     (auto simp: bij_betw_def nn_integral_pmf)

lemma pmf_le_0_iff[simp]: "pmf M p \ 0 \ pmf M p = 0"
  using pmf_nonneg[of M p] by arith

lemma min_pmf_0[simp]: "min (pmf M p) 0 = 0" "min 0 (pmf M p) = 0"
  using pmf_nonneg[of M p] by arith+

lemma pmf_eq_0_set_pmf: "pmf M p = 0 \ p \ set_pmf M"
  unfolding set_pmf_iff by simp

lemma pmf_map_inj: "inj_on f (set_pmf M) \ x \ set_pmf M \ pmf (map_pmf f M) (f x) = pmf M x"
  by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD
           intro!: measure_pmf.finite_measure_eq_AE)

lemma pair_return_pmf [simp]: "pair_pmf (return_pmf x) (return_pmf y) = return_pmf (x, y)"
  by (auto simp: pair_pmf_def bind_return_pmf)

lemma pmf_map_inj': "inj f \ pmf (map_pmf f M) (f x) = pmf M x"
apply(cases "x \ set_pmf M")
apply(simp add: pmf_map_inj[OF inj_on_subset])
apply(simp add: pmf_eq_0_set_pmf[symmetric])
apply(auto simp add: pmf_eq_0_set_pmf dest: injD)
done

lemma expectation_pair_pmf_fst [simp]:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  shows "measure_pmf.expectation (pair_pmf p q) (\x. f (fst x)) = measure_pmf.expectation p f"
proof -
  have "measure_pmf.expectation (pair_pmf p q) (\x. f (fst x)) =
          measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f" by simp
  also have "map_pmf fst (pair_pmf p q) = p"
    by (simp add: map_fst_pair_pmf)
  finally show ?thesis .
qed

lemma expectation_pair_pmf_snd [simp]:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  shows "measure_pmf.expectation (pair_pmf p q) (\x. f (snd x)) = measure_pmf.expectation q f"
proof -
  have "measure_pmf.expectation (pair_pmf p q) (\x. f (snd x)) =
          measure_pmf.expectation (map_pmf snd (pair_pmf p q)) f" by simp
  also have "map_pmf snd (pair_pmf p q) = q"
    by (simp add: map_snd_pair_pmf)
  finally show ?thesis .
qed

lemma pmf_map_outside: "x \ f ` set_pmf M \ pmf (map_pmf f M) x = 0"
  unfolding pmf_eq_0_set_pmf by simp

lemma measurable_set_pmf[measurable]: "Measurable.pred (count_space UNIV) (\x. x \ set_pmf M)"
  by simp

subsection \<open> PMFs as function \<close>

context
  fixes f :: "'a \ real"
  assumes nonneg: "\x. 0 \ f x"
  assumes prob: "(\\<^sup>+x. f x \count_space UNIV) = 1"
begin

lift_definition embed_pmf :: "'a pmf" is "density (count_space UNIV) (ennreal \ f)"
proof (intro conjI)
  have *[simp]: "\x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y"
    by (simp split: split_indicator)
  show "AE x in density (count_space UNIV) (ennreal \ f).
    measure (density (count_space UNIV) (ennreal \<circ> f)) {x} \<noteq> 0"
    by (simp add: AE_density nonneg measure_def emeasure_density max_def)
  show "prob_space (density (count_space UNIV) (ennreal \ f))"
    by standard (simp add: emeasure_density prob)
qed simp

lemma pmf_embed_pmf: "pmf embed_pmf x = f x"
proof transfer
  have *[simp]: "\x y. ennreal (f y) * indicator {x} y = ennreal (f x) * indicator {x} y"
    by (simp split: split_indicator)
  fix x show "measure (density (count_space UNIV) (ennreal \ f)) {x} = f x"
    by transfer (simp add: measure_def emeasure_density nonneg max_def)
qed

lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \ 0}"
by(auto simp add: set_pmf_eq pmf_embed_pmf)

end

lemma embed_pmf_transfer:
  "rel_fun (eq_onp (\f. (\x. 0 \ f x) \ (\\<^sup>+x. ennreal (f x) \count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\f. density (count_space UNIV) (ennreal \ f)) embed_pmf"
  by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer)

lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)"
proof (transfer, elim conjE)
  fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \ 0"
  assume "prob_space M" then interpret prob_space M .
  show "M = density (count_space UNIV) (\x. ennreal (measure M {x}))"
  proof (rule measure_eqI)
    fix A :: "'a set"
    have "(\\<^sup>+ x. ennreal (measure M {x}) * indicator A x \count_space UNIV) =
      (\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)"
      by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator)
    also have "\ = (\\<^sup>+ x. emeasure M {x} \count_space (A \ {x. measure M {x} \ 0}))"
      by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space)
    also have "\ = emeasure M (\x\(A \ {x. measure M {x} \ 0}). {x})"
      by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support)
         (auto simp: disjoint_family_on_def)
    also have "\ = emeasure M A"
      using ae by (intro emeasure_eq_AE) auto
    finally show " emeasure M A = emeasure (density (count_space UNIV) (\x. ennreal (measure M {x}))) A"
      using emeasure_space_1 by (simp add: emeasure_density)
  qed simp
qed

lemma td_pmf_embed_pmf:
  "type_definition pmf embed_pmf {f::'a \ real. (\x. 0 \ f x) \ (\\<^sup>+x. ennreal (f x) \count_space UNIV) = 1}"
  unfolding type_definition_def
proof safe
  fix p :: "'a pmf"
  have "(\\<^sup>+ x. 1 \measure_pmf p) = 1"
    using measure_pmf.emeasure_space_1[of p] by simp
  then show *: "(\\<^sup>+ x. ennreal (pmf p x) \count_space UNIV) = 1"
    by (simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg del: nn_integral_const)

  show "embed_pmf (pmf p) = p"
    by (intro measure_pmf_inject[THEN iffD1])
       (simp add: * embed_pmf.rep_eq pmf_nonneg measure_pmf_eq_density[of p] comp_def)
next
  fix f :: "'a \ real" assume "\x. 0 \ f x" "(\\<^sup>+x. f x \count_space UNIV) = 1"
  then show "pmf (embed_pmf f) = f"
    by (auto intro!: pmf_embed_pmf)
qed (rule pmf_nonneg)

end

lemma nn_integral_measure_pmf: "(\\<^sup>+ x. f x \measure_pmf p) = \\<^sup>+ x. ennreal (pmf p x) * f x \count_space UNIV"
by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg)

lemma integral_measure_pmf:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  assumes A: "finite A"
  shows "(\a. a \ set_pmf M \ f a \ 0 \ a \ A) \ (LINT x|M. f x) = (\a\A. pmf M a *\<^sub>R f a)"
  unfolding measure_pmf_eq_density
  apply (simp add: integral_density)
  apply (subst lebesgue_integral_count_space_finite_support)
  apply (auto intro!: finite_subset[OF _ \<open>finite A\<close>] sum.mono_neutral_left simp: pmf_eq_0_set_pmf)
  done

lemma expectation_return_pmf [simp]:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  shows "measure_pmf.expectation (return_pmf x) f = f x"
  by (subst integral_measure_pmf[of "{x}"]) simp_all

lemma pmf_expectation_bind:
  fixes p :: "'a pmf" and f :: "'a \ 'b pmf"
    and  h :: "'b \ 'c::{banach, second_countable_topology}"
  assumes "finite A" "\x. x \ A \ finite (set_pmf (f x))" "set_pmf p \ A"
  shows "measure_pmf.expectation (p \ f) h =
           (\<Sum>a\<in>A. pmf p a *\<^sub>R measure_pmf.expectation (f a) h)"
proof -
  have "measure_pmf.expectation (p \ f) h = (\a\(\x\A. set_pmf (f x)). pmf (p \ f) a *\<^sub>R h a)"
    using assms by (intro integral_measure_pmf) auto
  also have "\ = (\x\(\x\A. set_pmf (f x)). (\a\A. (pmf p a * pmf (f a) x) *\<^sub>R h x))"
  proof (intro sum.cong refl, goal_cases)
    case (1 x)
    thus ?case
      by (subst pmf_bind, subst integral_measure_pmf[of A])
         (insert assms, auto simp: scaleR_sum_left)
  qed
  also have "\ = (\j\A. pmf p j *\<^sub>R (\i\(\x\A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))"
    by (subst sum.swap) (simp add: scaleR_sum_right)
  also have "\ = (\j\A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)"
  proof (intro sum.cong refl, goal_cases)
    case (1 x)
    thus ?case
      by (subst integral_measure_pmf[of "(\x\A. set_pmf (f x))"])
         (insert assms, auto simp: scaleR_sum_left)
  qed
  finally show ?thesis .
qed

lemma continuous_on_LINT_pmf: \<comment> \<open>This is dominated convergence!?\<close>
  fixes f :: "'i \ 'a::topological_space \ 'b::{banach, second_countable_topology}"
  assumes f: "\i. i \ set_pmf M \ continuous_on A (f i)"
    and bnd: "\a i. a \ A \ i \ set_pmf M \ norm (f i a) \ B"
  shows "continuous_on A (\a. LINT i|M. f i a)"
proof cases
  assume "finite M" with f show ?thesis
    using integral_measure_pmf[OF \<open>finite M\<close>]
    by (subst integral_measure_pmf[OF \<open>finite M\<close>])
       (auto intro!: continuous_on_sum continuous_on_scaleR continuous_on_const)
next
  assume "infinite M"
  let ?f = "\i x. pmf (map_pmf (to_nat_on M) M) i *\<^sub>R f (from_nat_into M i) x"

  show ?thesis
  proof (rule uniform_limit_theorem)
    show "\\<^sub>F n in sequentially. continuous_on A (\a. \i
      by (intro always_eventually allI continuous_on_sum continuous_on_scaleR continuous_on_const f
                from_nat_into set_pmf_not_empty)
    show "uniform_limit A (\n a. \ia. LINT i|M. f i a) sequentially"
    proof (subst uniform_limit_cong[where g="\n a. \i
      fix a assume "a \ A"
      have 1: "(LINT i|M. f i a) = (LINT i|map_pmf (to_nat_on M) M. f (from_nat_into M i) a)"
        by (auto intro!: integral_cong_AE AE_pmfI)
      have 2: "\ = (LINT i|count_space UNIV. pmf (map_pmf (to_nat_on M) M) i *\<^sub>R f (from_nat_into M i) a)"
        by (simp add: measure_pmf_eq_density integral_density)
      have "(\n. ?f n a) sums (LINT i|M. f i a)"
        unfolding 1 2
      proof (intro sums_integral_count_space_nat)
        have A: "integrable M (\i. f i a)"
          using \<open>a\<in>A\<close> by (auto intro!: measure_pmf.integrable_const_bound AE_pmfI bnd)
        have "integrable (map_pmf (to_nat_on M) M) (\i. f (from_nat_into M i) a)"
          by (auto simp add: map_pmf_rep_eq integrable_distr_eq intro!: AE_pmfI integrable_cong_AE_imp[OF A])
        then show "integrable (count_space UNIV) (\n. ?f n a)"
          by (simp add: measure_pmf_eq_density integrable_density)
      qed
      then show "(LINT i|M. f i a) = (\ n. ?f n a)"
        by (simp add: sums_unique)
    next
      show "uniform_limit A (\n a. \ia. (\ n. ?f n a)) sequentially"
      proof (rule Weierstrass_m_test)
        fix n a assume "a\A"
        then show "norm (?f n a) \ pmf (map_pmf (to_nat_on M) M) n * B"
          using bnd by (auto intro!: mult_mono simp: from_nat_into set_pmf_not_empty)
      next
        have "integrable (map_pmf (to_nat_on M) M) (\n. B)"
          by auto
        then show "summable (\n. pmf (map_pmf (to_nat_on (set_pmf M)) M) n * B)"
          by (fastforce simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_mult2)
      qed
    qed simp
  qed simp
qed

lemma continuous_on_LBINT:
  fixes f :: "real \ real"
  assumes f: "\b. a \ b \ set_integrable lborel {a..b} f"
  shows "continuous_on UNIV (\b. LBINT x:{a..b}. f x)"
proof (subst set_borel_integral_eq_integral)
  { fix b :: real assume "a \ b"
    from f[OF this] have "continuous_on {a..b} (\b. integral {a..b} f)"
      by (intro indefinite_integral_continuous_1 set_borel_integral_eq_integral) }
  note * = this

  have "continuous_on (\b\{a..}. {a <..< b}) (\b. integral {a..b} f)"
  proof (intro continuous_on_open_UN)
    show "b \ {a..} \ continuous_on {a<..b. integral {a..b} f)" for b
      using *[of b] by (rule continuous_on_subset) auto
  qed simp
  also have "(\b\{a..}. {a <..< b}) = {a <..}"
    by (auto simp: lt_ex gt_ex less_imp_le) (simp add: Bex_def less_imp_le gt_ex cong: rev_conj_cong)
  finally have "continuous_on {a+1 ..} (\b. integral {a..b} f)"
    by (rule continuous_on_subset) auto
  moreover have "continuous_on {a..a+1} (\b. integral {a..b} f)"
    by (rule *) simp
  moreover
  have "x \ a \ {a..x} = (if a = x then {a} else {})" for x
    by auto
  then have "continuous_on {..a} (\b. integral {a..b} f)"
    by (subst continuous_on_cong[OF refl, where g="\x. 0"]) (auto intro!: continuous_on_const)
  ultimately have "continuous_on ({..a} \ {a..a+1} \ {a+1 ..}) (\b. integral {a..b} f)"
    by (intro continuous_on_closed_Un) auto
  also have "{..a} \ {a..a+1} \ {a+1 ..} = UNIV"
    by auto
  finally show "continuous_on UNIV (\b. integral {a..b} f)"
    by auto
next
  show "set_integrable lborel {a..b} f" for b
    using f by (cases "a \ b") auto
qed

locale pmf_as_function
begin

setup_lifting td_pmf_embed_pmf

lemma set_pmf_transfer[transfer_rule]:
  assumes "bi_total A"
  shows "rel_fun (pcr_pmf A) (rel_set A) (\f. {x. f x \ 0}) set_pmf"
  using \<open>bi_total A\<close>
  by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
     metis+

end

context
begin

interpretation pmf_as_function .

lemma pmf_eqI: "(\i. pmf M i = pmf N i) \ M = N"
  by transfer auto

lemma pmf_eq_iff: "M = N \ (\i. pmf M i = pmf N i)"
  by (auto intro: pmf_eqI)

lemma pmf_neq_exists_less:
  assumes "M \ N"
  shows   "\x. pmf M x < pmf N x"
proof (rule ccontr)
  assume "\(\x. pmf M x < pmf N x)"
  hence ge: "pmf M x \ pmf N x" for x by (auto simp: not_less)
  from assms obtain x where "pmf M x \ pmf N x" by (auto simp: pmf_eq_iff)
  with ge[of x] have gt: "pmf M x > pmf N x" by simp
  have "1 = measure (measure_pmf M) UNIV" by simp
  also have "\ = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})"
    by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
  also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}"
    by (simp add: measure_pmf_single)
  also have "measure (measure_pmf N) (UNIV - {x}) \ measure (measure_pmf M) (UNIV - {x})"
    by (subst (1 2) integral_pmf [symmetric])
       (intro integral_mono integrable_pmf, simp_all add: ge)
  also have "measure (measure_pmf M) {x} + \ = 1"
    by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
  finally show False by simp_all
qed

lemma bind_commute_pmf: "bind_pmf A (\x. bind_pmf B (C x)) = bind_pmf B (\y. bind_pmf A (\x. C x y))"
  unfolding pmf_eq_iff pmf_bind
proof
  fix i
  interpret B: prob_space "restrict_space B B"
    by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE)
       (auto simp: AE_measure_pmf_iff)
  interpret A: prob_space "restrict_space A A"
    by (intro prob_space_restrict_space measure_pmf.emeasure_eq_1_AE)
       (auto simp: AE_measure_pmf_iff)

  interpret AB: pair_prob_space "restrict_space A A" "restrict_space B B"
    by unfold_locales

  have "(\ x. \ y. pmf (C x y) i \B \A) = (\ x. (\ y. pmf (C x y) i \restrict_space B B) \A)"
    by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict)
  also have "\ = (\ x. (\ y. pmf (C x y) i \restrict_space B B) \restrict_space A A)"
    by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
              countable_set_pmf borel_measurable_count_space)
  also have "\ = (\ y. \ x. pmf (C x y) i \restrict_space A A \restrict_space B B)"
    by (rule AB.Fubini_integral[symmetric])
       (auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2
             simp: pmf_nonneg pmf_le_1 measurable_restrict_space1)
  also have "\ = (\ y. \ x. pmf (C x y) i \restrict_space A A \B)"
    by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
              countable_set_pmf borel_measurable_count_space)
  also have "\ = (\ y. \ x. pmf (C x y) i \A \B)"
    by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
  finally show "(\ x. \ y. pmf (C x y) i \B \A) = (\ y. \ x. pmf (C x y) i \A \B)" .
qed

lemma pair_map_pmf1: "pair_pmf (map_pmf f A) B = map_pmf (apfst f) (pair_pmf A B)"
proof (safe intro!: pmf_eqI)
  fix a :: "'a" and b :: "'b"
  have [simp]: "\c d. indicator (apfst f -` {(a, b)}) (c, d) = indicator (f -` {a}) c * (indicator {b} d::ennreal)"
    by (auto split: split_indicator)

  have "ennreal (pmf (pair_pmf (map_pmf f A) B) (a, b)) =
         ennreal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))"
    unfolding pmf_pair ennreal_pmf_map
    by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg
                  emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf)
  then show "pmf (pair_pmf (map_pmf f A) B) (a, b) = pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b)"
    by (simp add: pmf_nonneg)
qed

lemma pair_map_pmf2: "pair_pmf A (map_pmf f B) = map_pmf (apsnd f) (pair_pmf A B)"
proof (safe intro!: pmf_eqI)
  fix a :: "'a" and b :: "'b"
  have [simp]: "\c d. indicator (apsnd f -` {(a, b)}) (c, d) = indicator {a} c * (indicator (f -` {b}) d::ennreal)"
    by (auto split: split_indicator)

  have "ennreal (pmf (pair_pmf A (map_pmf f B)) (a, b)) =
         ennreal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))"
    unfolding pmf_pair ennreal_pmf_map
    by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg
                  emeasure_map_pmf[symmetric] ennreal_mult del: emeasure_map_pmf)
  then show "pmf (pair_pmf A (map_pmf f B)) (a, b) = pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b)"
    by (simp add: pmf_nonneg)
qed

lemma map_pair: "map_pmf (\(a, b). (f a, g b)) (pair_pmf A B) = pair_pmf (map_pmf f A) (map_pmf g B)"
  by (simp add: pair_map_pmf2 pair_map_pmf1 map_pmf_comp split_beta')

end

lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y"
by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)

lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\x. (x, y)) x"
by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)

lemma pair_pair_pmf: "pair_pmf (pair_pmf u v) w = map_pmf (\(x, (y, z)). ((x, y), z)) (pair_pmf u (pair_pmf v w))"
by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf)

lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\(x, y). (y, x)) (pair_pmf y x)"
unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf)

lemma set_pmf_subset_singleton: "set_pmf p \ {x} \ p = return_pmf x"
proof(intro iffI pmf_eqI)
  fix i
  assume x: "set_pmf p \ {x}"
  hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto
  have "ennreal (pmf p x) = \\<^sup>+ i. indicator {x} i \p" by(simp add: emeasure_pmf_single)
  also have "\ = \\<^sup>+ i. 1 \p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
  also have "\ = 1" by simp
  finally show "pmf p i = pmf (return_pmf x) i" using x
    by(auto split: split_indicator simp add: pmf_eq_0_set_pmf)
qed auto

lemma bind_eq_return_pmf:
  "bind_pmf p f = return_pmf x \ (\y\set_pmf p. f y = return_pmf x)"
  (is "?lhs \ ?rhs")
proof(intro iffI strip)
  fix y
  assume y: "y \ set_pmf p"
  assume "?lhs"
  hence "set_pmf (bind_pmf p f) = {x}" by simp
  hence "(\y\set_pmf p. set_pmf (f y)) = {x}" by simp
  hence "set_pmf (f y) \ {x}" using y by auto
  thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton)
next
  assume *: ?rhs
  show ?lhs
  proof(rule pmf_eqI)
    fix i
    have "ennreal (pmf (bind_pmf p f) i) = \\<^sup>+ y. ennreal (pmf (f y) i) \p"
      by (simp add: ennreal_pmf_bind)
    also have "\ = \\<^sup>+ y. ennreal (pmf (return_pmf x) i) \p"
      by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
    also have "\ = ennreal (pmf (return_pmf x) i)"
      by simp
    finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i"
      by (simp add: pmf_nonneg)
  qed
qed

lemma pmf_False_conv_True: "pmf p False = 1 - pmf p True"
proof -
  have "pmf p False + pmf p True = measure p {False} + measure p {True}"
    by(simp add: measure_pmf_single)
  also have "\ = measure p ({False} \ {True})"
    by(subst measure_pmf.finite_measure_Union) simp_all
  also have "{False} \ {True} = space p" by auto
  finally show ?thesis by simp
qed

lemma pmf_True_conv_False: "pmf p True = 1 - pmf p False"
by(simp add: pmf_False_conv_True)

subsection \<open> Conditional Probabilities \<close>

lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \ set_pmf p \ s = {}"
  by (subst measure_pmf.prob_eq_0) (auto simp: AE_measure_pmf_iff)

context
  fixes p :: "'a pmf" and s :: "'a set"
  assumes not_empty: "set_pmf p \ s \ {}"
begin

interpretation pmf_as_measure .

lemma emeasure_measure_pmf_not_zero: "emeasure (measure_pmf p) s \ 0"
proof
  assume "emeasure (measure_pmf p) s = 0"
  then have "AE x in measure_pmf p. x \ s"
    by (rule AE_I[rotated]) auto
  with not_empty show False
    by (auto simp: AE_measure_pmf_iff)
qed

lemma measure_measure_pmf_not_zero: "measure (measure_pmf p) s \ 0"
  using emeasure_measure_pmf_not_zero by (simp add: measure_pmf.emeasure_eq_measure measure_nonneg)

lift_definition cond_pmf :: "'a pmf" is
  "uniform_measure (measure_pmf p) s"
proof (intro conjI)
  show "prob_space (uniform_measure (measure_pmf p) s)"
    by (intro prob_space_uniform_measure) (auto simp: emeasure_measure_pmf_not_zero)
  show "AE x in uniform_measure (measure_pmf p) s. measure (uniform_measure (measure_pmf p) s) {x} \ 0"
    by (simp add: emeasure_measure_pmf_not_zero measure_measure_pmf_not_zero AE_uniform_measure
                  AE_measure_pmf_iff set_pmf.rep_eq less_top[symmetric])
qed simp

lemma pmf_cond: "pmf cond_pmf x = (if x \ s then pmf p x / measure p s else 0)"
  by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq)

lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \ s"
  by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: if_split_asm)

end

lemma measure_pmf_posI: "x \ set_pmf p \ x \ A \ measure_pmf.prob p A > 0"
  using measure_measure_pmf_not_zero[of p A] by (subst zero_less_measure_iff) blast

lemma cond_map_pmf:
  assumes "set_pmf p \ f -` s \ {}"
  shows "cond_pmf (map_pmf f p) s = map_pmf f (cond_pmf p (f -` s))"
proof -
  have *: "set_pmf (map_pmf f p) \ s \ {}"
    using assms by auto
  { fix x
    have "ennreal (pmf (map_pmf f (cond_pmf p (f -` s))) x) =
      emeasure p (f -` s \<inter> f -` {x}) / emeasure p (f -` s)"
      unfolding ennreal_pmf_map cond_pmf.rep_eq[OF assms] by (simp add: nn_integral_uniform_measure)
    also have "f -` s \ f -` {x} = (if x \ s then f -` {x} else {})"
      by auto
    also have "emeasure p (if x \ s then f -` {x} else {}) / emeasure p (f -` s) =
      ennreal (pmf (cond_pmf (map_pmf f p) s) x)"
      using measure_measure_pmf_not_zero[OF *]
      by (simp add: pmf_cond[OF *] ennreal_pmf_map measure_pmf.emeasure_eq_measure
                    divide_ennreal pmf_nonneg measure_nonneg zero_less_measure_iff pmf_map)
    finally have "ennreal (pmf (cond_pmf (map_pmf f p) s) x) = ennreal (pmf (map_pmf f (cond_pmf p (f -` s))) x)"
      by simp }
  then show ?thesis
    by (intro pmf_eqI) (simp add: pmf_nonneg)
qed

lemma bind_cond_pmf_cancel:
  assumes [simp]: "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}"
  assumes [simp]: "\y. y \ set_pmf q \ set_pmf p \ {x. R x y} \ {}"
  assumes [simp]: "\x y. x \ set_pmf p \ y \ set_pmf q \ R x y \ measure q {y. R x y} = measure p {x. R x y}"
  shows "bind_pmf p (\x. cond_pmf q {y. R x y}) = q"
proof (rule pmf_eqI)
  fix i
  have "ennreal (pmf (bind_pmf p (\x. cond_pmf q {y. R x y})) i) =
    (\<integral>\<^sup>+x. ennreal (pmf q i / measure p {x. R x i}) * ennreal (indicator {x. R x i} x) \<partial>p)"
    by (auto simp add: ennreal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf pmf_nonneg measure_nonneg
             intro!: nn_integral_cong_AE)
  also have "\ = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}"
    by (simp add: pmf_nonneg measure_nonneg zero_ennreal_def[symmetric] ennreal_indicator
                  nn_integral_cmult measure_pmf.emeasure_eq_measure ennreal_mult[symmetric])
  also have "\ = pmf q i"
    by (cases "pmf q i = 0")
       (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero pmf_nonneg)
  finally show "pmf (bind_pmf p (\x. cond_pmf q {y. R x y})) i = pmf q i"
    by (simp add: pmf_nonneg)
qed

subsection \<open> Relator \<close>

inductive rel_pmf :: "('a \ 'b \ bool) \ 'a pmf \ 'b pmf \ bool"
for R p q
where
  "\ \x y. (x, y) \ set_pmf pq \ R x y;
     map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
  \<Longrightarrow> rel_pmf R p q"

lemma rel_pmfI:
  assumes R: "rel_set R (set_pmf p) (set_pmf q)"
  assumes eq: "\x y. x \ set_pmf p \ y \ set_pmf q \ R x y \
    measure p {x. R x y} = measure q {y. R x y}"
  shows "rel_pmf R p q"
proof
  let ?pq = "bind_pmf p (\x. bind_pmf (cond_pmf q {y. R x y}) (\y. return_pmf (x, y)))"
  have "\x. x \ set_pmf p \ set_pmf q \ {y. R x y} \ {}"
    using R by (auto simp: rel_set_def)
  then show "\x y. (x, y) \ set_pmf ?pq \ R x y"
    by auto
  show "map_pmf fst ?pq = p"
    by (simp add: map_bind_pmf bind_return_pmf')

  show "map_pmf snd ?pq = q"
    using R eq
    apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf')
    apply (rule bind_cond_pmf_cancel)
    apply (auto simp: rel_set_def)
    done
qed

lemma rel_pmf_imp_rel_set: "rel_pmf R p q \ rel_set R (set_pmf p) (set_pmf q)"
  by (force simp add: rel_pmf.simps rel_set_def)

lemma rel_pmfD_measure:
  assumes rel_R: "rel_pmf R p q" and R: "\a b. R a b \ R a y \ R x b"
  assumes "x \ set_pmf p" "y \ set_pmf q"
  shows "measure p {x. R x y} = measure q {y. R x y}"
proof -
  from rel_R obtain pq where pq: "\x y. (x, y) \ set_pmf pq \ R x y"
    and eq: "p = map_pmf fst pq" "q = map_pmf snd pq"
    by (auto elim: rel_pmf.cases)
  have "measure p {x. R x y} = measure pq {x. R (fst x) y}"
    by (simp add: eq map_pmf_rep_eq measure_distr)
  also have "\ = measure pq {y. R x (snd y)}"
    by (intro measure_pmf.finite_measure_eq_AE)
       (auto simp: AE_measure_pmf_iff R dest!: pq)
  also have "\ = measure q {y. R x y}"
    by (simp add: eq map_pmf_rep_eq measure_distr)
  finally show "measure p {x. R x y} = measure q {y. R x y}" .
qed

lemma rel_pmf_measureD:
  assumes "rel_pmf R p q"
  shows "measure (measure_pmf p) A \ measure (measure_pmf q) {y. \x\A. R x y}" (is "?lhs \ ?rhs")
using assms
proof cases
  fix pq
  assume R: "\x y. (x, y) \ set_pmf pq \ R x y"
    and p[symmetric]: "map_pmf fst pq = p"
    and q[symmetric]: "map_pmf snd pq = q"
  have "?lhs = measure (measure_pmf pq) (fst -` A)" by(simp add: p)
  also have "\ \ measure (measure_pmf pq) {y. \x\A. R x (snd y)}"
    by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R)
  also have "\ = ?rhs" by(simp add: q)
  finally show ?thesis .
qed

lemma rel_pmf_iff_measure:
  assumes "symp R" "transp R"
  shows "rel_pmf R p q \
    rel_set R (set_pmf p) (set_pmf q) \<and>
    (\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y})"
  by (safe intro!: rel_pmf_imp_rel_set rel_pmfI)
     (auto intro!: rel_pmfD_measure dest: sympD[OF \<open>symp R\<close>] transpD[OF \<open>transp R\<close>])

lemma quotient_rel_set_disjoint:
  "equivp R \ C \ UNIV // {(x, y). R x y} \ rel_set R A B \ A \ C = {} \ B \ C = {}"
  using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C]
  by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE)
     (blast dest: equivp_symp)+

lemma quotientD: "equiv X R \ A \ X // R \ x \ A \ A = R `` {x}"
  by (metis Image_singleton_iff equiv_class_eq_iff quotientE)

lemma rel_pmf_iff_equivp:
  assumes "equivp R"
  shows "rel_pmf R p q \ (\C\UNIV // {(x, y). R x y}. measure p C = measure q C)"
    (is "_ \ (\C\_//?R. _)")
proof (subst rel_pmf_iff_measure, safe)
  show "symp R" "transp R"
    using assms by (auto simp: equivp_reflp_symp_transp)
next
  fix C assume C: "C \ UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)"
  assume eq: "\x\set_pmf p. \y\set_pmf q. R x y \ measure p {x. R x y} = measure q {y. R x y}"

  show "measure p C = measure q C"
  proof (cases "p \ C = {}")
    case True
    then have "q \ C = {}"
      using quotient_rel_set_disjoint[OF assms C R] by simp
    with True show ?thesis
      unfolding measure_pmf_zero_iff[symmetric] by simp
  next
    case False
    then have "q \ C \ {}"
      using quotient_rel_set_disjoint[OF assms C R] by simp
    with False obtain x y where in_set: "x \ set_pmf p" "y \ set_pmf q" and in_C: "x \ C" "y \ C"
      by auto
    then have "R x y"
      using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms
      by (simp add: equivp_equiv)
    with in_set eq have "measure p {x. R x y} = measure q {y. R x y}"
      by auto
    moreover have "{y. R x y} = C"
      using assms \<open>x \<in> C\<close> C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv)
    moreover have "{x. R x y} = C"
      using assms \<open>y \<in> C\<close> C quotientD[of UNIV "?R" C y] sympD[of R]
      by (auto simp add: equivp_equiv elim: equivpE)
    ultimately show ?thesis
      by auto
  qed
next
  assume eq: "\C\UNIV // ?R. measure p C = measure q C"
  show "rel_set R (set_pmf p) (set_pmf q)"
    unfolding rel_set_def
  proof safe
    fix x assume x: "x \ set_pmf p"
    have "{y. R x y} \ UNIV // ?R"
      by (auto simp: quotient_def)
    with eq have *: "measure q {y. R x y} = measure p {y. R x y}"
      by auto
    have "measure q {y. R x y} \ 0"
      using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
    then show "\y\set_pmf q. R x y"
      unfolding measure_pmf_zero_iff by auto
  next
    fix y assume y: "y \ set_pmf q"
    have "{x. R x y} \ UNIV // ?R"
      using assms by (auto simp: quotient_def dest: equivp_symp)
    with eq have *: "measure p {x. R x y} = measure q {x. R x y}"
      by auto
    have "measure p {x. R x y} \ 0"
      using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
    then show "\x\set_pmf p. R x y"
      unfolding measure_pmf_zero_iff by auto
  qed

  fix x y assume "x \ set_pmf p" "y \ set_pmf q" "R x y"
  have "{y. R x y} \ UNIV // ?R" "{x. R x y} = {y. R x y}"
    using assms \<open>R x y\<close> by (auto simp: quotient_def dest: equivp_symp equivp_transp)
  with eq show "measure p {x. R x y} = measure q {y. R x y}"
    by auto
qed

bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "card_suc natLeq" rel: rel_pmf
proof -
  show "map_pmf id = id" by (rule map_pmf_id)
  show "\f g. map_pmf (f \ g) = map_pmf f \ map_pmf g" by (rule map_pmf_compose)
  show "\f g::'a \ 'b. \p. (\x. x \ set_pmf p \ f x = g x) \ map_pmf f p = map_pmf g p"
    by (intro map_pmf_cong refl)

  show "\f::'a \ 'b. set_pmf \ map_pmf f = (`) f \ set_pmf"
    by (rule pmf_set_map)

  show "card_order (card_suc natLeq)" using natLeq_card_order by (rule card_order_card_suc)
  show "BNF_Cardinal_Arithmetic.cinfinite (card_suc natLeq)"
    using natLeq_Cinfinite natLeq_card_order Cinfinite_card_suc by blast
  show "regularCard (card_suc natLeq)" using natLeq_card_order natLeq_Cinfinite
    by (rule regularCard_card_suc)

  show "(card_of (set_pmf p), card_suc natLeq) \ ordLess" for p :: "'s pmf"
  proof -
    have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \ ordLeq"
      by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"])
         (auto intro: countable_set_pmf)
    also have "(card_of (UNIV :: nat set), natLeq) \ ordLeq"
      by (metis Field_natLeq card_of_least natLeq_Well_order)
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ 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.0.16Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

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.