src/HOL/Probability/Finite_Product_Measure.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 59425 c5e79df8cc21
child 60580 7e741e22d7fc
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
hoelzl@42146
     1
(*  Title:      HOL/Probability/Finite_Product_Measure.thy
hoelzl@42067
     2
    Author:     Johannes Hölzl, TU München
hoelzl@42067
     3
*)
hoelzl@42067
     4
wenzelm@58876
     5
section {*Finite product measures*}
hoelzl@42067
     6
hoelzl@42146
     7
theory Finite_Product_Measure
hoelzl@42146
     8
imports Binary_Product_Measure
hoelzl@35833
     9
begin
hoelzl@35833
    10
hoelzl@57447
    11
lemma PiE_choice: "(\<exists>f\<in>PiE I F. \<forall>i\<in>I. P i (f i)) \<longleftrightarrow> (\<forall>i\<in>I. \<exists>x\<in>F i. P i x)"
hoelzl@57447
    12
  by (auto simp: Bex_def PiE_iff Ball_def dest!: choice_iff'[THEN iffD1])
hoelzl@57447
    13
     (force intro: exI[of _ "restrict f I" for f])
hoelzl@57447
    14
hoelzl@47694
    15
lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
hoelzl@47694
    16
  by auto
hoelzl@47694
    17
hoelzl@56994
    18
subsubsection {* More about Function restricted by @{const extensional}  *}
immler@50038
    19
hoelzl@35833
    20
definition
hoelzl@49780
    21
  "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
hoelzl@40859
    22
hoelzl@40859
    23
lemma merge_apply[simp]:
hoelzl@49780
    24
  "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
hoelzl@49780
    25
  "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
hoelzl@49780
    26
  "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I J (x, y) i = x i"
hoelzl@49780
    27
  "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I J (x, y) i = y i"
hoelzl@49780
    28
  "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I J (x, y) i = undefined"
hoelzl@40859
    29
  unfolding merge_def by auto
hoelzl@40859
    30
hoelzl@40859
    31
lemma merge_commute:
hoelzl@49780
    32
  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) = merge J I (y, x)"
hoelzl@50003
    33
  by (force simp: merge_def)
hoelzl@40859
    34
hoelzl@40859
    35
lemma Pi_cancel_merge_range[simp]:
hoelzl@49780
    36
  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
hoelzl@49780
    37
  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
hoelzl@49780
    38
  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I J (A, B)) \<longleftrightarrow> x \<in> Pi I A"
hoelzl@49780
    39
  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J I (B, A)) \<longleftrightarrow> x \<in> Pi I A"
hoelzl@40859
    40
  by (auto simp: Pi_def)
hoelzl@40859
    41
hoelzl@40859
    42
lemma Pi_cancel_merge[simp]:
hoelzl@49780
    43
  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
hoelzl@49780
    44
  "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
hoelzl@49780
    45
  "I \<inter> J = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
hoelzl@49780
    46
  "J \<inter> I = {} \<Longrightarrow> merge I J (x, y) \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
hoelzl@40859
    47
  by (auto simp: Pi_def)
hoelzl@40859
    48
hoelzl@49780
    49
lemma extensional_merge[simp]: "merge I J (x, y) \<in> extensional (I \<union> J)"
hoelzl@40859
    50
  by (auto simp: extensional_def)
hoelzl@40859
    51
hoelzl@40859
    52
lemma restrict_merge[simp]:
hoelzl@49780
    53
  "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
hoelzl@49780
    54
  "I \<inter> J = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
hoelzl@49780
    55
  "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) I = restrict x I"
hoelzl@49780
    56
  "J \<inter> I = {} \<Longrightarrow> restrict (merge I J (x, y)) J = restrict y J"
hoelzl@47694
    57
  by (auto simp: restrict_def)
hoelzl@40859
    58
immler@50042
    59
lemma split_merge: "P (merge I J (x,y) i) \<longleftrightarrow> (i \<in> I \<longrightarrow> P (x i)) \<and> (i \<in> J - I \<longrightarrow> P (y i)) \<and> (i \<notin> I \<union> J \<longrightarrow> P undefined)"
immler@50042
    60
  unfolding merge_def by auto
immler@50042
    61
hoelzl@50123
    62
lemma PiE_cancel_merge[simp]:
hoelzl@50123
    63
  "I \<inter> J = {} \<Longrightarrow>
hoelzl@50123
    64
    merge I J (x, y) \<in> PiE (I \<union> J) B \<longleftrightarrow> x \<in> Pi I B \<and> y \<in> Pi J B"
hoelzl@50123
    65
  by (auto simp: PiE_def restrict_Pi_cancel)
hoelzl@50123
    66
hoelzl@50123
    67
lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I {i} (x,y) = restrict (x(i := y i)) (insert i I)"
hoelzl@50123
    68
  unfolding merge_def by (auto simp: fun_eq_iff)
hoelzl@50123
    69
immler@50042
    70
lemma extensional_merge_sub: "I \<union> J \<subseteq> K \<Longrightarrow> merge I J (x, y) \<in> extensional K"
immler@50042
    71
  unfolding merge_def extensional_def by auto
immler@50042
    72
hoelzl@50123
    73
lemma merge_restrict[simp]:
hoelzl@50123
    74
  "merge I J (restrict x I, y) = merge I J (x, y)"
hoelzl@50123
    75
  "merge I J (x, restrict y J) = merge I J (x, y)"
hoelzl@50123
    76
  unfolding merge_def by auto
hoelzl@50123
    77
hoelzl@50123
    78
lemma merge_x_x_eq_restrict[simp]:
hoelzl@50123
    79
  "merge I J (x, x) = restrict x (I \<union> J)"
hoelzl@50123
    80
  unfolding merge_def by auto
hoelzl@50123
    81
immler@50042
    82
lemma injective_vimage_restrict:
immler@50042
    83
  assumes J: "J \<subseteq> I"
wenzelm@53015
    84
  and sets: "A \<subseteq> (\<Pi>\<^sub>E i\<in>J. S i)" "B \<subseteq> (\<Pi>\<^sub>E i\<in>J. S i)" and ne: "(\<Pi>\<^sub>E i\<in>I. S i) \<noteq> {}"
wenzelm@53015
    85
  and eq: "(\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i) = (\<lambda>x. restrict x J) -` B \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
immler@50042
    86
  shows "A = B"
immler@50042
    87
proof  (intro set_eqI)
immler@50042
    88
  fix x
immler@50042
    89
  from ne obtain y where y: "\<And>i. i \<in> I \<Longrightarrow> y i \<in> S i" by auto
immler@50042
    90
  have "J \<inter> (I - J) = {}" by auto
immler@50042
    91
  show "x \<in> A \<longleftrightarrow> x \<in> B"
immler@50042
    92
  proof cases
wenzelm@53015
    93
    assume x: "x \<in> (\<Pi>\<^sub>E i\<in>J. S i)"
wenzelm@53015
    94
    have "x \<in> A \<longleftrightarrow> merge J (I - J) (x,y) \<in> (\<lambda>x. restrict x J) -` A \<inter> (\<Pi>\<^sub>E i\<in>I. S i)"
hoelzl@50123
    95
      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S]
hoelzl@50123
    96
      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1)
immler@50042
    97
    then show "x \<in> A \<longleftrightarrow> x \<in> B"
hoelzl@50123
    98
      using y x `J \<subseteq> I` PiE_cancel_merge[of "J" "I - J" x y S]
hoelzl@50123
    99
      by (auto simp del: PiE_cancel_merge simp add: Un_absorb1 eq)
hoelzl@50123
   100
  qed (insert sets, auto)
immler@50042
   101
qed
immler@50042
   102
hoelzl@41095
   103
lemma restrict_vimage:
hoelzl@50123
   104
  "I \<inter> J = {} \<Longrightarrow>
wenzelm@53015
   105
    (\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^sub>E I E \<times> Pi\<^sub>E J F) = Pi (I \<union> J) (merge I J (E, F))"
hoelzl@50123
   106
  by (auto simp: restrict_Pi_cancel PiE_def)
hoelzl@41095
   107
hoelzl@41095
   108
lemma merge_vimage:
wenzelm@53015
   109
  "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^sub>E (I \<union> J) E = Pi I E \<times> Pi J E"
hoelzl@50123
   110
  by (auto simp: restrict_Pi_cancel PiE_def)
hoelzl@50104
   111
hoelzl@56994
   112
subsection {* Finite product spaces *}
hoelzl@40859
   113
hoelzl@56994
   114
subsubsection {* Products *}
hoelzl@40859
   115
hoelzl@47694
   116
definition prod_emb where
hoelzl@47694
   117
  "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (PIE i:I. space (M i))"
hoelzl@47694
   118
hoelzl@47694
   119
lemma prod_emb_iff: 
hoelzl@47694
   120
  "f \<in> prod_emb I M K X \<longleftrightarrow> f \<in> extensional I \<and> (restrict f K \<in> X) \<and> (\<forall>i\<in>I. f i \<in> space (M i))"
hoelzl@50123
   121
  unfolding prod_emb_def PiE_def by auto
hoelzl@40859
   122
hoelzl@47694
   123
lemma
hoelzl@47694
   124
  shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
hoelzl@47694
   125
    and prod_emb_Un[simp]: "prod_emb M L K (A \<union> B) = prod_emb M L K A \<union> prod_emb M L K B"
hoelzl@47694
   126
    and prod_emb_Int: "prod_emb M L K (A \<inter> B) = prod_emb M L K A \<inter> prod_emb M L K B"
hoelzl@47694
   127
    and prod_emb_UN[simp]: "prod_emb M L K (\<Union>i\<in>I. F i) = (\<Union>i\<in>I. prod_emb M L K (F i))"
hoelzl@47694
   128
    and prod_emb_INT[simp]: "I \<noteq> {} \<Longrightarrow> prod_emb M L K (\<Inter>i\<in>I. F i) = (\<Inter>i\<in>I. prod_emb M L K (F i))"
hoelzl@47694
   129
    and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B"
hoelzl@47694
   130
  by (auto simp: prod_emb_def)
hoelzl@40859
   131
hoelzl@47694
   132
lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
wenzelm@53015
   133
    prod_emb I M J (\<Pi>\<^sub>E i\<in>J. E i) = (\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i))"
hoelzl@50123
   134
  by (force simp: prod_emb_def PiE_iff split_if_mem2)
hoelzl@47694
   135
hoelzl@50123
   136
lemma prod_emb_PiE_same_index[simp]:
wenzelm@53015
   137
    "(\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow> prod_emb I M I (Pi\<^sub>E I E) = Pi\<^sub>E I E"
hoelzl@50123
   138
  by (auto simp: prod_emb_def PiE_iff)
hoelzl@41689
   139
immler@50038
   140
lemma prod_emb_trans[simp]:
immler@50038
   141
  "J \<subseteq> K \<Longrightarrow> K \<subseteq> L \<Longrightarrow> prod_emb L M K (prod_emb K M J X) = prod_emb L M J X"
hoelzl@50123
   142
  by (auto simp add: Int_absorb1 prod_emb_def PiE_def)
immler@50038
   143
immler@50038
   144
lemma prod_emb_Pi:
immler@50038
   145
  assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
wenzelm@53015
   146
  shows "prod_emb K M J (Pi\<^sub>E J X) = (\<Pi>\<^sub>E i\<in>K. if i \<in> J then X i else space (M i))"
immler@50244
   147
  using assms sets.space_closed
hoelzl@50123
   148
  by (auto simp: prod_emb_def PiE_iff split: split_if_asm) blast+
immler@50038
   149
immler@50038
   150
lemma prod_emb_id:
wenzelm@53015
   151
  "B \<subseteq> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
hoelzl@50123
   152
  by (auto simp: prod_emb_def subset_eq extensional_restrict)
immler@50038
   153
immler@50041
   154
lemma prod_emb_mono:
immler@50041
   155
  "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
immler@50041
   156
  by (auto simp: prod_emb_def)
immler@50041
   157
hoelzl@47694
   158
definition PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
wenzelm@53015
   159
  "PiM I M = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i))
hoelzl@47694
   160
    {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}
wenzelm@53015
   161
    (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j))
hoelzl@47694
   162
    (\<lambda>(J, X). \<Prod>j\<in>J \<union> {i\<in>I. emeasure (M i) (space (M i)) \<noteq> 1}. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
hoelzl@47694
   163
hoelzl@47694
   164
definition prod_algebra :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) set set" where
wenzelm@53015
   165
  "prod_algebra I M = (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j)) `
hoelzl@47694
   166
    {(J, X). (J \<noteq> {} \<or> I = {}) \<and> finite J \<and> J \<subseteq> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"
hoelzl@47694
   167
hoelzl@47694
   168
abbreviation
wenzelm@53015
   169
  "Pi\<^sub>M I M \<equiv> PiM I M"
hoelzl@41689
   170
hoelzl@40859
   171
syntax
hoelzl@47694
   172
  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3PIM _:_./ _)" 10)
hoelzl@40859
   173
hoelzl@40859
   174
syntax (xsymbols)
wenzelm@53015
   175
  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>M _\<in>_./ _)"  10)
hoelzl@40859
   176
hoelzl@40859
   177
syntax (HTML output)
wenzelm@53015
   178
  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>M _\<in>_./ _)"  10)
hoelzl@40859
   179
hoelzl@40859
   180
translations
hoelzl@47694
   181
  "PIM x:I. M" == "CONST PiM I (%x. M)"
hoelzl@41689
   182
hoelzl@59425
   183
lemma extend_measure_cong:
hoelzl@59425
   184
  assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
hoelzl@59425
   185
  shows "extend_measure \<Omega> I G \<mu> = extend_measure \<Omega>' I' G' \<mu>'"
hoelzl@59425
   186
  unfolding extend_measure_def by (auto simp add: assms)
hoelzl@59425
   187
hoelzl@59425
   188
lemma Pi_cong_sets:
hoelzl@59425
   189
    "\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
hoelzl@59425
   190
  unfolding Pi_def by auto 
hoelzl@59425
   191
hoelzl@59425
   192
lemma PiM_cong:
hoelzl@59425
   193
  assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
hoelzl@59425
   194
  shows "PiM I M = PiM J N"
hoelzl@59425
   195
unfolding PiM_def
hoelzl@59425
   196
proof (rule extend_measure_cong)
hoelzl@59425
   197
  case goal1 show ?case using assms
hoelzl@59425
   198
    by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
hoelzl@59425
   199
next
hoelzl@59425
   200
  case goal2
hoelzl@59425
   201
  have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
hoelzl@59425
   202
    using assms by (intro Pi_cong_sets) auto
hoelzl@59425
   203
  thus ?case by (auto simp: assms)
hoelzl@59425
   204
next
hoelzl@59425
   205
  case goal3 show ?case using assms 
hoelzl@59425
   206
    by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
hoelzl@59425
   207
next
hoelzl@59425
   208
  case (goal4 x)
hoelzl@59425
   209
  thus ?case using assms 
hoelzl@59425
   210
    by (auto intro!: setprod.cong split: split_if_asm)
hoelzl@59425
   211
qed
hoelzl@59425
   212
hoelzl@59425
   213
hoelzl@47694
   214
lemma prod_algebra_sets_into_space:
wenzelm@53015
   215
  "prod_algebra I M \<subseteq> Pow (\<Pi>\<^sub>E i\<in>I. space (M i))"
immler@50245
   216
  by (auto simp: prod_emb_def prod_algebra_def)
hoelzl@40859
   217
hoelzl@47694
   218
lemma prod_algebra_eq_finite:
hoelzl@47694
   219
  assumes I: "finite I"
wenzelm@53015
   220
  shows "prod_algebra I M = {(\<Pi>\<^sub>E i\<in>I. X i) |X. X \<in> (\<Pi> j\<in>I. sets (M j))}" (is "?L = ?R")
hoelzl@47694
   221
proof (intro iffI set_eqI)
hoelzl@47694
   222
  fix A assume "A \<in> ?L"
hoelzl@47694
   223
  then obtain J E where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
hoelzl@47694
   224
    and A: "A = prod_emb I M J (PIE j:J. E j)"
hoelzl@47694
   225
    by (auto simp: prod_algebra_def)
wenzelm@53015
   226
  let ?A = "\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i)"
hoelzl@47694
   227
  have A: "A = ?A"
immler@50244
   228
    unfolding A using J by (intro prod_emb_PiE sets.sets_into_space) auto
immler@50244
   229
  show "A \<in> ?R" unfolding A using J sets.top
hoelzl@47694
   230
    by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
hoelzl@47694
   231
next
hoelzl@47694
   232
  fix A assume "A \<in> ?R"
wenzelm@53015
   233
  then obtain X where A: "A = (\<Pi>\<^sub>E i\<in>I. X i)" and X: "X \<in> (\<Pi> j\<in>I. sets (M j))" by auto
wenzelm@53015
   234
  then have A: "A = prod_emb I M I (\<Pi>\<^sub>E i\<in>I. X i)"
immler@50244
   235
    by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff)
hoelzl@47694
   236
  from X I show "A \<in> ?L" unfolding A
hoelzl@47694
   237
    by (auto simp: prod_algebra_def)
hoelzl@47694
   238
qed
hoelzl@41095
   239
hoelzl@47694
   240
lemma prod_algebraI:
hoelzl@47694
   241
  "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
hoelzl@47694
   242
    \<Longrightarrow> prod_emb I M J (PIE j:J. E j) \<in> prod_algebra I M"
hoelzl@50123
   243
  by (auto simp: prod_algebra_def)
hoelzl@41689
   244
immler@50038
   245
lemma prod_algebraI_finite:
wenzelm@53015
   246
  "finite I \<Longrightarrow> (\<forall>i\<in>I. E i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>E I E) \<in> prod_algebra I M"
immler@50244
   247
  using prod_algebraI[of I I E M] prod_emb_PiE_same_index[of I E M, OF sets.sets_into_space] by simp
immler@50038
   248
wenzelm@53015
   249
lemma Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
immler@50038
   250
proof (safe intro!: Int_stableI)
immler@50038
   251
  fix E F assume "\<forall>i\<in>I. E i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
wenzelm@53015
   252
  then show "\<exists>G. Pi\<^sub>E J E \<inter> Pi\<^sub>E J F = Pi\<^sub>E J G \<and> (\<forall>i\<in>I. G i \<in> sets (M i))"
hoelzl@50123
   253
    by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int)
immler@50038
   254
qed
immler@50038
   255
hoelzl@47694
   256
lemma prod_algebraE:
hoelzl@47694
   257
  assumes A: "A \<in> prod_algebra I M"
hoelzl@47694
   258
  obtains J E where "A = prod_emb I M J (PIE j:J. E j)"
hoelzl@47694
   259
    "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)" 
hoelzl@47694
   260
  using A by (auto simp: prod_algebra_def)
hoelzl@42988
   261
hoelzl@47694
   262
lemma prod_algebraE_all:
hoelzl@47694
   263
  assumes A: "A \<in> prod_algebra I M"
wenzelm@53015
   264
  obtains E where "A = Pi\<^sub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
hoelzl@47694
   265
proof -
wenzelm@53015
   266
  from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)"
hoelzl@47694
   267
    and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
hoelzl@47694
   268
    by (auto simp: prod_algebra_def)
hoelzl@47694
   269
  from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)"
immler@50244
   270
    using sets.sets_into_space by auto
wenzelm@53015
   271
  then have "A = (\<Pi>\<^sub>E i\<in>I. if i\<in>J then E i else space (M i))"
hoelzl@47694
   272
    using A J by (auto simp: prod_emb_PiE)
wenzelm@53374
   273
  moreover have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
immler@50244
   274
    using sets.top E by auto
hoelzl@47694
   275
  ultimately show ?thesis using that by auto
hoelzl@47694
   276
qed
hoelzl@40859
   277
hoelzl@47694
   278
lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
hoelzl@47694
   279
proof (unfold Int_stable_def, safe)
hoelzl@47694
   280
  fix A assume "A \<in> prod_algebra I M"
hoelzl@47694
   281
  from prod_algebraE[OF this] guess J E . note A = this
hoelzl@47694
   282
  fix B assume "B \<in> prod_algebra I M"
hoelzl@47694
   283
  from prod_algebraE[OF this] guess K F . note B = this
wenzelm@53015
   284
  have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^sub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter> 
hoelzl@47694
   285
      (if i \<in> K then F i else space (M i)))"
immler@50244
   286
    unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
immler@50244
   287
      B(5)[THEN sets.sets_into_space]
hoelzl@47694
   288
    apply (subst (1 2 3) prod_emb_PiE)
hoelzl@47694
   289
    apply (simp_all add: subset_eq PiE_Int)
hoelzl@47694
   290
    apply blast
hoelzl@47694
   291
    apply (intro PiE_cong)
hoelzl@47694
   292
    apply auto
hoelzl@47694
   293
    done
hoelzl@47694
   294
  also have "\<dots> \<in> prod_algebra I M"
hoelzl@47694
   295
    using A B by (auto intro!: prod_algebraI)
hoelzl@47694
   296
  finally show "A \<inter> B \<in> prod_algebra I M" .
hoelzl@47694
   297
qed
hoelzl@47694
   298
hoelzl@47694
   299
lemma prod_algebra_mono:
hoelzl@47694
   300
  assumes space: "\<And>i. i \<in> I \<Longrightarrow> space (E i) = space (F i)"
hoelzl@47694
   301
  assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (E i) \<subseteq> sets (F i)"
hoelzl@47694
   302
  shows "prod_algebra I E \<subseteq> prod_algebra I F"
hoelzl@47694
   303
proof
hoelzl@47694
   304
  fix A assume "A \<in> prod_algebra I E"
hoelzl@47694
   305
  then obtain J G where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I"
wenzelm@53015
   306
    and A: "A = prod_emb I E J (\<Pi>\<^sub>E i\<in>J. G i)"
hoelzl@47694
   307
    and G: "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (E i)"
hoelzl@47694
   308
    by (auto simp: prod_algebra_def)
hoelzl@47694
   309
  moreover
wenzelm@53015
   310
  from space have "(\<Pi>\<^sub>E i\<in>I. space (E i)) = (\<Pi>\<^sub>E i\<in>I. space (F i))"
hoelzl@47694
   311
    by (rule PiE_cong)
wenzelm@53015
   312
  with A have "A = prod_emb I F J (\<Pi>\<^sub>E i\<in>J. G i)"
hoelzl@47694
   313
    by (simp add: prod_emb_def)
hoelzl@47694
   314
  moreover
hoelzl@47694
   315
  from sets G J have "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (F i)"
hoelzl@47694
   316
    by auto
hoelzl@47694
   317
  ultimately show "A \<in> prod_algebra I F"
hoelzl@47694
   318
    apply (simp add: prod_algebra_def image_iff)
hoelzl@47694
   319
    apply (intro exI[of _ J] exI[of _ G] conjI)
hoelzl@47694
   320
    apply auto
hoelzl@47694
   321
    done
hoelzl@41689
   322
qed
hoelzl@41689
   323
hoelzl@50104
   324
lemma prod_algebra_cong:
hoelzl@50104
   325
  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
hoelzl@50104
   326
  shows "prod_algebra I M = prod_algebra J N"
hoelzl@50104
   327
proof -
hoelzl@50104
   328
  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
hoelzl@50104
   329
    using sets_eq_imp_space_eq[OF sets] by auto
hoelzl@50104
   330
  with sets show ?thesis unfolding `I = J`
hoelzl@50104
   331
    by (intro antisym prod_algebra_mono) auto
hoelzl@50104
   332
qed
hoelzl@50104
   333
hoelzl@50104
   334
lemma space_in_prod_algebra:
wenzelm@53015
   335
  "(\<Pi>\<^sub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
hoelzl@50104
   336
proof cases
hoelzl@50104
   337
  assume "I = {}" then show ?thesis
hoelzl@50104
   338
    by (auto simp add: prod_algebra_def image_iff prod_emb_def)
hoelzl@50104
   339
next
hoelzl@50104
   340
  assume "I \<noteq> {}"
hoelzl@50104
   341
  then obtain i where "i \<in> I" by auto
wenzelm@53015
   342
  then have "(\<Pi>\<^sub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
hoelzl@50123
   343
    by (auto simp: prod_emb_def)
hoelzl@50104
   344
  also have "\<dots> \<in> prod_algebra I M"
hoelzl@50104
   345
    using `i \<in> I` by (intro prod_algebraI) auto
hoelzl@50104
   346
  finally show ?thesis .
hoelzl@50104
   347
qed
hoelzl@50104
   348
wenzelm@53015
   349
lemma space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@47694
   350
  using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
hoelzl@47694
   351
wenzelm@53015
   352
lemma sets_PiM: "sets (\<Pi>\<^sub>M i\<in>I. M i) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) (prod_algebra I M)"
hoelzl@47694
   353
  using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp
hoelzl@41689
   354
hoelzl@47694
   355
lemma sets_PiM_single: "sets (PiM I M) =
wenzelm@53015
   356
    sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {{f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> sets (M i)}"
hoelzl@47694
   357
    (is "_ = sigma_sets ?\<Omega> ?R")
hoelzl@47694
   358
  unfolding sets_PiM
hoelzl@47694
   359
proof (rule sigma_sets_eqI)
hoelzl@47694
   360
  interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto
hoelzl@47694
   361
  fix A assume "A \<in> prod_algebra I M"
hoelzl@47694
   362
  from prod_algebraE[OF this] guess J X . note X = this
hoelzl@47694
   363
  show "A \<in> sigma_sets ?\<Omega> ?R"
hoelzl@47694
   364
  proof cases
hoelzl@47694
   365
    assume "I = {}"
hoelzl@47694
   366
    with X have "A = {\<lambda>x. undefined}" by (auto simp: prod_emb_def)
hoelzl@47694
   367
    with `I = {}` show ?thesis by (auto intro!: sigma_sets_top)
hoelzl@47694
   368
  next
hoelzl@47694
   369
    assume "I \<noteq> {}"
wenzelm@53015
   370
    with X have "A = (\<Inter>j\<in>J. {f\<in>(\<Pi>\<^sub>E i\<in>I. space (M i)). f j \<in> X j})"
hoelzl@50123
   371
      by (auto simp: prod_emb_def)
hoelzl@47694
   372
    also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
hoelzl@47694
   373
      using X `I \<noteq> {}` by (intro R.finite_INT sigma_sets.Basic) auto
hoelzl@47694
   374
    finally show "A \<in> sigma_sets ?\<Omega> ?R" .
hoelzl@47694
   375
  qed
hoelzl@47694
   376
next
hoelzl@47694
   377
  fix A assume "A \<in> ?R"
wenzelm@53015
   378
  then obtain i B where A: "A = {f\<in>\<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> B}" "i \<in> I" "B \<in> sets (M i)" 
hoelzl@47694
   379
    by auto
wenzelm@53015
   380
  then have "A = prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. B)"
hoelzl@50123
   381
     by (auto simp: prod_emb_def)
hoelzl@47694
   382
  also have "\<dots> \<in> sigma_sets ?\<Omega> (prod_algebra I M)"
hoelzl@47694
   383
    using A by (intro sigma_sets.Basic prod_algebraI) auto
hoelzl@47694
   384
  finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
hoelzl@47694
   385
qed
hoelzl@47694
   386
hoelzl@58606
   387
lemma sets_PiM_eq_proj:
hoelzl@58606
   388
  "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
hoelzl@58606
   389
  apply (simp add: sets_PiM_single sets_Sup_sigma)
hoelzl@58606
   390
  apply (subst SUP_cong[OF refl])
hoelzl@58606
   391
  apply (rule sets_vimage_algebra2)
hoelzl@58606
   392
  apply auto []
hoelzl@58606
   393
  apply (auto intro!: arg_cong2[where f=sigma_sets])
hoelzl@58606
   394
  done
hoelzl@58606
   395
hoelzl@59088
   396
lemma
hoelzl@59088
   397
  shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
hoelzl@59088
   398
    and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
hoelzl@59088
   399
  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
hoelzl@59088
   400
hoelzl@59088
   401
lemma sets_PiM_sigma:
hoelzl@59088
   402
  assumes \<Omega>_cover: "\<And>i. i \<in> I \<Longrightarrow> \<exists>S\<subseteq>E i. countable S \<and> \<Omega> i = \<Union>S"
hoelzl@59088
   403
  assumes E: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (\<Omega> i)"
hoelzl@59088
   404
  assumes J: "\<And>j. j \<in> J \<Longrightarrow> finite j" "\<Union>J = I"
hoelzl@59088
   405
  defines "P \<equiv> {{f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i} | A j. j \<in> J \<and> A \<in> Pi j E}"
hoelzl@59088
   406
  shows "sets (\<Pi>\<^sub>M i\<in>I. sigma (\<Omega> i) (E i)) = sets (sigma (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P)"
hoelzl@59088
   407
proof cases
hoelzl@59088
   408
  assume "I = {}" 
hoelzl@59088
   409
  with `\<Union>J = I` have "P = {{\<lambda>_. undefined}} \<or> P = {}"
hoelzl@59088
   410
    by (auto simp: P_def)
hoelzl@59088
   411
  with `I = {}` show ?thesis
hoelzl@59088
   412
    by (auto simp add: sets_PiM_empty sigma_sets_empty_eq)
hoelzl@59088
   413
next
hoelzl@59088
   414
  let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
hoelzl@59088
   415
  assume "I \<noteq> {}"
hoelzl@59088
   416
  then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) = 
hoelzl@59088
   417
      sets (\<Squnion>\<^sub>\<sigma> i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
hoelzl@59088
   418
    by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
hoelzl@59088
   419
  also have "\<dots> = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
hoelzl@59088
   420
    using E by (intro SUP_sigma_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
hoelzl@59088
   421
  also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
hoelzl@59088
   422
    using `I \<noteq> {}` by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
hoelzl@59088
   423
  also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) P)"
hoelzl@59088
   424
  proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
hoelzl@59088
   425
    show "(\<Union>i\<in>I. ?F i) \<subseteq> Pow (Pi\<^sub>E I \<Omega>)" "P \<subseteq> Pow (Pi\<^sub>E I \<Omega>)"
hoelzl@59088
   426
      by (auto simp: P_def)
hoelzl@59088
   427
  next
hoelzl@59088
   428
    interpret P: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
hoelzl@59088
   429
      by (auto intro!: sigma_algebra_sigma_sets simp: P_def)
hoelzl@59088
   430
hoelzl@59088
   431
    fix Z assume "Z \<in> (\<Union>i\<in>I. ?F i)"
hoelzl@59088
   432
    then obtain i A where i: "i \<in> I" "A \<in> E i" and Z_def: "Z = (\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega>"
hoelzl@59088
   433
      by auto
hoelzl@59088
   434
    from `i \<in> I` J obtain j where j: "i \<in> j" "j \<in> J" "j \<subseteq> I" "finite j"
hoelzl@59088
   435
      by auto
hoelzl@59088
   436
    obtain S where S: "\<And>i. i \<in> j \<Longrightarrow> S i \<subseteq> E i" "\<And>i. i \<in> j \<Longrightarrow> countable (S i)"
hoelzl@59088
   437
      "\<And>i. i \<in> j \<Longrightarrow> \<Omega> i = \<Union>(S i)"
hoelzl@59088
   438
      by (metis subset_eq \<Omega>_cover `j \<subseteq> I`)
hoelzl@59088
   439
    def A' \<equiv> "\<lambda>n. n(i := A)"
hoelzl@59088
   440
    then have A'_i: "\<And>n. A' n i = A"
hoelzl@59088
   441
      by simp
hoelzl@59088
   442
    { fix n assume "n \<in> Pi\<^sub>E (j - {i}) S"
hoelzl@59088
   443
      then have "A' n \<in> Pi j E"
hoelzl@59088
   444
        unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def `A \<in> E i` )
hoelzl@59088
   445
      with `j \<in> J` have "{f \<in> Pi\<^sub>E I \<Omega>. \<forall>i\<in>j. f i \<in> A' n i} \<in> P"
hoelzl@59088
   446
        by (auto simp: P_def) }
hoelzl@59088
   447
    note A'_in_P = this
hoelzl@59088
   448
hoelzl@59088
   449
    { fix x assume "x i \<in> A" "x \<in> Pi\<^sub>E I \<Omega>"
hoelzl@59088
   450
      with S(3) `j \<subseteq> I` have "\<forall>i\<in>j. \<exists>s\<in>S i. x i \<in> s"
hoelzl@59088
   451
        by (auto simp: PiE_def Pi_def)
hoelzl@59088
   452
      then obtain s where s: "\<And>i. i \<in> j \<Longrightarrow> s i \<in> S i" "\<And>i. i \<in> j \<Longrightarrow> x i \<in> s i"
hoelzl@59088
   453
        by metis
hoelzl@59088
   454
      with `x i \<in> A` have "\<exists>n\<in>PiE (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
hoelzl@59088
   455
        by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
hoelzl@59088
   456
    then have "Z = (\<Union>n\<in>PiE (j-{i}) S. {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A' n i})"
hoelzl@59088
   457
      unfolding Z_def
hoelzl@59088
   458
      by (auto simp add: set_eq_iff ball_conj_distrib `i\<in>j` A'_i dest: bspec[OF _ `i\<in>j`]
hoelzl@59088
   459
               cong: conj_cong)
hoelzl@59088
   460
    also have "\<dots> \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
hoelzl@59088
   461
      using `finite j` S(2)
hoelzl@59088
   462
      by (intro P.countable_UN' countable_PiE) (simp_all add: image_subset_iff A'_in_P)
hoelzl@59088
   463
    finally show "Z \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P" .
hoelzl@59088
   464
  next
hoelzl@59088
   465
    interpret F: sigma_algebra "\<Pi>\<^sub>E i\<in>I. \<Omega> i" "sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<Union>i\<in>I. ?F i)"
hoelzl@59088
   466
      by (auto intro!: sigma_algebra_sigma_sets)
hoelzl@59088
   467
hoelzl@59088
   468
    fix b assume "b \<in> P"
hoelzl@59088
   469
    then obtain A j where b: "b = {f\<in>(\<Pi>\<^sub>E i\<in>I. \<Omega> i). \<forall>i\<in>j. f i \<in> A i}" "j \<in> J" "A \<in> Pi j E"
hoelzl@59088
   470
      by (auto simp: P_def)
hoelzl@59088
   471
    show "b \<in> sigma_sets (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i)"
hoelzl@59088
   472
    proof cases
hoelzl@59088
   473
      assume "j = {}"
hoelzl@59088
   474
      with b have "b = (\<Pi>\<^sub>E i\<in>I. \<Omega> i)"
hoelzl@59088
   475
        by auto
hoelzl@59088
   476
      then show ?thesis
hoelzl@59088
   477
        by blast
hoelzl@59088
   478
    next
hoelzl@59088
   479
      assume "j \<noteq> {}"
hoelzl@59088
   480
      with J b(2,3) have eq: "b = (\<Inter>i\<in>j. ((\<lambda>x. x i) -` A i \<inter> Pi\<^sub>E I \<Omega>))"
hoelzl@59088
   481
        unfolding b(1)
hoelzl@59088
   482
        by (auto simp: PiE_def Pi_def)
hoelzl@59088
   483
      show ?thesis
hoelzl@59088
   484
        unfolding eq using `A \<in> Pi j E` `j \<in> J` J(2)
hoelzl@59088
   485
        by (intro F.finite_INT J `j \<in> J` `j \<noteq> {}` sigma_sets.Basic) blast
hoelzl@59088
   486
    qed
hoelzl@59088
   487
  qed
hoelzl@59088
   488
  finally show "?thesis" .
hoelzl@59088
   489
qed
hoelzl@59088
   490
hoelzl@58606
   491
lemma sets_PiM_in_sets:
hoelzl@58606
   492
  assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@58606
   493
  assumes sets: "\<And>i A. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {x\<in>space N. x i \<in> A} \<in> sets N"
hoelzl@58606
   494
  shows "sets (\<Pi>\<^sub>M i \<in> I. M i) \<subseteq> sets N"
hoelzl@58606
   495
  unfolding sets_PiM_single space[symmetric]
hoelzl@58606
   496
  by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
hoelzl@58606
   497
hoelzl@59048
   498
lemma sets_PiM_cong[measurable_cong]:
hoelzl@59048
   499
  assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
hoelzl@58606
   500
  using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
hoelzl@58606
   501
hoelzl@47694
   502
lemma sets_PiM_I:
hoelzl@47694
   503
  assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
hoelzl@47694
   504
  shows "prod_emb I M J (PIE j:J. E j) \<in> sets (PIM i:I. M i)"
hoelzl@47694
   505
proof cases
hoelzl@47694
   506
  assume "J = {}"
hoelzl@47694
   507
  then have "prod_emb I M J (PIE j:J. E j) = (PIE j:I. space (M j))"
hoelzl@47694
   508
    by (auto simp: prod_emb_def)
hoelzl@47694
   509
  then show ?thesis
hoelzl@47694
   510
    by (auto simp add: sets_PiM intro!: sigma_sets_top)
hoelzl@47694
   511
next
hoelzl@47694
   512
  assume "J \<noteq> {}" with assms show ?thesis
hoelzl@50003
   513
    by (force simp add: sets_PiM prod_algebra_def)
hoelzl@40859
   514
qed
hoelzl@40859
   515
hoelzl@47694
   516
lemma measurable_PiM:
wenzelm@53015
   517
  assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@47694
   518
  assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow>
wenzelm@53015
   519
    f -` prod_emb I M J (Pi\<^sub>E J X) \<inter> space N \<in> sets N" 
hoelzl@47694
   520
  shows "f \<in> measurable N (PiM I M)"
hoelzl@47694
   521
  using sets_PiM prod_algebra_sets_into_space space
hoelzl@47694
   522
proof (rule measurable_sigma_sets)
hoelzl@47694
   523
  fix A assume "A \<in> prod_algebra I M"
hoelzl@47694
   524
  from prod_algebraE[OF this] guess J X .
hoelzl@47694
   525
  with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto
hoelzl@47694
   526
qed
hoelzl@47694
   527
hoelzl@47694
   528
lemma measurable_PiM_Collect:
wenzelm@53015
   529
  assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@47694
   530
  assumes sets: "\<And>X J. J \<noteq> {} \<or> I = {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)) \<Longrightarrow>
hoelzl@47694
   531
    {\<omega>\<in>space N. \<forall>i\<in>J. f \<omega> i \<in> X i} \<in> sets N" 
hoelzl@47694
   532
  shows "f \<in> measurable N (PiM I M)"
hoelzl@47694
   533
  using sets_PiM prod_algebra_sets_into_space space
hoelzl@47694
   534
proof (rule measurable_sigma_sets)
hoelzl@47694
   535
  fix A assume "A \<in> prod_algebra I M"
hoelzl@47694
   536
  from prod_algebraE[OF this] guess J X . note X = this
hoelzl@50123
   537
  then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
hoelzl@50123
   538
    using space by (auto simp: prod_emb_def del: PiE_I)
hoelzl@47694
   539
  also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
hoelzl@47694
   540
  finally show "f -` A \<inter> space N \<in> sets N" .
hoelzl@41689
   541
qed
hoelzl@41095
   542
hoelzl@47694
   543
lemma measurable_PiM_single:
wenzelm@53015
   544
  assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@47694
   545
  assumes sets: "\<And>A i. i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> {\<omega> \<in> space N. f \<omega> i \<in> A} \<in> sets N" 
hoelzl@47694
   546
  shows "f \<in> measurable N (PiM I M)"
hoelzl@47694
   547
  using sets_PiM_single
hoelzl@47694
   548
proof (rule measurable_sigma_sets)
wenzelm@53015
   549
  fix A assume "A \<in> {{f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> sets (M i)}"
wenzelm@53015
   550
  then obtain B i where "A = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> B}" and B: "i \<in> I" "B \<in> sets (M i)"
hoelzl@47694
   551
    by auto
hoelzl@47694
   552
  with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto
hoelzl@47694
   553
  also have "\<dots> \<in> sets N" using B by (rule sets)
hoelzl@47694
   554
  finally show "f -` A \<inter> space N \<in> sets N" .
hoelzl@47694
   555
qed (auto simp: space)
hoelzl@40859
   556
hoelzl@50099
   557
lemma measurable_PiM_single':
hoelzl@50099
   558
  assumes f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable N (M i)"
wenzelm@53015
   559
    and "(\<lambda>\<omega> i. f i \<omega>) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
wenzelm@53015
   560
  shows "(\<lambda>\<omega> i. f i \<omega>) \<in> measurable N (Pi\<^sub>M I M)"
hoelzl@50099
   561
proof (rule measurable_PiM_single)
hoelzl@50099
   562
  fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
hoelzl@50099
   563
  then have "{\<omega> \<in> space N. f i \<omega> \<in> A} = f i -` A \<inter> space N"
hoelzl@50099
   564
    by auto
hoelzl@50099
   565
  then show "{\<omega> \<in> space N. f i \<omega> \<in> A} \<in> sets N"
hoelzl@50099
   566
    using A f by (auto intro!: measurable_sets)
hoelzl@50099
   567
qed fact
hoelzl@50099
   568
hoelzl@50003
   569
lemma sets_PiM_I_finite[measurable]:
hoelzl@47694
   570
  assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
hoelzl@47694
   571
  shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
immler@50244
   572
  using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] `finite I` sets by auto
hoelzl@47694
   573
hoelzl@59353
   574
lemma measurable_component_singleton[measurable (raw)]:
wenzelm@53015
   575
  assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^sub>M I M) (M i)"
hoelzl@41689
   576
proof (unfold measurable_def, intro CollectI conjI ballI)
hoelzl@41689
   577
  fix A assume "A \<in> sets (M i)"
wenzelm@53015
   578
  then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) = prod_emb I M {i} (\<Pi>\<^sub>E j\<in>{i}. A)"
immler@50244
   579
    using sets.sets_into_space `i \<in> I`
hoelzl@47694
   580
    by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: split_if_asm)
wenzelm@53015
   581
  then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) \<in> sets (Pi\<^sub>M I M)"
hoelzl@47694
   582
    using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
hoelzl@47694
   583
qed (insert `i \<in> I`, auto simp: space_PiM)
hoelzl@47694
   584
hoelzl@59353
   585
lemma measurable_component_singleton'[measurable_dest]:
wenzelm@53015
   586
  assumes f: "f \<in> measurable N (Pi\<^sub>M I M)"
hoelzl@59353
   587
  assumes g: "g \<in> measurable L N"
hoelzl@50021
   588
  assumes i: "i \<in> I"
hoelzl@59353
   589
  shows "(\<lambda>x. (f (g x)) i) \<in> measurable L (M i)"
hoelzl@59353
   590
  using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] .
hoelzl@50021
   591
hoelzl@59353
   592
lemma measurable_PiM_component_rev:
hoelzl@50099
   593
  "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
hoelzl@50099
   594
  by simp
hoelzl@50099
   595
blanchet@55415
   596
lemma measurable_case_nat[measurable (raw)]:
hoelzl@50021
   597
  assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
hoelzl@50021
   598
    "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
blanchet@55415
   599
  shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N"
hoelzl@50021
   600
  by (cases i) simp_all
hoelzl@59048
   601
 
blanchet@55415
   602
lemma measurable_case_nat'[measurable (raw)]:
wenzelm@53015
   603
  assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
blanchet@55415
   604
  shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
hoelzl@50099
   605
  using fg[THEN measurable_space]
hoelzl@50123
   606
  by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
hoelzl@50099
   607
hoelzl@50003
   608
lemma measurable_add_dim[measurable]:
wenzelm@53015
   609
  "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M)"
hoelzl@47694
   610
    (is "?f \<in> measurable ?P ?I")
hoelzl@47694
   611
proof (rule measurable_PiM_single)
hoelzl@47694
   612
  fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
hoelzl@47694
   613
  have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} =
wenzelm@53015
   614
    (if j = i then space (Pi\<^sub>M I M) \<times> A else ((\<lambda>x. x j) \<circ> fst) -` A \<inter> space ?P)"
immler@50244
   615
    using sets.sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
hoelzl@47694
   616
  also have "\<dots> \<in> sets ?P"
hoelzl@47694
   617
    using A j
hoelzl@47694
   618
    by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
blanchet@55414
   619
  finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
hoelzl@50123
   620
qed (auto simp: space_pair_measure space_PiM PiE_def)
hoelzl@41661
   621
hoelzl@50003
   622
lemma measurable_component_update:
wenzelm@53015
   623
  "x \<in> space (Pi\<^sub>M I M) \<Longrightarrow> i \<notin> I \<Longrightarrow> (\<lambda>v. x(i := v)) \<in> measurable (M i) (Pi\<^sub>M (insert i I) M)"
hoelzl@50003
   624
  by simp
hoelzl@50003
   625
hoelzl@50003
   626
lemma measurable_merge[measurable]:
wenzelm@53015
   627
  "merge I J \<in> measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M)"
hoelzl@47694
   628
    (is "?f \<in> measurable ?P ?U")
hoelzl@47694
   629
proof (rule measurable_PiM_single)
hoelzl@47694
   630
  fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
hoelzl@49780
   631
  then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} =
hoelzl@47694
   632
    (if i \<in> I then ((\<lambda>x. x i) \<circ> fst) -` A \<inter> space ?P else ((\<lambda>x. x i) \<circ> snd) -` A \<inter> space ?P)"
hoelzl@49776
   633
    by (auto simp: merge_def)
hoelzl@47694
   634
  also have "\<dots> \<in> sets ?P"
hoelzl@47694
   635
    using A
hoelzl@47694
   636
    by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
hoelzl@49780
   637
  finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
hoelzl@50123
   638
qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def)
hoelzl@42988
   639
hoelzl@50003
   640
lemma measurable_restrict[measurable (raw)]:
hoelzl@47694
   641
  assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
wenzelm@53015
   642
  shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^sub>M I M)"
hoelzl@47694
   643
proof (rule measurable_PiM_single)
hoelzl@47694
   644
  fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
hoelzl@47694
   645
  then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N"
hoelzl@47694
   646
    by auto
hoelzl@47694
   647
  then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
hoelzl@47694
   648
    using A X by (auto intro!: measurable_sets)
hoelzl@50123
   649
qed (insert X, auto simp add: PiE_def dest: measurable_space)
hoelzl@47694
   650
hoelzl@57025
   651
lemma measurable_abs_UNIV: 
hoelzl@57025
   652
  "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)"
hoelzl@57025
   653
  by (intro measurable_PiM_single) (auto dest: measurable_space)
hoelzl@57025
   654
wenzelm@53015
   655
lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
immler@50038
   656
  by (intro measurable_restrict measurable_component_singleton) auto
immler@50038
   657
hoelzl@59425
   658
lemma measurable_restrict_subset':
hoelzl@59425
   659
  assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
hoelzl@59425
   660
  shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
hoelzl@59425
   661
proof-
hoelzl@59425
   662
  from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
hoelzl@59425
   663
    by (rule measurable_restrict_subset)
hoelzl@59425
   664
  also from assms(2) have "measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M) = measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
hoelzl@59425
   665
    by (intro sets_PiM_cong measurable_cong_sets) simp_all
hoelzl@59425
   666
  finally show ?thesis .
hoelzl@59425
   667
qed
hoelzl@59425
   668
immler@50038
   669
lemma measurable_prod_emb[intro, simp]:
wenzelm@53015
   670
  "J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)"
immler@50038
   671
  unfolding prod_emb_def space_PiM[symmetric]
immler@50038
   672
  by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
immler@50038
   673
hoelzl@50003
   674
lemma sets_in_Pi_aux:
hoelzl@50003
   675
  "finite I \<Longrightarrow> (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
hoelzl@50003
   676
  {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
hoelzl@50003
   677
  by (simp add: subset_eq Pi_iff)
hoelzl@50003
   678
hoelzl@50003
   679
lemma sets_in_Pi[measurable (raw)]:
hoelzl@50003
   680
  "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
hoelzl@50003
   681
  (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
hoelzl@50387
   682
  Measurable.pred N (\<lambda>x. f x \<in> Pi I F)"
hoelzl@50003
   683
  unfolding pred_def
hoelzl@50003
   684
  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
hoelzl@50003
   685
hoelzl@50003
   686
lemma sets_in_extensional_aux:
hoelzl@50003
   687
  "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
hoelzl@50003
   688
proof -
hoelzl@50003
   689
  have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
hoelzl@50003
   690
    by (auto simp add: extensional_def space_PiM)
hoelzl@50003
   691
  then show ?thesis by simp
hoelzl@50003
   692
qed
hoelzl@50003
   693
hoelzl@50003
   694
lemma sets_in_extensional[measurable (raw)]:
hoelzl@50387
   695
  "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
hoelzl@50003
   696
  unfolding pred_def
hoelzl@50003
   697
  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
hoelzl@50003
   698
hoelzl@47694
   699
locale product_sigma_finite =
hoelzl@47694
   700
  fixes M :: "'i \<Rightarrow> 'a measure"
hoelzl@41689
   701
  assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
hoelzl@40859
   702
hoelzl@41689
   703
sublocale product_sigma_finite \<subseteq> M: sigma_finite_measure "M i" for i
hoelzl@40859
   704
  by (rule sigma_finite_measures)
hoelzl@40859
   705
hoelzl@47694
   706
locale finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
hoelzl@47694
   707
  fixes I :: "'i set"
hoelzl@47694
   708
  assumes finite_index: "finite I"
hoelzl@41689
   709
hoelzl@40859
   710
lemma (in finite_product_sigma_finite) sigma_finite_pairs:
hoelzl@40859
   711
  "\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
hoelzl@40859
   712
    (\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
wenzelm@53015
   713
    (\<forall>k. \<forall>i\<in>I. emeasure (M i) (F i k) \<noteq> \<infinity>) \<and> incseq (\<lambda>k. \<Pi>\<^sub>E i\<in>I. F i k) \<and>
wenzelm@53015
   714
    (\<Union>k. \<Pi>\<^sub>E i\<in>I. F i k) = space (PiM I M)"
hoelzl@40859
   715
proof -
hoelzl@47694
   716
  have "\<forall>i::'i. \<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (M i) \<and> incseq F \<and> (\<Union>i. F i) = space (M i) \<and> (\<forall>k. emeasure (M i) (F k) \<noteq> \<infinity>)"
hoelzl@47694
   717
    using M.sigma_finite_incseq by metis
hoelzl@40859
   718
  from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
hoelzl@47694
   719
  then have F: "\<And>i. range (F i) \<subseteq> sets (M i)" "\<And>i. incseq (F i)" "\<And>i. (\<Union>j. F i j) = space (M i)" "\<And>i k. emeasure (M i) (F i k) \<noteq> \<infinity>"
hoelzl@40859
   720
    by auto
wenzelm@53015
   721
  let ?F = "\<lambda>k. \<Pi>\<^sub>E i\<in>I. F i k"
hoelzl@47694
   722
  note space_PiM[simp]
hoelzl@40859
   723
  show ?thesis
hoelzl@41981
   724
  proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
hoelzl@40859
   725
    fix i show "range (F i) \<subseteq> sets (M i)" by fact
hoelzl@40859
   726
  next
hoelzl@47694
   727
    fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
hoelzl@40859
   728
  next
hoelzl@50123
   729
    fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
immler@50244
   730
      by (auto simp: PiE_def dest!: sets.sets_into_space)
hoelzl@40859
   731
  next
hoelzl@47694
   732
    fix f assume "f \<in> space (PiM I M)"
hoelzl@41981
   733
    with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
hoelzl@50123
   734
    show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def PiE_def)
hoelzl@40859
   735
  next
hoelzl@40859
   736
    fix i show "?F i \<subseteq> ?F (Suc i)"
hoelzl@41981
   737
      using `\<And>i. incseq (F i)`[THEN incseq_SucD] by auto
hoelzl@40859
   738
  qed
hoelzl@40859
   739
qed
hoelzl@40859
   740
hoelzl@49780
   741
lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
hoelzl@49780
   742
proof -
hoelzl@49780
   743
  let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ereal)"
wenzelm@53015
   744
  have "emeasure (Pi\<^sub>M {} M) (prod_emb {} M {} (\<Pi>\<^sub>E i\<in>{}. {})) = 1"
hoelzl@49780
   745
  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
hoelzl@49780
   746
    show "positive (PiM {} M) ?\<mu>"
hoelzl@49780
   747
      by (auto simp: positive_def)
hoelzl@49780
   748
    show "countably_additive (PiM {} M) ?\<mu>"
immler@50244
   749
      by (rule sets.countably_additiveI_finite)
hoelzl@49780
   750
         (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
hoelzl@49780
   751
  qed (auto simp: prod_emb_def)
wenzelm@53015
   752
  also have "(prod_emb {} M {} (\<Pi>\<^sub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
hoelzl@49780
   753
    by (auto simp: prod_emb_def)
hoelzl@49780
   754
  finally show ?thesis
hoelzl@49780
   755
    by simp
hoelzl@49780
   756
qed
hoelzl@49780
   757
hoelzl@49780
   758
lemma PiM_empty: "PiM {} M = count_space {\<lambda>_. undefined}"
hoelzl@49780
   759
  by (rule measure_eqI) (auto simp add: sets_PiM_empty one_ereal_def)
hoelzl@49780
   760
hoelzl@49776
   761
lemma (in product_sigma_finite) emeasure_PiM:
wenzelm@53015
   762
  "finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
hoelzl@49776
   763
proof (induct I arbitrary: A rule: finite_induct)
hoelzl@40859
   764
  case (insert i I)
hoelzl@41689
   765
  interpret finite_product_sigma_finite M I by default fact
hoelzl@40859
   766
  have "finite (insert i I)" using `finite I` by auto
hoelzl@41689
   767
  interpret I': finite_product_sigma_finite M "insert i I" by default fact
hoelzl@41661
   768
  let ?h = "(\<lambda>(f, y). f(i := y))"
hoelzl@47694
   769
wenzelm@53015
   770
  let ?P = "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M) ?h"
hoelzl@47694
   771
  let ?\<mu> = "emeasure ?P"
hoelzl@47694
   772
  let ?I = "{j \<in> insert i I. emeasure (M j) (space (M j)) \<noteq> 1}"
hoelzl@47694
   773
  let ?f = "\<lambda>J E j. if j \<in> J then emeasure (M j) (E j) else emeasure (M j) (space (M j))"
hoelzl@47694
   774
wenzelm@53015
   775
  have "emeasure (Pi\<^sub>M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi\<^sub>E (insert i I) A)) =
hoelzl@49776
   776
    (\<Prod>i\<in>insert i I. emeasure (M i) (A i))"
hoelzl@49776
   777
  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
hoelzl@49776
   778
    fix J E assume "(J \<noteq> {} \<or> insert i I = {}) \<and> finite J \<and> J \<subseteq> insert i I \<and> E \<in> (\<Pi> j\<in>J. sets (M j))"
hoelzl@49776
   779
    then have J: "J \<noteq> {}" "finite J" "J \<subseteq> insert i I" and E: "\<forall>j\<in>J. E j \<in> sets (M j)" by auto
wenzelm@53015
   780
    let ?p = "prod_emb (insert i I) M J (Pi\<^sub>E J E)"
wenzelm@53015
   781
    let ?p' = "prod_emb I M (J - {i}) (\<Pi>\<^sub>E j\<in>J-{i}. E j)"
hoelzl@49776
   782
    have "?\<mu> ?p =
wenzelm@53015
   783
      emeasure (Pi\<^sub>M I M \<Otimes>\<^sub>M (M i)) (?h -` ?p \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M M i))"
hoelzl@49776
   784
      by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
wenzelm@53015
   785
    also have "?h -` ?p \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) = ?p' \<times> (if i \<in> J then E i else space (M i))"
immler@50244
   786
      using J E[rule_format, THEN sets.sets_into_space]
hoelzl@50123
   787
      by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: split_if_asm)
wenzelm@53015
   788
    also have "emeasure (Pi\<^sub>M I M \<Otimes>\<^sub>M (M i)) (?p' \<times> (if i \<in> J then E i else space (M i))) =
wenzelm@53015
   789
      emeasure (Pi\<^sub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
hoelzl@49776
   790
      using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
wenzelm@53015
   791
    also have "?p' = (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
immler@50244
   792
      using J E[rule_format, THEN sets.sets_into_space]
hoelzl@50123
   793
      by (auto simp: prod_emb_iff PiE_def Pi_iff split: split_if_asm) blast+
wenzelm@53015
   794
    also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
hoelzl@49776
   795
      (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
haftmann@57418
   796
      using E by (subst insert) (auto intro!: setprod.cong)
hoelzl@49776
   797
    also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
hoelzl@49776
   798
       emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
haftmann@57512
   799
      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="op *"] setprod.cong)
hoelzl@49776
   800
    also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
haftmann@57418
   801
      using insert(1,2) J E by (intro setprod.mono_neutral_right) auto
hoelzl@49776
   802
    finally show "?\<mu> ?p = \<dots>" .
hoelzl@47694
   803
wenzelm@53015
   804
    show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \<in> Pow (\<Pi>\<^sub>E i\<in>insert i I. space (M i))"
immler@50244
   805
      using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
hoelzl@49776
   806
  next
wenzelm@53015
   807
    show "positive (sets (Pi\<^sub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^sub>M (insert i I) M)) ?\<mu>"
hoelzl@49776
   808
      using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
hoelzl@49776
   809
  next
hoelzl@49776
   810
    show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
hoelzl@49776
   811
      insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
hoelzl@49776
   812
      using insert by auto
haftmann@57418
   813
  qed (auto intro!: setprod.cong)
hoelzl@49776
   814
  with insert show ?case
immler@50244
   815
    by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
hoelzl@50003
   816
qed simp
hoelzl@47694
   817
hoelzl@49776
   818
lemma (in product_sigma_finite) sigma_finite: 
hoelzl@49776
   819
  assumes "finite I"
hoelzl@49776
   820
  shows "sigma_finite_measure (PiM I M)"
hoelzl@57447
   821
proof
hoelzl@49776
   822
  interpret finite_product_sigma_finite M I by default fact
hoelzl@49776
   823
hoelzl@57447
   824
  obtain F where F: "\<And>j. countable (F j)" "\<And>j f. f \<in> F j \<Longrightarrow> f \<in> sets (M j)"
hoelzl@57447
   825
    "\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
hoelzl@57447
   826
    in_space: "\<And>j. space (M j) = (\<Union>F j)"
hoelzl@57447
   827
    using sigma_finite_countable by (metis subset_eq)
hoelzl@57447
   828
  moreover have "(\<Union>(PiE I ` PiE I F)) = space (Pi\<^sub>M I M)"
hoelzl@57447
   829
    using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
hoelzl@57447
   830
  ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
hoelzl@57447
   831
    by (intro exI[of _ "PiE I ` PiE I F"])
hoelzl@57447
   832
       (auto intro!: countable_PiE sets_PiM_I_finite
hoelzl@57447
   833
             simp: PiE_iff emeasure_PiM finite_index setprod_PInf emeasure_nonneg)
hoelzl@40859
   834
qed
hoelzl@40859
   835
wenzelm@53015
   836
sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^sub>M I M"
hoelzl@47694
   837
  using sigma_finite[OF finite_index] .
hoelzl@40859
   838
hoelzl@40859
   839
lemma (in finite_product_sigma_finite) measure_times:
wenzelm@53015
   840
  "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
hoelzl@47694
   841
  using emeasure_PiM[OF finite_index] by auto
hoelzl@41096
   842
hoelzl@56996
   843
lemma (in product_sigma_finite) nn_integral_empty:
hoelzl@41981
   844
  assumes pos: "0 \<le> f (\<lambda>k. undefined)"
hoelzl@56996
   845
  shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
hoelzl@40859
   846
proof -
hoelzl@41689
   847
  interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
wenzelm@53015
   848
  have "\<And>A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1"
hoelzl@40859
   849
    using assms by (subst measure_times) auto
hoelzl@40859
   850
  then show ?thesis
hoelzl@56996
   851
    unfolding nn_integral_def simple_function_def simple_integral_def[abs_def]
hoelzl@47694
   852
  proof (simp add: space_PiM_empty sets_PiM_empty, intro antisym)
hoelzl@41981
   853
    show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
hoelzl@44928
   854
      by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
hoelzl@41981
   855
    show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
hoelzl@44928
   856
      by (intro SUP_least) (auto simp: le_fun_def simp: max_def split: split_if_asm)
hoelzl@40859
   857
  qed
hoelzl@40859
   858
qed
hoelzl@40859
   859
hoelzl@47694
   860
lemma (in product_sigma_finite) distr_merge:
hoelzl@40859
   861
  assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
wenzelm@53015
   862
  shows "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J) = Pi\<^sub>M (I \<union> J) M"
hoelzl@47694
   863
   (is "?D = ?P")
hoelzl@40859
   864
proof -
hoelzl@41689
   865
  interpret I: finite_product_sigma_finite M I by default fact
hoelzl@41689
   866
  interpret J: finite_product_sigma_finite M J by default fact
hoelzl@40859
   867
  have "finite (I \<union> J)" using fin by auto
hoelzl@41689
   868
  interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
wenzelm@53015
   869
  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
hoelzl@49780
   870
  let ?g = "merge I J"
hoelzl@47694
   871
hoelzl@41661
   872
  from IJ.sigma_finite_pairs obtain F where
hoelzl@41661
   873
    F: "\<And>i. i\<in> I \<union> J \<Longrightarrow> range (F i) \<subseteq> sets (M i)"
wenzelm@53015
   874
       "incseq (\<lambda>k. \<Pi>\<^sub>E i\<in>I \<union> J. F i k)"
wenzelm@53015
   875
       "(\<Union>k. \<Pi>\<^sub>E i\<in>I \<union> J. F i k) = space ?P"
hoelzl@47694
   876
       "\<And>k. \<forall>i\<in>I\<union>J. emeasure (M i) (F i k) \<noteq> \<infinity>"
hoelzl@41661
   877
    by auto
wenzelm@53015
   878
  let ?F = "\<lambda>k. \<Pi>\<^sub>E i\<in>I \<union> J. F i k"
hoelzl@47694
   879
  
hoelzl@47694
   880
  show ?thesis
hoelzl@47694
   881
  proof (rule measure_eqI_generator_eq[symmetric])
hoelzl@47694
   882
    show "Int_stable (prod_algebra (I \<union> J) M)"
hoelzl@47694
   883
      by (rule Int_stable_prod_algebra)
wenzelm@53015
   884
    show "prod_algebra (I \<union> J) M \<subseteq> Pow (\<Pi>\<^sub>E i \<in> I \<union> J. space (M i))"
hoelzl@47694
   885
      by (rule prod_algebra_sets_into_space)
wenzelm@53015
   886
    show "sets ?P = sigma_sets (\<Pi>\<^sub>E i\<in>I \<union> J. space (M i)) (prod_algebra (I \<union> J) M)"
hoelzl@47694
   887
      by (rule sets_PiM)
wenzelm@53015
   888
    then show "sets ?D = sigma_sets (\<Pi>\<^sub>E i\<in>I \<union> J. space (M i)) (prod_algebra (I \<union> J) M)"
hoelzl@47694
   889
      by simp
hoelzl@47694
   890
hoelzl@47694
   891
    show "range ?F \<subseteq> prod_algebra (I \<union> J) M" using F
hoelzl@47694
   892
      using fin by (auto simp: prod_algebra_eq_finite)
wenzelm@53015
   893
    show "(\<Union>i. \<Pi>\<^sub>E ia\<in>I \<union> J. F ia i) = (\<Pi>\<^sub>E i\<in>I \<union> J. space (M i))"
hoelzl@47694
   894
      using F(3) by (simp add: space_PiM)
hoelzl@41981
   895
  next
hoelzl@41981
   896
    fix k
hoelzl@47694
   897
    from F `finite I` setprod_PInf[of "I \<union> J", OF emeasure_nonneg, of M]
hoelzl@47694
   898
    show "emeasure ?P (?F k) \<noteq> \<infinity>" by (subst IJ.measure_times) auto
hoelzl@41661
   899
  next
hoelzl@47694
   900
    fix A assume A: "A \<in> prod_algebra (I \<union> J) M"
wenzelm@53015
   901
    with fin obtain F where A_eq: "A = (Pi\<^sub>E (I \<union> J) F)" and F: "\<forall>i\<in>J. F i \<in> sets (M i)" "\<forall>i\<in>I. F i \<in> sets (M i)"
hoelzl@47694
   902
      by (auto simp add: prod_algebra_eq_finite)
wenzelm@53015
   903
    let ?B = "Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M"
hoelzl@47694
   904
    let ?X = "?g -` A \<inter> space ?B"
wenzelm@53015
   905
    have "Pi\<^sub>E I F \<subseteq> space (Pi\<^sub>M I M)" "Pi\<^sub>E J F \<subseteq> space (Pi\<^sub>M J M)"
immler@50244
   906
      using F[rule_format, THEN sets.sets_into_space] by (force simp: space_PiM)+
wenzelm@53015
   907
    then have X: "?X = (Pi\<^sub>E I F \<times> Pi\<^sub>E J F)"
hoelzl@47694
   908
      unfolding A_eq by (subst merge_vimage) (auto simp: space_pair_measure space_PiM)
hoelzl@47694
   909
    have "emeasure ?D A = emeasure ?B ?X"
hoelzl@47694
   910
      using A by (intro emeasure_distr measurable_merge) (auto simp: sets_PiM)
hoelzl@47694
   911
    also have "emeasure ?B ?X = (\<Prod>i\<in>I. emeasure (M i) (F i)) * (\<Prod>i\<in>J. emeasure (M i) (F i))"
hoelzl@50003
   912
      using `finite J` `finite I` F unfolding X
hoelzl@50123
   913
      by (simp add: J.emeasure_pair_measure_Times I.measure_times J.measure_times)
hoelzl@47694
   914
    also have "\<dots> = (\<Prod>i\<in>I \<union> J. emeasure (M i) (F i))"
haftmann@57418
   915
      using `finite J` `finite I` `I \<inter> J = {}`  by (simp add: setprod.union_inter_neutral)
wenzelm@53015
   916
    also have "\<dots> = emeasure ?P (Pi\<^sub>E (I \<union> J) F)"
hoelzl@41661
   917
      using `finite J` `finite I` F unfolding A
hoelzl@41661
   918
      by (intro IJ.measure_times[symmetric]) auto
hoelzl@47694
   919
    finally show "emeasure ?P A = emeasure ?D A" using A_eq by simp
hoelzl@47694
   920
  qed
hoelzl@41661
   921
qed
hoelzl@41026
   922
hoelzl@56996
   923
lemma (in product_sigma_finite) product_nn_integral_fold:
hoelzl@47694
   924
  assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
wenzelm@53015
   925
  and f: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
hoelzl@56996
   926
  shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
wenzelm@53015
   927
    (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
hoelzl@41026
   928
proof -
hoelzl@41689
   929
  interpret I: finite_product_sigma_finite M I by default fact
hoelzl@41689
   930
  interpret J: finite_product_sigma_finite M J by default fact
wenzelm@53015
   931
  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
wenzelm@53015
   932
  have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
hoelzl@49776
   933
    using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
hoelzl@41661
   934
  show ?thesis
hoelzl@47694
   935
    apply (subst distr_merge[OF IJ, symmetric])
hoelzl@56996
   936
    apply (subst nn_integral_distr[OF measurable_merge f])
hoelzl@56996
   937
    apply (subst J.nn_integral_fst[symmetric, OF P_borel])
hoelzl@47694
   938
    apply simp
hoelzl@47694
   939
    done
hoelzl@40859
   940
qed
hoelzl@40859
   941
hoelzl@47694
   942
lemma (in product_sigma_finite) distr_singleton:
wenzelm@53015
   943
  "distr (Pi\<^sub>M {i} M) (M i) (\<lambda>x. x i) = M i" (is "?D = _")
hoelzl@47694
   944
proof (intro measure_eqI[symmetric])
hoelzl@41831
   945
  interpret I: finite_product_sigma_finite M "{i}" by default simp
hoelzl@47694
   946
  fix A assume A: "A \<in> sets (M i)"
wenzelm@53374
   947
  then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
immler@50244
   948
    using sets.sets_into_space by (auto simp: space_PiM)
wenzelm@53374
   949
  then show "emeasure (M i) A = emeasure ?D A"
hoelzl@47694
   950
    using A I.measure_times[of "\<lambda>_. A"]
hoelzl@47694
   951
    by (simp add: emeasure_distr measurable_component_singleton)
hoelzl@47694
   952
qed simp
hoelzl@41831
   953
hoelzl@56996
   954
lemma (in product_sigma_finite) product_nn_integral_singleton:
hoelzl@40859
   955
  assumes f: "f \<in> borel_measurable (M i)"
hoelzl@56996
   956
  shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
hoelzl@40859
   957
proof -
hoelzl@41689
   958
  interpret I: finite_product_sigma_finite M "{i}" by default simp
hoelzl@47694
   959
  from f show ?thesis
hoelzl@47694
   960
    apply (subst distr_singleton[symmetric])
hoelzl@56996
   961
    apply (subst nn_integral_distr[OF measurable_component_singleton])
hoelzl@47694
   962
    apply simp_all
hoelzl@47694
   963
    done
hoelzl@40859
   964
qed
hoelzl@40859
   965
hoelzl@56996
   966
lemma (in product_sigma_finite) product_nn_integral_insert:
hoelzl@49780
   967
  assumes I[simp]: "finite I" "i \<notin> I"
wenzelm@53015
   968
    and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
hoelzl@56996
   969
  shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^sub>M I M))"
hoelzl@41096
   970
proof -
hoelzl@41689
   971
  interpret I: finite_product_sigma_finite M I by default auto
hoelzl@41689
   972
  interpret i: finite_product_sigma_finite M "{i}" by default auto
hoelzl@41689
   973
  have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
hoelzl@41689
   974
    using f by auto
hoelzl@41096
   975
  show ?thesis
hoelzl@56996
   976
    unfolding product_nn_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
hoelzl@56996
   977
  proof (rule nn_integral_cong, subst product_nn_integral_singleton[symmetric])
wenzelm@53015
   978
    fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
hoelzl@49780
   979
    let ?f = "\<lambda>y. f (x(i := y))"
hoelzl@49780
   980
    show "?f \<in> borel_measurable (M i)"
hoelzl@47694
   981
      using measurable_comp[OF measurable_component_update f, OF x `i \<notin> I`]
hoelzl@47694
   982
      unfolding comp_def .
wenzelm@53015
   983
    show "(\<integral>\<^sup>+ y. f (merge I {i} (x, y)) \<partial>Pi\<^sub>M {i} M) = (\<integral>\<^sup>+ y. f (x(i := y i)) \<partial>Pi\<^sub>M {i} M)"
hoelzl@49780
   984
      using x
hoelzl@56996
   985
      by (auto intro!: nn_integral_cong arg_cong[where f=f]
hoelzl@50123
   986
               simp add: space_PiM extensional_def PiE_def)
hoelzl@41096
   987
  qed
hoelzl@41096
   988
qed
hoelzl@41096
   989
hoelzl@59425
   990
lemma (in product_sigma_finite) product_nn_integral_insert_rev:
hoelzl@59425
   991
  assumes I[simp]: "finite I" "i \<notin> I"
hoelzl@59425
   992
    and [measurable]: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
hoelzl@59425
   993
  shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x(i := y)) \<partial>(Pi\<^sub>M I M)) \<partial>(M i))"
hoelzl@59425
   994
  apply (subst product_nn_integral_insert[OF assms])
hoelzl@59425
   995
  apply (rule pair_sigma_finite.Fubini')
hoelzl@59425
   996
  apply intro_locales []
hoelzl@59425
   997
  apply (rule sigma_finite[OF I(1)])
hoelzl@59425
   998
  apply measurable
hoelzl@59425
   999
  done
hoelzl@59425
  1000
hoelzl@56996
  1001
lemma (in product_sigma_finite) product_nn_integral_setprod:
hoelzl@43920
  1002
  fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
hoelzl@41096
  1003
  assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
hoelzl@41981
  1004
  and pos: "\<And>i x. i \<in> I \<Longrightarrow> 0 \<le> f i x"
hoelzl@56996
  1005
  shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>N (M i) (f i))"
hoelzl@41096
  1006
using assms proof induct
hoelzl@41096
  1007
  case (insert i I)
hoelzl@41096
  1008
  note `finite I`[intro, simp]
hoelzl@41689
  1009
  interpret I: finite_product_sigma_finite M I by default auto
hoelzl@41096
  1010
  have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
haftmann@57418
  1011
    using insert by (auto intro!: setprod.cong)
wenzelm@53015
  1012
  have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^sub>M J M)"
immler@50244
  1013
    using sets.sets_into_space insert
hoelzl@47694
  1014
    by (intro borel_measurable_ereal_setprod
hoelzl@41689
  1015
              measurable_comp[OF measurable_component_singleton, unfolded comp_def])
hoelzl@41096
  1016
       auto
hoelzl@41981
  1017
  then show ?case
hoelzl@56996
  1018
    apply (simp add: product_nn_integral_insert[OF insert(1,2) prod])
hoelzl@56996
  1019
    apply (simp add: insert(2-) * pos borel setprod_ereal_pos nn_integral_multc)
hoelzl@56996
  1020
    apply (subst nn_integral_cmult)
hoelzl@56996
  1021
    apply (auto simp add: pos borel insert(2-) setprod_ereal_pos nn_integral_nonneg)
hoelzl@41981
  1022
    done
hoelzl@47694
  1023
qed (simp add: space_PiM)
hoelzl@41096
  1024
hoelzl@59425
  1025
lemma (in product_sigma_finite) product_nn_integral_pair:
hoelzl@59425
  1026
  assumes [measurable]: "split f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
hoelzl@59425
  1027
  assumes xy: "x \<noteq> y"
hoelzl@59425
  1028
  shows "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {x, y} M) = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
hoelzl@59425
  1029
proof-
hoelzl@59425
  1030
  interpret psm: pair_sigma_finite "M x" "M y"
hoelzl@59425
  1031
    unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all
hoelzl@59425
  1032
  have "{x, y} = {y, x}" by auto
hoelzl@59425
  1033
  also have "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {y, x} M) = (\<integral>\<^sup>+y. \<integral>\<^sup>+\<sigma>. f (\<sigma> x) y \<partial>PiM {x} M \<partial>M y)"
hoelzl@59425
  1034
    using xy by (subst product_nn_integral_insert_rev) simp_all
hoelzl@59425
  1035
  also have "... = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. f x y \<partial>M x \<partial>M y)"
hoelzl@59425
  1036
    by (intro nn_integral_cong, subst product_nn_integral_singleton) simp_all
hoelzl@59425
  1037
  also have "... = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
hoelzl@59425
  1038
    by (subst psm.nn_integral_snd[symmetric]) simp_all
hoelzl@59425
  1039
  finally show ?thesis .
hoelzl@59425
  1040
qed
hoelzl@59425
  1041
hoelzl@50104
  1042
lemma (in product_sigma_finite) distr_component:
wenzelm@53015
  1043
  "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
hoelzl@50104
  1044
proof (intro measure_eqI[symmetric])
hoelzl@50104
  1045
  interpret I: finite_product_sigma_finite M "{i}" by default simp
hoelzl@50104
  1046
hoelzl@50104
  1047
  have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
hoelzl@50104
  1048
    by (auto simp: extensional_def restrict_def)
hoelzl@50104
  1049
hoelzl@59048
  1050
  have [measurable]: "\<And>j. j \<in> {i} \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)" by simp
hoelzl@59048
  1051
hoelzl@50104
  1052
  fix A assume A: "A \<in> sets ?P"
wenzelm@53015
  1053
  then have "emeasure ?P A = (\<integral>\<^sup>+x. indicator A x \<partial>?P)" 
hoelzl@50104
  1054
    by simp
wenzelm@53015
  1055
  also have "\<dots> = (\<integral>\<^sup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)" 
hoelzl@56996
  1056
    by (intro nn_integral_cong) (auto simp: space_PiM indicator_def PiE_def eq)
hoelzl@50104
  1057
  also have "\<dots> = emeasure ?D A"
hoelzl@56996
  1058
    using A by (simp add: product_nn_integral_singleton emeasure_distr)
wenzelm@53015
  1059
  finally show "emeasure (Pi\<^sub>M {i} M) A = emeasure ?D A" .
hoelzl@50104
  1060
qed simp
hoelzl@41026
  1061
hoelzl@49776
  1062
lemma (in product_sigma_finite)
wenzelm@53015
  1063
  assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^sub>M (I \<union> J) M)"
hoelzl@49776
  1064
  shows emeasure_fold_integral:
wenzelm@53015
  1065
    "emeasure (Pi\<^sub>M (I \<union> J) M) A = (\<integral>\<^sup>+x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M)) \<partial>Pi\<^sub>M I M)" (is ?I)
hoelzl@49776
  1066
    and emeasure_fold_measurable:
wenzelm@53015
  1067
    "(\<lambda>x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M))) \<in> borel_measurable (Pi\<^sub>M I M)" (is ?B)
hoelzl@49776
  1068
proof -
hoelzl@49776
  1069
  interpret I: finite_product_sigma_finite M I by default fact
hoelzl@49776
  1070
  interpret J: finite_product_sigma_finite M J by default fact
wenzelm@53015
  1071
  interpret IJ: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
wenzelm@53015
  1072
  have merge: "merge I J -` A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) \<in> sets (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
hoelzl@49776
  1073
    by (intro measurable_sets[OF _ A] measurable_merge assms)
hoelzl@49776
  1074
hoelzl@49776
  1075
  show ?I
hoelzl@49776
  1076
    apply (subst distr_merge[symmetric, OF IJ])
hoelzl@49776
  1077
    apply (subst emeasure_distr[OF measurable_merge A])
hoelzl@49776
  1078
    apply (subst J.emeasure_pair_measure_alt[OF merge])
hoelzl@56996
  1079
    apply (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
hoelzl@49776
  1080
    done
hoelzl@49776
  1081
hoelzl@49776
  1082
  show ?B
hoelzl@49776
  1083
    using IJ.measurable_emeasure_Pair1[OF merge]
haftmann@56154
  1084
    by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong)
hoelzl@49776
  1085
qed
hoelzl@49776
  1086
hoelzl@49776
  1087
lemma sets_Collect_single:
wenzelm@53015
  1088
  "i \<in> I \<Longrightarrow> A \<in> sets (M i) \<Longrightarrow> { x \<in> space (Pi\<^sub>M I M). x i \<in> A } \<in> sets (Pi\<^sub>M I M)"
hoelzl@50003
  1089
  by simp
hoelzl@49776
  1090
hoelzl@50104
  1091
lemma pair_measure_eq_distr_PiM:
hoelzl@50104
  1092
  fixes M1 :: "'a measure" and M2 :: "'a measure"
hoelzl@50104
  1093
  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
blanchet@55414
  1094
  shows "(M1 \<Otimes>\<^sub>M M2) = distr (Pi\<^sub>M UNIV (case_bool M1 M2)) (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. (x True, x False))"
hoelzl@50104
  1095
    (is "?P = ?D")
hoelzl@50104
  1096
proof (rule pair_measure_eqI[OF assms])
blanchet@55414
  1097
  interpret B: product_sigma_finite "case_bool M1 M2"
hoelzl@50104
  1098
    unfolding product_sigma_finite_def using assms by (auto split: bool.split)
blanchet@55414
  1099
  let ?B = "Pi\<^sub>M UNIV (case_bool M1 M2)"
hoelzl@50104
  1100
hoelzl@50104
  1101
  have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
hoelzl@50104
  1102
    by auto
hoelzl@50104
  1103
  fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
blanchet@55414
  1104
  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (case_bool M1 M2 i) (case_bool A B i))"
hoelzl@50104
  1105
    by (simp add: UNIV_bool ac_simps)
blanchet@55414
  1106
  also have "\<dots> = emeasure ?B (Pi\<^sub>E UNIV (case_bool A B))"
hoelzl@50104
  1107
    using A B by (subst B.emeasure_PiM) (auto split: bool.split)
blanchet@55414
  1108
  also have "Pi\<^sub>E UNIV (case_bool A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
immler@50244
  1109
    using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
hoelzl@50123
  1110
    by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
hoelzl@50104
  1111
  finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
hoelzl@50104
  1112
    using A B
blanchet@55414
  1113
      measurable_component_singleton[of True UNIV "case_bool M1 M2"]
blanchet@55414
  1114
      measurable_component_singleton[of False UNIV "case_bool M1 M2"]
hoelzl@50104
  1115
    by (subst emeasure_distr) (auto simp: measurable_pair_iff)
hoelzl@50104
  1116
qed simp
hoelzl@50104
  1117
hoelzl@47694
  1118
end