src/HOL/Probability/Giry_Monad.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 60067 f1a5bcf5658f
child 61169 4de9ff3ea29a
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
hoelzl@58606
     1
(*  Title:      HOL/Probability/Giry_Monad.thy
hoelzl@58606
     2
    Author:     Johannes Hölzl, TU München
hoelzl@58606
     3
    Author:     Manuel Eberl, TU München
hoelzl@58606
     4
hoelzl@58606
     5
Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability
hoelzl@58606
     6
spaces.
hoelzl@58606
     7
*)
hoelzl@58606
     8
hoelzl@58606
     9
theory Giry_Monad
hoelzl@59092
    10
  imports Probability_Measure Lebesgue_Integral_Substitution "~~/src/HOL/Library/Monad_Syntax" 
hoelzl@58606
    11
begin
hoelzl@58606
    12
hoelzl@58606
    13
section {* Sub-probability spaces *}
hoelzl@58606
    14
hoelzl@58606
    15
locale subprob_space = finite_measure +
hoelzl@58606
    16
  assumes emeasure_space_le_1: "emeasure M (space M) \<le> 1"
hoelzl@58606
    17
  assumes subprob_not_empty: "space M \<noteq> {}"
hoelzl@58606
    18
hoelzl@58606
    19
lemma subprob_spaceI[Pure.intro!]:
hoelzl@58606
    20
  assumes *: "emeasure M (space M) \<le> 1"
hoelzl@58606
    21
  assumes "space M \<noteq> {}"
hoelzl@58606
    22
  shows "subprob_space M"
hoelzl@58606
    23
proof -
hoelzl@58606
    24
  interpret finite_measure M
hoelzl@58606
    25
  proof
hoelzl@58606
    26
    show "emeasure M (space M) \<noteq> \<infinity>" using * by auto
hoelzl@58606
    27
  qed
hoelzl@58606
    28
  show "subprob_space M" by default fact+
hoelzl@58606
    29
qed
hoelzl@58606
    30
hoelzl@58606
    31
lemma prob_space_imp_subprob_space:
hoelzl@58606
    32
  "prob_space M \<Longrightarrow> subprob_space M"
hoelzl@58606
    33
  by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty)
hoelzl@58606
    34
hoelzl@59425
    35
lemma subprob_space_imp_sigma_finite: "subprob_space M \<Longrightarrow> sigma_finite_measure M"
hoelzl@59425
    36
  unfolding subprob_space_def finite_measure_def by simp
hoelzl@59425
    37
hoelzl@58606
    38
sublocale prob_space \<subseteq> subprob_space
hoelzl@58606
    39
  by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
hoelzl@58606
    40
Andreas@60067
    41
lemma subprob_space_sigma [simp]: "\<Omega> \<noteq> {} \<Longrightarrow> subprob_space (sigma \<Omega> X)"
Andreas@60067
    42
by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv)
Andreas@60067
    43
Andreas@60067
    44
lemma subprob_space_null_measure: "space M \<noteq> {} \<Longrightarrow> subprob_space (null_measure M)"
Andreas@60067
    45
by(simp add: null_measure_def)
Andreas@60067
    46
hoelzl@58606
    47
lemma (in subprob_space) subprob_space_distr:
hoelzl@58606
    48
  assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)"
hoelzl@58606
    49
proof (rule subprob_spaceI)
hoelzl@58606
    50
  have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
hoelzl@58606
    51
  with f show "emeasure (distr M M' f) (space (distr M M' f)) \<le> 1"
hoelzl@58606
    52
    by (auto simp: emeasure_distr emeasure_space_le_1)
hoelzl@58606
    53
  show "space (distr M M' f) \<noteq> {}" by (simp add: assms)
hoelzl@58606
    54
qed
hoelzl@58606
    55
hoelzl@59000
    56
lemma (in subprob_space) subprob_emeasure_le_1: "emeasure M X \<le> 1"
hoelzl@58606
    57
  by (rule order.trans[OF emeasure_space emeasure_space_le_1])
hoelzl@58606
    58
hoelzl@59000
    59
lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1"
hoelzl@59000
    60
  using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure)
hoelzl@59000
    61
Andreas@59427
    62
lemma (in subprob_space) nn_integral_le_const:
Andreas@59427
    63
  assumes "0 \<le> c" "AE x in M. f x \<le> c"
Andreas@59427
    64
  shows "(\<integral>\<^sup>+x. f x \<partial>M) \<le> c"
Andreas@59427
    65
proof -
Andreas@59427
    66
  have "(\<integral>\<^sup>+ x. f x \<partial>M) \<le> (\<integral>\<^sup>+ x. c \<partial>M)"
Andreas@59427
    67
    by(rule nn_integral_mono_AE) fact
Andreas@59427
    68
  also have "\<dots> \<le> c * emeasure M (space M)"
Andreas@59427
    69
    using \<open>0 \<le> c\<close> by(simp add: nn_integral_const_If)
Andreas@59427
    70
  also have "\<dots> \<le> c * 1" using emeasure_space_le_1 \<open>0 \<le> c\<close> by(rule ereal_mult_left_mono)
Andreas@59427
    71
  finally show ?thesis by simp
Andreas@59427
    72
qed
Andreas@59427
    73
hoelzl@59092
    74
lemma emeasure_density_distr_interval:
hoelzl@59092
    75
  fixes h :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real" and g' :: "real \<Rightarrow> real"
hoelzl@59092
    76
  assumes [simp]: "a \<le> b"
hoelzl@59092
    77
  assumes Mf[measurable]: "f \<in> borel_measurable borel"
hoelzl@59092
    78
  assumes Mg[measurable]: "g \<in> borel_measurable borel"
hoelzl@59092
    79
  assumes Mg'[measurable]: "g' \<in> borel_measurable borel"
hoelzl@59092
    80
  assumes Mh[measurable]: "h \<in> borel_measurable borel"
hoelzl@59092
    81
  assumes prob: "subprob_space (density lborel f)"
hoelzl@59092
    82
  assumes nonnegf: "\<And>x. f x \<ge> 0"
hoelzl@59092
    83
  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
hoelzl@59092
    84
  assumes contg': "continuous_on {a..b} g'"
hoelzl@59092
    85
  assumes mono: "strict_mono_on g {a..b}" and inv: "\<And>x. h x \<in> {a..b} \<Longrightarrow> g (h x) = x"
hoelzl@59092
    86
  assumes range: "{a..b} \<subseteq> range h"
hoelzl@59092
    87
  shows "emeasure (distr (density lborel f) lborel h) {a..b} = 
hoelzl@59092
    88
             emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}"
hoelzl@59092
    89
proof (cases "a < b")
hoelzl@59092
    90
  assume "a < b"
hoelzl@59092
    91
  from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
hoelzl@59092
    92
  from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on)
hoelzl@59092
    93
  from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0"
hoelzl@59092
    94
    by (rule mono_on_imp_deriv_nonneg) (auto simp: interior_atLeastAtMost_real)
hoelzl@59092
    95
  from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
hoelzl@59092
    96
    by (rule continuous_ge_on_Iii) (simp_all add: `a < b`)
hoelzl@59092
    97
hoelzl@59092
    98
  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
hoelzl@59092
    99
  have A: "h -` {a..b} = {g a..g b}"
hoelzl@59092
   100
  proof (intro equalityI subsetI)
hoelzl@59092
   101
    fix x assume x: "x \<in> h -` {a..b}"
hoelzl@59092
   102
    hence "g (h x) \<in> {g a..g b}" by (auto intro: mono_onD[OF mono'])
hoelzl@59092
   103
    with inv and x show "x \<in> {g a..g b}" by simp
hoelzl@59092
   104
  next
hoelzl@59092
   105
    fix y assume y: "y \<in> {g a..g b}"
hoelzl@59092
   106
    with IVT'[OF _ _ _ contg, of y] obtain x where "x \<in> {a..b}" "y = g x" by auto
hoelzl@59092
   107
    with range and inv show "y \<in> h -` {a..b}" by auto
hoelzl@59092
   108
  qed
hoelzl@59092
   109
hoelzl@59092
   110
  have prob': "subprob_space (distr (density lborel f) lborel h)"
hoelzl@59092
   111
    by (rule subprob_space.subprob_space_distr[OF prob]) (simp_all add: Mh)
hoelzl@59092
   112
  have B: "emeasure (distr (density lborel f) lborel h) {a..b} = 
hoelzl@59092
   113
            \<integral>\<^sup>+x. f x * indicator (h -` {a..b}) x \<partial>lborel"
hoelzl@59092
   114
    by (subst emeasure_distr) (simp_all add: emeasure_density Mf Mh measurable_sets_borel[OF Mh])
hoelzl@59092
   115
  also note A
hoelzl@59092
   116
  also have "emeasure (distr (density lborel f) lborel h) {a..b} \<le> 1"
hoelzl@59092
   117
    by (rule subprob_space.subprob_emeasure_le_1) (rule prob')
hoelzl@59092
   118
  hence "emeasure (distr (density lborel f) lborel h) {a..b} \<noteq> \<infinity>" by auto
hoelzl@59092
   119
  with assms have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
hoelzl@59092
   120
                      (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
hoelzl@59092
   121
    by (intro nn_integral_substitution_aux)
hoelzl@59092
   122
       (auto simp: derivg_nonneg A B emeasure_density mult.commute `a < b`)
hoelzl@59092
   123
  also have "... = emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}" 
hoelzl@59092
   124
    by (simp add: emeasure_density)
hoelzl@59092
   125
  finally show ?thesis .
hoelzl@59092
   126
next
hoelzl@59092
   127
  assume "\<not>a < b"
hoelzl@59092
   128
  with `a \<le> b` have [simp]: "b = a" by (simp add: not_less del: `a \<le> b`)
hoelzl@59092
   129
  from inv and range have "h -` {a} = {g a}" by auto
hoelzl@59092
   130
  thus ?thesis by (simp_all add: emeasure_distr emeasure_density measurable_sets_borel[OF Mh])
hoelzl@59092
   131
qed
hoelzl@59092
   132
hoelzl@58606
   133
locale pair_subprob_space = 
hoelzl@58606
   134
  pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
hoelzl@58606
   135
hoelzl@58606
   136
sublocale pair_subprob_space \<subseteq> P: subprob_space "M1 \<Otimes>\<^sub>M M2"
hoelzl@58606
   137
proof
hoelzl@58606
   138
  have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)"
haftmann@59559
   139
    by (metis monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)
hoelzl@58606
   140
  from this[OF _ _ M1.emeasure_space_le_1 M2.emeasure_space_le_1]
hoelzl@58606
   141
    show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) \<le> 1"
hoelzl@58606
   142
    by (simp add: M2.emeasure_pair_measure_Times space_pair_measure emeasure_nonneg)
hoelzl@58606
   143
  from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \<Otimes>\<^sub>M M2) \<noteq> {}"
hoelzl@58606
   144
    by (simp add: space_pair_measure)
hoelzl@58606
   145
qed
hoelzl@58606
   146
hoelzl@59425
   147
lemma subprob_space_null_measure_iff:
hoelzl@59425
   148
    "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}"
hoelzl@59425
   149
  by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)
hoelzl@59425
   150
Andreas@59525
   151
lemma subprob_space_restrict_space:
Andreas@59525
   152
  assumes M: "subprob_space M"
Andreas@59525
   153
  and A: "A \<inter> space M \<in> sets M" "A \<inter> space M \<noteq> {}"
Andreas@59525
   154
  shows "subprob_space (restrict_space M A)"
Andreas@59525
   155
proof(rule subprob_spaceI)
Andreas@59525
   156
  have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \<inter> space M)"
Andreas@59525
   157
    using A by(simp add: emeasure_restrict_space space_restrict_space)
Andreas@59525
   158
  also have "\<dots> \<le> 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M)
Andreas@59525
   159
  finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \<le> 1" .
Andreas@59525
   160
next
Andreas@59525
   161
  show "space (restrict_space M A) \<noteq> {}"
Andreas@59525
   162
    using A by(simp add: space_restrict_space)
Andreas@59525
   163
qed
Andreas@59525
   164
hoelzl@58606
   165
definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
hoelzl@58606
   166
  "subprob_algebra K =
hoelzl@58606
   167
    (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
hoelzl@58606
   168
hoelzl@58606
   169
lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}"
hoelzl@58606
   170
  by (auto simp add: subprob_algebra_def space_Sup_sigma)
hoelzl@58606
   171
hoelzl@58606
   172
lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N"
hoelzl@58606
   173
  by (simp add: subprob_algebra_def)
hoelzl@58606
   174
hoelzl@58606
   175
lemma measurable_emeasure_subprob_algebra[measurable]: 
hoelzl@58606
   176
  "a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)"
hoelzl@58606
   177
  by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def)
hoelzl@58606
   178
hoelzl@59000
   179
lemma subprob_measurableD:
hoelzl@59000
   180
  assumes N: "N \<in> measurable M (subprob_algebra S)" and x: "x \<in> space M"
hoelzl@59000
   181
  shows "space (N x) = space S"
hoelzl@59000
   182
    and "sets (N x) = sets S"
hoelzl@59000
   183
    and "measurable (N x) K = measurable S K"
hoelzl@59000
   184
    and "measurable K (N x) = measurable K S"
hoelzl@59000
   185
  using measurable_space[OF N x]
hoelzl@59000
   186
  by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)
hoelzl@59000
   187
hoelzl@59048
   188
ML {*
hoelzl@59048
   189
hoelzl@59048
   190
fun subprob_cong thm ctxt = (
hoelzl@59048
   191
  let
hoelzl@59048
   192
    val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm
wenzelm@59582
   193
    val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
hoelzl@59048
   194
      dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
hoelzl@59048
   195
  in
hoelzl@59048
   196
    if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt)
hoelzl@59048
   197
            else ([], ctxt)
hoelzl@59048
   198
  end
hoelzl@59048
   199
  handle THM _ => ([], ctxt) | TERM _ => ([], ctxt))
hoelzl@59048
   200
hoelzl@59048
   201
*}
hoelzl@59048
   202
hoelzl@59048
   203
setup \<open>
hoelzl@59048
   204
  Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong)
hoelzl@59048
   205
\<close>
hoelzl@59048
   206
hoelzl@58606
   207
context
hoelzl@58606
   208
  fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
hoelzl@58606
   209
begin
hoelzl@58606
   210
hoelzl@58606
   211
lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)"
hoelzl@58606
   212
  using measurable_space[OF K] by (simp add: space_subprob_algebra)
hoelzl@58606
   213
hoelzl@58606
   214
lemma sets_kernel: "a \<in> space M \<Longrightarrow> sets (K a) = sets N"
hoelzl@58606
   215
  using measurable_space[OF K] by (simp add: space_subprob_algebra)
hoelzl@58606
   216
hoelzl@58606
   217
lemma measurable_emeasure_kernel[measurable]: 
hoelzl@58606
   218
    "A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M"
hoelzl@58606
   219
  using measurable_compose[OF K measurable_emeasure_subprob_algebra] .
hoelzl@58606
   220
hoelzl@58606
   221
end
hoelzl@58606
   222
hoelzl@58606
   223
lemma measurable_subprob_algebra:
hoelzl@58606
   224
  "(\<And>a. a \<in> space M \<Longrightarrow> subprob_space (K a)) \<Longrightarrow>
hoelzl@58606
   225
  (\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow>
hoelzl@58606
   226
  (\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow>
hoelzl@58606
   227
  K \<in> measurable M (subprob_algebra N)"
hoelzl@58606
   228
  by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def)
hoelzl@58606
   229
hoelzl@59778
   230
lemma measurable_submarkov:
hoelzl@59778
   231
  "K \<in> measurable M (subprob_algebra M) \<longleftrightarrow>
hoelzl@59778
   232
    (\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
hoelzl@59778
   233
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> measurable M borel)"
hoelzl@59778
   234
proof
hoelzl@59778
   235
  assume "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
hoelzl@59778
   236
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
hoelzl@59778
   237
  then show "K \<in> measurable M (subprob_algebra M)"
hoelzl@59778
   238
    by (intro measurable_subprob_algebra) auto
hoelzl@59778
   239
next
hoelzl@59778
   240
  assume "K \<in> measurable M (subprob_algebra M)"
hoelzl@59778
   241
  then show "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
hoelzl@59778
   242
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
hoelzl@59778
   243
    by (auto dest: subprob_space_kernel sets_kernel)
hoelzl@59778
   244
qed
hoelzl@59778
   245
hoelzl@58606
   246
lemma space_subprob_algebra_empty_iff:
hoelzl@58606
   247
  "space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}"
hoelzl@58606
   248
proof
hoelzl@58606
   249
  have "\<And>x. x \<in> space N \<Longrightarrow> density N (\<lambda>_. 0) \<in> space (subprob_algebra N)"
hoelzl@58606
   250
    by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI)
hoelzl@58606
   251
  then show "space (subprob_algebra N) = {} \<Longrightarrow> space N = {}"
hoelzl@58606
   252
    by auto
hoelzl@58606
   253
next
hoelzl@58606
   254
  assume "space N = {}"
hoelzl@58606
   255
  hence "sets N = {{}}" by (simp add: space_empty_iff)
hoelzl@58606
   256
  moreover have "\<And>M. subprob_space M \<Longrightarrow> sets M \<noteq> {{}}"
hoelzl@58606
   257
    by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric])
hoelzl@58606
   258
  ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
hoelzl@58606
   259
qed
hoelzl@58606
   260
hoelzl@59048
   261
lemma nn_integral_measurable_subprob_algebra':
hoelzl@59000
   262
  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
hoelzl@59000
   263
  shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
hoelzl@59000
   264
  using f
hoelzl@59000
   265
proof induct
hoelzl@59000
   266
  case (cong f g)
hoelzl@59000
   267
  moreover have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. \<integral>\<^sup>+M''. g M'' \<partial>M') \<in> ?B"
hoelzl@59000
   268
    by (intro measurable_cong nn_integral_cong cong)
hoelzl@59000
   269
       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
hoelzl@59000
   270
  ultimately show ?case by simp
hoelzl@59000
   271
next
hoelzl@59000
   272
  case (set B)
hoelzl@59000
   273
  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
hoelzl@59000
   274
    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
hoelzl@59000
   275
  ultimately show ?case
hoelzl@59000
   276
    by (simp add: measurable_emeasure_subprob_algebra)
hoelzl@59000
   277
next
hoelzl@59000
   278
  case (mult f c)
hoelzl@59000
   279
  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
hoelzl@59048
   280
    by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
hoelzl@59000
   281
  ultimately show ?case
hoelzl@59048
   282
    using [[simp_trace_new]]
hoelzl@59000
   283
    by simp
hoelzl@59000
   284
next
hoelzl@59000
   285
  case (add f g)
hoelzl@59000
   286
  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
hoelzl@59048
   287
    by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
hoelzl@59000
   288
  ultimately show ?case
hoelzl@59000
   289
    by (simp add: ac_simps)
hoelzl@59000
   290
next
hoelzl@59000
   291
  case (seq F)
hoelzl@59000
   292
  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
hoelzl@59000
   293
    unfolding SUP_apply
hoelzl@59048
   294
    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)
hoelzl@59000
   295
  ultimately show ?case
hoelzl@59000
   296
    by (simp add: ac_simps)
hoelzl@59000
   297
qed
hoelzl@59000
   298
hoelzl@59048
   299
lemma nn_integral_measurable_subprob_algebra:
hoelzl@59048
   300
  "f \<in> borel_measurable N \<Longrightarrow> (\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)"
hoelzl@59048
   301
  by (subst nn_integral_max_0[symmetric])
hoelzl@59048
   302
     (auto intro!: nn_integral_measurable_subprob_algebra')
hoelzl@59048
   303
hoelzl@58606
   304
lemma measurable_distr:
hoelzl@58606
   305
  assumes [measurable]: "f \<in> measurable M N"
hoelzl@58606
   306
  shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
hoelzl@58606
   307
proof (cases "space N = {}")
hoelzl@58606
   308
  assume not_empty: "space N \<noteq> {}"
hoelzl@58606
   309
  show ?thesis
hoelzl@58606
   310
  proof (rule measurable_subprob_algebra)
hoelzl@58606
   311
    fix A assume A: "A \<in> sets N"
hoelzl@58606
   312
    then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow>
hoelzl@58606
   313
      (\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"
hoelzl@58606
   314
      by (intro measurable_cong)
hoelzl@59048
   315
         (auto simp: emeasure_distr space_subprob_algebra
hoelzl@59048
   316
               intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="op \<inter>"])
hoelzl@58606
   317
    also have "\<dots>"
hoelzl@58606
   318
      using A by (intro measurable_emeasure_subprob_algebra) simp
hoelzl@58606
   319
    finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .
hoelzl@59048
   320
  qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets)
hoelzl@58606
   321
qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
hoelzl@58606
   322
hoelzl@59000
   323
lemma emeasure_space_subprob_algebra[measurable]:
hoelzl@59000
   324
  "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"
hoelzl@59000
   325
proof-
hoelzl@59000
   326
  have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M")
hoelzl@59000
   327
    by (rule measurable_emeasure_subprob_algebra) simp
hoelzl@59000
   328
  also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
hoelzl@59000
   329
    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
hoelzl@59000
   330
  finally show ?thesis .
hoelzl@59000
   331
qed
hoelzl@59000
   332
Andreas@60067
   333
lemma integral_measurable_subprob_algebra:
Andreas@60067
   334
  fixes f :: "_ \<Rightarrow> real"
Andreas@60067
   335
  assumes f_measurable [measurable]: "f \<in> borel_measurable N"
Andreas@60067
   336
  and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B"
Andreas@60067
   337
  shows "(\<lambda>M. integral\<^sup>L M f) \<in> borel_measurable (subprob_algebra N)"
Andreas@60067
   338
proof -
Andreas@60067
   339
  note [measurable] = nn_integral_measurable_subprob_algebra
Andreas@60067
   340
  have "?thesis \<longleftrightarrow> (\<lambda>M. real (\<integral>\<^sup>+ x. f x \<partial>M) - real (\<integral>\<^sup>+ x. - f x \<partial>M)) \<in> borel_measurable (subprob_algebra N)"
Andreas@60067
   341
  proof(rule measurable_cong)
Andreas@60067
   342
    fix M
Andreas@60067
   343
    assume "M \<in> space (subprob_algebra N)"
Andreas@60067
   344
    hence "subprob_space M" and M [measurable_cong]: "sets M = sets N" 
Andreas@60067
   345
      by(simp_all add: space_subprob_algebra)
Andreas@60067
   346
    interpret subprob_space M by fact
Andreas@60067
   347
    have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M)"
Andreas@60067
   348
      by(rule nn_integral_mono)(simp add: sets_eq_imp_space_eq[OF M] f_bounded)
Andreas@60067
   349
    also have "\<dots> = max B 0 * emeasure M (space M)" by(simp add: nn_integral_const_If max_def)
Andreas@60067
   350
    also have "\<dots> \<le> ereal (max B 0) * 1"
Andreas@60067
   351
      by(rule ereal_mult_left_mono)(simp_all add: emeasure_space_le_1 zero_ereal_def)
Andreas@60067
   352
    finally have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<noteq> \<infinity>" by(auto simp add: max_def)
Andreas@60067
   353
    then have "integrable M f" using f_measurable
Andreas@60067
   354
      by(auto intro: integrableI_bounded)
Andreas@60067
   355
    thus "(\<integral> x. f x \<partial>M) = real (\<integral>\<^sup>+ x. f x \<partial>M) - real (\<integral>\<^sup>+ x. - f x \<partial>M)"
Andreas@60067
   356
      by(simp add: real_lebesgue_integral_def)
Andreas@60067
   357
  qed
Andreas@60067
   358
  also have "\<dots>" by measurable
Andreas@60067
   359
  finally show ?thesis .
Andreas@60067
   360
qed
Andreas@60067
   361
wenzelm@59978
   362
(* TODO: Rename. This name is too general -- Manuel *)
hoelzl@59000
   363
lemma measurable_pair_measure:
hoelzl@59000
   364
  assumes f: "f \<in> measurable M (subprob_algebra N)"
hoelzl@59000
   365
  assumes g: "g \<in> measurable M (subprob_algebra L)"
hoelzl@59000
   366
  shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
hoelzl@59000
   367
proof (rule measurable_subprob_algebra)
hoelzl@59000
   368
  { fix x assume "x \<in> space M"
hoelzl@59000
   369
    with measurable_space[OF f] measurable_space[OF g]
hoelzl@59000
   370
    have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"
hoelzl@59000
   371
      by auto
hoelzl@59000
   372
    interpret F: subprob_space "f x"
hoelzl@59000
   373
      using fx by (simp add: space_subprob_algebra)
hoelzl@59000
   374
    interpret G: subprob_space "g x"
hoelzl@59000
   375
      using gx by (simp add: space_subprob_algebra)
hoelzl@59000
   376
hoelzl@59000
   377
    interpret pair_subprob_space "f x" "g x" ..
hoelzl@59000
   378
    show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales
hoelzl@59000
   379
    show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"
hoelzl@59000
   380
      using fx gx by (simp add: space_subprob_algebra)
hoelzl@59000
   381
hoelzl@59000
   382
    have 1: "\<And>A B. A \<in> sets N \<Longrightarrow> B \<in> sets L \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (A \<times> B) = emeasure (f x) A * emeasure (g x) B"
hoelzl@59000
   383
      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 
hoelzl@59000
   384
    have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 
hoelzl@59000
   385
              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
hoelzl@59000
   386
      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
hoelzl@59000
   387
    hence 2: "\<And>A. A \<in> sets (N \<Otimes>\<^sub>M L) \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (space N \<times> space L - A) =
hoelzl@59000
   388
                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
hoelzl@59000
   389
      using emeasure_compl[OF _ P.emeasure_finite]
hoelzl@59000
   390
      unfolding sets_eq
hoelzl@59000
   391
      unfolding sets_eq_imp_space_eq[OF sets_eq]
hoelzl@59000
   392
      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
hoelzl@59000
   393
    note 1 2 sets_eq }
hoelzl@59000
   394
  note Times = this(1) and Compl = this(2) and sets_eq = this(3)
hoelzl@59000
   395
hoelzl@59000
   396
  fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
hoelzl@59000
   397
  show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"
hoelzl@59000
   398
    using Int_stable_pair_measure_generator pair_measure_closed A
hoelzl@59000
   399
    unfolding sets_pair_measure
hoelzl@59000
   400
  proof (induct A rule: sigma_sets_induct_disjoint)
hoelzl@59000
   401
    case (basic A) then show ?case
hoelzl@59000
   402
      by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)
hoelzl@59000
   403
         (auto intro!: measurable_emeasure_kernel f g)
hoelzl@59000
   404
  next
hoelzl@59000
   405
    case (compl A)
hoelzl@59000
   406
    then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
hoelzl@59000
   407
      by (auto simp: sets_pair_measure)
hoelzl@59000
   408
    have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 
hoelzl@59000
   409
                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
hoelzl@59000
   410
      using compl(2) f g by measurable
hoelzl@59000
   411
    thus ?case by (simp add: Compl A cong: measurable_cong)
hoelzl@59000
   412
  next
hoelzl@59000
   413
    case (union A)
hoelzl@59000
   414
    then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"
hoelzl@59000
   415
      by (auto simp: sets_pair_measure)
hoelzl@59000
   416
    then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>
hoelzl@59000
   417
      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
hoelzl@59000
   418
      by (intro measurable_cong suminf_emeasure[symmetric])
hoelzl@59000
   419
         (auto simp: sets_eq)
hoelzl@59000
   420
    also have "\<dots>"
hoelzl@59000
   421
      using union by auto
hoelzl@59000
   422
    finally show ?case .
hoelzl@59000
   423
  qed simp
hoelzl@59000
   424
qed
hoelzl@59000
   425
hoelzl@59000
   426
lemma restrict_space_measurable:
hoelzl@59000
   427
  assumes X: "X \<noteq> {}" "X \<in> sets K"
hoelzl@59000
   428
  assumes N: "N \<in> measurable M (subprob_algebra K)"
hoelzl@59000
   429
  shows "(\<lambda>x. restrict_space (N x) X) \<in> measurable M (subprob_algebra (restrict_space K X))"
hoelzl@59000
   430
proof (rule measurable_subprob_algebra)
hoelzl@59000
   431
  fix a assume a: "a \<in> space M"
hoelzl@59000
   432
  from N[THEN measurable_space, OF this]
hoelzl@59000
   433
  have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K"
hoelzl@59000
   434
    by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
hoelzl@59000
   435
  then interpret subprob_space "N a"
hoelzl@59000
   436
    by simp
hoelzl@59000
   437
  show "subprob_space (restrict_space (N a) X)"
hoelzl@59000
   438
  proof
hoelzl@59000
   439
    show "space (restrict_space (N a) X) \<noteq> {}"
hoelzl@59000
   440
      using X by (auto simp add: space_restrict_space)
hoelzl@59000
   441
    show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \<le> 1"
hoelzl@59000
   442
      using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1)
hoelzl@59000
   443
  qed
hoelzl@59000
   444
  show "sets (restrict_space (N a) X) = sets (restrict_space K X)"
hoelzl@59000
   445
    by (intro sets_restrict_space_cong) fact
hoelzl@59000
   446
next
hoelzl@59000
   447
  fix A assume A: "A \<in> sets (restrict_space K X)"
hoelzl@59000
   448
  show "(\<lambda>a. emeasure (restrict_space (N a) X) A) \<in> borel_measurable M"
hoelzl@59000
   449
  proof (subst measurable_cong)
hoelzl@59000
   450
    fix a assume "a \<in> space M"
hoelzl@59000
   451
    from N[THEN measurable_space, OF this]
hoelzl@59000
   452
    have [simp]: "sets (N a) = sets K" "space (N a) = space K"
hoelzl@59000
   453
      by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
hoelzl@59000
   454
    show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \<inter> X)"
hoelzl@59000
   455
      using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps)
hoelzl@59000
   456
  next
hoelzl@59000
   457
    show "(\<lambda>w. emeasure (N w) (A \<inter> X)) \<in> borel_measurable M"
hoelzl@59000
   458
      using A X
hoelzl@59000
   459
      by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra])
hoelzl@59000
   460
         (auto simp: sets_restrict_space)
hoelzl@59000
   461
  qed
hoelzl@59000
   462
qed
hoelzl@59000
   463
hoelzl@58606
   464
section {* Properties of return *}
hoelzl@58606
   465
hoelzl@58606
   466
definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where
hoelzl@58606
   467
  "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)"
hoelzl@58606
   468
hoelzl@58606
   469
lemma space_return[simp]: "space (return M x) = space M"
hoelzl@58606
   470
  by (simp add: return_def)
hoelzl@58606
   471
hoelzl@58606
   472
lemma sets_return[simp]: "sets (return M x) = sets M"
hoelzl@58606
   473
  by (simp add: return_def)
hoelzl@58606
   474
hoelzl@58606
   475
lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"
hoelzl@58606
   476
  by (simp cong: measurable_cong_sets) 
hoelzl@58606
   477
hoelzl@58606
   478
lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
hoelzl@58606
   479
  by (simp cong: measurable_cong_sets) 
hoelzl@58606
   480
hoelzl@59000
   481
lemma return_sets_cong: "sets M = sets N \<Longrightarrow> return M = return N"
hoelzl@59000
   482
  by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def)
hoelzl@59000
   483
hoelzl@59000
   484
lemma return_cong: "sets A = sets B \<Longrightarrow> return A x = return B x"
hoelzl@59000
   485
  by (auto simp add: return_def dest: sets_eq_imp_space_eq)
hoelzl@59000
   486
hoelzl@58606
   487
lemma emeasure_return[simp]:
hoelzl@58606
   488
  assumes "A \<in> sets M"
hoelzl@58606
   489
  shows "emeasure (return M x) A = indicator A x"
hoelzl@58606
   490
proof (rule emeasure_measure_of[OF return_def])
hoelzl@58606
   491
  show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed)
hoelzl@58606
   492
  show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def)
hoelzl@58606
   493
  from assms show "A \<in> sets (return M x)" unfolding return_def by simp
hoelzl@58606
   494
  show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)"
hoelzl@58606
   495
    by (auto intro: countably_additiveI simp: suminf_indicator)
hoelzl@58606
   496
qed
hoelzl@58606
   497
hoelzl@58606
   498
lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)"
hoelzl@58606
   499
  by rule simp
hoelzl@58606
   500
hoelzl@58606
   501
lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"
hoelzl@58606
   502
  by (intro prob_space_return prob_space_imp_subprob_space)
hoelzl@58606
   503
hoelzl@59000
   504
lemma subprob_space_return_ne: 
hoelzl@59000
   505
  assumes "space M \<noteq> {}" shows "subprob_space (return M x)"
hoelzl@59000
   506
proof
hoelzl@59000
   507
  show "emeasure (return M x) (space (return M x)) \<le> 1"
hoelzl@59000
   508
    by (subst emeasure_return) (auto split: split_indicator)
hoelzl@59000
   509
qed (simp, fact)
hoelzl@59000
   510
hoelzl@59000
   511
lemma measure_return: assumes X: "X \<in> sets M" shows "measure (return M x) X = indicator X x"
hoelzl@59000
   512
  unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator)
hoelzl@59000
   513
hoelzl@58606
   514
lemma AE_return:
hoelzl@58606
   515
  assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P"
hoelzl@58606
   516
  shows "(AE y in return M x. P y) \<longleftrightarrow> P x"
hoelzl@58606
   517
proof -
hoelzl@58606
   518
  have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x"
hoelzl@58606
   519
    by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator)
hoelzl@58606
   520
  also have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> (AE y in return M x. P y)"
hoelzl@58606
   521
    by (rule AE_cong) auto
hoelzl@58606
   522
  finally show ?thesis .
hoelzl@58606
   523
qed
hoelzl@58606
   524
  
hoelzl@58606
   525
lemma nn_integral_return:
hoelzl@58606
   526
  assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M"
hoelzl@58606
   527
  shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x"
hoelzl@58606
   528
proof-
hoelzl@58606
   529
  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
hoelzl@58606
   530
  have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms
hoelzl@58606
   531
    by (intro nn_integral_cong_AE) (auto simp: AE_return)
hoelzl@58606
   532
  also have "... = g x"
hoelzl@58606
   533
    using nn_integral_const[OF `g x \<ge> 0`, of "return M x"] emeasure_space_1 by simp
hoelzl@58606
   534
  finally show ?thesis .
hoelzl@58606
   535
qed
hoelzl@58606
   536
hoelzl@59000
   537
lemma integral_return:
hoelzl@59000
   538
  fixes g :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
hoelzl@59000
   539
  assumes "x \<in> space M" "g \<in> borel_measurable M"
hoelzl@59000
   540
  shows "(\<integral>a. g a \<partial>return M x) = g x"
hoelzl@59000
   541
proof-
hoelzl@59000
   542
  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
hoelzl@59000
   543
  have "(\<integral>a. g a \<partial>return M x) = (\<integral>a. g x \<partial>return M x)" using assms
hoelzl@59000
   544
    by (intro integral_cong_AE) (auto simp: AE_return)
hoelzl@59000
   545
  then show ?thesis
hoelzl@59000
   546
    using prob_space by simp
hoelzl@59000
   547
qed
hoelzl@59000
   548
hoelzl@59000
   549
lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)"
hoelzl@58606
   550
  by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)
hoelzl@58606
   551
hoelzl@58606
   552
lemma distr_return:
hoelzl@58606
   553
  assumes "f \<in> measurable M N" and "x \<in> space M"
hoelzl@58606
   554
  shows "distr (return M x) N f = return N (f x)"
hoelzl@58606
   555
  using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)
hoelzl@58606
   556
hoelzl@59000
   557
lemma return_restrict_space:
hoelzl@59000
   558
  "\<Omega> \<in> sets M \<Longrightarrow> return (restrict_space M \<Omega>) x = restrict_space (return M x) \<Omega>"
hoelzl@59000
   559
  by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)
hoelzl@59000
   560
hoelzl@59000
   561
lemma measurable_distr2:
hoelzl@59000
   562
  assumes f[measurable]: "split f \<in> measurable (L \<Otimes>\<^sub>M M) N"
hoelzl@59000
   563
  assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
hoelzl@59000
   564
  shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
hoelzl@59000
   565
proof -
hoelzl@59000
   566
  have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
hoelzl@59000
   567
    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (split f)) \<in> measurable L (subprob_algebra N)"
hoelzl@59000
   568
  proof (rule measurable_cong)
hoelzl@59000
   569
    fix x assume x: "x \<in> space L"
hoelzl@59000
   570
    have gx: "g x \<in> space (subprob_algebra M)"
hoelzl@59000
   571
      using measurable_space[OF g x] .
hoelzl@59000
   572
    then have [simp]: "sets (g x) = sets M"
hoelzl@59000
   573
      by (simp add: space_subprob_algebra)
hoelzl@59000
   574
    then have [simp]: "space (g x) = space M"
hoelzl@59000
   575
      by (rule sets_eq_imp_space_eq)
hoelzl@59000
   576
    let ?R = "return L x"
hoelzl@59000
   577
    from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"
hoelzl@59000
   578
      by simp
hoelzl@59000
   579
    interpret subprob_space "g x"
hoelzl@59000
   580
      using gx by (simp add: space_subprob_algebra)
hoelzl@59000
   581
    have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
hoelzl@59000
   582
      by (simp add: space_pair_measure)
hoelzl@59000
   583
    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (split f)" (is "?l = ?r")
hoelzl@59000
   584
    proof (rule measure_eqI)
hoelzl@59000
   585
      show "sets ?l = sets ?r"
hoelzl@59000
   586
        by simp
hoelzl@59000
   587
    next
hoelzl@59000
   588
      fix A assume "A \<in> sets ?l"
hoelzl@59000
   589
      then have A[measurable]: "A \<in> sets N"
hoelzl@59000
   590
        by simp
hoelzl@59000
   591
      then have "emeasure ?r A = emeasure (?R \<Otimes>\<^sub>M g x) ((\<lambda>(x, y). f x y) -` A \<inter> space (?R \<Otimes>\<^sub>M g x))"
hoelzl@59000
   592
        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
hoelzl@59000
   593
      also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)"
hoelzl@59000
   594
        apply (subst emeasure_pair_measure_alt)
hoelzl@59000
   595
        apply (rule measurable_sets[OF _ A])
hoelzl@59000
   596
        apply (auto simp add: f_M' cong: measurable_cong_sets)
hoelzl@59000
   597
        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
hoelzl@59000
   598
        apply (auto simp: space_subprob_algebra space_pair_measure)
hoelzl@59000
   599
        done
hoelzl@59000
   600
      also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)"
hoelzl@59000
   601
        by (subst nn_integral_return)
hoelzl@59000
   602
           (auto simp: x intro!: measurable_emeasure)
hoelzl@59000
   603
      also have "\<dots> = emeasure ?l A"
hoelzl@59000
   604
        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
hoelzl@59000
   605
      finally show "emeasure ?l A = emeasure ?r A" ..
hoelzl@59000
   606
    qed
hoelzl@59000
   607
  qed
hoelzl@59000
   608
  also have "\<dots>"
hoelzl@59000
   609
    apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])
hoelzl@59000
   610
    apply (rule return_measurable)
hoelzl@59000
   611
    apply measurable
hoelzl@59000
   612
    done
hoelzl@59000
   613
  finally show ?thesis .
hoelzl@59000
   614
qed
hoelzl@59000
   615
hoelzl@59000
   616
lemma nn_integral_measurable_subprob_algebra2:
hoelzl@59048
   617
  assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"
hoelzl@59000
   618
  assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)"
hoelzl@59000
   619
  shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
hoelzl@59000
   620
proof -
hoelzl@59048
   621
  note nn_integral_measurable_subprob_algebra[measurable]
hoelzl@59048
   622
  note measurable_distr2[measurable]
hoelzl@59000
   623
  have "(\<lambda>x. integral\<^sup>N (distr (L x) (M \<Otimes>\<^sub>M N) (\<lambda>y. (x, y))) (\<lambda>(x, y). f x y)) \<in> borel_measurable M"
hoelzl@59048
   624
    by measurable
hoelzl@59000
   625
  then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
hoelzl@59048
   626
    by (rule measurable_cong[THEN iffD1, rotated])
hoelzl@59048
   627
       (simp add: nn_integral_distr)
hoelzl@59000
   628
qed
hoelzl@59000
   629
hoelzl@59000
   630
lemma emeasure_measurable_subprob_algebra2:
hoelzl@59000
   631
  assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"
hoelzl@59000
   632
  assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"
hoelzl@59000
   633
  shows "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"
hoelzl@59000
   634
proof -
hoelzl@59000
   635
  { fix x assume "x \<in> space M"
hoelzl@59000
   636
    then have "Pair x -` Sigma (space M) A = A x"
hoelzl@59000
   637
      by auto
hoelzl@59000
   638
    with sets_Pair1[OF A, of x] have "A x \<in> sets N"
hoelzl@59000
   639
      by auto }
hoelzl@59000
   640
  note ** = this
hoelzl@59000
   641
hoelzl@59000
   642
  have *: "\<And>x. fst x \<in> space M \<Longrightarrow> snd x \<in> A (fst x) \<longleftrightarrow> x \<in> (SIGMA x:space M. A x)"
hoelzl@59000
   643
    by (auto simp: fun_eq_iff)
hoelzl@59000
   644
  have "(\<lambda>(x, y). indicator (A x) y::ereal) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"
hoelzl@59000
   645
    apply measurable
hoelzl@59000
   646
    apply (subst measurable_cong)
hoelzl@59000
   647
    apply (rule *)
hoelzl@59000
   648
    apply (auto simp: space_pair_measure)
hoelzl@59000
   649
    done
hoelzl@59000
   650
  then have "(\<lambda>x. integral\<^sup>N (L x) (indicator (A x))) \<in> borel_measurable M"
hoelzl@59000
   651
    by (intro nn_integral_measurable_subprob_algebra2[where N=N] ereal_indicator_nonneg L)
hoelzl@59000
   652
  then show "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"
hoelzl@59000
   653
    apply (rule measurable_cong[THEN iffD1, rotated])
hoelzl@59000
   654
    apply (rule nn_integral_indicator)
hoelzl@59000
   655
    apply (simp add: subprob_measurableD[OF L] **)
hoelzl@59000
   656
    done
hoelzl@59000
   657
qed
hoelzl@59000
   658
hoelzl@59000
   659
lemma measure_measurable_subprob_algebra2:
hoelzl@59000
   660
  assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"
hoelzl@59000
   661
  assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"
hoelzl@59000
   662
  shows "(\<lambda>x. measure (L x) (A x)) \<in> borel_measurable M"
hoelzl@59000
   663
  unfolding measure_def
hoelzl@59000
   664
  by (intro borel_measurable_real_of_ereal emeasure_measurable_subprob_algebra2[OF assms])
hoelzl@59000
   665
hoelzl@58606
   666
definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"
hoelzl@58606
   667
hoelzl@58606
   668
lemma select_sets1:
hoelzl@58606
   669
  "sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))"
hoelzl@58606
   670
  unfolding select_sets_def by (rule someI)
hoelzl@58606
   671
hoelzl@58606
   672
lemma sets_select_sets[simp]:
hoelzl@58606
   673
  assumes sets: "sets M = sets (subprob_algebra N)"
hoelzl@58606
   674
  shows "sets (select_sets M) = sets N"
hoelzl@58606
   675
  unfolding select_sets_def
hoelzl@58606
   676
proof (rule someI2)
hoelzl@58606
   677
  show "sets M = sets (subprob_algebra N)"
hoelzl@58606
   678
    by fact
hoelzl@58606
   679
next
hoelzl@58606
   680
  fix L assume "sets M = sets (subprob_algebra L)"
hoelzl@58606
   681
  with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)"
hoelzl@58606
   682
    by (intro sets_eq_imp_space_eq) simp
hoelzl@58606
   683
  show "sets L = sets N"
hoelzl@58606
   684
  proof cases
hoelzl@58606
   685
    assume "space (subprob_algebra N) = {}"
hoelzl@58606
   686
    with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L]
hoelzl@58606
   687
    show ?thesis
hoelzl@58606
   688
      by (simp add: eq space_empty_iff)
hoelzl@58606
   689
  next
hoelzl@58606
   690
    assume "space (subprob_algebra N) \<noteq> {}"
hoelzl@58606
   691
    with eq show ?thesis
hoelzl@58606
   692
      by (fastforce simp add: space_subprob_algebra)
hoelzl@58606
   693
  qed
hoelzl@58606
   694
qed
hoelzl@58606
   695
hoelzl@58606
   696
lemma space_select_sets[simp]:
hoelzl@58606
   697
  "sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N"
hoelzl@58606
   698
  by (intro sets_eq_imp_space_eq sets_select_sets)
hoelzl@58606
   699
hoelzl@58606
   700
section {* Join *}
hoelzl@58606
   701
hoelzl@58606
   702
definition join :: "'a measure measure \<Rightarrow> 'a measure" where
hoelzl@58606
   703
  "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
hoelzl@58606
   704
hoelzl@58606
   705
lemma
hoelzl@58606
   706
  shows space_join[simp]: "space (join M) = space (select_sets M)"
hoelzl@58606
   707
    and sets_join[simp]: "sets (join M) = sets (select_sets M)"
hoelzl@58606
   708
  by (simp_all add: join_def)
hoelzl@58606
   709
hoelzl@58606
   710
lemma emeasure_join:
hoelzl@59048
   711
  assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
hoelzl@58606
   712
  shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
hoelzl@58606
   713
proof (rule emeasure_measure_of[OF join_def])
hoelzl@58606
   714
  show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
hoelzl@58606
   715
  proof (rule countably_additiveI)
hoelzl@58606
   716
    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"
hoelzl@58606
   717
    have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"
hoelzl@59048
   718
      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra)
hoelzl@58606
   719
    also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"
hoelzl@58606
   720
    proof (rule nn_integral_cong)
hoelzl@58606
   721
      fix M' assume "M' \<in> space M"
hoelzl@58606
   722
      then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)"
hoelzl@58606
   723
        using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra)
hoelzl@58606
   724
    qed
hoelzl@58606
   725
    finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" .
hoelzl@58606
   726
  qed
hoelzl@58606
   727
qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg)
hoelzl@58606
   728
hoelzl@58606
   729
lemma measurable_join:
hoelzl@58606
   730
  "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
hoelzl@58606
   731
proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra)
hoelzl@58606
   732
  fix A assume "A \<in> sets N"
hoelzl@58606
   733
  let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))"
hoelzl@58606
   734
  have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B"
hoelzl@58606
   735
  proof (rule measurable_cong)
hoelzl@58606
   736
    fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))"
hoelzl@58606
   737
    then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')"
hoelzl@58606
   738
      by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`)
hoelzl@58606
   739
  qed
hoelzl@58606
   740
  also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"
hoelzl@59048
   741
    using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`]
hoelzl@58606
   742
    by (rule nn_integral_measurable_subprob_algebra)
hoelzl@58606
   743
  finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .
hoelzl@58606
   744
next
hoelzl@58606
   745
  assume [simp]: "space N \<noteq> {}"
hoelzl@58606
   746
  fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))"
hoelzl@58606
   747
  then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)"
hoelzl@58606
   748
    apply (intro nn_integral_mono)
hoelzl@58606
   749
    apply (auto simp: space_subprob_algebra 
hoelzl@58606
   750
                 dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1)
hoelzl@58606
   751
    done
hoelzl@58606
   752
  with M show "subprob_space (join M)"
hoelzl@58606
   753
    by (intro subprob_spaceI)
hoelzl@58606
   754
       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
hoelzl@58606
   755
next
hoelzl@58606
   756
  assume "\<not>(space N \<noteq> {})"
hoelzl@58606
   757
  thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
hoelzl@58606
   758
qed (auto simp: space_subprob_algebra)
hoelzl@58606
   759
hoelzl@59048
   760
lemma nn_integral_join':
hoelzl@59048
   761
  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
hoelzl@59048
   762
    and M[measurable_cong]: "sets M = sets (subprob_algebra N)"
hoelzl@58606
   763
  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
hoelzl@58606
   764
  using f
hoelzl@58606
   765
proof induct
hoelzl@58606
   766
  case (cong f g)
hoelzl@58606
   767
  moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g"
hoelzl@58606
   768
    by (intro nn_integral_cong cong) (simp add: M)
hoelzl@58606
   769
  moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)"
hoelzl@58606
   770
    by (intro nn_integral_cong cong)
hoelzl@58606
   771
       (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq)
hoelzl@58606
   772
  ultimately show ?case
hoelzl@58606
   773
    by simp
hoelzl@58606
   774
next
hoelzl@58606
   775
  case (set A)
hoelzl@58606
   776
  moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 
hoelzl@58606
   777
    by (intro nn_integral_cong nn_integral_indicator)
hoelzl@58606
   778
       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
hoelzl@58606
   779
  ultimately show ?case
hoelzl@58606
   780
    using M by (simp add: emeasure_join)
hoelzl@58606
   781
next
hoelzl@58606
   782
  case (mult f c)
hoelzl@58606
   783
  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. c * f x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. c * \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
hoelzl@59048
   784
    using mult M M[THEN sets_eq_imp_space_eq]
hoelzl@59048
   785
    by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
hoelzl@58606
   786
  also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
hoelzl@59048
   787
    using nn_integral_measurable_subprob_algebra[OF mult(3)]
hoelzl@58606
   788
    by (intro nn_integral_cmult mult) (simp add: M)
hoelzl@58606
   789
  also have "\<dots> = c * (integral\<^sup>N (join M) f)"
hoelzl@58606
   790
    by (simp add: mult)
hoelzl@58606
   791
  also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"
hoelzl@59048
   792
    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets)
hoelzl@58606
   793
  finally show ?case by simp
hoelzl@58606
   794
next
hoelzl@58606
   795
  case (add f g)
hoelzl@58606
   796
  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x + g x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (\<integral>\<^sup>+ x. f x \<partial>M') + (\<integral>\<^sup>+ x. g x \<partial>M') \<partial>M)"
hoelzl@59048
   797
    using add M M[THEN sets_eq_imp_space_eq]
hoelzl@59048
   798
    by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra)
hoelzl@58606
   799
  also have "\<dots> = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) + (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. g x \<partial>M' \<partial>M)"
hoelzl@59048
   800
    using nn_integral_measurable_subprob_algebra[OF add(1)]
hoelzl@59048
   801
    using nn_integral_measurable_subprob_algebra[OF add(5)]
hoelzl@58606
   802
    by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)
hoelzl@58606
   803
  also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
hoelzl@58606
   804
    by (simp add: add)
hoelzl@58606
   805
  also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
hoelzl@59048
   806
    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets)
hoelzl@58606
   807
  finally show ?case by (simp add: ac_simps)
hoelzl@58606
   808
next
hoelzl@58606
   809
  case (seq F)
hoelzl@58606
   810
  have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. (SUP i. F i) x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (SUP i. \<integral>\<^sup>+ x. F i x \<partial>M') \<partial>M)"
hoelzl@59048
   811
    using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply
hoelzl@58606
   812
    by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
hoelzl@59048
   813
       (auto simp add: space_subprob_algebra)
hoelzl@58606
   814
  also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"
hoelzl@59048
   815
    using nn_integral_measurable_subprob_algebra[OF seq(1)] seq
hoelzl@58606
   816
    by (intro nn_integral_monotone_convergence_SUP)
hoelzl@58606
   817
       (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
hoelzl@58606
   818
  also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"
hoelzl@58606
   819
    by (simp add: seq)
hoelzl@58606
   820
  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
hoelzl@59048
   821
    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)
hoelzl@59048
   822
                 (simp_all add: M cong: measurable_cong_sets)
hoelzl@58606
   823
  finally show ?case by (simp add: ac_simps)
hoelzl@58606
   824
qed
hoelzl@58606
   825
hoelzl@59048
   826
lemma nn_integral_join:
hoelzl@59048
   827
  assumes f[measurable]: "f \<in> borel_measurable N" "sets M = sets (subprob_algebra N)"
hoelzl@59048
   828
  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
hoelzl@59048
   829
  apply (subst (1 3) nn_integral_max_0[symmetric])
hoelzl@59048
   830
  apply (rule nn_integral_join')
hoelzl@59048
   831
  apply (auto simp: f)
hoelzl@59048
   832
  done
hoelzl@59048
   833
Andreas@60067
   834
lemma measurable_join1:
Andreas@60067
   835
  "\<lbrakk> f \<in> measurable N K; sets M = sets (subprob_algebra N) \<rbrakk>
Andreas@60067
   836
  \<Longrightarrow> f \<in> measurable (join M) K"
Andreas@60067
   837
by(simp add: measurable_def)
Andreas@60067
   838
Andreas@60067
   839
lemma 
Andreas@60067
   840
  fixes f :: "_ \<Rightarrow> real"
Andreas@60067
   841
  assumes f_measurable [measurable]: "f \<in> borel_measurable N"
Andreas@60067
   842
  and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
Andreas@60067
   843
  and M [measurable_cong]: "sets M = sets (subprob_algebra N)"
Andreas@60067
   844
  and fin: "finite_measure M"
Andreas@60067
   845
  and M_bounded: "AE M' in M. emeasure M' (space M') \<le> ereal B'"
Andreas@60067
   846
  shows integrable_join: "integrable (join M) f" (is ?integrable)
Andreas@60067
   847
  and integral_join: "integral\<^sup>L (join M) f = \<integral> M'. integral\<^sup>L M' f \<partial>M" (is ?integral)
Andreas@60067
   848
proof(case_tac [!] "space N = {}")
Andreas@60067
   849
  assume *: "space N = {}"
Andreas@60067
   850
  show ?integrable 
Andreas@60067
   851
    using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
Andreas@60067
   852
  have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
Andreas@60067
   853
  proof(rule integral_cong)
Andreas@60067
   854
    fix M'
Andreas@60067
   855
    assume "M' \<in> space M"
Andreas@60067
   856
    with sets_eq_imp_space_eq[OF M] have "space M' = space N"
Andreas@60067
   857
      by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
Andreas@60067
   858
    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
Andreas@60067
   859
  qed simp
Andreas@60067
   860
  then show ?integral
Andreas@60067
   861
    using M * by(simp add: integral_empty)
Andreas@60067
   862
next
Andreas@60067
   863
  assume *: "space N \<noteq> {}"
Andreas@60067
   864
Andreas@60067
   865
  from * have B [simp]: "0 \<le> B" by(auto dest: f_bounded)
Andreas@60067
   866
Andreas@60067
   867
  have [measurable]: "f \<in> borel_measurable (join M)" using f_measurable M
Andreas@60067
   868
    by(rule measurable_join1)
Andreas@60067
   869
Andreas@60067
   870
  { fix f M'
Andreas@60067
   871
    assume [measurable]: "f \<in> borel_measurable N"
Andreas@60067
   872
      and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"
Andreas@60067
   873
      and "M' \<in> space M" "emeasure M' (space M') \<le> ereal B'"
Andreas@60067
   874
    have "AE x in M'. ereal (f x) \<le> ereal B"
Andreas@60067
   875
    proof(rule AE_I2)
Andreas@60067
   876
      fix x
Andreas@60067
   877
      assume "x \<in> space M'"
Andreas@60067
   878
      with \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
Andreas@60067
   879
      have "x \<in> space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
Andreas@60067
   880
      from f_bounded[OF this] show "ereal (f x) \<le> ereal B" by simp
Andreas@60067
   881
    qed
Andreas@60067
   882
    then have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M')"
Andreas@60067
   883
      by(rule nn_integral_mono_AE)
Andreas@60067
   884
    also have "\<dots> = ereal B * emeasure M' (space M')" by(simp)
Andreas@60067
   885
    also have "\<dots> \<le> ereal B * ereal B'" by(rule ereal_mult_left_mono)(fact, simp)
Andreas@60067
   886
    also have "\<dots> \<le> ereal B * ereal \<bar>B'\<bar>" by(rule ereal_mult_left_mono)(simp_all)
Andreas@60067
   887
    finally have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)" by simp }
Andreas@60067
   888
  note bounded1 = this
Andreas@60067
   889
Andreas@60067
   890
  have bounded:
Andreas@60067
   891
    "\<And>f. \<lbrakk> f \<in> borel_measurable N; \<And>x. x \<in> space N \<Longrightarrow> f x \<le> B \<rbrakk>
Andreas@60067
   892
    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"
Andreas@60067
   893
  proof -
Andreas@60067
   894
    fix f
Andreas@60067
   895
    assume [measurable]: "f \<in> borel_measurable N"
Andreas@60067
   896
      and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"
Andreas@60067
   897
    have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. ereal (f x) \<partial>M' \<partial>M)"
Andreas@60067
   898
      by(rule nn_integral_join[OF _ M]) simp
Andreas@60067
   899
    also have "\<dots> \<le> \<integral>\<^sup>+ M'. B * \<bar>B'\<bar> \<partial>M"
Andreas@60067
   900
      using bounded1[OF \<open>f \<in> borel_measurable N\<close> f_bounded]
Andreas@60067
   901
      by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format])
Andreas@60067
   902
    also have "\<dots> = B * \<bar>B'\<bar> * emeasure M (space M)" by simp
Andreas@60067
   903
    also have "\<dots> < \<infinity>" by(simp add: finite_measure.finite_emeasure_space[OF fin])
Andreas@60067
   904
    finally show "?thesis f" by simp
Andreas@60067
   905
  qed
Andreas@60067
   906
  have f_pos: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"
Andreas@60067
   907
    and f_neg: "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>join M) \<noteq> \<infinity>"
Andreas@60067
   908
    using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff)
Andreas@60067
   909
  
Andreas@60067
   910
  show ?integrable using f_pos f_neg by(simp add: real_integrable_def)
Andreas@60067
   911
Andreas@60067
   912
  note [measurable] = nn_integral_measurable_subprob_algebra
Andreas@60067
   913
Andreas@60067
   914
  have "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>join M)"
Andreas@60067
   915
    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
Andreas@60067
   916
  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (f x) \<partial>M' \<partial>M"
Andreas@60067
   917
    by(simp add: nn_integral_join[OF _ M])
Andreas@60067
   918
  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M"
Andreas@60067
   919
    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
Andreas@60067
   920
  finally have int_f: "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" .
Andreas@60067
   921
Andreas@60067
   922
  have "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (- f x) \<partial>join M)"
Andreas@60067
   923
    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
Andreas@60067
   924
  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (- f x) \<partial>M' \<partial>M"
Andreas@60067
   925
    by(simp add: nn_integral_join[OF _ M])
Andreas@60067
   926
  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M"
Andreas@60067
   927
    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
Andreas@60067
   928
  finally have int_mf: "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)" .
Andreas@60067
   929
Andreas@60067
   930
  have f_pos1:
Andreas@60067
   931
    "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>
Andreas@60067
   932
    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"
Andreas@60067
   933
    using f_measurable by(auto intro!: bounded1 dest: f_bounded)
Andreas@60067
   934
  have "AE M' in M. (\<integral>\<^sup>+ x. f x \<partial>M') \<noteq> \<infinity>"
Andreas@60067
   935
    using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_pos1)
Andreas@60067
   936
  hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real (\<integral>\<^sup>+ x. f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
Andreas@60067
   937
    by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)
Andreas@60067
   938
  from f_pos have [simp]: "integrable M (\<lambda>M'. real (\<integral>\<^sup>+ x. f x \<partial>M'))"
Andreas@60067
   939
    by(simp add: int_f real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal)
Andreas@60067
   940
Andreas@60067
   941
  have f_neg1:
Andreas@60067
   942
    "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>
Andreas@60067
   943
    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (- f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"
Andreas@60067
   944
    using f_measurable by(auto intro!: bounded1 dest: f_bounded)
Andreas@60067
   945
  have "AE M' in M. (\<integral>\<^sup>+ x. - f x \<partial>M') \<noteq> \<infinity>"
Andreas@60067
   946
    using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_neg1)
Andreas@60067
   947
  hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real (\<integral>\<^sup>+ x. - f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)"
Andreas@60067
   948
    by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)
Andreas@60067
   949
  from f_neg have [simp]: "integrable M (\<lambda>M'. real (\<integral>\<^sup>+ x. - f x \<partial>M'))"
Andreas@60067
   950
    by(simp add: int_mf real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal)
Andreas@60067
   951
Andreas@60067
   952
  from \<open>?integrable\<close>
Andreas@60067
   953
  have "ereal (\<integral> x. f x \<partial>join M) = (\<integral>\<^sup>+ x. f x \<partial>join M) - (\<integral>\<^sup>+ x. - f x \<partial>join M)"
Andreas@60067
   954
    by(simp add: real_lebesgue_integral_def ereal_minus(1)[symmetric] ereal_real nn_integral_nonneg f_pos f_neg del: ereal_minus(1))
Andreas@60067
   955
  also note int_f
Andreas@60067
   956
  also note int_mf
Andreas@60067
   957
  also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) = 
Andreas@60067
   958
    ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)) - 
Andreas@60067
   959
    ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M))"
Andreas@60067
   960
    by(subst (7 11) nn_integral_0_iff_AE[THEN iffD2])(simp_all add: nn_integral_nonneg)
Andreas@60067
   961
  also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) = \<integral> M'. real (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M"
Andreas@60067
   962
    using f_pos
Andreas@60067
   963
    by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_f nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric])
Andreas@60067
   964
  also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) = \<integral> M'. real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"
Andreas@60067
   965
    using f_neg
Andreas@60067
   966
    by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_mf nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric])
Andreas@60067
   967
  also note ereal_minus(1)
Andreas@60067
   968
  also have "(\<integral> M'. real (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M) - (\<integral> M'. real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M) = 
Andreas@60067
   969
    \<integral>M'. real (\<integral>\<^sup>+ x. f x \<partial>M') - real (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"
Andreas@60067
   970
    by simp
Andreas@60067
   971
  also have "\<dots> = \<integral>M'. \<integral> x. f x \<partial>M' \<partial>M" using _ _ M_bounded
Andreas@60067
   972
  proof(rule integral_cong_AE[OF _ _ AE_mp[OF _ AE_I2], rule_format])
Andreas@60067
   973
    show "(\<lambda>M'. integral\<^sup>L M' f) \<in> borel_measurable M"
Andreas@60067
   974
      by measurable(simp add: integral_measurable_subprob_algebra[OF _ f_bounded])
Andreas@60067
   975
      
Andreas@60067
   976
    fix M'
Andreas@60067
   977
    assume "M' \<in> space M" "emeasure M' (space M') \<le> B'"
Andreas@60067
   978
    then interpret finite_measure M' by(auto intro: finite_measureI)
Andreas@60067
   979
    
Andreas@60067
   980
    from \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
Andreas@60067
   981
    have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra)
Andreas@60067
   982
    hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq)
Andreas@60067
   983
    have "integrable M' f"
Andreas@60067
   984
      by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded)
Andreas@60067
   985
    then show "real (\<integral>\<^sup>+ x. f x \<partial>M') - real (\<integral>\<^sup>+ x. - f x \<partial>M') = \<integral> x. f x \<partial>M'"
Andreas@60067
   986
      by(simp add: real_lebesgue_integral_def)
Andreas@60067
   987
  qed simp_all
Andreas@60067
   988
  finally show ?integral by simp
Andreas@60067
   989
qed
Andreas@60067
   990
hoelzl@58606
   991
lemma join_assoc:
hoelzl@59048
   992
  assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))"
hoelzl@58606
   993
  shows "join (distr M (subprob_algebra N) join) = join (join M)"
hoelzl@58606
   994
proof (rule measure_eqI)
hoelzl@58606
   995
  fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"
hoelzl@58606
   996
  then have A: "A \<in> sets N" by simp
hoelzl@58606
   997
  show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
hoelzl@58606
   998
    using measurable_join[of N]
hoelzl@58606
   999
    by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg
hoelzl@59048
  1000
                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M]
hoelzl@59048
  1001
             intro!: nn_integral_cong emeasure_join)
hoelzl@58606
  1002
qed (simp add: M)
hoelzl@58606
  1003
hoelzl@58606
  1004
lemma join_return: 
hoelzl@58606
  1005
  assumes "sets M = sets N" and "subprob_space M"
hoelzl@58606
  1006
  shows "join (return (subprob_algebra N) M) = M"
hoelzl@58606
  1007
  by (rule measure_eqI)
hoelzl@58606
  1008
     (simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra  
hoelzl@58606
  1009
                    measurable_emeasure_subprob_algebra nn_integral_return assms)
hoelzl@58606
  1010
hoelzl@58606
  1011
lemma join_return':
hoelzl@58606
  1012
  assumes "sets N = sets M"
hoelzl@58606
  1013
  shows "join (distr M (subprob_algebra N) (return N)) = M"
hoelzl@58606
  1014
apply (rule measure_eqI)
hoelzl@58606
  1015
apply (simp add: assms)
hoelzl@58606
  1016
apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)")
hoelzl@58606
  1017
apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)
hoelzl@58606
  1018
apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable)
hoelzl@58606
  1019
done
hoelzl@58606
  1020
hoelzl@58606
  1021
lemma join_distr_distr:
hoelzl@58606
  1022
  fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure"
hoelzl@58606
  1023
  assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N"
hoelzl@58606
  1024
  shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l")
hoelzl@58606
  1025
proof (rule measure_eqI)
hoelzl@58606
  1026
  fix A assume "A \<in> sets ?r"
hoelzl@58606
  1027
  hence A_in_N: "A \<in> sets N" by simp
hoelzl@58606
  1028
hoelzl@58606
  1029
  from assms have "f \<in> measurable (join M) N" 
hoelzl@58606
  1030
      by (simp cong: measurable_cong_sets)
hoelzl@58606
  1031
  moreover from assms and A_in_N have "f-`A \<inter> space R \<in> sets R" 
hoelzl@58606
  1032
      by (intro measurable_sets) simp_all
hoelzl@58606
  1033
  ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-`A \<inter> space R) \<partial>M"
hoelzl@58606
  1034
      by (simp_all add: A_in_N emeasure_distr emeasure_join assms)
hoelzl@58606
  1035
  
hoelzl@58606
  1036
  also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N
hoelzl@58606
  1037
  proof (intro nn_integral_cong, subst emeasure_distr)
hoelzl@58606
  1038
    fix M' assume "M' \<in> space M"
hoelzl@58606
  1039
    from assms have "space M = space (subprob_algebra R)"
hoelzl@58606
  1040
        using sets_eq_imp_space_eq by blast
hoelzl@58606
  1041
    with `M' \<in> space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast
hoelzl@58606
  1042
    show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms)
hoelzl@58606
  1043
    have "space M' = space R" by (rule sets_eq_imp_space_eq) simp
hoelzl@58606
  1044
    thus "emeasure M' (f -` A \<inter> space R) = emeasure M' (f -` A \<inter> space M')" by simp
hoelzl@58606
  1045
  qed
hoelzl@58606
  1046
hoelzl@58606
  1047
  also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)"
hoelzl@58606
  1048
      by (simp cong: measurable_cong_sets add: assms measurable_distr)
hoelzl@58606
  1049
  hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = 
hoelzl@58606
  1050
             emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A"
hoelzl@58606
  1051
      by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra)
hoelzl@58606
  1052
  finally show "emeasure ?r A = emeasure ?l A" ..
hoelzl@58606
  1053
qed simp
hoelzl@58606
  1054
hoelzl@58606
  1055
definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where
hoelzl@58606
  1056
  "bind M f = (if space M = {} then count_space {} else
hoelzl@58606
  1057
    join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
hoelzl@58606
  1058
hoelzl@58606
  1059
adhoc_overloading Monad_Syntax.bind bind
hoelzl@58606
  1060
hoelzl@58606
  1061
lemma bind_empty: 
hoelzl@58606
  1062
  "space M = {} \<Longrightarrow> bind M f = count_space {}"
hoelzl@58606
  1063
  by (simp add: bind_def)
hoelzl@58606
  1064
hoelzl@58606
  1065
lemma bind_nonempty:
hoelzl@58606
  1066
  "space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)"
hoelzl@58606
  1067
  by (simp add: bind_def)
hoelzl@58606
  1068
hoelzl@58606
  1069
lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}"
hoelzl@58606
  1070
  by (auto simp: bind_def)
hoelzl@58606
  1071
hoelzl@58606
  1072
lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
hoelzl@58606
  1073
  by (simp add: bind_def)
hoelzl@58606
  1074
hoelzl@59048
  1075
lemma sets_bind[simp, measurable_cong]:
hoelzl@59048
  1076
  assumes f: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and M: "space M \<noteq> {}"
hoelzl@58606
  1077
  shows "sets (bind M f) = sets N"
hoelzl@59048
  1078
  using f [of "SOME x. x \<in> space M"] by (simp add: bind_nonempty M some_in_eq)
hoelzl@58606
  1079
hoelzl@58606
  1080
lemma space_bind[simp]: 
hoelzl@59048
  1081
  assumes "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and "space M \<noteq> {}"
hoelzl@58606
  1082
  shows "space (bind M f) = space N"
hoelzl@59048
  1083
  using assms by (intro sets_eq_imp_space_eq sets_bind)
hoelzl@58606
  1084
hoelzl@58606
  1085
lemma bind_cong: 
hoelzl@58606
  1086
  assumes "\<forall>x \<in> space M. f x = g x"
hoelzl@58606
  1087
  shows "bind M f = bind M g"
hoelzl@58606
  1088
proof (cases "space M = {}")
hoelzl@58606
  1089
  assume "space M \<noteq> {}"
hoelzl@58606
  1090
  hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast
hoelzl@58606
  1091
  with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast
hoelzl@58606
  1092
  with `space M \<noteq> {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong)
hoelzl@58606
  1093
qed (simp add: bind_empty)
hoelzl@58606
  1094
hoelzl@58606
  1095
lemma bind_nonempty':
hoelzl@58606
  1096
  assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M"
hoelzl@58606
  1097
  shows "bind M f = join (distr M (subprob_algebra N) f)"
hoelzl@58606
  1098
  using assms
hoelzl@58606
  1099
  apply (subst bind_nonempty, blast)
hoelzl@58606
  1100
  apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast)
hoelzl@58606
  1101
  apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]])
hoelzl@58606
  1102
  done
hoelzl@58606
  1103
hoelzl@58606
  1104
lemma bind_nonempty'':
hoelzl@58606
  1105
  assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}"
hoelzl@58606
  1106
  shows "bind M f = join (distr M (subprob_algebra N) f)"
hoelzl@58606
  1107
  using assms by (auto intro: bind_nonempty')
hoelzl@58606
  1108
hoelzl@58606
  1109
lemma emeasure_bind:
hoelzl@58606
  1110
    "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>
hoelzl@58606
  1111
      \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
hoelzl@58606
  1112
  by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
hoelzl@58606
  1113
hoelzl@59048
  1114
lemma nn_integral_bind:
hoelzl@59048
  1115
  assumes f: "f \<in> borel_measurable B"
hoelzl@59000
  1116
  assumes N: "N \<in> measurable M (subprob_algebra B)"
hoelzl@59000
  1117
  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
hoelzl@59000
  1118
proof cases
hoelzl@59000
  1119
  assume M: "space M \<noteq> {}" show ?thesis
hoelzl@59000
  1120
    unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr]
hoelzl@59000
  1121
    by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])
hoelzl@59000
  1122
qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
hoelzl@59000
  1123
hoelzl@59000
  1124
lemma AE_bind:
hoelzl@59000
  1125
  assumes P[measurable]: "Measurable.pred B P"
hoelzl@59000
  1126
  assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
hoelzl@59000
  1127
  shows "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)"
hoelzl@59000
  1128
proof cases
hoelzl@59000
  1129
  assume M: "space M = {}" show ?thesis
hoelzl@59000
  1130
    unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
hoelzl@59000
  1131
next
hoelzl@59000
  1132
  assume M: "space M \<noteq> {}"
hoelzl@59048
  1133
  note sets_kernel[OF N, simp]
hoelzl@59000
  1134
  have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<guillemotright>= N))"
hoelzl@59048
  1135
    by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator)
hoelzl@59000
  1136
hoelzl@59000
  1137
  have "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0"
hoelzl@59048
  1138
    by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B]
hoelzl@59000
  1139
             del: nn_integral_indicator)
hoelzl@59000
  1140
  also have "\<dots> = (AE x in M. AE y in N x. P y)"
hoelzl@59000
  1141
    apply (subst nn_integral_0_iff_AE)
hoelzl@59000
  1142
    apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra])
hoelzl@59000
  1143
    apply measurable
hoelzl@59000
  1144
    apply (intro eventually_subst AE_I2)
hoelzl@59048
  1145
    apply (auto simp add: emeasure_le_0_iff subprob_measurableD(1)[OF N]
hoelzl@59048
  1146
                intro!: AE_iff_measurable[symmetric])
hoelzl@59000
  1147
    done
hoelzl@59000
  1148
  finally show ?thesis .
hoelzl@59000
  1149
qed
hoelzl@59000
  1150
hoelzl@59000
  1151
lemma measurable_bind':
hoelzl@59000
  1152
  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
hoelzl@59000
  1153
          M2: "split g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
hoelzl@59000
  1154
  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
hoelzl@59000
  1155
proof (subst measurable_cong)
hoelzl@59000
  1156
  fix x assume x_in_M: "x \<in> space M"
hoelzl@59000
  1157
  with assms have "space (f x) \<noteq> {}" 
hoelzl@59000
  1158
      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
hoelzl@59000
  1159
  moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)"
hoelzl@59000
  1160
      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
hoelzl@59000
  1161
         (auto dest: measurable_Pair2)
hoelzl@59000
  1162
  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 
hoelzl@59000
  1163
      by (simp_all add: bind_nonempty'')
hoelzl@59000
  1164
next
hoelzl@59000
  1165
  show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)"
hoelzl@59000
  1166
    apply (rule measurable_compose[OF _ measurable_join])
hoelzl@59000
  1167
    apply (rule measurable_distr2[OF M2 M1])
hoelzl@59000
  1168
    done
hoelzl@59000
  1169
qed
hoelzl@58606
  1170
hoelzl@59048
  1171
lemma measurable_bind[measurable (raw)]:
hoelzl@59000
  1172
  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
hoelzl@59000
  1173
          M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
hoelzl@59000
  1174
  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
hoelzl@59000
  1175
  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)
hoelzl@59000
  1176
hoelzl@59000
  1177
lemma measurable_bind2:
hoelzl@59000
  1178
  assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)"
hoelzl@59000
  1179
  shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)"
hoelzl@59000
  1180
    using assms by (intro measurable_bind' measurable_const) auto
hoelzl@59000
  1181
hoelzl@59000
  1182
lemma subprob_space_bind:
hoelzl@59000
  1183
  assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
hoelzl@59000
  1184
  shows "subprob_space (M \<guillemotright>= f)"
hoelzl@59000
  1185
proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
hoelzl@59000
  1186
  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
hoelzl@59000
  1187
    by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
hoelzl@59000
  1188
        rule measurable_compose[OF measurable_snd assms(2)])
hoelzl@59000
  1189
  from assms(1) show "M \<in> space (subprob_algebra M)"
hoelzl@59000
  1190
    by (simp add: space_subprob_algebra)
hoelzl@59000
  1191
qed
hoelzl@58606
  1192
Andreas@60067
  1193
lemma 
Andreas@60067
  1194
  fixes f :: "_ \<Rightarrow> real"
Andreas@60067
  1195
  assumes f_measurable [measurable]: "f \<in> borel_measurable K"
Andreas@60067
  1196
  and f_bounded: "\<And>x. x \<in> space K \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
Andreas@60067
  1197
  and N [measurable]: "N \<in> measurable M (subprob_algebra K)"
Andreas@60067
  1198
  and fin: "finite_measure M"
Andreas@60067
  1199
  and M_bounded: "AE x in M. emeasure (N x) (space (N x)) \<le> ereal B'"
Andreas@60067
  1200
  shows integrable_bind: "integrable (bind M N) f" (is ?integrable)
Andreas@60067
  1201
  and integral_bind: "integral\<^sup>L (bind M N) f = \<integral> x. integral\<^sup>L (N x) f \<partial>M" (is ?integral)
Andreas@60067
  1202
proof(case_tac [!] "space M = {}")
Andreas@60067
  1203
  assume [simp]: "space M \<noteq> {}"
Andreas@60067
  1204
  interpret finite_measure M by(rule fin)
Andreas@60067
  1205
Andreas@60067
  1206
  have "integrable (join (distr M (subprob_algebra K) N)) f"
Andreas@60067
  1207
    using f_measurable f_bounded
Andreas@60067
  1208
    by(rule integrable_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
Andreas@60067
  1209
  then show ?integrable by(simp add: bind_nonempty''[where N=K])
Andreas@60067
  1210
Andreas@60067
  1211
  have "integral\<^sup>L (join (distr M (subprob_algebra K) N)) f = \<integral> M'. integral\<^sup>L M' f \<partial>distr M (subprob_algebra K) N"
Andreas@60067
  1212
    using f_measurable f_bounded
Andreas@60067
  1213
    by(rule integral_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
Andreas@60067
  1214
  also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
Andreas@60067
  1215
    by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _ f_bounded])
Andreas@60067
  1216
  finally show ?integral by(simp add: bind_nonempty''[where N=K])
Andreas@60067
  1217
qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
Andreas@60067
  1218
hoelzl@59000
  1219
lemma (in prob_space) prob_space_bind: 
hoelzl@59000
  1220
  assumes ae: "AE x in M. prob_space (N x)"
hoelzl@59000
  1221
    and N[measurable]: "N \<in> measurable M (subprob_algebra S)"
hoelzl@59000
  1222
  shows "prob_space (M \<guillemotright>= N)"
hoelzl@59000
  1223
proof
hoelzl@59000
  1224
  have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
hoelzl@59000
  1225
    by (subst emeasure_bind[where N=S])
hoelzl@59048
  1226
       (auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong)
hoelzl@59000
  1227
  also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)"
hoelzl@59000
  1228
    using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1)
hoelzl@59000
  1229
  finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1"
hoelzl@59000
  1230
    by (simp add: emeasure_space_1)
hoelzl@59000
  1231
qed
hoelzl@59000
  1232
hoelzl@59000
  1233
lemma (in subprob_space) bind_in_space:
hoelzl@59000
  1234
  "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)"
hoelzl@59048
  1235
  by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind)
hoelzl@59000
  1236
     unfold_locales
hoelzl@59000
  1237
hoelzl@59000
  1238
lemma (in subprob_space) measure_bind:
hoelzl@59000
  1239
  assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N"
hoelzl@59000
  1240
  shows "measure (M \<guillemotright>= f) X = \<integral>x. measure (f x) X \<partial>M"
hoelzl@59000
  1241
proof -
hoelzl@59000
  1242
  interpret Mf: subprob_space "M \<guillemotright>= f"
hoelzl@59000
  1243
    by (rule subprob_space_bind[OF _ f]) unfold_locales
hoelzl@59000
  1244
hoelzl@59000
  1245
  { fix x assume "x \<in> space M"
hoelzl@59000
  1246
    from f[THEN measurable_space, OF this] interpret subprob_space "f x"
hoelzl@59000
  1247
      by (simp add: space_subprob_algebra)
hoelzl@59000
  1248
    have "emeasure (f x) X = ereal (measure (f x) X)" "measure (f x) X \<le> 1"
hoelzl@59000
  1249
      by (auto simp: emeasure_eq_measure subprob_measure_le_1) }
hoelzl@59000
  1250
  note this[simp]
hoelzl@59000
  1251
hoelzl@59000
  1252
  have "emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
hoelzl@59000
  1253
    using subprob_not_empty f X by (rule emeasure_bind)
hoelzl@59000
  1254
  also have "\<dots> = \<integral>\<^sup>+x. ereal (measure (f x) X) \<partial>M"
hoelzl@59000
  1255
    by (intro nn_integral_cong) simp
hoelzl@59000
  1256
  also have "\<dots> = \<integral>x. measure (f x) X \<partial>M"
hoelzl@59000
  1257
    by (intro nn_integral_eq_integral integrable_const_bound[where B=1]
hoelzl@59000
  1258
              measure_measurable_subprob_algebra2[OF _ f] pair_measureI X)
hoelzl@59000
  1259
       (auto simp: measure_nonneg)
hoelzl@59000
  1260
  finally show ?thesis
hoelzl@59000
  1261
    by (simp add: Mf.emeasure_eq_measure)
hoelzl@58606
  1262
qed
hoelzl@58606
  1263
hoelzl@58606
  1264
lemma emeasure_bind_const: 
hoelzl@58606
  1265
    "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 
hoelzl@58606
  1266
         emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
hoelzl@58606
  1267
  by (simp add: bind_nonempty emeasure_join nn_integral_distr 
hoelzl@58606
  1268
                space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg)
hoelzl@58606
  1269
hoelzl@58606
  1270
lemma emeasure_bind_const':
hoelzl@58606
  1271
  assumes "subprob_space M" "subprob_space N"
hoelzl@58606
  1272
  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
hoelzl@58606
  1273
using assms
hoelzl@58606
  1274
proof (case_tac "X \<in> sets N")
hoelzl@58606
  1275
  fix X assume "X \<in> sets N"
hoelzl@58606
  1276
  thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
hoelzl@58606
  1277
      by (subst emeasure_bind_const) 
hoelzl@58606
  1278
         (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1)
hoelzl@58606
  1279
next
hoelzl@58606
  1280
  fix X assume "X \<notin> sets N"
hoelzl@58606
  1281
  with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
hoelzl@58606
  1282
      by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty
hoelzl@58606
  1283
                    space_subprob_algebra emeasure_notin_sets)
hoelzl@58606
  1284
qed
hoelzl@58606
  1285
hoelzl@58606
  1286
lemma emeasure_bind_const_prob_space:
hoelzl@58606
  1287
  assumes "prob_space M" "subprob_space N"
hoelzl@58606
  1288
  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X"
hoelzl@58606
  1289
  using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 
hoelzl@58606
  1290
                            prob_space.emeasure_space_1)
hoelzl@58606
  1291
hoelzl@59000
  1292
lemma bind_return: 
hoelzl@59000
  1293
  assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M"
hoelzl@59000
  1294
  shows "bind (return M x) f = f x"
hoelzl@59000
  1295
  using sets_kernel[OF assms] assms
hoelzl@59000
  1296
  by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty'
hoelzl@59000
  1297
               cong: subprob_algebra_cong)
hoelzl@59000
  1298
hoelzl@59000
  1299
lemma bind_return':
hoelzl@59000
  1300
  shows "bind M (return M) = M"
hoelzl@59000
  1301
  by (cases "space M = {}")
hoelzl@59000
  1302
     (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 
hoelzl@59000
  1303
               cong: subprob_algebra_cong)
hoelzl@59000
  1304
hoelzl@59000
  1305
lemma distr_bind:
hoelzl@59000
  1306
  assumes N: "N \<in> measurable M (subprob_algebra K)" "space M \<noteq> {}"
hoelzl@59000
  1307
  assumes f: "f \<in> measurable K R"
hoelzl@59000
  1308
  shows "distr (M \<guillemotright>= N) R f = (M \<guillemotright>= (\<lambda>x. distr (N x) R f))"
hoelzl@59000
  1309
  unfolding bind_nonempty''[OF N]
hoelzl@59000
  1310
  apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)])
hoelzl@59000
  1311
  apply (rule f)
hoelzl@59000
  1312
  apply (simp add: join_distr_distr[OF _ f, symmetric])
hoelzl@59000
  1313
  apply (subst distr_distr[OF measurable_distr, OF f N(1)])
hoelzl@59000
  1314
  apply (simp add: comp_def)
hoelzl@59000
  1315
  done
hoelzl@59000
  1316
hoelzl@59000
  1317
lemma bind_distr:
hoelzl@59000
  1318
  assumes f[measurable]: "f \<in> measurable M X"
hoelzl@59000
  1319
  assumes N[measurable]: "N \<in> measurable X (subprob_algebra K)" and "space M \<noteq> {}"
hoelzl@59000
  1320
  shows "(distr M X f \<guillemotright>= N) = (M \<guillemotright>= (\<lambda>x. N (f x)))"
hoelzl@59000
  1321
proof -
hoelzl@59000
  1322
  have "space X \<noteq> {}" "space M \<noteq> {}"
hoelzl@59000
  1323
    using `space M \<noteq> {}` f[THEN measurable_space] by auto
hoelzl@59000
  1324
  then show ?thesis
hoelzl@59000
  1325
    by (simp add: bind_nonempty''[where N=K] distr_distr comp_def)
hoelzl@59000
  1326
qed
hoelzl@59000
  1327
hoelzl@59000
  1328
lemma bind_count_space_singleton:
hoelzl@59000
  1329
  assumes "subprob_space (f x)"
hoelzl@59000
  1330
  shows "count_space {x} \<guillemotright>= f = f x"
hoelzl@59000
  1331
proof-
hoelzl@59000
  1332
  have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
hoelzl@59000
  1333
  have "count_space {x} = return (count_space {x}) x"
hoelzl@59000
  1334
    by (intro measure_eqI) (auto dest: A)
hoelzl@59000
  1335
  also have "... \<guillemotright>= f = f x"
hoelzl@59000
  1336
    by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
hoelzl@59000
  1337
  finally show ?thesis .
hoelzl@59000
  1338
qed
hoelzl@59000
  1339
hoelzl@59000
  1340
lemma restrict_space_bind:
hoelzl@59000
  1341
  assumes N: "N \<in> measurable M (subprob_algebra K)"
hoelzl@59000
  1342
  assumes "space M \<noteq> {}"
hoelzl@59000
  1343
  assumes X[simp]: "X \<in> sets K" "X \<noteq> {}"
hoelzl@59000
  1344
  shows "restrict_space (bind M N) X = bind M (\<lambda>x. restrict_space (N x) X)"
hoelzl@59000
  1345
proof (rule measure_eqI)
hoelzl@59048
  1346
  note N_sets = sets_bind[OF sets_kernel[OF N] assms(2), simp]
hoelzl@59048
  1347
  note N_space = sets_eq_imp_space_eq[OF N_sets, simp]
hoelzl@59048
  1348
  show "sets (restrict_space (bind M N) X) = sets (bind M (\<lambda>x. restrict_space (N x) X))"
hoelzl@59048
  1349
    by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]])
hoelzl@59000
  1350
  fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)"
hoelzl@59000
  1351
  with X have "A \<in> sets K" "A \<subseteq> X"
hoelzl@59048
  1352
    by (auto simp: sets_restrict_space)
hoelzl@59000
  1353
  then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A"
hoelzl@59000
  1354
    using assms
hoelzl@59000
  1355
    apply (subst emeasure_restrict_space)
hoelzl@59048
  1356
    apply (simp_all add: emeasure_bind[OF assms(2,1)])
hoelzl@59000
  1357
    apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]])
hoelzl@59000
  1358
    apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra
hoelzl@59000
  1359
                intro!: nn_integral_cong dest!: measurable_space)
hoelzl@59000
  1360
    done
hoelzl@59048
  1361
qed
hoelzl@59000
  1362
Andreas@60067
  1363
lemma bind_restrict_space:
Andreas@60067
  1364
  assumes A: "A \<inter> space M \<noteq> {}" "A \<inter> space M \<in> sets M"
Andreas@60067
  1365
  and f: "f \<in> measurable (restrict_space M A) (subprob_algebra N)"
Andreas@60067
  1366
  shows "restrict_space M A \<guillemotright>= f = M \<guillemotright>= (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))"
Andreas@60067
  1367
  (is "?lhs = ?rhs" is "_ = M \<guillemotright>= ?f")
Andreas@60067
  1368
proof -
Andreas@60067
  1369
  let ?P = "\<lambda>x. x \<in> A \<and> x \<in> space M"
Andreas@60067
  1370
  let ?x = "Eps ?P"
Andreas@60067
  1371
  let ?c = "null_measure (f ?x)"
Andreas@60067
  1372
  from A have "?P ?x" by-(rule someI_ex, blast)
Andreas@60067
  1373
  hence "?x \<in> space (restrict_space M A)" by(simp add: space_restrict_space)
Andreas@60067
  1374
  with f have "f ?x \<in> space (subprob_algebra N)" by(rule measurable_space)
Andreas@60067
  1375
  hence sps: "subprob_space (f ?x)"
Andreas@60067
  1376
    and sets: "sets (f ?x) = sets N" 
Andreas@60067
  1377
    by(simp_all add: space_subprob_algebra)
Andreas@60067
  1378
  have "space (f ?x) \<noteq> {}" using sps by(rule subprob_space.subprob_not_empty)
Andreas@60067
  1379
  moreover have "sets ?c = sets N" by(simp add: null_measure_def)(simp add: sets)
Andreas@60067
  1380
  ultimately have c: "?c \<in> space (subprob_algebra N)"
Andreas@60067
  1381
    by(simp add: space_subprob_algebra subprob_space_null_measure)
Andreas@60067
  1382
  from f A c have f': "?f \<in> measurable M (subprob_algebra N)"
Andreas@60067
  1383
    by(simp add: measurable_restrict_space_iff)
Andreas@60067
  1384
Andreas@60067
  1385
  from A have [simp]: "space M \<noteq> {}" by blast
Andreas@60067
  1386
Andreas@60067
  1387
  have "?lhs = join (distr (restrict_space M A) (subprob_algebra N) f)"
Andreas@60067
  1388
    using assms by(simp add: space_restrict_space bind_nonempty'')
Andreas@60067
  1389
  also have "\<dots> = join (distr M (subprob_algebra N) ?f)"
Andreas@60067
  1390
    by(rule measure_eqI)(auto simp add: emeasure_join nn_integral_distr nn_integral_restrict_space f f' A intro: nn_integral_cong)
Andreas@60067
  1391
  also have "\<dots> = ?rhs" using f' by(simp add: bind_nonempty'')
Andreas@60067
  1392
  finally show ?thesis .
Andreas@60067
  1393
qed
Andreas@60067
  1394
hoelzl@58606
  1395
lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
hoelzl@58606
  1396
  by (intro measure_eqI) 
hoelzl@58606
  1397
     (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
hoelzl@58606
  1398
hoelzl@58606
  1399
lemma bind_return_distr: 
hoelzl@58606
  1400
    "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (return N \<circ> f) = distr M N f"
hoelzl@58606
  1401
  apply (simp add: bind_nonempty)
hoelzl@58606
  1402
  apply (subst subprob_algebra_cong)
hoelzl@58606
  1403
  apply (rule sets_return)
hoelzl@58606
  1404
  apply (subst distr_distr[symmetric])
hoelzl@58606
  1405
  apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return')
hoelzl@58606
  1406
  done
hoelzl@58606
  1407
hoelzl@58606
  1408
lemma bind_assoc:
hoelzl@58606
  1409
  fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure"
hoelzl@58606
  1410
  assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)"
hoelzl@58606
  1411
  shows "bind (bind M f) g = bind M (\<lambda>x. bind (f x) g)"
hoelzl@58606
  1412
proof (cases "space M = {}")
hoelzl@58606
  1413
  assume [simp]: "space M \<noteq> {}"
hoelzl@58606
  1414
  from assms have [simp]: "space N \<noteq> {}" "space R \<noteq> {}"
hoelzl@58606
  1415
      by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
hoelzl@58606
  1416
  from assms have sets_fx[simp]: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N"
hoelzl@58606
  1417
      by (simp add: sets_kernel)
hoelzl@58606
  1418
  have ex_in: "\<And>A. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A" by blast
hoelzl@58606
  1419
  note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF `space M \<noteq> {}`]]]
hoelzl@58606
  1420
                         sets_kernel[OF M2 someI_ex[OF ex_in[OF `space N \<noteq> {}`]]]
hoelzl@58606
  1421
  note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)]
hoelzl@58606
  1422
hoelzl@58606
  1423
  have "bind M (\<lambda>x. bind (f x) g) = 
hoelzl@58606
  1424
        join (distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f))"
hoelzl@58606
  1425
    by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def
hoelzl@58606
  1426
             cong: subprob_algebra_cong distr_cong)
hoelzl@58606
  1427
  also have "distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f) =
hoelzl@58606
  1428
             distr (distr (distr M (subprob_algebra N) f)
hoelzl@58606
  1429
                          (subprob_algebra (subprob_algebra R))
hoelzl@58606
  1430
                          (\<lambda>x. distr x (subprob_algebra R) g)) 
hoelzl@58606
  1431
                   (subprob_algebra R) join"
hoelzl@58606
  1432
      apply (subst distr_distr, 
hoelzl@58606
  1433
             (blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+
hoelzl@58606
  1434
      apply (simp add: o_assoc)
hoelzl@58606
  1435
      done
hoelzl@58606
  1436
  also have "join ... = bind (bind M f) g"
hoelzl@58606
  1437
      by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong)
hoelzl@58606
  1438
  finally show ?thesis ..
hoelzl@58606
  1439
qed (simp add: bind_empty)
hoelzl@58606
  1440
hoelzl@58606
  1441
lemma double_bind_assoc:
hoelzl@58606
  1442
  assumes Mg: "g \<in> measurable N (subprob_algebra N')"
hoelzl@58606
  1443
  assumes Mf: "f \<in> measurable M (subprob_algebra M')"
hoelzl@58606
  1444
  assumes Mh: "split h \<in> measurable (M \<Otimes>\<^sub>M M') N"
hoelzl@58606
  1445
  shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g"
hoelzl@58606
  1446
proof-
hoelzl@58606
  1447
  have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g = 
hoelzl@58606
  1448
            do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g}"
hoelzl@58606
  1449
    using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg
hoelzl@58606
  1450
                      measurable_compose[OF _ return_measurable] simp: measurable_split_conv)
hoelzl@58606
  1451
  also from Mh have "\<And>x. x \<in> space M \<Longrightarrow> h x \<in> measurable M' N" by measurable
hoelzl@58606
  1452
  hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g} = 
hoelzl@58606
  1453
            do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g}"
hoelzl@58606
  1454
    apply (intro ballI bind_cong bind_assoc)
hoelzl@58606
  1455
    apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp)
hoelzl@58606
  1456
    apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg)
hoelzl@58606
  1457
    done
hoelzl@58606
  1458
  also have "\<And>x. x \<in> space M \<Longrightarrow> space (f x) = space M'"
hoelzl@58606
  1459
    by (intro sets_eq_imp_space_eq sets_kernel[OF Mf])
hoelzl@58606
  1460
  with measurable_space[OF Mh] 
hoelzl@58606
  1461
    have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}"
hoelzl@58606
  1462
    by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure)
hoelzl@58606
  1463
  finally show ?thesis ..
hoelzl@58606
  1464
qed
hoelzl@58606
  1465
hoelzl@59048
  1466
lemma (in prob_space) M_in_subprob[measurable (raw)]: "M \<in> space (subprob_algebra M)"
hoelzl@59048
  1467
  by (simp add: space_subprob_algebra) unfold_locales
hoelzl@59048
  1468
hoelzl@59000
  1469
lemma (in pair_prob_space) pair_measure_eq_bind:
hoelzl@59000
  1470
  "(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
hoelzl@59000
  1471
proof (rule measure_eqI)
hoelzl@59000
  1472
  have ps_M2: "prob_space M2" by unfold_locales
hoelzl@59000
  1473
  note return_measurable[measurable]
hoelzl@59000
  1474
  show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
hoelzl@59048
  1475
    by (simp_all add: M1.not_empty M2.not_empty)
hoelzl@59000
  1476
  fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)"
hoelzl@59000
  1477
  show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A"
hoelzl@59048
  1478
    by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"]
hoelzl@59000
  1479
             intro!: nn_integral_cong)
hoelzl@59000
  1480
qed
hoelzl@59000
  1481
hoelzl@59000
  1482
lemma (in pair_prob_space) bind_rotate:
hoelzl@59000
  1483
  assumes C[measurable]: "(\<lambda>(x, y). C x y) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (subprob_algebra N)"
hoelzl@59000
  1484
  shows "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
hoelzl@59000
  1485
proof - 
hoelzl@59000
  1486
  interpret swap: pair_prob_space M2 M1 by unfold_locales
hoelzl@59000
  1487
  note measurable_bind[where N="M2", measurable]
hoelzl@59000
  1488
  note measurable_bind[where N="M1", measurable]
hoelzl@59000
  1489
  have [simp]: "M1 \<in> space (subprob_algebra M1)" "M2 \<in> space (subprob_algebra M2)"
hoelzl@59000
  1490
    by (auto simp: space_subprob_algebra) unfold_locales
hoelzl@59000
  1491
  have "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = 
hoelzl@59000
  1492
    (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<guillemotright>= (\<lambda>(x, y). C x y)"
hoelzl@59000
  1493
    by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M1 \<Otimes>\<^sub>M M2" and R=N])
hoelzl@59000
  1494
  also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<guillemotright>= (\<lambda>(x, y). C x y)"
hoelzl@59000
  1495
    unfolding pair_measure_eq_bind[symmetric] distr_pair_swap[symmetric] ..
hoelzl@59000
  1496
  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>x. M1 \<guillemotright>= (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<guillemotright>= (\<lambda>(y, x). C x y)"
hoelzl@59000
  1497
    unfolding swap.pair_measure_eq_bind[symmetric]
hoelzl@59000
  1498
    by (auto simp add: space_pair_measure M1.not_empty M2.not_empty bind_distr[OF _ C] intro!: bind_cong)
hoelzl@59000
  1499
  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
hoelzl@59000
  1500
    by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M2 \<Otimes>\<^sub>M M1" and R=N])
hoelzl@59000
  1501
  finally show ?thesis .
hoelzl@59000
  1502
qed
hoelzl@59000
  1503
hoelzl@58608
  1504
section {* Measures form a $\omega$-chain complete partial order *}
hoelzl@58606
  1505
hoelzl@58606
  1506
definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where
hoelzl@58606
  1507
  "SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)"
hoelzl@58606
  1508
hoelzl@58606
  1509
lemma
hoelzl@58606
  1510
  assumes const: "\<And>i j. sets (M i) = sets (M j)"
hoelzl@58606
  1511
  shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp)
hoelzl@58606
  1512
    and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st)
hoelzl@58606
  1513
proof -
hoelzl@58606
  1514
  have "(\<Union>i. sets (M i)) = sets (M i)"
hoelzl@58606
  1515
    using const by auto
hoelzl@58606
  1516
  moreover have "(\<Union>i. space (M i)) = space (M i)"
hoelzl@58606
  1517
    using const[THEN sets_eq_imp_space_eq] by auto
hoelzl@58606
  1518
  moreover have "\<And>i. sets (M i) \<subseteq> Pow (space (M i))"
hoelzl@58606
  1519
    by (auto dest: sets.sets_into_space)
hoelzl@58606
  1520
  ultimately show ?sp ?st
hoelzl@58606
  1521
    by (simp_all add: SUP_measure_def)
hoelzl@58606
  1522
qed
hoelzl@58606
  1523
hoelzl@58606
  1524
lemma emeasure_SUP_measure:
hoelzl@58606
  1525
  assumes const: "\<And>i j. sets (M i) = sets (M j)"
hoelzl@58606
  1526
    and mono: "mono (\<lambda>i. emeasure (M i))"
hoelzl@58606
  1527
  shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)"
hoelzl@58606
  1528
proof cases
hoelzl@58606
  1529
  assume "A \<in> sets (SUP_measure M)"
hoelzl@58606
  1530
  show ?thesis
hoelzl@58606
  1531
  proof (rule emeasure_measure_of[OF SUP_measure_def])
hoelzl@58606
  1532
    show "countably_additive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"
hoelzl@58606
  1533
    proof (rule countably_additiveI)
hoelzl@58606
  1534
      fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (SUP_measure M)"
hoelzl@58606
  1535
      then have "\<And>i j. A i \<in> sets (M j)"
hoelzl@58606
  1536
        using sets_SUP_measure[of M, OF const] by simp
hoelzl@58606
  1537
      moreover assume "disjoint_family A"
hoelzl@58606
  1538
      ultimately show "(\<Sum>i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\<Union>i. A i))"
hoelzl@58606
  1539
        using mono by (subst suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure)
hoelzl@58606
  1540
    qed
hoelzl@58606
  1541
    show "positive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"
hoelzl@58606
  1542
      by (auto simp: positive_def intro: SUP_upper2)
hoelzl@58606
  1543
    show "(\<Union>i. sets (M i)) \<subseteq> Pow (\<Union>i. space (M i))"
hoelzl@58606
  1544
      using sets.sets_into_space by auto
hoelzl@58606
  1545
  qed fact
hoelzl@58606
  1546
next
hoelzl@58606
  1547
  assume "A \<notin> sets (SUP_measure M)"
hoelzl@58606
  1548
  with sets_SUP_measure[of M, OF const] show ?thesis
hoelzl@58606
  1549
    by (simp add: emeasure_notin_sets)
hoelzl@58606
  1550
qed
hoelzl@58606
  1551
hoelzl@59425
  1552
lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
hoelzl@59425
  1553
   by (cases "space M = {}")
hoelzl@59425
  1554
      (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
hoelzl@59425
  1555
                cong: subprob_algebra_cong)
hoelzl@59425
  1556
hoelzl@59425
  1557
lemma (in prob_space) distr_const[simp]:
hoelzl@59425
  1558
  "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
hoelzl@59425
  1559
  by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
hoelzl@59425
  1560
hoelzl@59425
  1561
lemma return_count_space_eq_density:
hoelzl@59425
  1562
    "return (count_space M) x = density (count_space M) (indicator {x})"
hoelzl@59425
  1563
  by (rule measure_eqI) 
hoelzl@59425
  1564
     (auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)
hoelzl@59425
  1565
hoelzl@58606
  1566
end