src/HOL/Probability/Giry_Monad.thy
author wenzelm
Sat, 28 Nov 2015 23:59:08 +0100
changeset 61753 865bb718bdb9
parent 61634 48e2de1b1df5
child 61808 fc1556774cfe
permissions -rw-r--r--
removed junk;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     1
(*  Title:      HOL/Probability/Giry_Monad.thy
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     2
    Author:     Johannes Hölzl, TU München
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     3
    Author:     Manuel Eberl, TU München
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     4
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     5
Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     6
spaces.
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     7
*)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     8
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
     9
theory Giry_Monad
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    10
  imports Probability_Measure Lebesgue_Integral_Substitution "~~/src/HOL/Library/Monad_Syntax" 
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    11
begin
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    12
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    13
section {* Sub-probability spaces *}
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    14
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    15
locale subprob_space = finite_measure +
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    16
  assumes emeasure_space_le_1: "emeasure M (space M) \<le> 1"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    17
  assumes subprob_not_empty: "space M \<noteq> {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    18
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    19
lemma subprob_spaceI[Pure.intro!]:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    20
  assumes *: "emeasure M (space M) \<le> 1"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    21
  assumes "space M \<noteq> {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    22
  shows "subprob_space M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    23
proof -
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    24
  interpret finite_measure M
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    25
  proof
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    26
    show "emeasure M (space M) \<noteq> \<infinity>" using * by auto
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    27
  qed
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60067
diff changeset
    28
  show "subprob_space M" by standard fact+
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    29
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    30
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    31
lemma prob_space_imp_subprob_space:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    32
  "prob_space M \<Longrightarrow> subprob_space M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    33
  by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    34
59425
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 59092
diff changeset
    35
lemma subprob_space_imp_sigma_finite: "subprob_space M \<Longrightarrow> sigma_finite_measure M"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 59092
diff changeset
    36
  unfolding subprob_space_def finite_measure_def by simp
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 59092
diff changeset
    37
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    38
sublocale prob_space \<subseteq> subprob_space
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    39
  by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    40
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
    41
lemma subprob_space_sigma [simp]: "\<Omega> \<noteq> {} \<Longrightarrow> subprob_space (sigma \<Omega> X)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
    42
by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
    43
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
    44
lemma subprob_space_null_measure: "space M \<noteq> {} \<Longrightarrow> subprob_space (null_measure M)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
    45
by(simp add: null_measure_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
    46
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    47
lemma (in subprob_space) subprob_space_distr:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    48
  assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    49
proof (rule subprob_spaceI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    50
  have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    51
  with f show "emeasure (distr M M' f) (space (distr M M' f)) \<le> 1"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    52
    by (auto simp: emeasure_distr emeasure_space_le_1)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    53
  show "space (distr M M' f) \<noteq> {}" by (simp add: assms)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    54
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    55
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
    56
lemma (in subprob_space) subprob_emeasure_le_1: "emeasure M X \<le> 1"
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    57
  by (rule order.trans[OF emeasure_space emeasure_space_le_1])
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
    58
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
    59
lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
    60
  using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
    61
59427
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    62
lemma (in subprob_space) nn_integral_le_const:
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    63
  assumes "0 \<le> c" "AE x in M. f x \<le> c"
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    64
  shows "(\<integral>\<^sup>+x. f x \<partial>M) \<le> c"
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    65
proof -
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    66
  have "(\<integral>\<^sup>+ x. f x \<partial>M) \<le> (\<integral>\<^sup>+ x. c \<partial>M)"
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    67
    by(rule nn_integral_mono_AE) fact
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    68
  also have "\<dots> \<le> c * emeasure M (space M)"
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    69
    using \<open>0 \<le> c\<close> by(simp add: nn_integral_const_If)
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    70
  also have "\<dots> \<le> c * 1" using emeasure_space_le_1 \<open>0 \<le> c\<close> by(rule ereal_mult_left_mono)
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    71
  finally show ?thesis by simp
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    72
qed
084330e2ec5e generalise lemma
Andreas Lochbihler
parents: 59425
diff changeset
    73
59092
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    74
lemma emeasure_density_distr_interval:
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    75
  fixes h :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real" and g' :: "real \<Rightarrow> real"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    76
  assumes [simp]: "a \<le> b"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    77
  assumes Mf[measurable]: "f \<in> borel_measurable borel"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    78
  assumes Mg[measurable]: "g \<in> borel_measurable borel"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    79
  assumes Mg'[measurable]: "g' \<in> borel_measurable borel"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    80
  assumes Mh[measurable]: "h \<in> borel_measurable borel"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    81
  assumes prob: "subprob_space (density lborel f)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    82
  assumes nonnegf: "\<And>x. f x \<ge> 0"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    83
  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    84
  assumes contg': "continuous_on {a..b} g'"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    85
  assumes mono: "strict_mono_on g {a..b}" and inv: "\<And>x. h x \<in> {a..b} \<Longrightarrow> g (h x) = x"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    86
  assumes range: "{a..b} \<subseteq> range h"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    87
  shows "emeasure (distr (density lborel f) lborel h) {a..b} = 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    88
             emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    89
proof (cases "a < b")
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    90
  assume "a < b"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    91
  from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    92
  from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    93
  from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    94
    by (rule mono_on_imp_deriv_nonneg) (auto simp: interior_atLeastAtMost_real)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    95
  from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    96
    by (rule continuous_ge_on_Iii) (simp_all add: `a < b`)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    97
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    98
  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
    99
  have A: "h -` {a..b} = {g a..g b}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   100
  proof (intro equalityI subsetI)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   101
    fix x assume x: "x \<in> h -` {a..b}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   102
    hence "g (h x) \<in> {g a..g b}" by (auto intro: mono_onD[OF mono'])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   103
    with inv and x show "x \<in> {g a..g b}" by simp
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   104
  next
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   105
    fix y assume y: "y \<in> {g a..g b}"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   106
    with IVT'[OF _ _ _ contg, of y] obtain x where "x \<in> {a..b}" "y = g x" by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   107
    with range and inv show "y \<in> h -` {a..b}" by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   108
  qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   109
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   110
  have prob': "subprob_space (distr (density lborel f) lborel h)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   111
    by (rule subprob_space.subprob_space_distr[OF prob]) (simp_all add: Mh)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   112
  have B: "emeasure (distr (density lborel f) lborel h) {a..b} = 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   113
            \<integral>\<^sup>+x. f x * indicator (h -` {a..b}) x \<partial>lborel"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   114
    by (subst emeasure_distr) (simp_all add: emeasure_density Mf Mh measurable_sets_borel[OF Mh])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   115
  also note A
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   116
  also have "emeasure (distr (density lborel f) lborel h) {a..b} \<le> 1"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   117
    by (rule subprob_space.subprob_emeasure_le_1) (rule prob')
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   118
  hence "emeasure (distr (density lborel f) lborel h) {a..b} \<noteq> \<infinity>" by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   119
  with assms have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   120
                      (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   121
    by (intro nn_integral_substitution_aux)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   122
       (auto simp: derivg_nonneg A B emeasure_density mult.commute `a < b`)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   123
  also have "... = emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}" 
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   124
    by (simp add: emeasure_density)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   125
  finally show ?thesis .
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   126
next
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   127
  assume "\<not>a < b"
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   128
  with `a \<le> b` have [simp]: "b = a" by (simp add: not_less del: `a \<le> b`)
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   129
  from inv and range have "h -` {a} = {g a}" by auto
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   130
  thus ?thesis by (simp_all add: emeasure_distr emeasure_density measurable_sets_borel[OF Mh])
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   131
qed
d469103c0737 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
hoelzl
parents: 59048
diff changeset
   132
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   133
locale pair_subprob_space = 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   134
  pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   135
61565
352c73a689da Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents: 61424
diff changeset
   136
sublocale pair_subprob_space \<subseteq> P?: subprob_space "M1 \<Otimes>\<^sub>M M2"
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   137
proof
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   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)"
59559
35da1bbf234e more canonical order of subscriptions avoids superfluous facts
haftmann
parents: 59525
diff changeset
   139
    by (metis monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   140
  from this[OF _ _ M1.emeasure_space_le_1 M2.emeasure_space_le_1]
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   141
    show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) \<le> 1"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   142
    by (simp add: M2.emeasure_pair_measure_Times space_pair_measure emeasure_nonneg)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   143
  from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \<Otimes>\<^sub>M M2) \<noteq> {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   144
    by (simp add: space_pair_measure)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   145
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   146
59425
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 59092
diff changeset
   147
lemma subprob_space_null_measure_iff:
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 59092
diff changeset
   148
    "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}"
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 59092
diff changeset
   149
  by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)
c5e79df8cc21 import general thms from Density_Compiler
hoelzl
parents: 59092
diff changeset
   150
59525
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   151
lemma subprob_space_restrict_space:
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   152
  assumes M: "subprob_space M"
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   153
  and A: "A \<inter> space M \<in> sets M" "A \<inter> space M \<noteq> {}"
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   154
  shows "subprob_space (restrict_space M A)"
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   155
proof(rule subprob_spaceI)
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   156
  have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \<inter> space M)"
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   157
    using A by(simp add: emeasure_restrict_space space_restrict_space)
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   158
  also have "\<dots> \<le> 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M)
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   159
  finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \<le> 1" .
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   160
next
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   161
  show "space (restrict_space M A) \<noteq> {}"
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   162
    using A by(simp add: space_restrict_space)
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   163
qed
dfe6449aecd8 more lemmas
Andreas Lochbihler
parents: 59427
diff changeset
   164
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   165
definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   166
  "subprob_algebra K =
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   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)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   168
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   169
lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   170
  by (auto simp add: subprob_algebra_def space_Sup_sigma)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   171
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   172
lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   173
  by (simp add: subprob_algebra_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   174
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   175
lemma measurable_emeasure_subprob_algebra[measurable]: 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   176
  "a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   177
  by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   178
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   179
lemma subprob_measurableD:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   180
  assumes N: "N \<in> measurable M (subprob_algebra S)" and x: "x \<in> space M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   181
  shows "space (N x) = space S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   182
    and "sets (N x) = sets S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   183
    and "measurable (N x) K = measurable S K"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   184
    and "measurable K (N x) = measurable K S"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   185
  using measurable_space[OF N x]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   186
  by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   187
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   188
ML {*
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   189
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   190
fun subprob_cong thm ctxt = (
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   191
  let
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   192
    val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59559
diff changeset
   193
    val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   194
      dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   195
  in
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   196
    if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt)
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   197
            else ([], ctxt)
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   198
  end
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   199
  handle THM _ => ([], ctxt) | TERM _ => ([], ctxt))
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   200
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   201
*}
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   202
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   203
setup \<open>
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   204
  Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong)
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   205
\<close>
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   206
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   207
context
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   208
  fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   209
begin
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   210
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   211
lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   212
  using measurable_space[OF K] by (simp add: space_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   213
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   214
lemma sets_kernel: "a \<in> space M \<Longrightarrow> sets (K a) = sets N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   215
  using measurable_space[OF K] by (simp add: space_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   216
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   217
lemma measurable_emeasure_kernel[measurable]: 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   218
    "A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   219
  using measurable_compose[OF K measurable_emeasure_subprob_algebra] .
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   220
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   221
end
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   222
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   223
lemma measurable_subprob_algebra:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   224
  "(\<And>a. a \<in> space M \<Longrightarrow> subprob_space (K a)) \<Longrightarrow>
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   225
  (\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow>
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   226
  (\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow>
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   227
  K \<in> measurable M (subprob_algebra N)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   228
  by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   229
59778
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   230
lemma measurable_submarkov:
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   231
  "K \<in> measurable M (subprob_algebra M) \<longleftrightarrow>
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   232
    (\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   233
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> measurable M borel)"
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   234
proof
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   235
  assume "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   236
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   237
  then show "K \<in> measurable M (subprob_algebra M)"
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   238
    by (intro measurable_subprob_algebra) auto
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   239
next
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   240
  assume "K \<in> measurable M (subprob_algebra M)"
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   241
  then show "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   242
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   243
    by (auto dest: subprob_space_kernel sets_kernel)
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   244
qed
fe5b796d6b2a add measurable_submarkov
hoelzl
parents: 59582
diff changeset
   245
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   246
lemma space_subprob_algebra_empty_iff:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   247
  "space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   248
proof
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   249
  have "\<And>x. x \<in> space N \<Longrightarrow> density N (\<lambda>_. 0) \<in> space (subprob_algebra N)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   250
    by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   251
  then show "space (subprob_algebra N) = {} \<Longrightarrow> space N = {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   252
    by auto
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   253
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   254
  assume "space N = {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   255
  hence "sets N = {{}}" by (simp add: space_empty_iff)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   256
  moreover have "\<And>M. subprob_space M \<Longrightarrow> sets M \<noteq> {{}}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   257
    by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric])
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   258
  ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   259
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   260
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   261
lemma nn_integral_measurable_subprob_algebra':
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   262
  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   263
  shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   264
  using f
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   265
proof induct
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   266
  case (cong f g)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   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"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   268
    by (intro measurable_cong nn_integral_cong cong)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   269
       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   270
  ultimately show ?case by simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   271
next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   272
  case (set B)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   273
  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   274
    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   275
  ultimately show ?case
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   276
    by (simp add: measurable_emeasure_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   277
next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   278
  case (mult f c)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   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"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   280
    by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   281
  ultimately show ?case
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   282
    by simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   283
next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   284
  case (add f g)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   285
  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"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   286
    by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   287
  ultimately show ?case
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   288
    by (simp add: ac_simps)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   289
next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   290
  case (seq F)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   291
  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"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   292
    unfolding SUP_apply
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   293
    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   294
  ultimately show ?case
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   295
    by (simp add: ac_simps)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   296
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   297
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   298
lemma nn_integral_measurable_subprob_algebra:
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   299
  "f \<in> borel_measurable N \<Longrightarrow> (\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)"
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   300
  by (subst nn_integral_max_0[symmetric])
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   301
     (auto intro!: nn_integral_measurable_subprob_algebra')
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   302
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   303
lemma measurable_distr:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   304
  assumes [measurable]: "f \<in> measurable M N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   305
  shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   306
proof (cases "space N = {}")
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   307
  assume not_empty: "space N \<noteq> {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   308
  show ?thesis
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   309
  proof (rule measurable_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   310
    fix A assume A: "A \<in> sets N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   311
    then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow>
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   312
      (\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   313
      by (intro measurable_cong)
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   314
         (auto simp: emeasure_distr space_subprob_algebra
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   315
               intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="op \<inter>"])
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   316
    also have "\<dots>"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   317
      using A by (intro measurable_emeasure_subprob_algebra) simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   318
    finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   319
  qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   320
qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   321
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   322
lemma emeasure_space_subprob_algebra[measurable]:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   323
  "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   324
proof-
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   325
  have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M")
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   326
    by (rule measurable_emeasure_subprob_algebra) simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   327
  also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   328
    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   329
  finally show ?thesis .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   330
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   331
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   332
lemma integral_measurable_subprob_algebra:
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   333
  fixes f :: "_ \<Rightarrow> real"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   334
  assumes f_measurable [measurable]: "f \<in> borel_measurable N"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   335
  and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   336
  shows "(\<lambda>M. integral\<^sup>L M f) \<in> borel_measurable (subprob_algebra N)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   337
proof -
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   338
  note [measurable] = nn_integral_measurable_subprob_algebra
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   339
  have "?thesis \<longleftrightarrow> (\<lambda>M. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M) - real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M)) \<in> borel_measurable (subprob_algebra N)"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   340
  proof(rule measurable_cong)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   341
    fix M
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   342
    assume "M \<in> space (subprob_algebra N)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   343
    hence "subprob_space M" and M [measurable_cong]: "sets M = sets N" 
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   344
      by(simp_all add: space_subprob_algebra)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   345
    interpret subprob_space M by fact
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   346
    have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   347
      by(rule nn_integral_mono)(simp add: sets_eq_imp_space_eq[OF M] f_bounded)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   348
    also have "\<dots> = max B 0 * emeasure M (space M)" by(simp add: nn_integral_const_If max_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   349
    also have "\<dots> \<le> ereal (max B 0) * 1"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   350
      by(rule ereal_mult_left_mono)(simp_all add: emeasure_space_le_1 zero_ereal_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   351
    finally have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<noteq> \<infinity>" by(auto simp add: max_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   352
    then have "integrable M f" using f_measurable
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   353
      by(auto intro: integrableI_bounded)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   354
    thus "(\<integral> x. f x \<partial>M) = real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M) - real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M)"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   355
      by(simp add: real_lebesgue_integral_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   356
  qed
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   357
  also have "\<dots>" by measurable
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   358
  finally show ?thesis .
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   359
qed
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   360
59978
c2dc7856e2e5 eliminated suspicious Unicode character;
wenzelm
parents: 59778
diff changeset
   361
(* TODO: Rename. This name is too general -- Manuel *)
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   362
lemma measurable_pair_measure:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   363
  assumes f: "f \<in> measurable M (subprob_algebra N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   364
  assumes g: "g \<in> measurable M (subprob_algebra L)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   365
  shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   366
proof (rule measurable_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   367
  { fix x assume "x \<in> space M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   368
    with measurable_space[OF f] measurable_space[OF g]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   369
    have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   370
      by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   371
    interpret F: subprob_space "f x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   372
      using fx by (simp add: space_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   373
    interpret G: subprob_space "g x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   374
      using gx by (simp add: space_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   375
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   376
    interpret pair_subprob_space "f x" "g x" ..
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   377
    show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   378
    show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   379
      using fx gx by (simp add: space_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   380
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   381
    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"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   382
      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   383
    have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   384
              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   385
      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   386
    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) =
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   387
                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   388
      using emeasure_compl[OF _ P.emeasure_finite]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   389
      unfolding sets_eq
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   390
      unfolding sets_eq_imp_space_eq[OF sets_eq]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   391
      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   392
    note 1 2 sets_eq }
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   393
  note Times = this(1) and Compl = this(2) and sets_eq = this(3)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   394
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   395
  fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   396
  show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   397
    using Int_stable_pair_measure_generator pair_measure_closed A
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   398
    unfolding sets_pair_measure
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   399
  proof (induct A rule: sigma_sets_induct_disjoint)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   400
    case (basic A) then show ?case
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   401
      by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   402
         (auto intro!: measurable_emeasure_kernel f g)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   403
  next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   404
    case (compl A)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   405
    then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   406
      by (auto simp: sets_pair_measure)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   407
    have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   408
                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   409
      using compl(2) f g by measurable
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   410
    thus ?case by (simp add: Compl A cong: measurable_cong)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   411
  next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   412
    case (union A)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   413
    then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   414
      by (auto simp: sets_pair_measure)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   415
    then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   416
      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   417
      by (intro measurable_cong suminf_emeasure[symmetric])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   418
         (auto simp: sets_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   419
    also have "\<dots>"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   420
      using union by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   421
    finally show ?case .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   422
  qed simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   423
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   424
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   425
lemma restrict_space_measurable:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   426
  assumes X: "X \<noteq> {}" "X \<in> sets K"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   427
  assumes N: "N \<in> measurable M (subprob_algebra K)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   428
  shows "(\<lambda>x. restrict_space (N x) X) \<in> measurable M (subprob_algebra (restrict_space K X))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   429
proof (rule measurable_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   430
  fix a assume a: "a \<in> space M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   431
  from N[THEN measurable_space, OF this]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   432
  have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   433
    by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   434
  then interpret subprob_space "N a"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   435
    by simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   436
  show "subprob_space (restrict_space (N a) X)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   437
  proof
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   438
    show "space (restrict_space (N a) X) \<noteq> {}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   439
      using X by (auto simp add: space_restrict_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   440
    show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \<le> 1"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   441
      using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   442
  qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   443
  show "sets (restrict_space (N a) X) = sets (restrict_space K X)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   444
    by (intro sets_restrict_space_cong) fact
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   445
next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   446
  fix A assume A: "A \<in> sets (restrict_space K X)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   447
  show "(\<lambda>a. emeasure (restrict_space (N a) X) A) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   448
  proof (subst measurable_cong)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   449
    fix a assume "a \<in> space M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   450
    from N[THEN measurable_space, OF this]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   451
    have [simp]: "sets (N a) = sets K" "space (N a) = space K"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   452
      by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   453
    show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \<inter> X)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   454
      using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   455
  next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   456
    show "(\<lambda>w. emeasure (N w) (A \<inter> X)) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   457
      using A X
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   458
      by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   459
         (auto simp: sets_restrict_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   460
  qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   461
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   462
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   463
section {* Properties of return *}
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   464
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   465
definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   466
  "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   467
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   468
lemma space_return[simp]: "space (return M x) = space M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   469
  by (simp add: return_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   470
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   471
lemma sets_return[simp]: "sets (return M x) = sets M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   472
  by (simp add: return_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   473
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   474
lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   475
  by (simp cong: measurable_cong_sets) 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   476
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   477
lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   478
  by (simp cong: measurable_cong_sets) 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   479
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   480
lemma return_sets_cong: "sets M = sets N \<Longrightarrow> return M = return N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   481
  by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   482
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   483
lemma return_cong: "sets A = sets B \<Longrightarrow> return A x = return B x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   484
  by (auto simp add: return_def dest: sets_eq_imp_space_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   485
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   486
lemma emeasure_return[simp]:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   487
  assumes "A \<in> sets M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   488
  shows "emeasure (return M x) A = indicator A x"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   489
proof (rule emeasure_measure_of[OF return_def])
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   490
  show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   491
  show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   492
  from assms show "A \<in> sets (return M x)" unfolding return_def by simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   493
  show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   494
    by (auto intro: countably_additiveI simp: suminf_indicator)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   495
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   496
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   497
lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   498
  by rule simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   499
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   500
lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   501
  by (intro prob_space_return prob_space_imp_subprob_space)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   502
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   503
lemma subprob_space_return_ne: 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   504
  assumes "space M \<noteq> {}" shows "subprob_space (return M x)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   505
proof
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   506
  show "emeasure (return M x) (space (return M x)) \<le> 1"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   507
    by (subst emeasure_return) (auto split: split_indicator)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   508
qed (simp, fact)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   509
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   510
lemma measure_return: assumes X: "X \<in> sets M" shows "measure (return M x) X = indicator X x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   511
  unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   512
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   513
lemma AE_return:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   514
  assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   515
  shows "(AE y in return M x. P y) \<longleftrightarrow> P x"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   516
proof -
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   517
  have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   518
    by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   519
  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)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   520
    by (rule AE_cong) auto
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   521
  finally show ?thesis .
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   522
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   523
  
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   524
lemma nn_integral_return:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   525
  assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   526
  shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   527
proof-
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   528
  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   529
  have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   530
    by (intro nn_integral_cong_AE) (auto simp: AE_return)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   531
  also have "... = g x"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   532
    using nn_integral_const[OF `g x \<ge> 0`, of "return M x"] emeasure_space_1 by simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   533
  finally show ?thesis .
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   534
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   535
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   536
lemma integral_return:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   537
  fixes g :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   538
  assumes "x \<in> space M" "g \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   539
  shows "(\<integral>a. g a \<partial>return M x) = g x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   540
proof-
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   541
  interpret prob_space "return M x" by (rule prob_space_return[OF `x \<in> space M`])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   542
  have "(\<integral>a. g a \<partial>return M x) = (\<integral>a. g x \<partial>return M x)" using assms
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   543
    by (intro integral_cong_AE) (auto simp: AE_return)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   544
  then show ?thesis
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   545
    using prob_space by simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   546
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   547
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   548
lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)"
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   549
  by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   550
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   551
lemma distr_return:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   552
  assumes "f \<in> measurable M N" and "x \<in> space M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   553
  shows "distr (return M x) N f = return N (f x)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   554
  using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   555
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   556
lemma return_restrict_space:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   557
  "\<Omega> \<in> sets M \<Longrightarrow> return (restrict_space M \<Omega>) x = restrict_space (return M x) \<Omega>"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   558
  by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   559
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   560
lemma measurable_distr2:
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61359
diff changeset
   561
  assumes f[measurable]: "case_prod f \<in> measurable (L \<Otimes>\<^sub>M M) N"
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   562
  assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   563
  shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   564
proof -
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   565
  have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61359
diff changeset
   566
    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)"
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   567
  proof (rule measurable_cong)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   568
    fix x assume x: "x \<in> space L"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   569
    have gx: "g x \<in> space (subprob_algebra M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   570
      using measurable_space[OF g x] .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   571
    then have [simp]: "sets (g x) = sets M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   572
      by (simp add: space_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   573
    then have [simp]: "space (g x) = space M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   574
      by (rule sets_eq_imp_space_eq)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   575
    let ?R = "return L x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   576
    from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   577
      by simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   578
    interpret subprob_space "g x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   579
      using gx by (simp add: space_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   580
    have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   581
      by (simp add: space_pair_measure)
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61359
diff changeset
   582
    show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (case_prod f)" (is "?l = ?r")
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   583
    proof (rule measure_eqI)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   584
      show "sets ?l = sets ?r"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   585
        by simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   586
    next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   587
      fix A assume "A \<in> sets ?l"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   588
      then have A[measurable]: "A \<in> sets N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   589
        by simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   590
      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))"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   591
        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   592
      also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   593
        apply (subst emeasure_pair_measure_alt)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   594
        apply (rule measurable_sets[OF _ A])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   595
        apply (auto simp add: f_M' cong: measurable_cong_sets)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   596
        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   597
        apply (auto simp: space_subprob_algebra space_pair_measure)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   598
        done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   599
      also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   600
        by (subst nn_integral_return)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   601
           (auto simp: x intro!: measurable_emeasure)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   602
      also have "\<dots> = emeasure ?l A"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   603
        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   604
      finally show "emeasure ?l A = emeasure ?r A" ..
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   605
    qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   606
  qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   607
  also have "\<dots>"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   608
    apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   609
    apply (rule return_measurable)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   610
    apply measurable
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   611
    done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   612
  finally show ?thesis .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   613
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   614
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   615
lemma nn_integral_measurable_subprob_algebra2:
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   616
  assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   617
  assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   618
  shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   619
proof -
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   620
  note nn_integral_measurable_subprob_algebra[measurable]
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   621
  note measurable_distr2[measurable]
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   622
  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"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   623
    by measurable
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   624
  then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   625
    by (rule measurable_cong[THEN iffD1, rotated])
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   626
       (simp add: nn_integral_distr)
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   627
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   628
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   629
lemma emeasure_measurable_subprob_algebra2:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   630
  assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   631
  assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   632
  shows "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   633
proof -
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   634
  { fix x assume "x \<in> space M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   635
    then have "Pair x -` Sigma (space M) A = A x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   636
      by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   637
    with sets_Pair1[OF A, of x] have "A x \<in> sets N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   638
      by auto }
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   639
  note ** = this
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   640
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   641
  have *: "\<And>x. fst x \<in> space M \<Longrightarrow> snd x \<in> A (fst x) \<longleftrightarrow> x \<in> (SIGMA x:space M. A x)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   642
    by (auto simp: fun_eq_iff)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   643
  have "(\<lambda>(x, y). indicator (A x) y::ereal) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   644
    apply measurable
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   645
    apply (subst measurable_cong)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   646
    apply (rule *)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   647
    apply (auto simp: space_pair_measure)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   648
    done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   649
  then have "(\<lambda>x. integral\<^sup>N (L x) (indicator (A x))) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   650
    by (intro nn_integral_measurable_subprob_algebra2[where N=N] ereal_indicator_nonneg L)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   651
  then show "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   652
    apply (rule measurable_cong[THEN iffD1, rotated])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   653
    apply (rule nn_integral_indicator)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   654
    apply (simp add: subprob_measurableD[OF L] **)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   655
    done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   656
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   657
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   658
lemma measure_measurable_subprob_algebra2:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   659
  assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   660
  assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   661
  shows "(\<lambda>x. measure (L x) (A x)) \<in> borel_measurable M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   662
  unfolding measure_def
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   663
  by (intro borel_measurable_real_of_ereal emeasure_measurable_subprob_algebra2[OF assms])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
   664
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   665
definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   666
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   667
lemma select_sets1:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   668
  "sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   669
  unfolding select_sets_def by (rule someI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   670
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   671
lemma sets_select_sets[simp]:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   672
  assumes sets: "sets M = sets (subprob_algebra N)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   673
  shows "sets (select_sets M) = sets N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   674
  unfolding select_sets_def
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   675
proof (rule someI2)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   676
  show "sets M = sets (subprob_algebra N)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   677
    by fact
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   678
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   679
  fix L assume "sets M = sets (subprob_algebra L)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   680
  with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   681
    by (intro sets_eq_imp_space_eq) simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   682
  show "sets L = sets N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   683
  proof cases
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   684
    assume "space (subprob_algebra N) = {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   685
    with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L]
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   686
    show ?thesis
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   687
      by (simp add: eq space_empty_iff)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   688
  next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   689
    assume "space (subprob_algebra N) \<noteq> {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   690
    with eq show ?thesis
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   691
      by (fastforce simp add: space_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   692
  qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   693
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   694
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   695
lemma space_select_sets[simp]:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   696
  "sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   697
  by (intro sets_eq_imp_space_eq sets_select_sets)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   698
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   699
section {* Join *}
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   700
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   701
definition join :: "'a measure measure \<Rightarrow> 'a measure" where
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   702
  "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   703
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   704
lemma
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   705
  shows space_join[simp]: "space (join M) = space (select_sets M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   706
    and sets_join[simp]: "sets (join M) = sets (select_sets M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   707
  by (simp_all add: join_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   708
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   709
lemma emeasure_join:
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   710
  assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   711
  shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   712
proof (rule emeasure_measure_of[OF join_def])
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   713
  show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   714
  proof (rule countably_additiveI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   715
    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   716
    have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   717
      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   718
    also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   719
    proof (rule nn_integral_cong)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   720
      fix M' assume "M' \<in> space M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   721
      then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   722
        using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   723
    qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   724
    finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" .
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   725
  qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   726
qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   727
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   728
lemma measurable_join:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   729
  "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   730
proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   731
  fix A assume "A \<in> sets N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   732
  let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   733
  have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   734
  proof (rule measurable_cong)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   735
    fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   736
    then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   737
      by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   738
  qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   739
  also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   740
    using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`]
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   741
    by (rule nn_integral_measurable_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   742
  finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   743
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   744
  assume [simp]: "space N \<noteq> {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   745
  fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   746
  then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   747
    apply (intro nn_integral_mono)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   748
    apply (auto simp: space_subprob_algebra 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   749
                 dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   750
    done
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   751
  with M show "subprob_space (join M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   752
    by (intro subprob_spaceI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   753
       (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   754
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   755
  assume "\<not>(space N \<noteq> {})"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   756
  thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   757
qed (auto simp: space_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   758
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   759
lemma nn_integral_join':
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   760
  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   761
    and M[measurable_cong]: "sets M = sets (subprob_algebra N)"
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   762
  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   763
  using f
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   764
proof induct
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   765
  case (cong f g)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   766
  moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   767
    by (intro nn_integral_cong cong) (simp add: M)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   768
  moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   769
    by (intro nn_integral_cong cong)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   770
       (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   771
  ultimately show ?case
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   772
    by simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   773
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   774
  case (set A)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   775
  moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   776
    by (intro nn_integral_cong nn_integral_indicator)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   777
       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   778
  ultimately show ?case
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   779
    using M by (simp add: emeasure_join)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   780
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   781
  case (mult f c)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   782
  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)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   783
    using mult M M[THEN sets_eq_imp_space_eq]
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   784
    by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   785
  also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   786
    using nn_integral_measurable_subprob_algebra[OF mult(3)]
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   787
    by (intro nn_integral_cmult mult) (simp add: M)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   788
  also have "\<dots> = c * (integral\<^sup>N (join M) f)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   789
    by (simp add: mult)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   790
  also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   791
    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   792
  finally show ?case by simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   793
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   794
  case (add f g)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   795
  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)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   796
    using add M M[THEN sets_eq_imp_space_eq]
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   797
    by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   798
  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)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   799
    using nn_integral_measurable_subprob_algebra[OF add(1)]
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   800
    using nn_integral_measurable_subprob_algebra[OF add(5)]
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   801
    by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   802
  also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   803
    by (simp add: add)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   804
  also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   805
    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   806
  finally show ?case by (simp add: ac_simps)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   807
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   808
  case (seq F)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   809
  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)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   810
    using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   811
    by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   812
       (auto simp add: space_subprob_algebra)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   813
  also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   814
    using nn_integral_measurable_subprob_algebra[OF seq(1)] seq
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   815
    by (intro nn_integral_monotone_convergence_SUP)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   816
       (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   817
  also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   818
    by (simp add: seq)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   819
  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   820
    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   821
                 (simp_all add: M cong: measurable_cong_sets)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   822
  finally show ?case by (simp add: ac_simps)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   823
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   824
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   825
lemma nn_integral_join:
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   826
  assumes f[measurable]: "f \<in> borel_measurable N" "sets M = sets (subprob_algebra N)"
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   827
  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   828
  apply (subst (1 3) nn_integral_max_0[symmetric])
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   829
  apply (rule nn_integral_join')
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   830
  apply (auto simp: f)
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   831
  done
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   832
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   833
lemma measurable_join1:
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   834
  "\<lbrakk> f \<in> measurable N K; sets M = sets (subprob_algebra N) \<rbrakk>
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   835
  \<Longrightarrow> f \<in> measurable (join M) K"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   836
by(simp add: measurable_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   837
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   838
lemma 
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   839
  fixes f :: "_ \<Rightarrow> real"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   840
  assumes f_measurable [measurable]: "f \<in> borel_measurable N"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   841
  and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   842
  and M [measurable_cong]: "sets M = sets (subprob_algebra N)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   843
  and fin: "finite_measure M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   844
  and M_bounded: "AE M' in M. emeasure M' (space M') \<le> ereal B'"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   845
  shows integrable_join: "integrable (join M) f" (is ?integrable)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   846
  and integral_join: "integral\<^sup>L (join M) f = \<integral> M'. integral\<^sup>L M' f \<partial>M" (is ?integral)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   847
proof(case_tac [!] "space N = {}")
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   848
  assume *: "space N = {}"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   849
  show ?integrable 
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   850
    using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   851
  have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   852
  proof(rule integral_cong)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   853
    fix M'
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   854
    assume "M' \<in> space M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   855
    with sets_eq_imp_space_eq[OF M] have "space M' = space N"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   856
      by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   857
    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   858
  qed simp
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   859
  then show ?integral
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   860
    using M * by(simp add: integral_empty)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   861
next
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   862
  assume *: "space N \<noteq> {}"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   863
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   864
  from * have B [simp]: "0 \<le> B" by(auto dest: f_bounded)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   865
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   866
  have [measurable]: "f \<in> borel_measurable (join M)" using f_measurable M
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   867
    by(rule measurable_join1)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   868
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   869
  { fix f M'
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   870
    assume [measurable]: "f \<in> borel_measurable N"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   871
      and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   872
      and "M' \<in> space M" "emeasure M' (space M') \<le> ereal B'"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   873
    have "AE x in M'. ereal (f x) \<le> ereal B"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   874
    proof(rule AE_I2)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   875
      fix x
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   876
      assume "x \<in> space M'"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   877
      with \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   878
      have "x \<in> space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   879
      from f_bounded[OF this] show "ereal (f x) \<le> ereal B" by simp
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   880
    qed
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   881
    then have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M')"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   882
      by(rule nn_integral_mono_AE)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   883
    also have "\<dots> = ereal B * emeasure M' (space M')" by(simp)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   884
    also have "\<dots> \<le> ereal B * ereal B'" by(rule ereal_mult_left_mono)(fact, simp)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   885
    also have "\<dots> \<le> ereal B * ereal \<bar>B'\<bar>" by(rule ereal_mult_left_mono)(simp_all)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   886
    finally have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)" by simp }
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   887
  note bounded1 = this
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   888
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   889
  have bounded:
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   890
    "\<And>f. \<lbrakk> f \<in> borel_measurable N; \<And>x. x \<in> space N \<Longrightarrow> f x \<le> B \<rbrakk>
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   891
    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   892
  proof -
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   893
    fix f
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   894
    assume [measurable]: "f \<in> borel_measurable N"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   895
      and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   896
    have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. ereal (f x) \<partial>M' \<partial>M)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   897
      by(rule nn_integral_join[OF _ M]) simp
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   898
    also have "\<dots> \<le> \<integral>\<^sup>+ M'. B * \<bar>B'\<bar> \<partial>M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   899
      using bounded1[OF \<open>f \<in> borel_measurable N\<close> f_bounded]
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   900
      by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   901
    also have "\<dots> = B * \<bar>B'\<bar> * emeasure M (space M)" by simp
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   902
    also have "\<dots> < \<infinity>" by(simp add: finite_measure.finite_emeasure_space[OF fin])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   903
    finally show "?thesis f" by simp
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   904
  qed
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   905
  have f_pos: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   906
    and f_neg: "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>join M) \<noteq> \<infinity>"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   907
    using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   908
  
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   909
  show ?integrable using f_pos f_neg by(simp add: real_integrable_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   910
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   911
  note [measurable] = nn_integral_measurable_subprob_algebra
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   912
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   913
  have "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>join M)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   914
    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   915
  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (f x) \<partial>M' \<partial>M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   916
    by(simp add: nn_integral_join[OF _ M])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   917
  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   918
    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   919
  finally have int_f: "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" .
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   920
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   921
  have "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (- f x) \<partial>join M)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   922
    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   923
  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (- f x) \<partial>M' \<partial>M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   924
    by(simp add: nn_integral_join[OF _ M])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   925
  also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   926
    by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   927
  finally have int_mf: "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)" .
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   928
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   929
  have f_pos1:
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   930
    "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   931
    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   932
    using f_measurable by(auto intro!: bounded1 dest: f_bounded)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   933
  have "AE M' in M. (\<integral>\<^sup>+ x. f x \<partial>M') \<noteq> \<infinity>"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   934
    using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_pos1)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   935
  hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   936
    by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   937
  from f_pos have [simp]: "integrable M (\<lambda>M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M'))"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   938
    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)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   939
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   940
  have f_neg1:
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   941
    "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   942
    \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (- f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   943
    using f_measurable by(auto intro!: bounded1 dest: f_bounded)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   944
  have "AE M' in M. (\<integral>\<^sup>+ x. - f x \<partial>M') \<noteq> \<infinity>"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   945
    using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_neg1)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   946
  hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   947
    by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   948
  from f_neg have [simp]: "integrable M (\<lambda>M'. real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M'))"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   949
    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)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   950
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   951
  from \<open>?integrable\<close>
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   952
  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)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   953
    by(simp add: real_lebesgue_integral_def ereal_minus(1)[symmetric] ereal_real nn_integral_nonneg f_pos f_neg del: ereal_minus(1))
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   954
  also note int_f
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   955
  also note int_mf
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   956
  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) = 
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   957
    ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)) - 
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   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))"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   959
    by(subst (7 11) nn_integral_0_iff_AE[THEN iffD2])(simp_all add: nn_integral_nonneg)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   960
  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_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   961
    using f_pos
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   962
    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])
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   963
  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_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   964
    using f_neg
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   965
    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])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   966
  also note ereal_minus(1)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   967
  also have "(\<integral> M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M) - (\<integral> M'. real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M) = 
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   968
    \<integral>M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') - real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   969
    by simp
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   970
  also have "\<dots> = \<integral>M'. \<integral> x. f x \<partial>M' \<partial>M" using _ _ M_bounded
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   971
  proof(rule integral_cong_AE[OF _ _ AE_mp[OF _ AE_I2], rule_format])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   972
    show "(\<lambda>M'. integral\<^sup>L M' f) \<in> borel_measurable M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   973
      by measurable(simp add: integral_measurable_subprob_algebra[OF _ f_bounded])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   974
      
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   975
    fix M'
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   976
    assume "M' \<in> space M" "emeasure M' (space M') \<le> B'"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   977
    then interpret finite_measure M' by(auto intro: finite_measureI)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   978
    
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   979
    from \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   980
    have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   981
    hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   982
    have "integrable M' f"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   983
      by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded)
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61424
diff changeset
   984
    then show "real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') - real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M') = \<integral> x. f x \<partial>M'"
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   985
      by(simp add: real_lebesgue_integral_def)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   986
  qed simp_all
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   987
  finally show ?integral by simp
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   988
qed
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
   989
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   990
lemma join_assoc:
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   991
  assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))"
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   992
  shows "join (distr M (subprob_algebra N) join) = join (join M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   993
proof (rule measure_eqI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   994
  fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   995
  then have A: "A \<in> sets N" by simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   996
  show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   997
    using measurable_join[of N]
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
   998
    by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
   999
                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M]
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1000
             intro!: nn_integral_cong emeasure_join)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1001
qed (simp add: M)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1002
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1003
lemma join_return: 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1004
  assumes "sets M = sets N" and "subprob_space M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1005
  shows "join (return (subprob_algebra N) M) = M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1006
  by (rule measure_eqI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1007
     (simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra  
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1008
                    measurable_emeasure_subprob_algebra nn_integral_return assms)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1009
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1010
lemma join_return':
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1011
  assumes "sets N = sets M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1012
  shows "join (distr M (subprob_algebra N) (return N)) = M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1013
apply (rule measure_eqI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1014
apply (simp add: assms)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1015
apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)")
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1016
apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1017
apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1018
done
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1019
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1020
lemma join_distr_distr:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1021
  fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1022
  assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1023
  shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l")
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1024
proof (rule measure_eqI)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1025
  fix A assume "A \<in> sets ?r"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1026
  hence A_in_N: "A \<in> sets N" by simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1027
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1028
  from assms have "f \<in> measurable (join M) N" 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1029
      by (simp cong: measurable_cong_sets)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1030
  moreover from assms and A_in_N have "f-`A \<inter> space R \<in> sets R" 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1031
      by (intro measurable_sets) simp_all
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1032
  ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-`A \<inter> space R) \<partial>M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1033
      by (simp_all add: A_in_N emeasure_distr emeasure_join assms)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1034
  
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1035
  also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1036
  proof (intro nn_integral_cong, subst emeasure_distr)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1037
    fix M' assume "M' \<in> space M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1038
    from assms have "space M = space (subprob_algebra R)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1039
        using sets_eq_imp_space_eq by blast
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1040
    with `M' \<in> space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1041
    show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1042
    have "space M' = space R" by (rule sets_eq_imp_space_eq) simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1043
    thus "emeasure M' (f -` A \<inter> space R) = emeasure M' (f -` A \<inter> space M')" by simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1044
  qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1045
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1046
  also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1047
      by (simp cong: measurable_cong_sets add: assms measurable_distr)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1048
  hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1049
             emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1050
      by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1051
  finally show "emeasure ?r A = emeasure ?l A" ..
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1052
qed simp
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1053
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1054
definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1055
  "bind M f = (if space M = {} then count_space {} else
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1056
    join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1057
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1058
adhoc_overloading Monad_Syntax.bind bind
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1059
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1060
lemma bind_empty: 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1061
  "space M = {} \<Longrightarrow> bind M f = count_space {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1062
  by (simp add: bind_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1063
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1064
lemma bind_nonempty:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1065
  "space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1066
  by (simp add: bind_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1067
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1068
lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1069
  by (auto simp: bind_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1070
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1071
lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1072
  by (simp add: bind_def)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1073
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1074
lemma sets_bind[simp, measurable_cong]:
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1075
  assumes f: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and M: "space M \<noteq> {}"
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1076
  shows "sets (bind M f) = sets N"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1077
  using f [of "SOME x. x \<in> space M"] by (simp add: bind_nonempty M some_in_eq)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1078
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1079
lemma space_bind[simp]: 
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1080
  assumes "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and "space M \<noteq> {}"
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1081
  shows "space (bind M f) = space N"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1082
  using assms by (intro sets_eq_imp_space_eq sets_bind)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1083
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1084
lemma bind_cong: 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1085
  assumes "\<forall>x \<in> space M. f x = g x"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1086
  shows "bind M f = bind M g"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1087
proof (cases "space M = {}")
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1088
  assume "space M \<noteq> {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1089
  hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1090
  with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1091
  with `space M \<noteq> {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1092
qed (simp add: bind_empty)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1093
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1094
lemma bind_nonempty':
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1095
  assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1096
  shows "bind M f = join (distr M (subprob_algebra N) f)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1097
  using assms
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1098
  apply (subst bind_nonempty, blast)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1099
  apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1100
  apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]])
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1101
  done
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1102
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1103
lemma bind_nonempty'':
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1104
  assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1105
  shows "bind M f = join (distr M (subprob_algebra N) f)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1106
  using assms by (auto intro: bind_nonempty')
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1107
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1108
lemma emeasure_bind:
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1109
    "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1110
      \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1111
  by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1112
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1113
lemma nn_integral_bind:
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1114
  assumes f: "f \<in> borel_measurable B"
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1115
  assumes N: "N \<in> measurable M (subprob_algebra B)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1116
  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1117
proof cases
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1118
  assume M: "space M \<noteq> {}" show ?thesis
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1119
    unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1120
    by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1121
qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1122
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1123
lemma AE_bind:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1124
  assumes P[measurable]: "Measurable.pred B P"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1125
  assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1126
  shows "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1127
proof cases
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1128
  assume M: "space M = {}" show ?thesis
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1129
    unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1130
next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1131
  assume M: "space M \<noteq> {}"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1132
  note sets_kernel[OF N, simp]
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1133
  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))"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1134
    by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator)
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1135
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1136
  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"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1137
    by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B]
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1138
             del: nn_integral_indicator)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1139
  also have "\<dots> = (AE x in M. AE y in N x. P y)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1140
    apply (subst nn_integral_0_iff_AE)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1141
    apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1142
    apply measurable
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1143
    apply (intro eventually_subst AE_I2)
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1144
    apply (auto simp add: emeasure_le_0_iff subprob_measurableD(1)[OF N]
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1145
                intro!: AE_iff_measurable[symmetric])
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1146
    done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1147
  finally show ?thesis .
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1148
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1149
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1150
lemma measurable_bind':
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1151
  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61359
diff changeset
  1152
          M2: "case_prod g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1153
  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1154
proof (subst measurable_cong)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1155
  fix x assume x_in_M: "x \<in> space M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1156
  with assms have "space (f x) \<noteq> {}" 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1157
      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1158
  moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1159
      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1160
         (auto dest: measurable_Pair2)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1161
  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1162
      by (simp_all add: bind_nonempty'')
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1163
next
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1164
  show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1165
    apply (rule measurable_compose[OF _ measurable_join])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1166
    apply (rule measurable_distr2[OF M2 M1])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1167
    done
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1168
qed
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1169
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1170
lemma measurable_bind[measurable (raw)]:
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1171
  assumes M1: "f \<in> measurable M (subprob_algebra N)" and
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1172
          M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1173
  shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1174
  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1175
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1176
lemma measurable_bind2:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1177
  assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1178
  shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1179
    using assms by (intro measurable_bind' measurable_const) auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1180
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1181
lemma subprob_space_bind:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1182
  assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1183
  shows "subprob_space (M \<guillemotright>= f)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1184
proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1185
  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1186
    by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1187
        rule measurable_compose[OF measurable_snd assms(2)])
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1188
  from assms(1) show "M \<in> space (subprob_algebra M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1189
    by (simp add: space_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1190
qed
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1191
60067
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1192
lemma 
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1193
  fixes f :: "_ \<Rightarrow> real"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1194
  assumes f_measurable [measurable]: "f \<in> borel_measurable K"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1195
  and f_bounded: "\<And>x. x \<in> space K \<Longrightarrow> \<bar>f x\<bar> \<le> B" 
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1196
  and N [measurable]: "N \<in> measurable M (subprob_algebra K)"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1197
  and fin: "finite_measure M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1198
  and M_bounded: "AE x in M. emeasure (N x) (space (N x)) \<le> ereal B'"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1199
  shows integrable_bind: "integrable (bind M N) f" (is ?integrable)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1200
  and integral_bind: "integral\<^sup>L (bind M N) f = \<integral> x. integral\<^sup>L (N x) f \<partial>M" (is ?integral)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1201
proof(case_tac [!] "space M = {}")
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1202
  assume [simp]: "space M \<noteq> {}"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1203
  interpret finite_measure M by(rule fin)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1204
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1205
  have "integrable (join (distr M (subprob_algebra K) N)) f"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1206
    using f_measurable f_bounded
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1207
    by(rule integrable_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1208
  then show ?integrable by(simp add: bind_nonempty''[where N=K])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1209
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1210
  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"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1211
    using f_measurable f_bounded
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1212
    by(rule integral_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1213
  also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1214
    by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _ f_bounded])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1215
  finally show ?integral by(simp add: bind_nonempty''[where N=K])
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1216
qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
f1a5bcf5658f lemmas about integrals over bind and join on measures
Andreas Lochbihler
parents: 59978
diff changeset
  1217
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1218
lemma (in prob_space) prob_space_bind: 
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1219
  assumes ae: "AE x in M. prob_space (N x)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1220
    and N[measurable]: "N \<in> measurable M (subprob_algebra S)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1221
  shows "prob_space (M \<guillemotright>= N)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1222
proof
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1223
  have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1224
    by (subst emeasure_bind[where N=S])
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1225
       (auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong)
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1226
  also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1227
    using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1228
  finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1229
    by (simp add: emeasure_space_1)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1230
qed
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1231
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1232
lemma (in subprob_space) bind_in_space:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1233
  "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)"
59048
7dc8ac6f0895 add congruence solver to measurability prover
hoelzl
parents: 59002
diff changeset
  1234
  by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind)
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1235
     unfold_locales
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1236
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1237
lemma (in subprob_space) measure_bind:
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1238
  assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1239
  shows "measure (M \<guillemotright>= f) X = \<integral>x. measure (f x) X \<partial>M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1240
proof -
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1241
  interpret Mf: subprob_space "M \<guillemotright>= f"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1242
    by (rule subprob_space_bind[OF _ f]) unfold_locales
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1243
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1244
  { fix x assume "x \<in> space M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1245
    from f[THEN measurable_space, OF this] interpret subprob_space "f x"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1246
      by (simp add: space_subprob_algebra)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1247
    have "emeasure (f x) X = ereal (measure (f x) X)" "measure (f x) X \<le> 1"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1248
      by (auto simp: emeasure_eq_measure subprob_measure_le_1) }
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1249
  note this[simp]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1250
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1251
  have "emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1252
    using subprob_not_empty f X by (rule emeasure_bind)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1253
  also have "\<dots> = \<integral>\<^sup>+x. ereal (measure (f x) X) \<partial>M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1254
    by (intro nn_integral_cong) simp
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1255
  also have "\<dots> = \<integral>x. measure (f x) X \<partial>M"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1256
    by (intro nn_integral_eq_integral integrable_const_bound[where B=1]
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1257
              measure_measurable_subprob_algebra2[OF _ f] pair_measureI X)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1258
       (auto simp: measure_nonneg)
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1259
  finally show ?thesis
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58608
diff changeset
  1260
    by (simp add: Mf.emeasure_eq_measure)
58606
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1261
qed
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1262
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1263
lemma emeasure_bind_const: 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1264
    "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1265
         emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1266
  by (simp add: bind_nonempty emeasure_join nn_integral_distr 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1267
                space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1268
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1269
lemma emeasure_bind_const':
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1270
  assumes "subprob_space M" "subprob_space N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1271
  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1272
using assms
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1273
proof (case_tac "X \<in> sets N")
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1274
  fix X assume "X \<in> sets N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1275
  thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1276
      by (subst emeasure_bind_const) 
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1277
         (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1)
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1278
next
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1279
  fix X assume "X \<notin> sets N"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset
  1280
  with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
9c66f7c541fb add Giry monad
hoelzl
parents:
diff changeset