Theory HOL-Probability.Probability_Measure

(*  Title:      HOL/Probability/Probability_Measure.thy
    Author:     Johannes Hölzl, TU München
    Author:     Armin Heller, TU München
*)

section ‹Probability measure›

theory Probability_Measure
  imports "HOL-Analysis.Analysis"
begin

locale prob_space = finite_measure +
  assumes emeasure_space_1: "emeasure M (space M) = 1"

lemma prob_spaceI[Pure.intro!]:
  assumes *: "emeasure M (space M) = 1"
  shows "prob_space M"
  by (simp add: assms finite_measureI prob_space_axioms.intro prob_space_def)

lemma prob_space_imp_sigma_finite: "prob_space M  sigma_finite_measure M"
  unfolding prob_space_def finite_measure_def by simp

abbreviation (in prob_space) "events  sets M"
abbreviation (in prob_space) "prob  measure M"
abbreviation (in prob_space) "random_variable M' X  X  measurable M M'"
abbreviation (in prob_space) "expectation  integralL M"
abbreviation (in prob_space) "variance X  integralL M (λx. (X x - expectation X)2)"

lemma (in prob_space) finite_measure [simp]: "finite_measure M"
  by unfold_locales

lemma (in prob_space) prob_space_distr:
  assumes f: "f  measurable M M'" shows "prob_space (distr M M' f)"
proof (rule prob_spaceI)
  have "f -` space M'  space M = space M" using f by (auto dest: measurable_space)
  with f show "emeasure (distr M M' f) (space (distr M M' f)) = 1"
    by (auto simp: emeasure_distr emeasure_space_1)
qed

lemma prob_space_distrD:
  assumes f: "f  measurable M N" and M: "prob_space (distr M N f)" shows "prob_space M"
proof
  interpret M: prob_space "distr M N f" by fact
  have "f -` space N  space M = space M"
    using f[THEN measurable_space] by auto
  then show "emeasure M (space M) = 1"
    using M.emeasure_space_1 by (simp add: emeasure_distr[OF f])
qed

lemma (in prob_space) prob_space: "prob (space M) = 1"
  by (simp add: emeasure_space_1 measure_eq_emeasure_eq_ennreal)

lemma (in prob_space) prob_le_1[simp, intro]: "prob A  1"
  using bounded_measure[of A] by (simp add: prob_space)

lemma (in prob_space) not_empty: "space M  {}"
  using prob_space by auto

lemma (in prob_space) emeasure_eq_1_AE:
  "S  sets M  AE x in M. x  S  emeasure M S = 1"
  by (subst emeasure_eq_AE[where B="space M"]) (auto simp: emeasure_space_1)

lemma (in prob_space) emeasure_le_1: "emeasure M S  1"
  unfolding ennreal_1[symmetric] emeasure_eq_measure by (subst ennreal_le_iff) auto

lemma (in prob_space) emeasure_ge_1_iff: "emeasure M A  1  emeasure M A = 1"
  by (rule iffI, intro antisym emeasure_le_1) simp_all

lemma (in prob_space) AE_iff_emeasure_eq_1:
  assumes [measurable]: "Measurable.pred M P"
  shows "(AE x in M. P x)  emeasure M {xspace M. P x} = 1"
proof -
  have *: "{x  space M. ¬ P x} = space M - {xspace M. P x}"
    by auto
  show ?thesis
    by (auto simp add: ennreal_minus_eq_0 * emeasure_compl emeasure_space_1 AE_iff_measurable[OF _ refl]
             intro: antisym emeasure_le_1)
qed

lemma (in prob_space) measure_le_1: "emeasure M X  1"
  using emeasure_space[of M X] by (simp add: emeasure_space_1)

lemma (in prob_space) measure_ge_1_iff: "measure M A  1  measure M A = 1"
  by (auto intro!: antisym)

lemma (in prob_space) AE_I_eq_1:
  assumes "emeasure M {xspace M. P x} = 1" "{xspace M. P x}  sets M"
  shows "AE x in M. P x"
proof (rule AE_I)
  show "emeasure M (space M - {x  space M. P x}) = 0"
    using assms emeasure_space_1 by (simp add: emeasure_compl)
qed (insert assms, auto)

lemma prob_space_restrict_space:
  "S  sets M  emeasure M S = 1  prob_space (restrict_space M S)"
  by (intro prob_spaceI)
     (simp add: emeasure_restrict_space space_restrict_space)

lemma (in prob_space) prob_compl:
  assumes A: "A  events"
  shows "prob (space M - A) = 1 - prob A"
  using finite_measure_compl[OF A] by (simp add: prob_space)

lemma (in prob_space) AE_in_set_eq_1:
  assumes A[measurable]: "A  events" shows "(AE x in M. x  A)  prob A = 1"
proof -
  have *: "{xspace M. x  A} = A"
    using A[THEN sets.sets_into_space] by auto
  show ?thesis
    by (subst AE_iff_emeasure_eq_1) (auto simp: emeasure_eq_measure *)
qed

lemma (in prob_space) AE_False: "(AE x in M. False)  False"
proof
  assume "AE x in M. False"
  then have "AE x in M. x  {}" by simp
  then show False
    by (subst (asm) AE_in_set_eq_1) auto
qed simp

lemma (in prob_space) AE_prob_1:
  assumes "prob A = 1" shows "AE x in M. x  A"
proof -
  from prob A = 1 have "A  events"
    by (metis measure_notin_sets zero_neq_one)
  with AE_in_set_eq_1 assms show ?thesis by simp
qed

lemma (in prob_space) AE_const[simp]: "(AE x in M. P)  P"
  by (cases P) (auto simp: AE_False)

lemma (in prob_space) ae_filter_bot: "ae_filter M  bot"
  by (simp add: trivial_limit_def)

lemma (in prob_space) AE_contr:
  assumes ae: "AE ω in M. P ω" "AE ω in M. ¬ P ω"
  shows False
proof -
  from ae have "AE ω in M. False" by eventually_elim auto
  then show False by auto
qed

lemma (in prob_space) integral_ge_const:
  fixes c :: real
  shows "integrable M f  (AE x in M. c  f x)  c  (x. f x M)"
  using integral_mono_AE[of M "λx. c" f] prob_space by simp

lemma (in prob_space) integral_le_const:
  fixes c :: real
  shows "integrable M f  (AE x in M. f x  c)  (x. f x M)  c"
  using integral_mono_AE[of M f "λx. c"] prob_space by simp

lemma (in prob_space) nn_integral_ge_const:
  "(AE x in M. c  f x)  c  (+x. f x M)"
  using nn_integral_mono_AE[of "λx. c" f M] emeasure_space_1
  by (simp split: if_split_asm)

lemma (in prob_space) expectation_less:
  fixes X :: "_  real"
  assumes [simp]: "integrable M X"
  assumes gt: "AE x in M. X x < b"
  shows "expectation X < b"
proof -
  have "expectation X < expectation (λx. b)"
    using gt emeasure_space_1
    by (intro integral_less_AE_space) auto
  then show ?thesis using prob_space by simp
qed

lemma (in prob_space) expectation_greater:
  fixes X :: "_  real"
  assumes [simp]: "integrable M X"
  assumes gt: "AE x in M. a < X x"
  shows "a < expectation X"
proof -
  have "expectation (λx. a) < expectation X"
    using gt emeasure_space_1
    by (intro integral_less_AE_space) auto
  then show ?thesis using prob_space by simp
qed

lemma (in prob_space) jensens_inequality:
  fixes q :: "real  real"
  assumes X: "integrable M X" "AE x in M. X x  I"
  assumes I: "I = {a <..< b}  I = {a <..}  I = {..< b}  I = UNIV"
  assumes q: "integrable M (λx. q (X x))" "convex_on I q"
  shows "q (expectation X)  expectation (λx. q (X x))"
proof -
  let ?F = "λx. Inf ((λt. (q x - q t) / (x - t)) ` ({x<..}  I))"
  from X(2) AE_False have "I  {}" by auto

  from I have "open I" by auto

  note I
  moreover
  { assume "I  {a <..}"
    with X have "a < expectation X"
      by (intro expectation_greater) auto }
  moreover
  { assume "I  {..< b}"
    with X have "expectation X < b"
      by (intro expectation_less) auto }
  ultimately have "expectation X  I"
    by (elim disjE)  (auto simp: subset_eq)
  moreover
  { fix y assume y: "y  I"
    with q(2) open I have "Sup ((λx. q x + ?F x * (y - x)) ` I) = q y"
      by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open) }
  ultimately have "q (expectation X) = Sup ((λx. q x + ?F x * (expectation X - x)) ` I)"
    by simp
  also have "  expectation (λw. q (X w))"
  proof (rule cSup_least)
    show "(λx. q x + ?F x * (expectation X - x)) ` I  {}"
      using I  {} by auto
  next
    fix k assume "k  (λx. q x + ?F x * (expectation X - x)) ` I"
    then obtain x
      where x: "k = q x + (INF t{x<..}  I. (q x - q t) / (x - t)) * (expectation X - x)" "x  I" ..
    have "q x + ?F x * (expectation X  - x) = expectation (λw. q x + ?F x * (X w - x))"
      using prob_space by (simp add: X)
    also have "  expectation (λw. q (X w))"
      using x  I open I X(2)
      apply (intro integral_mono_AE Bochner_Integration.integrable_add Bochner_Integration.integrable_mult_right Bochner_Integration.integrable_diff
                integrable_const X q)
      apply (elim eventually_mono)
      apply (intro convex_le_Inf_differential)
      apply (auto simp: interior_open q)
      done
    finally show "k  expectation (λw. q (X w))" using x by auto
  qed
  finally show "q (expectation X)  expectation (λx. q (X x))" .
qed

lemma (in prob_space) finite_borel_measurable_integrable:
  assumes "f borel_measurable M"
  and "finite (f`(space M))"
  shows "integrable M f"
proof -
  have "simple_function M f" using assms by (simp add: simple_function_borel_measurable)
  moreover have "emeasure M {y  space M. f y  0}  " by simp
  ultimately have "Bochner_Integration.simple_bochner_integrable M f"
    using Bochner_Integration.simple_bochner_integrable.simps by blast
  hence "has_bochner_integral M f (Bochner_Integration.simple_bochner_integral M f)"
    using has_bochner_integral_simple_bochner_integrable by auto
  thus ?thesis using integrable.simps by auto
qed

subsection  ‹Introduce binder for probability›

syntax
  "_prob" :: "pttrn  logic  logic  logic" (('𝒫'((/_ in _./ _)')))

translations
  "𝒫(x in M. P)" => "CONST measure M {x  CONST space M. P}"

print_translation let
    fun to_pattern (Const (const_syntaxPair, _) $ l $ r) =
      Syntax.const const_syntaxPair :: to_pattern l @ to_pattern r
    | to_pattern (t as (Const (syntax_const‹_bound›, _)) $ _) = [t]

    fun mk_pattern ((t, n) :: xs) = mk_patterns n xs |>> curry list_comb t
    and mk_patterns 0 xs = ([], xs)
    | mk_patterns n xs =
      let
        val (t, xs') = mk_pattern xs
        val (ts, xs'') = mk_patterns (n - 1) xs'
      in
        (t :: ts, xs'')
      end

    fun unnest_tuples
      (Const (syntax_const‹_pattern›, _) $
        t1 $
        (t as (Const (syntax_const‹_pattern›, _) $ _ $ _)))
      = let
        val (_ $ t2 $ t3) = unnest_tuples t
      in
        Syntax.const syntax_const‹_pattern› $
          unnest_tuples t1 $
          (Syntax.const syntax_const‹_patterns› $ t2 $ t3)
      end
    | unnest_tuples pat = pat

    fun tr' [sig_alg, Const (const_syntaxCollect, _) $ t] =
      let
        val bound_dummyT = Const (syntax_const‹_bound›, dummyT)

        fun go pattern elem
          (Const (const_syntaxconj, _) $
            (Const (const_syntaxSet.member, _) $ elem' $ (Const (const_syntaxspace, _) $ sig_alg')) $
            u)
          = let
              val _ = if sig_alg aconv sig_alg' andalso to_pattern elem' = rev elem then () else raise Match;
              val (pat, rest) = mk_pattern (rev pattern);
              val _ = case rest of [] => () | _ => raise Match
            in
              Syntax.const syntax_const‹_prob› $ unnest_tuples pat $ sig_alg $ u
            end
        | go pattern elem (Abs abs) =
            let
              val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' abs
            in
              go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
            end
        | go pattern elem (Const (const_syntaxcase_prod, _) $ t) =
            go
              ((Syntax.const syntax_const‹_pattern›, 2) :: pattern)
              (Syntax.const const_syntaxPair :: elem)
              t
      in
        go [] [] t
      end
  in
    [(const_syntaxSigma_Algebra.measure, K tr')]
  end

definition
  "cond_prob M P Q = 𝒫(ω in M. P ω  Q ω) / 𝒫(ω in M. Q ω)"

syntax
  "_conditional_prob" :: "pttrn  logic  logic  logic  logic" (('𝒫'(_ in _. _ ¦/ _')))

translations
  "𝒫(x in M. P ¦ Q)" => "CONST cond_prob M (λx. P) (λx. Q)"

lemma (in prob_space) AE_E_prob:
  assumes ae: "AE x in M. P x"
  obtains S where "S  {x  space M. P x}" "S  events" "prob S = 1"
proof -
  from ae[THEN AE_E] obtain N
    where "{x  space M. ¬ P x}  N" "emeasure M N = 0" "N  events" by auto
  then show thesis
    by (intro that[of "space M - N"])
       (auto simp: prob_compl prob_space emeasure_eq_measure measure_nonneg)
qed

lemma (in prob_space) prob_neg: "{xspace M. P x}  events  𝒫(x in M. ¬ P x) = 1 - 𝒫(x in M. P x)"
  by (auto intro!: arg_cong[where f=prob] simp add: prob_compl[symmetric])

lemma (in prob_space) prob_eq_AE:
  "(AE x in M. P x  Q x)  {xspace M. P x}  events  {xspace M. Q x}  events  𝒫(x in M. P x) = 𝒫(x in M. Q x)"
  by (rule finite_measure_eq_AE) auto

lemma (in prob_space) prob_eq_0_AE:
  assumes not: "AE x in M. ¬ P x" shows "𝒫(x in M. P x) = 0"
proof cases
  assume "{xspace M. P x}  events"
  with not have "𝒫(x in M. P x) = 𝒫(x in M. False)"
    by (intro prob_eq_AE) auto
  then show ?thesis by simp
qed (simp add: measure_notin_sets)

lemma (in prob_space) prob_Collect_eq_0:
  "{x  space M. P x}  sets M  𝒫(x in M. P x) = 0  (AE x in M. ¬ P x)"
  using AE_iff_measurable[OF _ refl, of M "λx. ¬ P x"] by (simp add: emeasure_eq_measure measure_nonneg)

lemma (in prob_space) prob_Collect_eq_1:
  "{x  space M. P x}  sets M  𝒫(x in M. P x) = 1  (AE x in M. P x)"
  using AE_in_set_eq_1[of "{xspace M. P x}"] by simp

lemma (in prob_space) prob_eq_0:
  "A  sets M  prob A = 0  (AE x in M. x  A)"
  using AE_iff_measurable[OF _ refl, of M "λx. x  A"]
  by (auto simp add: emeasure_eq_measure Int_def[symmetric] measure_nonneg)

lemma (in prob_space) prob_eq_1:
  "A  sets M  prob A = 1  (AE x in M. x  A)"
  using AE_in_set_eq_1[of A] by simp

lemma (in prob_space) prob_sums:
  assumes P: "n. {xspace M. P n x}  events"
  assumes Q: "{xspace M. Q x}  events"
  assumes ae: "AE x in M. (n. P n x  Q x)  (Q x  (∃!n. P n x))"
  shows "(λn. 𝒫(x in M. P n x)) sums 𝒫(x in M. Q x)"
proof -
  from ae[THEN AE_E_prob] obtain S
    where S:
      "S  {x  space M. (n. P n x  Q x)  (Q x  (∃!n. P n x))}"
      "S  events"
      "prob S = 1"
    by auto
  then have disj: "disjoint_family (λn. {xspace M. P n x}  S)"
    by (auto simp: disjoint_family_on_def)
  from S have ae_S:
    "AE x in M. x  {xspace M. Q x}  x  (n. {xspace M. P n x}  S)"
    "n. AE x in M. x  {xspace M. P n x}  x  {xspace M. P n x}  S"
    using ae by (auto dest!: AE_prob_1)
  from ae_S have *:
    "𝒫(x in M. Q x) = prob (n. {xspace M. P n x}  S)"
    using P Q S by (intro finite_measure_eq_AE) auto
  from ae_S have **:
    "n. 𝒫(x in M. P n x) = prob ({xspace M. P n x}  S)"
    using P Q S by (intro finite_measure_eq_AE) auto
  show ?thesis
    unfolding * ** using S P disj
    by (intro finite_measure_UNION) auto
qed

lemma (in prob_space) prob_sum:
  assumes [simp, intro]: "finite I"
  assumes P: "n. n  I  {xspace M. P n x}  events"
  assumes Q: "{xspace M. Q x}  events"
  assumes ae: "AE x in M. (nI. P n x  Q x)  (Q x  (∃!nI. P n x))"
  shows "𝒫(x in M. Q x) = (nI. 𝒫(x in M. P n x))"
proof -
  from ae[THEN AE_E_prob] obtain S
    where S:
      "S  {x  space M. (nI. P n x  Q x)  (Q x  (∃!n. n  I  P n x))}"
      "S  events"
      "prob S = 1"
    by auto
  then have disj: "disjoint_family_on (λn. {xspace M. P n x}  S) I"
    by (auto simp: disjoint_family_on_def)
  from S have ae_S:
    "AE x in M. x  {xspace M. Q x}  x  (nI. {xspace M. P n x}  S)"
    "n. n  I  AE x in M. x  {xspace M. P n x}  x  {xspace M. P n x}  S"
    using ae by (auto dest!: AE_prob_1)
  from ae_S have *:
    "𝒫(x in M. Q x) = prob (nI. {xspace M. P n x}  S)"
    using P Q S by (intro finite_measure_eq_AE) (auto intro!: sets.Int)
  from ae_S have **:
    "n. n  I  𝒫(x in M. P n x) = prob ({xspace M. P n x}  S)"
    using P Q S by (intro finite_measure_eq_AE) auto
  show ?thesis
    using S P disj
    by (auto simp add: * ** simp del: UN_simps intro!: finite_measure_finite_Union)
qed

lemma (in prob_space) prob_EX_countable:
  assumes sets: "i. i  I  {xspace M. P i x}  sets M" and I: "countable I"
  assumes disj: "AE x in M. iI. jI. P i x  P j x  i = j"
  shows "𝒫(x in M. iI. P i x) = (+i. 𝒫(x in M. P i x) count_space I)"
proof -
  let ?N= "λx. ∃!iI. P i x"
  have "ennreal (𝒫(x in M. iI. P i x)) = 𝒫(x in M. (iI. P i x  ?N x))"
    unfolding ennreal_inj[OF measure_nonneg measure_nonneg]
  proof (rule prob_eq_AE)
    show "AE x in M. (iI. P i x) = (iI. P i x  ?N x)"
      using disj by eventually_elim blast
  qed (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets)+
  also have "𝒫(x in M. (iI. P i x  ?N x)) = emeasure M (iI. {xspace M. P i x  ?N x})"
    unfolding emeasure_eq_measure by (auto intro!: arg_cong[where f=prob] simp: measure_nonneg)
  also have " = (+i. emeasure M {xspace M. P i x  ?N x} count_space I)"
    by (rule emeasure_UN_countable)
       (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets
             simp: disjoint_family_on_def)
  also have " = (+i. 𝒫(x in M. P i x) count_space I)"
    unfolding emeasure_eq_measure using disj
    by (intro nn_integral_cong ennreal_inj[THEN iffD2] prob_eq_AE)
       (auto intro!: sets.sets_Collect_countable_Ex' sets.sets_Collect_conj sets.sets_Collect_countable_Ex1' I sets measure_nonneg)+
  finally show ?thesis .
qed

lemma (in prob_space) cond_prob_eq_AE:
  assumes P: "AE x in M. Q x  P x  P' x" "{xspace M. P x}  events" "{xspace M. P' x}  events"
  assumes Q: "AE x in M. Q x  Q' x" "{xspace M. Q x}  events" "{xspace M. Q' x}  events"
  shows "cond_prob M P Q = cond_prob M P' Q'"
  using P Q
  by (auto simp: cond_prob_def intro!: arg_cong2[where f="(/)"] prob_eq_AE sets.sets_Collect_conj)


lemma (in prob_space) joint_distribution_Times_le_fst:
  "random_variable MX X  random_variable MY Y  A  sets MX  B  sets MY
     emeasure (distr M (MX M MY) (λx. (X x, Y x))) (A × B)  emeasure (distr M MX X) A"
  by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)

lemma (in prob_space) joint_distribution_Times_le_snd:
  "random_variable MX X  random_variable MY Y  A  sets MX  B  sets MY
     emeasure (distr M (MX M MY) (λx. (X x, Y x))) (A × B)  emeasure (distr M MY Y) B"
  by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)

lemma (in prob_space) variance_eq:
  fixes X :: "'a  real"
  assumes [simp]: "integrable M X"
  assumes [simp]: "integrable M (λx. (X x)2)"
  shows "variance X = expectation (λx. (X x)2) - (expectation X)2"
  by (simp add: field_simps prob_space power2_diff power2_eq_square[symmetric])

lemma (in prob_space) variance_positive: "0  variance (X::'a  real)"
  by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE)

lemma (in prob_space) variance_mean_zero:
  "expectation X = 0  variance X = expectation (λx. (X x)^2)"
  by simp

theorem%important (in prob_space) Chebyshev_inequality:
  assumes [measurable]: "random_variable borel f"
  assumes "integrable M (λx. f x ^ 2)"
  defines "μ  expectation f"
  assumes "a > 0"
  shows "prob {xspace M. ¦f x - μ¦  a}  variance f / a2"
  unfolding μ_def
proof (rule second_moment_method)
  have integrable: "integrable M f"
    using assms by (blast dest: square_integrable_imp_integrable)
  show "integrable M (λx. (f x - expectation f)2)"
    using assms integrable unfolding power2_eq_square ring_distribs
    by (intro Bochner_Integration.integrable_diff) auto
qed (use assms in auto)

locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2

sublocale pair_prob_space  P?: prob_space "M1 M M2"
proof
  show "emeasure (M1 M M2) (space (M1 M M2)) = 1"
    by (simp add: M2.emeasure_pair_measure_Times M1.emeasure_space_1 M2.emeasure_space_1 space_pair_measure)
qed

locale product_prob_space = product_sigma_finite M for M :: "'i  'a measure" +
  fixes I :: "'i set"
  assumes prob_space: "i. prob_space (M i)"

sublocale product_prob_space  M?: prob_space "M i" for i
  by (rule prob_space)

locale finite_product_prob_space = finite_product_sigma_finite M I + product_prob_space M I for M I

sublocale finite_product_prob_space  prob_space "ΠM iI. M i"
proof
  show "emeasure (ΠM iI. M i) (space (ΠM iI. M i)) = 1"
    by (simp add: measure_times M.emeasure_space_1 prod.neutral_const space_PiM)
qed

lemma (in finite_product_prob_space) prob_times:
  assumes X: "i. i  I  X i  sets (M i)"
  shows "prob (ΠE iI. X i) = (iI. M.prob i (X i))"
proof -
  have "ennreal (measure (ΠM iI. M i) (ΠE iI. X i)) = emeasure (ΠM iI. M i) (ΠE iI. X i)"
    using X by (simp add: emeasure_eq_measure)
  also have " = (iI. emeasure (M i) (X i))"
    using measure_times X by simp
  also have " = ennreal (iI. measure (M i) (X i))"
    using X by (simp add: M.emeasure_eq_measure prod_ennreal measure_nonneg)
  finally show ?thesis by (simp add: measure_nonneg prod_nonneg)
qed

lemma product_prob_spaceI:
  assumes "i. prob_space (M i)"
  shows   "product_prob_space M"
  unfolding product_prob_space_def product_prob_space_axioms_def product_sigma_finite_def
proof safe
  fix i
  interpret prob_space "M i"
    by (rule assms)
  show "sigma_finite_measure (M i)" "prob_space (M i)"
    by unfold_locales
qed

subsection ‹Distributions›

definition distributed :: "'a measure  'b measure  ('a  'b)  ('b  ennreal)  bool"
where
  "distributed M N X f 
  distr M N X = density N f  f  borel_measurable N  X  measurable M N"

lemma
  assumes "distributed M N X f"
  shows distributed_distr_eq_density: "distr M N X = density N f"
    and distributed_measurable: "X  measurable M N"
    and distributed_borel_measurable: "f  borel_measurable N"
  using assms by (simp_all add: distributed_def)

lemma
  assumes D: "distributed M N X f"
  shows distributed_measurable'[measurable_dest]:
      "g  measurable L M  (λx. X (g x))  measurable L N"
    and distributed_borel_measurable'[measurable_dest]:
      "h  measurable L N  (λx. f (h x))  borel_measurable L"
  using distributed_measurable[OF D] distributed_borel_measurable[OF D]
  by simp_all

lemma distributed_real_measurable:
  "(x. x  space N  0  f x)  distributed M N X (λx. ennreal (f x))  f  borel_measurable N"
  by (simp_all add: distributed_def)

lemma distributed_real_measurable':
  "(x. x  space N  0  f x)  distributed M N X (λx. ennreal (f x)) 
    h  measurable L N  (λx. f (h x))  borel_measurable L"
  using distributed_real_measurable[measurable] by simp

lemma joint_distributed_measurable1:
  "distributed M (S M T) (λx. (X x, Y x)) f  h1  measurable N M  (λx. X (h1 x))  measurable N S"
  by simp

lemma joint_distributed_measurable2:
  "distributed M (S M T) (λx. (X x, Y x)) f  h2  measurable N M  (λx. Y (h2 x))  measurable N T"
  by simp

lemma distributed_count_space:
  assumes X: "distributed M (count_space A) X P" and a: "a  A" and A: "finite A"
  shows "P a = emeasure M (X -` {a}  space M)"
proof -
  have "emeasure M (X -` {a}  space M) = emeasure (distr M (count_space A) X) {a}"
    using X a A by (simp add: emeasure_distr)
  also have " = emeasure (density (count_space A) P) {a}"
    using X by (simp add: distributed_distr_eq_density)
  also have " = (+x. P a * indicator {a} x count_space A)"
    using X a by (auto simp add: emeasure_density distributed_def indicator_def intro!: nn_integral_cong)
  also have " = P a"
    using X a by (subst nn_integral_cmult_indicator) (auto simp: distributed_def one_ennreal_def[symmetric] AE_count_space)
  finally show ?thesis ..
qed

lemma distributed_cong_density:
  "(AE x in N. f x = g x)  g  borel_measurable N  f  borel_measurable N 
    distributed M N X f  distributed M N X g"
  by (auto simp: distributed_def intro!: density_cong)

lemma (in prob_space) distributed_imp_emeasure_nonzero:
  assumes X: "distributed M MX X Px"
  shows "emeasure MX {x  space MX. Px x  0}  0"
proof
  note Px = distributed_borel_measurable[OF X]
  interpret X: prob_space "distr M MX X"
    using distributed_measurable[OF X] by (rule prob_space_distr)

  assume "emeasure MX {x  space MX. Px x  0} = 0"
  with Px have "AE x in MX. Px x = 0"
    by (intro AE_I[OF subset_refl]) (auto simp: borel_measurable_ennreal_iff)
  moreover
  from X.emeasure_space_1 have "(+x. Px x MX) = 1"
    unfolding distributed_distr_eq_density[OF X] using Px
    by (subst (asm) emeasure_density)
       (auto simp: borel_measurable_ennreal_iff intro!: integral_cong cong: nn_integral_cong)
  ultimately show False
    by (simp add: nn_integral_cong_AE)
qed

lemma subdensity:
  assumes T: "T  measurable P Q"
  assumes f: "distributed M P X f"
  assumes g: "distributed M Q Y g"
  assumes Y: "Y = T  X"
  shows "AE x in P. g (T x) = 0  f x = 0"
proof -
  have "{xspace Q. g x = 0}  null_sets (distr M Q (T  X))"
    using g Y by (auto simp: null_sets_density_iff distributed_def)
  also have "distr M Q (T  X) = distr (distr M P X) Q T"
    using T f[THEN distributed_measurable] by (rule distr_distr[symmetric])
  finally have "T -` {xspace Q. g x = 0}  space P  null_sets (distr M P X)"
    using T by (subst (asm) null_sets_distr_iff) auto
  also have "T -` {xspace Q. g x = 0}  space P = {xspace P. g (T x) = 0}"
    using T by (auto dest: measurable_space)
  finally show ?thesis
    using f g by (auto simp add: null_sets_density_iff distributed_def)
qed

lemma subdensity_real:
  fixes g :: "'a  real" and f :: "'b  real"
  assumes T: "T  measurable P Q"
  assumes f: "distributed M P X f"
  assumes g: "distributed M Q Y g"
  assumes Y: "Y = T  X"
  shows "(AE x in P. 0  g (T x))  (AE x in P. 0  f x)  AE x in P. g (T x) = 0  f x = 0"
  using subdensity[OF T, of M X "λx. ennreal (f x)" Y "λx. ennreal (g x)"] assms
  by auto

lemma distributed_emeasure:
  "distributed M N X f  A  sets N  emeasure M (X -` A  space M) = (+x. f x * indicator A x N)"
  by (auto simp: distributed_distr_eq_density[symmetric] emeasure_density[symmetric] emeasure_distr)

lemma distributed_nn_integral:
  "distributed M N X f  g  borel_measurable N  (+x. f x * g x N) = (+x. g (X x) M)"
  by (auto simp: distributed_distr_eq_density[symmetric] nn_integral_density[symmetric] nn_integral_distr)

lemma distributed_integral:
  "distributed M N X f  g  borel_measurable N  (x. x  space N  0  f x) 
    (x. f x * g x N) = (x. g (X x) M)"
  supply distributed_real_measurable[measurable]
  by (auto simp: distributed_distr_eq_density[symmetric] integral_real_density[symmetric] integral_distr)

lemma distributed_transform_integral:
  assumes Px: "distributed M N X Px" "x. x  space N  0  Px x"
  assumes "distributed M P Y Py" "x. x  space P  0  Py x"
  assumes Y: "Y = T  X" and T: "T  measurable N P" and f: "f  borel_measurable P"
  shows "(x. Py x * f x P) = (x. Px x * f (T x) N)"
proof -
  have "(x. Py x * f x P) = (x. f (Y x) M)"
    by (rule distributed_integral) fact+
  also have " = (x. f (T (X x)) M)"
    using Y by simp
  also have " = (x. Px x * f (T x) N)"
    using measurable_comp[OF T f] Px by (intro distributed_integral[symmetric]) (auto simp: comp_def)
  finally show ?thesis .
qed

lemma (in prob_space) distributed_unique:
  assumes Px: "distributed M S X Px"
  assumes Py: "distributed M S X Py"
  shows "AE x in S. Px x = Py x"
proof -
  interpret X: prob_space "distr M S X"
    using Px by (intro prob_space_distr) simp
  have "sigma_finite_measure (distr M S X)" ..
  with sigma_finite_density_unique[of Px S Py ] Px Py
  show ?thesis
    by (auto simp: distributed_def)
qed

lemma (in prob_space) distributed_jointI:
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
  assumes X[measurable]: "X  measurable M S" and Y[measurable]: "Y  measurable M T"
  assumes [measurable]: "f  borel_measurable (S M T)" and f: "AE x in S M T. 0  f x"
  assumes eq: "A B. A  sets S  B  sets T 
    emeasure M {x  space M. X x  A  Y x  B} = (+x. (+y. f (x, y) * indicator B y T) * indicator A x S)"
  shows "distributed M (S M T) (λx. (X x, Y x)) f"
  unfolding distributed_def
proof safe
  interpret S: sigma_finite_measure S by fact
  interpret T: sigma_finite_measure T by fact
  interpret ST: pair_sigma_finite S T ..

  from ST.sigma_finite_up_in_pair_measure_generator
  obtain F :: "nat  ('b × 'c) set"
    where F: "range F  {A × B |A B. A  sets S  B  sets T}  incseq F 
       (range F) = space S × space T  (i. emeasure (S M T) (F i)  )" ..
  let ?E = "{a × b |a b. a  sets S  b  sets T}"
  let ?P = "S M T"
  show "distr M ?P (λx. (X x, Y x)) = density ?P f" (is "?L = ?R")
  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of S T]])
    show "?E  Pow (space ?P)"
      using sets.space_closed[of S] sets.space_closed[of T] by (auto simp: space_pair_measure)
    show "sets ?L = sigma_sets (space ?P) ?E"
      by (simp add: sets_pair_measure space_pair_measure)
    then show "sets ?R = sigma_sets (space ?P) ?E"
      by simp
  next
    interpret L: prob_space ?L
      by (rule prob_space_distr) (auto intro!: measurable_Pair)
    show "range F  ?E" "(i. F i) = space ?P" "i. emeasure ?L (F i)  "
      using F by (auto simp: space_pair_measure)
  next
    fix E assume "E  ?E"
    then obtain A B where E[simp]: "E = A × B"
      and A[measurable]: "A  sets S" and B[measurable]: "B  sets T" by auto
    have "emeasure ?L E = emeasure M {x  space M. X x  A  Y x  B}"
      by (auto intro!: arg_cong[where f="emeasure M"] simp add: emeasure_distr measurable_Pair)
    also have " = (+x. (+y. (f (x, y) * indicator B y) * indicator A x T) S)"
      using f by (auto simp add: eq nn_integral_multc intro!: nn_integral_cong)
    also have " = emeasure ?R E"
      by (auto simp add: emeasure_density T.nn_integral_fst[symmetric]
               intro!: nn_integral_cong split: split_indicator)
    finally show "emeasure ?L E = emeasure ?R E" .
  qed
qed (auto simp: f)

lemma (in prob_space) distributed_swap:
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
  assumes Pxy: "distributed M (S M T) (λx. (X x, Y x)) Pxy"
  shows "distributed M (T M S) (λx. (Y x, X x)) (λ(x, y). Pxy (y, x))"
proof -
  interpret S: sigma_finite_measure S by fact
  interpret T: sigma_finite_measure T by fact
  interpret ST: pair_sigma_finite S T ..
  interpret TS: pair_sigma_finite T S ..

  note Pxy[measurable]
  show ?thesis
    apply (subst TS.distr_pair_swap)
    unfolding distributed_def
  proof safe
    let ?D = "distr (S M T) (T M S) (λ(x, y). (y, x))"
    show 1: "(λ(x, y). Pxy (y, x))  borel_measurable ?D"
      by auto
    show 2: "random_variable (distr (S M T) (T M S) (λ(x, y). (y, x))) (λx. (Y x, X x))"
      using Pxy by auto
    { fix A assume A: "A  sets (T M S)"
      let ?B = "(λ(x, y). (y, x)) -` A  space (S M T)"
      from sets.sets_into_space[OF A]
      have "emeasure M ((λx. (Y x, X x)) -` A  space M) =
        emeasure M ((λx. (X x, Y x)) -` ?B  space M)"
        by (auto intro!: arg_cong2[where f=emeasure] simp: space_pair_measure)
      also have " = (+ x. Pxy x * indicator ?B x (S M T))"
        using Pxy A by (intro distributed_emeasure) auto
      finally have "emeasure M ((λx. (Y x, X x)) -` A  space M) =
        (+ x. Pxy x * indicator A (snd x, fst x) (S M T))"
        by (auto intro!: nn_integral_cong split: split_indicator) }
    note * = this
    show "distr M ?D (λx. (Y x, X x)) = density ?D (λ(x, y). Pxy (y, x))"
      apply (intro measure_eqI)
      apply (simp_all add: emeasure_distr[OF 2] emeasure_density[OF 1])
      apply (subst nn_integral_distr)
      apply (auto intro!: * simp: comp_def split_beta)
      done
  qed
qed

lemma (in prob_space) distr_marginal1:
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
  assumes Pxy: "distributed M (S M T) (λx. (X x, Y x)) Pxy"
  defines "Px  λx. (+z. Pxy (x, z) T)"
  shows "distributed M S X Px"
  unfolding distributed_def
proof safe
  interpret S: sigma_finite_measure S by fact
  interpret T: sigma_finite_measure T by fact
  interpret ST: pair_sigma_finite S T ..

  note Pxy[measurable]
  show X: "X  measurable M S" by simp

  show borel: "Px  borel_measurable S"
    by (auto intro!: T.nn_integral_fst simp: Px_def)

  interpret Pxy: prob_space "distr M (S M T) (λx. (X x, Y x))"
    by (intro prob_space_distr) simp

  show "distr M S X = density S Px"
  proof (rule measure_eqI)
    fix A assume A: "A  sets (distr M S X)"
    with X measurable_space[of Y M T]
    have "emeasure (distr M S X) A = emeasure (distr M (S M T) (λx. (X x, Y x))) (A × space T)"
      by (auto simp add: emeasure_distr intro!: arg_cong[where f="emeasure M"])
    also have " = emeasure (density (S M T) Pxy) (A × space T)"
      using Pxy by (simp add: distributed_def)
    also have " = + x. + y. Pxy (x, y) * indicator (A × space T) (x, y) T S"
      using A borel Pxy
      by (simp add: emeasure_density T.nn_integral_fst[symmetric])
    also have " = + x. Px x * indicator A x S"
    proof (rule nn_integral_cong)
      fix x assume "x  space S"
      moreover have eq: "y. y  space T  indicator (A × space T) (x, y) = indicator A x"
        by (auto simp: indicator_def)
      ultimately have "(+ y. Pxy (x, y) * indicator (A × space T) (x, y) T) = (+ y. Pxy (x, y) T) * indicator A x"
        by (simp add: eq nn_integral_multc cong: nn_integral_cong)
      also have "(+ y. Pxy (x, y) T) = Px x"
        by (simp add: Px_def)
      finally show "(+ y. Pxy (x, y) * indicator (A × space T) (x, y) T) = Px x * indicator A x" .
    qed
    finally show "emeasure (distr M S X) A = emeasure (density S Px) A"
      using A borel Pxy by (simp add: emeasure_density)
  qed simp
qed

lemma (in prob_space) distr_marginal2:
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  assumes Pxy: "distributed M (S M T) (λx. (X x, Y x)) Pxy"
  shows "distributed M T Y (λy. (+x. Pxy (x, y) S))"
  using distr_marginal1[OF T S distributed_swap[OF S T]] Pxy by simp

lemma (in prob_space) distributed_marginal_eq_joint1:
  assumes T: "sigma_finite_measure T"
  assumes S: "sigma_finite_measure S"
  assumes Px: "distributed M S X Px"
  assumes Pxy: "distributed M (S M T) (λx. (X x, Y x)) Pxy"
  shows "AE x in S. Px x = (+y. Pxy (x, y) T)"
  using Px distr_marginal1[OF S T Pxy] by (rule distributed_unique)

lemma (in prob_space) distributed_marginal_eq_joint2:
  assumes T: "sigma_finite_measure T"
  assumes S: "sigma_finite_measure S"
  assumes Py: "distributed M T Y Py"
  assumes Pxy: "distributed M (S M T) (λx. (X x, Y x)) Pxy"
  shows "AE y in T. Py y = (+x. Pxy (x, y) S)"
  using Py distr_marginal2[OF S T Pxy] by (rule distributed_unique)

lemma (in prob_space) distributed_joint_indep':
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
  assumes X[measurable]: "distributed M S X Px" and Y[measurable]: "distributed M T Y Py"
  assumes indep: "distr M S X M distr M T Y = distr M (S M T) (λx. (X x, Y x))"
  shows "distributed M (S M T) (λx. (X x, Y x)) (λ(x, y). Px x * Py y)"
  unfolding distributed_def
proof safe
  interpret S: sigma_finite_measure S by fact
  interpret T: sigma_finite_measure T by fact
  interpret ST: pair_sigma_finite S T ..

  interpret X: prob_space "density S Px"
    unfolding distributed_distr_eq_density[OF X, symmetric]
    by (rule prob_space_distr) simp
  have sf_X: "sigma_finite_measure (density S Px)" ..

  interpret Y: prob_space "density T Py"
    unfolding distributed_distr_eq_density[OF Y, symmetric]
    by (rule prob_space_distr) simp
  have sf_Y: "sigma_finite_measure (density T Py)" ..

  show "distr M (S M T) (λx. (X x, Y x)) = density (S M T) (λ(x, y). Px x * Py y)"
    unfolding indep[symmetric] distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
    using distributed_borel_measurable[OF X]
    using distributed_borel_measurable[OF Y]
    by (rule pair_measure_density[OF _ _ T sf_Y])

  show "random_variable (S M T) (λx. (X x, Y x))" by auto

  show Pxy: "(λ(x, y). Px x * Py y)  borel_measurable (S M T)" by auto
qed

lemma distributed_integrable:
  "distributed M N X f  g  borel_measurable N  (x. x  space N  0  f x) 
    integrable N (λx. f x * g x)  integrable M (λx. g (X x))"
  supply distributed_real_measurable[measurable]
  by (auto simp: distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq)

lemma distributed_transform_integrable:
  assumes Px: "distributed M N X Px" "x. x  space N  0  Px x"
  assumes "distributed M P Y Py" "x. x  space P  0  Py x"
  assumes Y: "Y = (λx. T (X x))" and T: "T  measurable N P" and f: "f  borel_measurable P"
  shows "integrable P (λx. Py x * f x)  integrable N (λx. Px x * f (T x))"
proof -
  have "integrable P (λx. Py x * f x)  integrable M (λx. f (Y x))"
    by (rule distributed_integrable) fact+
  also have "  integrable M (λx. f (T (X x)))"
    using Y by simp
  also have "  integrable N (λx. Px x * f (T x))"
    using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
  finally show ?thesis .
qed

lemma distributed_integrable_var:
  fixes X :: "'a  real"
  shows "distributed M lborel X (λx. ennreal (f x))  (x. 0  f x) 
    integrable lborel (λx. f x * x)  integrable M X"
  using distributed_integrable[of M lborel X f "λx. x"] by simp

lemma (in prob_space) distributed_variance:
  fixes f::"real  real"
  assumes D: "distributed M lborel X f" and [simp]: "x. 0  f x"
  shows "variance X = (x. x2 * f (x + expectation X) lborel)"
proof (subst distributed_integral[OF D, symmetric])
  show "( x. f x * (x - expectation X)2 lborel) = ( x. x2 * f (x + expectation X) lborel)"
    by (subst lborel_integral_real_affine[where c=1 and t="expectation X"])  (auto simp: ac_simps)
qed simp_all

lemma (in prob_space) variance_affine:
  fixes f::"real  real"
  assumes [arith]: "b  0"
  assumes D[intro]: "distributed M lborel X f"
  assumes [simp]: "prob_space (density lborel f)"
  assumes I[simp]: "integrable M X"
  assumes I2[simp]: "integrable M (λx. (X x)2)"
  shows "variance (λx. a + b * X x) = b2 * variance X"
  by (subst variance_eq)
     (auto simp: power2_sum power_mult_distrib prob_space variance_eq right_diff_distrib)

definition
  "simple_distributed M X f 
    (x. 0  f x) 
    distributed M (count_space (X`space M)) X (λx. ennreal (f x)) 
    finite (X`space M)"

lemma simple_distributed_nonneg[dest]: "simple_distributed M X f  0  f x"
  by (auto simp: simple_distributed_def)

lemma simple_distributed:
  "simple_distributed M X Px  distributed M (count_space (X`space M)) X Px"
  unfolding simple_distributed_def by auto

lemma simple_distributed_finite[dest]: "simple_distributed M X P  finite (X`space M)"
  by (simp add: simple_distributed_def)

lemma (in prob_space) distributed_simple_function_superset:
  assumes X: "simple_function M X" "x. x  X ` space M  P x = measure M (X -` {x}  space M)"
  assumes A: "X`space M  A" "finite A"
  defines "S  count_space A" and "P'  (λx. if x  X`space M then P x else 0)"
  shows "distributed M S X P'"
  unfolding distributed_def
proof safe
  show "(λx. ennreal (P' x))  borel_measurable S" unfolding S_def by simp
  show "distr M S X = density S P'"
  proof (rule measure_eqI_finite)
    show "sets (distr M S X) = Pow A" "sets (density S P') = Pow A"
      using A unfolding S_def by auto
    show "finite A" by fact
    fix a assume a: "a  A"
    then have "a  X`space M  X -` {a}  space M = {}" by auto
    with A a X have "emeasure (distr M S X) {a} = P' a"
      by (subst emeasure_distr)
         (auto simp add: S_def P'_def simple_functionD emeasure_eq_measure measurable_count_space_eq2
               intro!: arg_cong[where f=prob])
    also have " = (+x. ennreal (P' a) * indicator {a} x S)"
      using A X a
      by (subst nn_integral_cmult_indicator)
         (auto simp: S_def P'_def simple_distributed_def simple_functionD measure_nonneg)
    also have " = (+x. ennreal (P' x) * indicator {a} x S)"
      by (auto simp: indicator_def intro!: nn_integral_cong)
    also have " = emeasure (density S P') {a}"
      using a A by (intro emeasure_density[symmetric]) (auto simp: S_def)
    finally show "emeasure (distr M S X) {a} = emeasure (density S P') {a}" .
  qed
  show "random_variable S X"
    using X(1) A by (auto simp: measurable_def simple_functionD S_def)
qed

lemma (in prob_space) simple_distributedI:
  assumes X: "simple_function M X"
    "x. 0  P x"
    "x. x  X ` space M  P x = measure M (X -` {x}  space M)"
  shows "simple_distributed M X P"
  unfolding simple_distributed_def
proof (safe intro!: X)
  have "distributed M (count_space (X ` space M)) X (λx. ennreal (if x  X`space M then P x else 0))"
    (is "?A")
    using simple_functionD[OF X(1)] by (intro distributed_simple_function_superset[OF X(1,3)]) auto
  also have "?A  distributed M (count_space (X ` space M)) X (λx. ennreal (P x))"
    by (rule distributed_cong_density) auto
  finally show "" .
qed (rule simple_functionD[OF X(1)])

lemma simple_distributed_joint_finite:
  assumes X: "simple_distributed M (λx. (X x, Y x)) Px"
  shows "finite (X ` space M)" "finite (Y ` space M)"
proof -
  have "finite ((λx. (X x, Y x)) ` space M)"
    using X by (auto simp: simple_distributed_def simple_functionD)
  then have "finite (fst ` (λx. (X x, Y x)) ` space M)" "finite (snd ` (λx. (X x, Y x)) ` space M)"
    by auto
  then show fin: "finite (X ` space M)" "finite (Y ` space M)"
    by (auto simp: image_image)
qed

lemma simple_distributed_joint2_finite:
  assumes X: "simple_distributed M (λx. (X x, Y x, Z x)) Px"
  shows "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
proof -
  have "finite ((λx. (X x, Y x, Z x)) ` space M)"
    using X by (auto simp: simple_distributed_def simple_functionD)
  then have "finite (fst ` (λx. (X x, Y x, Z x)) ` space M)"
    "finite ((fst  snd) ` (λx. (X x, Y x, Z x)) ` space M)"
    "finite ((snd  snd) ` (λx. (X x, Y x, Z x)) ` space M)"
    by auto
  then show fin: "finite (X ` space M)" "finite (Y ` space M)" "finite (Z ` space M)"
    by (auto simp: image_image)
qed

lemma simple_distributed_simple_function:
  "simple_distributed M X Px  simple_function M X"
  unfolding simple_distributed_def distributed_def
  by (auto simp: simple_function_def measurable_count_space_eq2)

lemma simple_distributed_measure:
  "simple_distributed M X P  a  X`space M  P a = measure M (X -` {a}  space M)"
  using distributed_count_space[of M "X`space M" X P a, symmetric]
  by (auto simp: simple_distributed_def measure_def)

lemma (in prob_space) simple_distributed_joint:
  assumes X: "simple_distributed M (λx. (X x, Y x)) Px"
  defines "S  count_space (X`space M) M count_space (Y`space M)"
  defines "P  (λx. if x  (λx. (X x, Y x))`space M then Px x else 0)"
  shows "distributed M S (λx. (X x, Y x)) P"
proof -
  from simple_distributed_joint_finite[OF X, simp]
  have S_eq: "S = count_space (X`space M × Y`space M)"
    by (simp add: S_def pair_measure_count_space)
  show ?thesis
    unfolding S_eq P_def
  proof (rule distributed_simple_function_superset)
    show "simple_function M (λx. (X x, Y x))"
      using X by (rule simple_distributed_simple_function)
    fix x assume "x  (λx. (X x, Y x)) ` space M"
    from simple_distributed_measure[OF X this]
    show "Px x = prob ((λx. (X x, Y x)) -` {x}  space M)" .
  qed auto
qed

lemma (in prob_space) simple_distributed_joint2:
  assumes X: "simple_distributed M (λx. (X x, Y x, Z x)) Px"
  defines "S  count_space (X`space M) M count_space (Y`space M) M count_space (Z`space M)"
  defines "P  (λx. if x  (λx. (X x, Y x, Z x))`space M then Px x else 0)"
  shows "distributed M S (λx. (X x, Y x, Z x)) P"
proof -
  from simple_distributed_joint2_finite[OF X, simp]
  have S_eq: "S = count_space (X`space M × Y`space M × Z`space M)"
    by (simp add: S_def pair_measure_count_space)
  show ?thesis
    unfolding S_eq P_def
  proof (rule distributed_simple_function_superset)
    show "simple_function M (λx. (X x, Y x, Z x))"
      using X by (rule simple_distributed_simple_function)
    fix x assume "x  (λx. (X x, Y x, Z x)) ` space M"
    from simple_distributed_measure[OF X this]
    show "Px x = prob ((λx. (X x, Y x, Z x)) -` {x}  space M)" .
  qed auto
qed

lemma (in prob_space) simple_distributed_sum_space:
  assumes X: "simple_distributed M X f"
  shows "sum f (X`space M) = 1"
proof -
  from X have "sum f (X`space M) = prob (iX`space M. X -` {i}  space M)"
    by (subst finite_measure_finite_Union)
       (auto simp add: disjoint_family_on_def simple_distributed_measure simple_distributed_simple_function simple_functionD
             intro!: sum.cong arg_cong[where f="prob"])
  also have " = prob (space M)"
    by (auto intro!: arg_cong[where f=prob])
  finally show ?thesis
    using emeasure_space_1 by (simp add: emeasure_eq_measure)
qed

lemma (in prob_space) distributed_marginal_eq_joint_simple:
  assumes Px: "simple_function M X"
  assumes Py: "simple_distributed M Y Py"
  assumes Pxy: "simple_distributed M (λx. (X x, Y x)) Pxy"
  assumes y: "y  Y`space M"
  shows "Py y = (xX`space M. if (x, y)  (λx. (X x, Y x)) ` space M then Pxy (x, y) else 0)"
proof -
  note Px = simple_distributedI[OF Px measure_nonneg refl]
  have "AE y in count_space (Y ` space M). ennreal (Py y) =
       + x. ennreal (if (x, y)  (λx. (X x, Y x)) ` space M then Pxy (x, y) else 0) count_space (X ` space M)"
    using sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite
      simple_distributed[OF Py] simple_distributed_joint[OF Pxy]
    by (rule distributed_marginal_eq_joint2)
       (auto intro: Py Px simple_distributed_finite)
  then have "ennreal (Py y) =
    (xX`space M. ennreal (if (x, y)  (λx. (X x, Y x)) ` space M then Pxy (x, y) else 0))"
    using y Px[THEN simple_distributed_finite]
    by (auto simp: AE_count_space nn_integral_count_space_finite)
  also have " = (xX`space M. if (x, y)  (λx. (X x, Y x)) ` space M then Pxy (x, y) else 0)"
    using Pxy by (intro sum_ennreal) auto
  finally show ?thesis
    using simple_distributed_nonneg[OF Py] simple_distributed_nonneg[OF Pxy]
    by (subst (asm) ennreal_inj) (auto intro!: sum_nonneg)
qed

lemma distributedI_real:
  fixes f :: "'a  real"
  assumes gen: "sets M1 = sigma_sets (space M1) E" and "Int_stable E"
    and A: "range A  E" "(i::nat. A i) = space M1" "i. emeasure (distr M M1 X) (A i)  "
    and X: "X  measurable M M1"
    and f: "f  borel_measurable M1" "AE x in M1. 0  f x"
    and eq: "A. A  E  emeasure M (X -` A  space M) = (+ x. f x * indicator A x M1)"
  shows "distributed M M1 X f"
  unfolding distributed_def
proof (intro conjI)
  show "distr M M1 X = density M1 f"
  proof (rule measure_eqI_generator_eq[where A=A])
    { fix A assume A: "A  E"
      then have "A  sigma_sets (space M1) E" by auto
      then have "A  sets M1"
        using gen by simp
      with f A eq[of A] X show "emeasure (distr M M1 X) A = emeasure (density M1 f) A"
        by (auto simp add: emeasure_distr emeasure_density ennreal_indicator
                 intro!: nn_integral_cong split: split_indicator) }
    note eq_E = this
    show "Int_stable E" by fact
    { fix e assume "e  E"
      then have "e  sigma_sets (space M1) E" by auto
      then have "e  sets M1" unfolding gen .
      then have "e  space M1" by (rule sets.sets_into_space) }
    then show "E  Pow (space M1)" by auto
    show "sets (distr M M1 X) = sigma_sets (space M1) E"
      "sets (density M1 (λx. ennreal (f x))) = sigma_sets (space M1) E"
      unfolding gen[symmetric] by auto
  qed fact+
qed (insert X f, auto)

lemma distributedI_borel_atMost:
  fixes f :: "real  real"
  assumes [measurable]: "X  borel_measurable M"
    and [measurable]: "f  borel_measurable borel" and f[simp]: "AE x in lborel. 0  f x"
    and g_eq: "a. (+x. f x * indicator {..a} x lborel)  = ennreal (g a)"
    and M_eq: "a. emeasure M {xspace M. X x  a} = ennreal (g a)"
  shows "distributed M lborel X f"
proof (rule distributedI_real)
  show "sets (lborel::real measure) = sigma_sets (space lborel) (range atMost)"
    by (simp add: borel_eq_atMost)
  show "Int_stable (range atMost :: real set set)"
    by (auto simp: Int_stable_def)
  have vimage_eq: "a. (X -` {..a}  space M) = {xspace M. X x  a}" by auto
  define A where "A i = {.. real i}" for i :: nat
  then show "range A  range atMost" "(i. A i) = space lborel"
    "i. emeasure (distr M lborel X) (A i)  "
    by (auto simp: real_arch_simple emeasure_distr vimage_eq M_eq)

  fix A :: "real set" assume "A  range atMost"
  then obtain a where A: "A = {..a}" by auto
  show "emeasure M (X -` A  space M) = (+x. f x * indicator A x lborel)"
    unfolding vimage_eq A M_eq g_eq ..
qed auto

lemma (in prob_space) uniform_distributed_params:
  assumes X: "distributed M MX X (λx. indicator A x / measure MX A)"
  shows "A  sets MX" "measure MX A  0"
proof -
  interpret X: prob_space "distr M MX X"
    using distributed_measurable[OF X] by (rule prob_space_distr)

  show "measure MX A  0"
  proof
    assume "measure MX A = 0"
    with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
    show False
      by (simp add: emeasure_density zero_ennreal_def[symmetric])
  qed
  with measure_notin_sets[of A MX] show "A  sets MX"
    by blast
qed

lemma prob_space_uniform_measure:
  assumes A: "emeasure M A  0" "emeasure M A  "
  shows "prob_space (uniform_measure M A)"
proof
  show "emeasure (uniform_measure M A) (space (uniform_measure M A)) = 1"
    using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)], of "space M"]
    using sets.sets_into_space[OF emeasure_neq_0_sets[OF A(1)]] A
    by (simp add: Int_absorb2 less_top)
qed

lemma prob_space_uniform_count_measure: "finite A  A  {}  prob_space (uniform_count_measure A)"
  by standard (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ennreal_def)

lemma (in prob_space) measure_uniform_measure_eq_cond_prob:
  assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
  shows "𝒫(x in uniform_measure M {xspace M. Q x}. P x) = 𝒫(x in M. P x ¦ Q x)"
proof cases
  assume Q: "measure M {xspace M. Q x} = 0"
  then have *: "AE x in M. ¬ Q x"
    by (simp add: prob_eq_0)
  then have "density M (λx. indicator {x  space M. Q x} x / emeasure M {x  space M. Q x}) = density M (λx. 0)"
    by (intro density_cong) auto
  with * show ?thesis
    unfolding uniform_measure_def
    by (simp add: emeasure_density measure_def cond_prob_def emeasure_eq_0_AE)
next
  assume Q: "measure M {xspace M. Q x}  0"
  then show "𝒫(x in uniform_measure M {x  space M. Q x}. P x) = cond_prob M P Q"
    by (subst measure_uniform_measure)
       (auto simp: emeasure_eq_measure cond_prob_def measure_nonneg intro!: arg_cong[where f=prob])
qed

lemma prob_space_point_measure:
  "finite S  (s. s  S  0  p s)  (sS. p s) = 1  prob_space (point_measure S p)"
  by (rule prob_spaceI) (simp add: space_point_measure emeasure_point_measure_finite)

lemma (in prob_space) distr_pair_fst: "distr (N M M) N fst = N"
proof (intro measure_eqI)
  fix A assume A: "A  sets (distr (N M M) N fst)"
  from A have "emeasure (distr (N M M) N fst) A = emeasure (N M M) (A × space M)"
    by (auto simp add: emeasure_distr space_pair_measure dest: sets.sets_into_space intro!: arg_cong2[where f=emeasure])
  with A show "emeasure (distr (N M M) N fst) A = emeasure N A"
    by (simp add: emeasure_pair_measure_Times emeasure_space_1)
qed simp

lemma (in product_prob_space) distr_reorder:
  assumes "inj_on t J" "t  J  K" "finite K"
  shows "distr (PiM K M) (PiM J (λx. M (t x))) (λω. λnJ. ω (t n)) = PiM J (λx. M (t x))"
proof (rule product_sigma_finite.PiM_eqI)
  show "product_sigma_finite (λx. M (t x))" ..
  have "t`J  K" using assms by auto
  then show [simp]: "finite J"
    by (rule finite_imageD[OF finite_subset]) fact+
  fix A assume A: "i. i  J  A i  sets (M (t i))"
  moreover have "((λω. λnJ. ω (t n)) -` PiE J A  space (PiM K M)) =
    (ΠE iK. if i  t`J then A (the_inv_into J t i) else space (M i))"
    using A A[THEN sets.sets_into_space] t  J  K inj_on t J
    by (subst prod_emb_Pi[symmetric]) (auto simp: space_PiM PiE_iff the_inv_into_f_f prod_emb_def)
  ultimately show "distr (PiM K M) (PiM J (λx. M (t x))) (λω. λnJ. ω (t n)) (PiE J A) = (iJ. M (t i) (A i))"
    using assms
    apply (subst emeasure_distr)
    apply (auto intro!: sets_PiM_I_finite simp: Pi_iff)
    apply (subst emeasure_PiM)
    apply (auto simp: the_inv_into_f_f inj_on t J prod.reindex[OF inj_on t J]
      if_distrib[where f="emeasure (M _)"] prod.If_cases emeasure_space_1 Int_absorb1 t`J  K)
    done
qed simp

lemma (in product_prob_space) distr_restrict:
  "J  K  finite K  (ΠM iJ. M i) = distr (ΠM iK. M i) (ΠM iJ. M i) (λf. restrict f J)"
  using distr_reorder[of "λx. x" J K] by (simp add: Pi_iff subset_eq)

lemma (in product_prob_space) emeasure_prod_emb[simp]:
  assumes L: "J  L" "finite L" and X: "X  sets (PiM J M)"
  shows "emeasure (PiM L M) (prod_emb L M J X) = emeasure (PiM J M) X"
  by (subst distr_restrict[OF L])
     (simp add: prod_emb_def space_PiM emeasure_distr measurable_restrict_subset L X)

lemma emeasure_distr_restrict:
  assumes "I  K" and Q[measurable_cong]: "sets Q = sets (PiM K M)" and A[measurable]: "A  sets (PiM I M)"
  shows "emeasure (distr Q (PiM I M) (λω. restrict ω I)) A = emeasure Q (prod_emb K M I A)"
  using IK sets_eq_imp_space_eq[OF Q]
  by (subst emeasure_distr)
     (auto simp: measurable_cong_sets[OF Q] prod_emb_def space_PiM[symmetric] intro!: measurable_restrict)

lemma (in prob_space) prob_space_completion: "prob_space (completion M)"
  by (rule prob_spaceI) (simp add: emeasure_space_1)

lemma distr_PiM_finite_prob_space:
  assumes fin: "finite I"
  assumes "product_prob_space M"
  assumes "product_prob_space M'"
  assumes [measurable]: "i. i  I  f  measurable (M i) (M' i)"
  shows   "distr (PiM I M) (PiM I M') (compose I f) = PiM I (λi. distr (M i) (M' i) f)"
proof -
  interpret M: product_prob_space M by fact
  interpret M': product_prob_space M' by fact
  define N where "N = (λi. if i  I then distr (M i) (M' i) f else M' i)"
  have [intro]: "prob_space (N i)" for i
    by (auto simp: N_def intro!: M.M.prob_space_distr M'.prob_space)

  interpret N: product_prob_space N
    by (intro product_prob_spaceI) (auto simp: N_def M'.prob_space intro: M.M.prob_space_distr)

  have "distr (PiM I M) (PiM I M') (compose I f) = PiM I N"
  proof (rule N.PiM_eqI)
    have N_events_eq: "sets (PiM I N) = sets (PiM I M')"
      unfolding N_def by (intro sets_PiM_cong) auto
    also have " = sets (distr (PiM I M) (PiM I M') (compose I f))"
      by simp
    finally show "sets (distr (PiM I M) (PiM I M') (compose I f)) = sets (PiM I N)"  ..

    fix A assume A: "i. i  I  A i  N.M.events i"
    have "emeasure (distr (PiM I M) (PiM I M') (compose I f)) (PiE I A) =
          emeasure (PiM I M) (compose I f -` PiE I A  space (PiM I M))"
    proof (intro emeasure_distr)
      show "compose I f  PiM I M M PiM I M'"
        unfolding compose_def by measurable
      show "PiE I A  sets (PiM I M')"
        unfolding N_events_eq [symmetric] by (intro sets_PiM_I_finite fin A)
    qed
    also have "compose I f -` PiE I A  space (PiM I M) = PiE I (λi. f -` A i  space (M i))"
      using A by (auto simp: space_PiM PiE_def Pi_def extensional_def N_def compose_def)
    also have "emeasure (PiM I M) (PiE I (λi. f -` A i  space (M i))) =
          (iI. emeasure (M i) (f -` A i  space (M i)))"
      using A by (intro M.emeasure_PiM fin) (auto simp: N_def)
    also have " = (iI. emeasure (distr (M i) (M' i) f) (A i))"
      using A by (intro prod.cong emeasure_distr [symmetric]) (auto simp: N_def)
    also have " = (iI. emeasure (N i) (A i))"
      unfolding N_def by (intro prod.cong) (auto simp: N_def)
    finally show "emeasure (distr (PiM I M) (PiM I M') (compose I f)) (PiE I A) = " .
  qed fact+
  also have "PiM I N = PiM I (λi. distr (M i) (M' i) f)"
    by (intro PiM_cong) (auto simp: N_def)
  finally show ?thesis .
qed

end