src/HOL/Analysis/Finite_Product_Measure.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69918 eddcc7c726f3
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Finite_Product_Measure.thy
hoelzl@42067
     2
    Author:     Johannes Hölzl, TU München
hoelzl@42067
     3
*)
hoelzl@42067
     4
ak2110@69722
     5
section \<open>Finite Product Measure\<close>
hoelzl@42067
     6
hoelzl@42146
     7
theory Finite_Product_Measure
lp15@69918
     8
imports Binary_Product_Measure Function_Topology
hoelzl@35833
     9
begin
hoelzl@35833
    10
immler@69681
    11
lemma PiE_choice: "(\<exists>f\<in>Pi\<^sub>E 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
immler@69681
    15
lemma case_prod_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
hoelzl@47694
    16
  by auto
hoelzl@47694
    17
nipkow@69685
    18
subsection%unimportant \<open>More about Function restricted by \<^const>\<open>extensional\<close>\<close>
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>
wenzelm@64910
    64
    merge I J (x, y) \<in> Pi\<^sub>E (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)"
wenzelm@61808
    95
      using y x \<open>J \<subseteq> I\<close> 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"
wenzelm@61808
    98
      using y x \<open>J \<subseteq> I\<close> 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
immler@69683
   112
subsection \<open>Finite product spaces\<close>
hoelzl@40859
   113
ak2110@68833
   114
definition%important prod_emb where
wenzelm@64910
   115
  "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@47694
   116
immler@69681
   117
lemma prod_emb_iff:
hoelzl@47694
   118
  "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))"
ak2110@68833
   119
  unfolding%unimportant prod_emb_def PiE_def by auto
hoelzl@40859
   120
immler@69681
   121
lemma
hoelzl@47694
   122
  shows prod_emb_empty[simp]: "prod_emb M L K {} = {}"
hoelzl@47694
   123
    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
   124
    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
   125
    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
   126
    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
   127
    and prod_emb_Diff[simp]: "prod_emb M L K (A - B) = prod_emb M L K A - prod_emb M L K B"
immler@69681
   128
  by (auto simp: prod_emb_def)
hoelzl@40859
   129
immler@69681
   130
lemma prod_emb_PiE: "J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)) \<Longrightarrow>
wenzelm@53015
   131
    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))"
nipkow@62390
   132
  by (force simp: prod_emb_def PiE_iff if_split_mem2)
hoelzl@47694
   133
immler@69681
   134
lemma prod_emb_PiE_same_index[simp]:
wenzelm@53015
   135
    "(\<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
   136
  by (auto simp: prod_emb_def PiE_iff)
hoelzl@41689
   137
immler@69681
   138
lemma prod_emb_trans[simp]:
immler@50038
   139
  "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
   140
  by (auto simp add: Int_absorb1 prod_emb_def PiE_def)
immler@50038
   141
immler@69681
   142
lemma prod_emb_Pi:
immler@50038
   143
  assumes "X \<in> (\<Pi> j\<in>J. sets (M j))" "J \<subseteq> K"
wenzelm@53015
   144
  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
   145
  using assms sets.space_closed
nipkow@62390
   146
  by (auto simp: prod_emb_def PiE_iff split: if_split_asm) blast+
immler@50038
   147
immler@69681
   148
lemma prod_emb_id:
wenzelm@53015
   149
  "B \<subseteq> (\<Pi>\<^sub>E i\<in>L. space (M i)) \<Longrightarrow> prod_emb L M L B = B"
hoelzl@50123
   150
  by (auto simp: prod_emb_def subset_eq extensional_restrict)
immler@50038
   151
immler@69681
   152
lemma prod_emb_mono:
immler@50041
   153
  "F \<subseteq> G \<Longrightarrow> prod_emb A M B F \<subseteq> prod_emb A M B G"
immler@50041
   154
  by (auto simp: prod_emb_def)
immler@50041
   155
ak2110@68833
   156
definition%important PiM :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) measure" where
wenzelm@53015
   157
  "PiM I M = extend_measure (\<Pi>\<^sub>E i\<in>I. space (M i))
hoelzl@47694
   158
    {(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
   159
    (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j))
hoelzl@47694
   160
    (\<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
   161
ak2110@68833
   162
definition%important prod_algebra :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a measure) \<Rightarrow> ('i \<Rightarrow> 'a) set set" where
wenzelm@53015
   163
  "prod_algebra I M = (\<lambda>(J, X). prod_emb I M J (\<Pi>\<^sub>E j\<in>J. X j)) `
hoelzl@47694
   164
    {(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
   165
hoelzl@47694
   166
abbreviation
wenzelm@53015
   167
  "Pi\<^sub>M I M \<equiv> PiM I M"
hoelzl@41689
   168
hoelzl@40859
   169
syntax
wenzelm@53015
   170
  "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>M _\<in>_./ _)"  10)
hoelzl@40859
   171
translations
wenzelm@61988
   172
  "\<Pi>\<^sub>M x\<in>I. M" == "CONST PiM I (%x. M)"
hoelzl@41689
   173
immler@69681
   174
lemma extend_measure_cong:
hoelzl@59425
   175
  assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
hoelzl@59425
   176
  shows "extend_measure \<Omega> I G \<mu> = extend_measure \<Omega>' I' G' \<mu>'"
immler@69681
   177
  unfolding extend_measure_def by (auto simp add: assms)
hoelzl@59425
   178
immler@69681
   179
lemma Pi_cong_sets:
hoelzl@59425
   180
    "\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
hoelzl@62975
   181
  unfolding Pi_def by auto
hoelzl@59425
   182
immler@69681
   183
lemma PiM_cong:
hoelzl@59425
   184
  assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
hoelzl@59425
   185
  shows "PiM I M = PiM J N"
wenzelm@60580
   186
  unfolding PiM_def
immler@69681
   187
proof (rule extend_measure_cong, goal_cases)
wenzelm@60580
   188
  case 1
wenzelm@60580
   189
  show ?case using assms
hoelzl@59425
   190
    by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
hoelzl@59425
   191
next
wenzelm@60580
   192
  case 2
hoelzl@59425
   193
  have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
hoelzl@59425
   194
    using assms by (intro Pi_cong_sets) auto
hoelzl@59425
   195
  thus ?case by (auto simp: assms)
hoelzl@59425
   196
next
wenzelm@60580
   197
  case 3
hoelzl@62975
   198
  show ?case using assms
hoelzl@59425
   199
    by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
hoelzl@59425
   200
next
wenzelm@60580
   201
  case (4 x)
hoelzl@62975
   202
  thus ?case using assms
nipkow@64272
   203
    by (auto intro!: prod.cong split: if_split_asm)
hoelzl@59425
   204
qed
hoelzl@59425
   205
hoelzl@59425
   206
immler@69681
   207
lemma prod_algebra_sets_into_space:
wenzelm@53015
   208
  "prod_algebra I M \<subseteq> Pow (\<Pi>\<^sub>E i\<in>I. space (M i))"
immler@50245
   209
  by (auto simp: prod_emb_def prod_algebra_def)
hoelzl@40859
   210
immler@69681
   211
lemma prod_algebra_eq_finite:
hoelzl@47694
   212
  assumes I: "finite I"
wenzelm@53015
   213
  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")
immler@69681
   214
proof (intro iffI set_eqI)
hoelzl@47694
   215
  fix A assume "A \<in> ?L"
hoelzl@47694
   216
  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)"
wenzelm@64910
   217
    and A: "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
hoelzl@47694
   218
    by (auto simp: prod_algebra_def)
wenzelm@53015
   219
  let ?A = "\<Pi>\<^sub>E i\<in>I. if i \<in> J then E i else space (M i)"
hoelzl@47694
   220
  have A: "A = ?A"
immler@50244
   221
    unfolding A using J by (intro prod_emb_PiE sets.sets_into_space) auto
immler@50244
   222
  show "A \<in> ?R" unfolding A using J sets.top
hoelzl@47694
   223
    by (intro CollectI exI[of _ "\<lambda>i. if i \<in> J then E i else space (M i)"]) simp
hoelzl@47694
   224
next
hoelzl@47694
   225
  fix A assume "A \<in> ?R"
wenzelm@53015
   226
  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
   227
  then have A: "A = prod_emb I M I (\<Pi>\<^sub>E i\<in>I. X i)"
immler@50244
   228
    by (simp add: prod_emb_PiE_same_index[OF sets.sets_into_space] Pi_iff)
hoelzl@47694
   229
  from X I show "A \<in> ?L" unfolding A
hoelzl@47694
   230
    by (auto simp: prod_algebra_def)
hoelzl@47694
   231
qed
hoelzl@41095
   232
immler@69681
   233
lemma prod_algebraI:
hoelzl@47694
   234
  "finite J \<Longrightarrow> (J \<noteq> {} \<or> I = {}) \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i))
wenzelm@64910
   235
    \<Longrightarrow> prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> prod_algebra I M"
hoelzl@50123
   236
  by (auto simp: prod_algebra_def)
hoelzl@41689
   237
immler@69681
   238
lemma prod_algebraI_finite:
wenzelm@53015
   239
  "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
   240
  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
   241
immler@69681
   242
lemma Int_stable_PiE: "Int_stable {Pi\<^sub>E J E | E. \<forall>i\<in>I. E i \<in> sets (M i)}"
immler@50038
   243
proof (safe intro!: Int_stableI)
immler@50038
   244
  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
   245
  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
   246
    by (auto intro!: exI[of _ "\<lambda>i. E i \<inter> F i"] simp: PiE_Int)
immler@50038
   247
qed
immler@50038
   248
immler@69681
   249
lemma prod_algebraE:
hoelzl@47694
   250
  assumes A: "A \<in> prod_algebra I M"
wenzelm@64910
   251
  obtains J E where "A = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
hoelzl@62975
   252
    "finite J" "J \<noteq> {} \<or> I = {}" "J \<subseteq> I" "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)"
hoelzl@47694
   253
  using A by (auto simp: prod_algebra_def)
hoelzl@42988
   254
immler@69681
   255
lemma prod_algebraE_all:
hoelzl@47694
   256
  assumes A: "A \<in> prod_algebra I M"
wenzelm@53015
   257
  obtains E where "A = Pi\<^sub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
immler@69681
   258
proof -
wenzelm@53015
   259
  from A obtain E J where A: "A = prod_emb I M J (Pi\<^sub>E J E)"
hoelzl@47694
   260
    and J: "J \<subseteq> I" and E: "E \<in> (\<Pi> i\<in>J. sets (M i))"
hoelzl@47694
   261
    by (auto simp: prod_algebra_def)
hoelzl@47694
   262
  from E have "\<And>i. i \<in> J \<Longrightarrow> E i \<subseteq> space (M i)"
immler@50244
   263
    using sets.sets_into_space by auto
wenzelm@53015
   264
  then have "A = (\<Pi>\<^sub>E i\<in>I. if i\<in>J then E i else space (M i))"
hoelzl@47694
   265
    using A J by (auto simp: prod_emb_PiE)
wenzelm@53374
   266
  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
   267
    using sets.top E by auto
hoelzl@47694
   268
  ultimately show ?thesis using that by auto
hoelzl@47694
   269
qed
hoelzl@40859
   270
immler@69681
   271
lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
hoelzl@47694
   272
proof (unfold Int_stable_def, safe)
hoelzl@47694
   273
  fix A assume "A \<in> prod_algebra I M"
hoelzl@47694
   274
  from prod_algebraE[OF this] guess J E . note A = this
hoelzl@47694
   275
  fix B assume "B \<in> prod_algebra I M"
hoelzl@47694
   276
  from prod_algebraE[OF this] guess K F . note B = this
hoelzl@62975
   277
  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
   278
      (if i \<in> K then F i else space (M i)))"
immler@50244
   279
    unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
immler@50244
   280
      B(5)[THEN sets.sets_into_space]
hoelzl@47694
   281
    apply (subst (1 2 3) prod_emb_PiE)
hoelzl@47694
   282
    apply (simp_all add: subset_eq PiE_Int)
hoelzl@47694
   283
    apply blast
hoelzl@47694
   284
    apply (intro PiE_cong)
hoelzl@47694
   285
    apply auto
hoelzl@47694
   286
    done
hoelzl@47694
   287
  also have "\<dots> \<in> prod_algebra I M"
hoelzl@47694
   288
    using A B by (auto intro!: prod_algebraI)
hoelzl@47694
   289
  finally show "A \<inter> B \<in> prod_algebra I M" .
hoelzl@47694
   290
qed
hoelzl@47694
   291
immler@69681
   292
proposition prod_algebra_mono:
hoelzl@47694
   293
  assumes space: "\<And>i. i \<in> I \<Longrightarrow> space (E i) = space (F i)"
hoelzl@47694
   294
  assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (E i) \<subseteq> sets (F i)"
hoelzl@47694
   295
  shows "prod_algebra I E \<subseteq> prod_algebra I F"
immler@69681
   296
proof
hoelzl@47694
   297
  fix A assume "A \<in> prod_algebra I E"
hoelzl@47694
   298
  then obtain J G where J: "J \<noteq> {} \<or> I = {}" "finite J" "J \<subseteq> I"
wenzelm@53015
   299
    and A: "A = prod_emb I E J (\<Pi>\<^sub>E i\<in>J. G i)"
hoelzl@47694
   300
    and G: "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (E i)"
hoelzl@47694
   301
    by (auto simp: prod_algebra_def)
hoelzl@47694
   302
  moreover
wenzelm@53015
   303
  from space have "(\<Pi>\<^sub>E i\<in>I. space (E i)) = (\<Pi>\<^sub>E i\<in>I. space (F i))"
hoelzl@47694
   304
    by (rule PiE_cong)
wenzelm@53015
   305
  with A have "A = prod_emb I F J (\<Pi>\<^sub>E i\<in>J. G i)"
hoelzl@47694
   306
    by (simp add: prod_emb_def)
hoelzl@47694
   307
  moreover
hoelzl@47694
   308
  from sets G J have "\<And>i. i \<in> J \<Longrightarrow> G i \<in> sets (F i)"
hoelzl@47694
   309
    by auto
hoelzl@47694
   310
  ultimately show "A \<in> prod_algebra I F"
hoelzl@47694
   311
    apply (simp add: prod_algebra_def image_iff)
hoelzl@47694
   312
    apply (intro exI[of _ J] exI[of _ G] conjI)
hoelzl@47694
   313
    apply auto
hoelzl@47694
   314
    done
hoelzl@41689
   315
qed
immler@69681
   316
proposition prod_algebra_cong:
hoelzl@50104
   317
  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
hoelzl@50104
   318
  shows "prod_algebra I M = prod_algebra J N"
immler@69681
   319
proof -
hoelzl@50104
   320
  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
hoelzl@50104
   321
    using sets_eq_imp_space_eq[OF sets] by auto
wenzelm@61808
   322
  with sets show ?thesis unfolding \<open>I = J\<close>
hoelzl@50104
   323
    by (intro antisym prod_algebra_mono) auto
hoelzl@50104
   324
qed
hoelzl@50104
   325
immler@69681
   326
lemma space_in_prod_algebra:
wenzelm@53015
   327
  "(\<Pi>\<^sub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
hoelzl@50104
   328
proof cases
hoelzl@50104
   329
  assume "I = {}" then show ?thesis
hoelzl@50104
   330
    by (auto simp add: prod_algebra_def image_iff prod_emb_def)
hoelzl@50104
   331
next
hoelzl@50104
   332
  assume "I \<noteq> {}"
hoelzl@50104
   333
  then obtain i where "i \<in> I" by auto
wenzelm@53015
   334
  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
   335
    by (auto simp: prod_emb_def)
hoelzl@50104
   336
  also have "\<dots> \<in> prod_algebra I M"
wenzelm@61808
   337
    using \<open>i \<in> I\<close> by (intro prod_algebraI) auto
hoelzl@50104
   338
  finally show ?thesis .
hoelzl@50104
   339
qed
hoelzl@50104
   340
immler@69681
   341
lemma space_PiM: "space (\<Pi>\<^sub>M i\<in>I. M i) = (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@47694
   342
  using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
hoelzl@47694
   343
immler@69681
   344
lemma prod_emb_subset_PiM[simp]: "prod_emb I M K X \<subseteq> space (PiM I M)"
hoelzl@61359
   345
  by (auto simp: prod_emb_def space_PiM)
hoelzl@61359
   346
immler@69681
   347
lemma space_PiM_empty_iff[simp]: "space (PiM I M) = {} \<longleftrightarrow>  (\<exists>i\<in>I. space (M i) = {})"
hoelzl@61359
   348
  by (auto simp: space_PiM PiE_eq_empty_iff)
hoelzl@61359
   349
immler@69681
   350
lemma undefined_in_PiM_empty[simp]: "(\<lambda>x. undefined) \<in> space (PiM {} M)"
hoelzl@61359
   351
  by (auto simp: space_PiM)
hoelzl@61359
   352
immler@69681
   353
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
   354
  using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro sets_extend_measure) simp
hoelzl@41689
   355
immler@69681
   356
proposition sets_PiM_single: "sets (PiM I M) =
wenzelm@53015
   357
    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
   358
    (is "_ = sigma_sets ?\<Omega> ?R")
hoelzl@47694
   359
  unfolding sets_PiM
immler@69681
   360
proof (rule sigma_sets_eqI)
hoelzl@47694
   361
  interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto
hoelzl@47694
   362
  fix A assume "A \<in> prod_algebra I M"
hoelzl@47694
   363
  from prod_algebraE[OF this] guess J X . note X = this
hoelzl@47694
   364
  show "A \<in> sigma_sets ?\<Omega> ?R"
hoelzl@47694
   365
  proof cases
hoelzl@47694
   366
    assume "I = {}"
hoelzl@47694
   367
    with X have "A = {\<lambda>x. undefined}" by (auto simp: prod_emb_def)
wenzelm@61808
   368
    with \<open>I = {}\<close> show ?thesis by (auto intro!: sigma_sets_top)
hoelzl@47694
   369
  next
hoelzl@47694
   370
    assume "I \<noteq> {}"
wenzelm@53015
   371
    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
   372
      by (auto simp: prod_emb_def)
hoelzl@47694
   373
    also have "\<dots> \<in> sigma_sets ?\<Omega> ?R"
wenzelm@61808
   374
      using X \<open>I \<noteq> {}\<close> by (intro R.finite_INT sigma_sets.Basic) auto
hoelzl@47694
   375
    finally show "A \<in> sigma_sets ?\<Omega> ?R" .
hoelzl@47694
   376
  qed
hoelzl@47694
   377
next
hoelzl@47694
   378
  fix A assume "A \<in> ?R"
hoelzl@62975
   379
  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
   380
    by auto
wenzelm@53015
   381
  then have "A = prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. B)"
hoelzl@50123
   382
     by (auto simp: prod_emb_def)
hoelzl@47694
   383
  also have "\<dots> \<in> sigma_sets ?\<Omega> (prod_algebra I M)"
hoelzl@47694
   384
    using A by (intro sigma_sets.Basic prod_algebraI) auto
hoelzl@47694
   385
  finally show "A \<in> sigma_sets ?\<Omega> (prod_algebra I M)" .
hoelzl@47694
   386
qed
hoelzl@47694
   387
immler@69681
   388
lemma sets_PiM_eq_proj:
haftmann@69260
   389
  "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
hoelzl@63333
   390
  apply (simp add: sets_PiM_single)
hoelzl@63333
   391
  apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"])
hoelzl@63333
   392
  apply auto []
hoelzl@63333
   393
  apply auto []
hoelzl@63333
   394
  apply simp
haftmann@69661
   395
  apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
hoelzl@58606
   396
  apply (rule sets_vimage_algebra2)
hoelzl@58606
   397
  apply (auto intro!: arg_cong2[where f=sigma_sets])
hoelzl@58606
   398
  done
hoelzl@58606
   399
nipkow@69739
   400
lemma
hoelzl@59088
   401
  shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
hoelzl@59088
   402
    and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
hoelzl@59088
   403
  by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
hoelzl@59088
   404
immler@69681
   405
proposition sets_PiM_sigma:
hoelzl@59088
   406
  assumes \<Omega>_cover: "\<And>i. i \<in> I \<Longrightarrow> \<exists>S\<subseteq>E i. countable S \<and> \<Omega> i = \<Union>S"
hoelzl@59088
   407
  assumes E: "\<And>i. i \<in> I \<Longrightarrow> E i \<subseteq> Pow (\<Omega> i)"
hoelzl@59088
   408
  assumes J: "\<And>j. j \<in> J \<Longrightarrow> finite j" "\<Union>J = I"
hoelzl@59088
   409
  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
   410
  shows "sets (\<Pi>\<^sub>M i\<in>I. sigma (\<Omega> i) (E i)) = sets (sigma (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P)"
immler@69681
   411
proof cases
hoelzl@62975
   412
  assume "I = {}"
wenzelm@61808
   413
  with \<open>\<Union>J = I\<close> have "P = {{\<lambda>_. undefined}} \<or> P = {}"
hoelzl@59088
   414
    by (auto simp: P_def)
wenzelm@61808
   415
  with \<open>I = {}\<close> show ?thesis
hoelzl@59088
   416
    by (auto simp add: sets_PiM_empty sigma_sets_empty_eq)
hoelzl@59088
   417
next
hoelzl@59088
   418
  let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
hoelzl@59088
   419
  assume "I \<noteq> {}"
hoelzl@62975
   420
  then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) =
haftmann@69260
   421
      sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
hoelzl@59088
   422
    by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
haftmann@69260
   423
  also have "\<dots> = sets (SUP i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
hoelzl@63333
   424
    using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
hoelzl@59088
   425
  also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
wenzelm@61808
   426
    using \<open>I \<noteq> {}\<close> by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
hoelzl@59088
   427
  also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) P)"
hoelzl@59088
   428
  proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
hoelzl@59088
   429
    show "(\<Union>i\<in>I. ?F i) \<subseteq> Pow (Pi\<^sub>E I \<Omega>)" "P \<subseteq> Pow (Pi\<^sub>E I \<Omega>)"
hoelzl@59088
   430
      by (auto simp: P_def)
hoelzl@59088
   431
  next
hoelzl@59088
   432
    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
   433
      by (auto intro!: sigma_algebra_sigma_sets simp: P_def)
hoelzl@59088
   434
hoelzl@59088
   435
    fix Z assume "Z \<in> (\<Union>i\<in>I. ?F i)"
hoelzl@59088
   436
    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
   437
      by auto
wenzelm@61808
   438
    from \<open>i \<in> I\<close> J obtain j where j: "i \<in> j" "j \<in> J" "j \<subseteq> I" "finite j"
hoelzl@59088
   439
      by auto
hoelzl@59088
   440
    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
   441
      "\<And>i. i \<in> j \<Longrightarrow> \<Omega> i = \<Union>(S i)"
wenzelm@61808
   442
      by (metis subset_eq \<Omega>_cover \<open>j \<subseteq> I\<close>)
wenzelm@63040
   443
    define A' where "A' n = n(i := A)" for n
hoelzl@59088
   444
    then have A'_i: "\<And>n. A' n i = A"
hoelzl@59088
   445
      by simp
hoelzl@59088
   446
    { fix n assume "n \<in> Pi\<^sub>E (j - {i}) S"
hoelzl@59088
   447
      then have "A' n \<in> Pi j E"
wenzelm@61808
   448
        unfolding PiE_def Pi_def using S(1) by (auto simp: A'_def \<open>A \<in> E i\<close> )
wenzelm@61808
   449
      with \<open>j \<in> J\<close> have "{f \<in> Pi\<^sub>E I \<Omega>. \<forall>i\<in>j. f i \<in> A' n i} \<in> P"
hoelzl@59088
   450
        by (auto simp: P_def) }
hoelzl@59088
   451
    note A'_in_P = this
hoelzl@59088
   452
hoelzl@59088
   453
    { fix x assume "x i \<in> A" "x \<in> Pi\<^sub>E I \<Omega>"
wenzelm@61808
   454
      with S(3) \<open>j \<subseteq> I\<close> have "\<forall>i\<in>j. \<exists>s\<in>S i. x i \<in> s"
hoelzl@59088
   455
        by (auto simp: PiE_def Pi_def)
hoelzl@59088
   456
      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
   457
        by metis
wenzelm@64910
   458
      with \<open>x i \<in> A\<close> have "\<exists>n\<in>Pi\<^sub>E (j-{i}) S. \<forall>i\<in>j. x i \<in> A' n i"
hoelzl@59088
   459
        by (intro bexI[of _ "restrict (s(i := A)) (j-{i})"]) (auto simp: A'_def split: if_splits) }
wenzelm@64910
   460
    then have "Z = (\<Union>n\<in>Pi\<^sub>E (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
   461
      unfolding Z_def
wenzelm@61808
   462
      by (auto simp add: set_eq_iff ball_conj_distrib \<open>i\<in>j\<close> A'_i dest: bspec[OF _ \<open>i\<in>j\<close>]
hoelzl@59088
   463
               cong: conj_cong)
hoelzl@59088
   464
    also have "\<dots> \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P"
wenzelm@61808
   465
      using \<open>finite j\<close> S(2)
hoelzl@59088
   466
      by (intro P.countable_UN' countable_PiE) (simp_all add: image_subset_iff A'_in_P)
hoelzl@59088
   467
    finally show "Z \<in> sigma_sets (\<Pi>\<^sub>E i\<in>I. \<Omega> i) P" .
hoelzl@59088
   468
  next
hoelzl@59088
   469
    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
   470
      by (auto intro!: sigma_algebra_sigma_sets)
hoelzl@59088
   471
hoelzl@59088
   472
    fix b assume "b \<in> P"
hoelzl@59088
   473
    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
   474
      by (auto simp: P_def)
hoelzl@59088
   475
    show "b \<in> sigma_sets (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i)"
hoelzl@59088
   476
    proof cases
hoelzl@59088
   477
      assume "j = {}"
hoelzl@59088
   478
      with b have "b = (\<Pi>\<^sub>E i\<in>I. \<Omega> i)"
hoelzl@59088
   479
        by auto
hoelzl@59088
   480
      then show ?thesis
hoelzl@59088
   481
        by blast
hoelzl@59088
   482
    next
hoelzl@59088
   483
      assume "j \<noteq> {}"
hoelzl@59088
   484
      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
   485
        unfolding b(1)
hoelzl@59088
   486
        by (auto simp: PiE_def Pi_def)
hoelzl@59088
   487
      show ?thesis
wenzelm@61808
   488
        unfolding eq using \<open>A \<in> Pi j E\<close> \<open>j \<in> J\<close> J(2)
wenzelm@61808
   489
        by (intro F.finite_INT J \<open>j \<in> J\<close> \<open>j \<noteq> {}\<close> sigma_sets.Basic) blast
hoelzl@59088
   490
    qed
hoelzl@59088
   491
  qed
hoelzl@59088
   492
  finally show "?thesis" .
hoelzl@59088
   493
qed
hoelzl@59088
   494
immler@69681
   495
lemma sets_PiM_in_sets:
hoelzl@58606
   496
  assumes space: "space N = (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@58606
   497
  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
   498
  shows "sets (\<Pi>\<^sub>M i \<in> I. M i) \<subseteq> sets N"
hoelzl@58606
   499
  unfolding sets_PiM_single space[symmetric]
hoelzl@58606
   500
  by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
hoelzl@58606
   501
immler@69681
   502
lemma sets_PiM_cong[measurable_cong]:
hoelzl@59048
   503
  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
   504
  using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
hoelzl@58606
   505
immler@69681
   506
lemma sets_PiM_I:
hoelzl@47694
   507
  assumes "finite J" "J \<subseteq> I" "\<forall>i\<in>J. E i \<in> sets (M i)"
wenzelm@64910
   508
  shows "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
immler@69681
   509
proof cases
hoelzl@47694
   510
  assume "J = {}"
wenzelm@64910
   511
  then have "prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j) = (\<Pi>\<^sub>E j\<in>I. space (M j))"
hoelzl@47694
   512
    by (auto simp: prod_emb_def)
hoelzl@47694
   513
  then show ?thesis
hoelzl@47694
   514
    by (auto simp add: sets_PiM intro!: sigma_sets_top)
hoelzl@47694
   515
next
hoelzl@47694
   516
  assume "J \<noteq> {}" with assms show ?thesis
hoelzl@50003
   517
    by (force simp add: sets_PiM prod_algebra_def)
hoelzl@40859
   518
qed
hoelzl@40859
   519
immler@69681
   520
proposition measurable_PiM:
wenzelm@53015
   521
  assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@47694
   522
  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@62975
   523
    f -` prod_emb I M J (Pi\<^sub>E J X) \<inter> space N \<in> sets N"
hoelzl@47694
   524
  shows "f \<in> measurable N (PiM I M)"
hoelzl@47694
   525
  using sets_PiM prod_algebra_sets_into_space space
hoelzl@47694
   526
proof (rule measurable_sigma_sets)
hoelzl@47694
   527
  fix A assume "A \<in> prod_algebra I M"
hoelzl@47694
   528
  from prod_algebraE[OF this] guess J X .
hoelzl@47694
   529
  with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto
hoelzl@47694
   530
qed
hoelzl@47694
   531
immler@69681
   532
lemma measurable_PiM_Collect:
wenzelm@53015
   533
  assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@47694
   534
  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@62975
   535
    {\<omega>\<in>space N. \<forall>i\<in>J. f \<omega> i \<in> X i} \<in> sets N"
hoelzl@47694
   536
  shows "f \<in> measurable N (PiM I M)"
hoelzl@47694
   537
  using sets_PiM prod_algebra_sets_into_space space
immler@69681
   538
proof (rule measurable_sigma_sets)
hoelzl@47694
   539
  fix A assume "A \<in> prod_algebra I M"
hoelzl@47694
   540
  from prod_algebraE[OF this] guess J X . note X = this
hoelzl@50123
   541
  then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
hoelzl@50123
   542
    using space by (auto simp: prod_emb_def del: PiE_I)
hoelzl@47694
   543
  also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
hoelzl@47694
   544
  finally show "f -` A \<inter> space N \<in> sets N" .
hoelzl@41689
   545
qed
hoelzl@41095
   546
immler@69681
   547
lemma measurable_PiM_single:
wenzelm@53015
   548
  assumes space: "f \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@62975
   549
  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
   550
  shows "f \<in> measurable N (PiM I M)"
hoelzl@47694
   551
  using sets_PiM_single
hoelzl@47694
   552
proof (rule measurable_sigma_sets)
wenzelm@53015
   553
  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
   554
  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
   555
    by auto
hoelzl@47694
   556
  with space have "f -` A \<inter> space N = {\<omega> \<in> space N. f \<omega> i \<in> B}" by auto
hoelzl@47694
   557
  also have "\<dots> \<in> sets N" using B by (rule sets)
hoelzl@47694
   558
  finally show "f -` A \<inter> space N \<in> sets N" .
hoelzl@47694
   559
qed (auto simp: space)
hoelzl@40859
   560
immler@69681
   561
lemma measurable_PiM_single':
hoelzl@50099
   562
  assumes f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable N (M i)"
wenzelm@53015
   563
    and "(\<lambda>\<omega> i. f i \<omega>) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
wenzelm@53015
   564
  shows "(\<lambda>\<omega> i. f i \<omega>) \<in> measurable N (Pi\<^sub>M I M)"
immler@69681
   565
proof (rule measurable_PiM_single)
hoelzl@50099
   566
  fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
hoelzl@50099
   567
  then have "{\<omega> \<in> space N. f i \<omega> \<in> A} = f i -` A \<inter> space N"
hoelzl@50099
   568
    by auto
hoelzl@50099
   569
  then show "{\<omega> \<in> space N. f i \<omega> \<in> A} \<in> sets N"
hoelzl@50099
   570
    using A f by (auto intro!: measurable_sets)
hoelzl@50099
   571
qed fact
hoelzl@50099
   572
immler@69681
   573
lemma sets_PiM_I_finite[measurable]:
hoelzl@47694
   574
  assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
wenzelm@64910
   575
  shows "(\<Pi>\<^sub>E j\<in>I. E j) \<in> sets (\<Pi>\<^sub>M i\<in>I. M i)"
wenzelm@61808
   576
  using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] \<open>finite I\<close> sets by auto
hoelzl@47694
   577
immler@69681
   578
lemma measurable_component_singleton[measurable (raw)]:
wenzelm@53015
   579
  assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^sub>M I M) (M i)"
hoelzl@41689
   580
proof (unfold measurable_def, intro CollectI conjI ballI)
hoelzl@41689
   581
  fix A assume "A \<in> sets (M i)"
wenzelm@53015
   582
  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)"
wenzelm@61808
   583
    using sets.sets_into_space \<open>i \<in> I\<close>
nipkow@62390
   584
    by (fastforce dest: Pi_mem simp: prod_emb_def space_PiM split: if_split_asm)
wenzelm@53015
   585
  then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M I M) \<in> sets (Pi\<^sub>M I M)"
wenzelm@61808
   586
    using \<open>A \<in> sets (M i)\<close> \<open>i \<in> I\<close> by (auto intro!: sets_PiM_I)
wenzelm@61808
   587
qed (insert \<open>i \<in> I\<close>, auto simp: space_PiM)
hoelzl@47694
   588
immler@69681
   589
lemma measurable_component_singleton'[measurable_dest]:
wenzelm@53015
   590
  assumes f: "f \<in> measurable N (Pi\<^sub>M I M)"
hoelzl@59353
   591
  assumes g: "g \<in> measurable L N"
hoelzl@50021
   592
  assumes i: "i \<in> I"
hoelzl@59353
   593
  shows "(\<lambda>x. (f (g x)) i) \<in> measurable L (M i)"
hoelzl@59353
   594
  using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] .
hoelzl@50021
   595
immler@69681
   596
lemma measurable_PiM_component_rev:
hoelzl@50099
   597
  "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
hoelzl@50099
   598
  by simp
hoelzl@50099
   599
immler@69681
   600
lemma measurable_case_nat[measurable (raw)]:
hoelzl@50021
   601
  assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
hoelzl@50021
   602
    "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
blanchet@55415
   603
  shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N"
hoelzl@50021
   604
  by (cases i) simp_all
hoelzl@62975
   605
immler@69681
   606
lemma measurable_case_nat'[measurable (raw)]:
wenzelm@53015
   607
  assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
blanchet@55415
   608
  shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
hoelzl@50099
   609
  using fg[THEN measurable_space]
hoelzl@50123
   610
  by (auto intro!: measurable_PiM_single' simp add: space_PiM PiE_iff split: nat.split)
hoelzl@50099
   611
immler@69681
   612
lemma measurable_add_dim[measurable]:
wenzelm@53015
   613
  "(\<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
   614
    (is "?f \<in> measurable ?P ?I")
hoelzl@47694
   615
proof (rule measurable_PiM_single)
hoelzl@47694
   616
  fix j A assume j: "j \<in> insert i I" and A: "A \<in> sets (M j)"
hoelzl@47694
   617
  have "{\<omega> \<in> space ?P. (\<lambda>(f, x). fun_upd f i x) \<omega> j \<in> A} =
wenzelm@53015
   618
    (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
   619
    using sets.sets_into_space[OF A] by (auto simp add: space_pair_measure space_PiM)
hoelzl@47694
   620
  also have "\<dots> \<in> sets ?P"
hoelzl@47694
   621
    using A j
hoelzl@47694
   622
    by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
blanchet@55414
   623
  finally show "{\<omega> \<in> space ?P. case_prod (\<lambda>f. fun_upd f i) \<omega> j \<in> A} \<in> sets ?P" .
hoelzl@50123
   624
qed (auto simp: space_pair_measure space_PiM PiE_def)
hoelzl@41661
   625
immler@69681
   626
proposition measurable_fun_upd:
hoelzl@61359
   627
  assumes I: "I = J \<union> {i}"
hoelzl@61359
   628
  assumes f[measurable]: "f \<in> measurable N (PiM J M)"
hoelzl@61359
   629
  assumes h[measurable]: "h \<in> measurable N (M i)"
hoelzl@61359
   630
  shows "(\<lambda>x. (f x) (i := h x)) \<in> measurable N (PiM I M)"
immler@69681
   631
proof (intro measurable_PiM_single')
hoelzl@61359
   632
  fix j assume "j \<in> I" then show "(\<lambda>\<omega>. ((f \<omega>)(i := h \<omega>)) j) \<in> measurable N (M j)"
hoelzl@61359
   633
    unfolding I by (cases "j = i") auto
hoelzl@61359
   634
next
hoelzl@61359
   635
  show "(\<lambda>x. (f x)(i := h x)) \<in> space N \<rightarrow> (\<Pi>\<^sub>E i\<in>I. space (M i))"
hoelzl@61359
   636
    using I f[THEN measurable_space] h[THEN measurable_space]
hoelzl@61359
   637
    by (auto simp: space_PiM PiE_iff extensional_def)
hoelzl@61359
   638
qed
hoelzl@61359
   639
immler@69681
   640
lemma measurable_component_update:
wenzelm@53015
   641
  "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
   642
  by simp
hoelzl@50003
   643
immler@69681
   644
lemma measurable_merge[measurable]:
wenzelm@53015
   645
  "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
   646
    (is "?f \<in> measurable ?P ?U")
immler@69681
   647
proof (rule measurable_PiM_single)
hoelzl@47694
   648
  fix i A assume A: "A \<in> sets (M i)" "i \<in> I \<union> J"
hoelzl@49780
   649
  then have "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} =
hoelzl@47694
   650
    (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
   651
    by (auto simp: merge_def)
hoelzl@47694
   652
  also have "\<dots> \<in> sets ?P"
hoelzl@47694
   653
    using A
hoelzl@47694
   654
    by (auto intro!: measurable_sets[OF measurable_comp, OF _ measurable_component_singleton])
hoelzl@49780
   655
  finally show "{\<omega> \<in> space ?P. merge I J \<omega> i \<in> A} \<in> sets ?P" .
hoelzl@50123
   656
qed (auto simp: space_pair_measure space_PiM PiE_iff merge_def extensional_def)
hoelzl@42988
   657
immler@69681
   658
lemma measurable_restrict[measurable (raw)]:
hoelzl@47694
   659
  assumes X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable N (M i)"
wenzelm@53015
   660
  shows "(\<lambda>x. \<lambda>i\<in>I. X i x) \<in> measurable N (Pi\<^sub>M I M)"
hoelzl@47694
   661
proof (rule measurable_PiM_single)
hoelzl@47694
   662
  fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
hoelzl@47694
   663
  then have "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} = X i -` A \<inter> space N"
hoelzl@47694
   664
    by auto
hoelzl@47694
   665
  then show "{\<omega> \<in> space N. (\<lambda>i\<in>I. X i \<omega>) i \<in> A} \<in> sets N"
hoelzl@47694
   666
    using A X by (auto intro!: measurable_sets)
hoelzl@50123
   667
qed (insert X, auto simp add: PiE_def dest: measurable_space)
hoelzl@47694
   668
immler@69681
   669
lemma measurable_abs_UNIV:
hoelzl@57025
   670
  "(\<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
   671
  by (intro measurable_PiM_single) (auto dest: measurable_space)
hoelzl@57025
   672
immler@69681
   673
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
   674
  by (intro measurable_restrict measurable_component_singleton) auto
immler@50038
   675
immler@69681
   676
lemma measurable_restrict_subset':
hoelzl@59425
   677
  assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
hoelzl@59425
   678
  shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
hoelzl@59425
   679
proof-
hoelzl@59425
   680
  from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
hoelzl@59425
   681
    by (rule measurable_restrict_subset)
hoelzl@59425
   682
  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
   683
    by (intro sets_PiM_cong measurable_cong_sets) simp_all
hoelzl@59425
   684
  finally show ?thesis .
hoelzl@59425
   685
qed
hoelzl@59425
   686
immler@69681
   687
lemma measurable_prod_emb[intro, simp]:
wenzelm@53015
   688
  "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
   689
  unfolding prod_emb_def space_PiM[symmetric]
immler@50038
   690
  by (auto intro!: measurable_sets measurable_restrict measurable_component_singleton)
immler@50038
   691
immler@69681
   692
lemma merge_in_prod_emb:
hoelzl@61359
   693
  assumes "y \<in> space (PiM I M)" "x \<in> X" and X: "X \<in> sets (Pi\<^sub>M J M)" and "J \<subseteq> I"
hoelzl@61359
   694
  shows "merge J I (x, y) \<in> prod_emb I M J X"
hoelzl@61359
   695
  using assms sets.sets_into_space[OF X]
hoelzl@61359
   696
  by (simp add: merge_def prod_emb_def subset_eq space_PiM PiE_def extensional_restrict Pi_iff
hoelzl@61359
   697
           cong: if_cong restrict_cong)
hoelzl@61359
   698
     (simp add: extensional_def)
hoelzl@61359
   699
immler@69681
   700
lemma prod_emb_eq_emptyD:
hoelzl@61359
   701
  assumes J: "J \<subseteq> I" and ne: "space (PiM I M) \<noteq> {}" and X: "X \<in> sets (Pi\<^sub>M J M)"
hoelzl@61359
   702
    and *: "prod_emb I M J X = {}"
hoelzl@61359
   703
  shows "X = {}"
hoelzl@61359
   704
proof safe
hoelzl@61359
   705
  fix x assume "x \<in> X"
hoelzl@61359
   706
  obtain \<omega> where "\<omega> \<in> space (PiM I M)"
hoelzl@61359
   707
    using ne by blast
hoelzl@62975
   708
  from merge_in_prod_emb[OF this \<open>x\<in>X\<close> X J] * show "x \<in> {}" by auto
hoelzl@61359
   709
qed
hoelzl@61359
   710
immler@69681
   711
lemma sets_in_Pi_aux:
hoelzl@50003
   712
  "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
   713
  {x\<in>space (PiM I M). x \<in> Pi I F} \<in> sets (PiM I M)"
hoelzl@50003
   714
  by (simp add: subset_eq Pi_iff)
hoelzl@50003
   715
immler@69681
   716
lemma sets_in_Pi[measurable (raw)]:
hoelzl@50003
   717
  "finite I \<Longrightarrow> f \<in> measurable N (PiM I M) \<Longrightarrow>
hoelzl@50003
   718
  (\<And>j. j \<in> I \<Longrightarrow> {x\<in>space (M j). x \<in> F j} \<in> sets (M j)) \<Longrightarrow>
hoelzl@50387
   719
  Measurable.pred N (\<lambda>x. f x \<in> Pi I F)"
hoelzl@50003
   720
  unfolding pred_def
hoelzl@50003
   721
  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_Pi_aux]) auto
hoelzl@50003
   722
immler@69681
   723
lemma sets_in_extensional_aux:
hoelzl@50003
   724
  "{x\<in>space (PiM I M). x \<in> extensional I} \<in> sets (PiM I M)"
hoelzl@50003
   725
proof -
hoelzl@50003
   726
  have "{x\<in>space (PiM I M). x \<in> extensional I} = space (PiM I M)"
hoelzl@50003
   727
    by (auto simp add: extensional_def space_PiM)
hoelzl@50003
   728
  then show ?thesis by simp
hoelzl@50003
   729
qed
hoelzl@50003
   730
immler@69681
   731
lemma sets_in_extensional[measurable (raw)]:
hoelzl@50387
   732
  "f \<in> measurable N (PiM I M) \<Longrightarrow> Measurable.pred N (\<lambda>x. f x \<in> extensional I)"
hoelzl@50003
   733
  unfolding pred_def
hoelzl@50003
   734
  by (rule measurable_sets_Collect[of f N "PiM I M", OF _ sets_in_extensional_aux]) auto
hoelzl@50003
   735
immler@69681
   736
lemma sets_PiM_I_countable:
hoelzl@61363
   737
  assumes I: "countable I" and E: "\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i)" shows "Pi\<^sub>E I E \<in> sets (Pi\<^sub>M I M)"
hoelzl@61363
   738
proof cases
hoelzl@61363
   739
  assume "I \<noteq> {}"
wenzelm@64910
   740
  then have "Pi\<^sub>E I E = (\<Inter>i\<in>I. prod_emb I M {i} (Pi\<^sub>E {i} E))"
hoelzl@61363
   741
    using E[THEN sets.sets_into_space] by (auto simp: PiE_iff prod_emb_def fun_eq_iff)
hoelzl@61363
   742
  also have "\<dots> \<in> sets (PiM I M)"
hoelzl@61363
   743
    using I \<open>I \<noteq> {}\<close> by (safe intro!: sets.countable_INT' measurable_prod_emb sets_PiM_I_finite E)
hoelzl@61363
   744
  finally show ?thesis .
hoelzl@61363
   745
qed (simp add: sets_PiM_empty)
hoelzl@61363
   746
immler@69681
   747
lemma sets_PiM_D_countable:
hoelzl@61363
   748
  assumes A: "A \<in> PiM I M"
hoelzl@61363
   749
  shows "\<exists>J\<subseteq>I. \<exists>X\<in>PiM J M. countable J \<and> A = prod_emb I M J X"
hoelzl@61363
   750
  using A[unfolded sets_PiM_single]
immler@69681
   751
proof induction
hoelzl@61363
   752
  case (Basic A)
hoelzl@61363
   753
  then obtain i X where *: "i \<in> I" "X \<in> sets (M i)" and "A = {f \<in> \<Pi>\<^sub>E i\<in>I. space (M i). f i \<in> X}"
hoelzl@61363
   754
    by auto
hoelzl@61363
   755
  then have A: "A = prod_emb I M {i} (\<Pi>\<^sub>E _\<in>{i}. X)"
hoelzl@61363
   756
    by (auto simp: prod_emb_def)
hoelzl@61363
   757
  then show ?case
hoelzl@61363
   758
    by (intro exI[of _ "{i}"] conjI bexI[of _ "\<Pi>\<^sub>E _\<in>{i}. X"])
hoelzl@61363
   759
       (auto intro: countable_finite * sets_PiM_I_finite)
hoelzl@61363
   760
next
hoelzl@61363
   761
  case Empty then show ?case
hoelzl@61363
   762
    by (intro exI[of _ "{}"] conjI bexI[of _ "{}"]) auto
hoelzl@61363
   763
next
hoelzl@61363
   764
  case (Compl A)
hoelzl@61363
   765
  then obtain J X where "J \<subseteq> I" "X \<in> sets (Pi\<^sub>M J M)" "countable J" "A = prod_emb I M J X"
hoelzl@61363
   766
    by auto
hoelzl@61363
   767
  then show ?case
hoelzl@61363
   768
    by (intro exI[of _ J] bexI[of _ "space (PiM J M) - X"] conjI)
hoelzl@61363
   769
       (auto simp add: space_PiM prod_emb_PiE intro!: sets_PiM_I_countable)
hoelzl@61363
   770
next
hoelzl@61363
   771
  case (Union K)
hoelzl@61363
   772
  obtain J X where J: "\<And>i. J i \<subseteq> I" "\<And>i. countable (J i)" and X: "\<And>i. X i \<in> sets (Pi\<^sub>M (J i) M)"
hoelzl@61363
   773
    and K: "\<And>i. K i = prod_emb I M (J i) (X i)"
hoelzl@61363
   774
    by (metis Union.IH)
hoelzl@61363
   775
  show ?case
hoelzl@61363
   776
  proof (intro exI[of _ "\<Union>i. J i"] bexI[of _ "\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i)"] conjI)
hoelzl@61363
   777
    show "(\<Union>i. J i) \<subseteq> I" "countable (\<Union>i. J i)" using J by auto
haftmann@69313
   778
    with J show "\<Union>(K ` UNIV) = prod_emb I M (\<Union>i. J i) (\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i))"
hoelzl@61363
   779
      by (simp add: K[abs_def] SUP_upper)
hoelzl@61363
   780
  qed(auto intro: X)
hoelzl@61363
   781
qed
hoelzl@61363
   782
immler@69681
   783
proposition measure_eqI_PiM_finite:
hoelzl@61362
   784
  assumes [simp]: "finite I" "sets P = PiM I M" "sets Q = PiM I M"
hoelzl@61362
   785
  assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = Q (Pi\<^sub>E I A)"
hoelzl@61362
   786
  assumes A: "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = space (PiM I M)" "\<And>i::nat. P (A i) \<noteq> \<infinity>"
hoelzl@61362
   787
  shows "P = Q"
immler@69681
   788
proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
hoelzl@61362
   789
  show "range A \<subseteq> prod_algebra I M" "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. P (A i) \<noteq> \<infinity>"
hoelzl@61362
   790
    unfolding space_PiM[symmetric] by fact+
hoelzl@61362
   791
  fix X assume "X \<in> prod_algebra I M"
wenzelm@64910
   792
  then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
hoelzl@61362
   793
    and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
hoelzl@61362
   794
    by (force elim!: prod_algebraE)
hoelzl@61362
   795
  then show "emeasure P X = emeasure Q X"
hoelzl@61362
   796
    unfolding X by (subst (1 2) prod_emb_Pi) (auto simp: eq)
hoelzl@61362
   797
qed (simp_all add: sets_PiM)
hoelzl@61362
   798
immler@69681
   799
proposition measure_eqI_PiM_infinite:
hoelzl@61362
   800
  assumes [simp]: "sets P = PiM I M" "sets Q = PiM I M"
hoelzl@61362
   801
  assumes eq: "\<And>A J. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>i. i \<in> J \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow>
hoelzl@61362
   802
    P (prod_emb I M J (Pi\<^sub>E J A)) = Q (prod_emb I M J (Pi\<^sub>E J A))"
hoelzl@61362
   803
  assumes A: "finite_measure P"
hoelzl@61362
   804
  shows "P = Q"
immler@69681
   805
proof (rule measure_eqI_generator_eq[OF Int_stable_prod_algebra prod_algebra_sets_into_space])
hoelzl@61362
   806
  interpret finite_measure P by fact
wenzelm@63040
   807
  define i where "i = (SOME i. i \<in> I)"
hoelzl@61362
   808
  have i: "I \<noteq> {} \<Longrightarrow> i \<in> I"
hoelzl@61362
   809
    unfolding i_def by (rule someI_ex) auto
wenzelm@63040
   810
  define A where "A n =
wenzelm@63040
   811
    (if I = {} then prod_emb I M {} (\<Pi>\<^sub>E i\<in>{}. {}) else prod_emb I M {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)))"
wenzelm@63040
   812
    for n :: nat
hoelzl@61362
   813
  then show "range A \<subseteq> prod_algebra I M"
hoelzl@61362
   814
    using prod_algebraI[of "{}" I "\<lambda>i. space (M i)" M] by (auto intro!: prod_algebraI i)
hoelzl@61362
   815
  have "\<And>i. A i = space (PiM I M)"
hoelzl@61362
   816
    by (auto simp: prod_emb_def space_PiM PiE_iff A_def i ex_in_conv[symmetric] exI)
hoelzl@61362
   817
  then show "(\<Union>i. A i) = (\<Pi>\<^sub>E i\<in>I. space (M i))" "\<And>i. emeasure P (A i) \<noteq> \<infinity>"
hoelzl@61362
   818
    by (auto simp: space_PiM)
hoelzl@61362
   819
next
hoelzl@61362
   820
  fix X assume X: "X \<in> prod_algebra I M"
wenzelm@64910
   821
  then obtain J E where X: "X = prod_emb I M J (\<Pi>\<^sub>E j\<in>J. E j)"
hoelzl@61362
   822
    and J: "finite J" "J \<subseteq> I" "\<And>j. j \<in> J \<Longrightarrow> E j \<in> sets (M j)"
hoelzl@61362
   823
    by (force elim!: prod_algebraE)
hoelzl@61362
   824
  then show "emeasure P X = emeasure Q X"
hoelzl@61362
   825
    by (auto intro!: eq)
hoelzl@61362
   826
qed (auto simp: sets_PiM)
hoelzl@61362
   827
ak2110@68833
   828
locale%unimportant product_sigma_finite =
hoelzl@47694
   829
  fixes M :: "'i \<Rightarrow> 'a measure"
hoelzl@41689
   830
  assumes sigma_finite_measures: "\<And>i. sigma_finite_measure (M i)"
hoelzl@40859
   831
ak2110@68833
   832
sublocale%unimportant product_sigma_finite \<subseteq> M?: sigma_finite_measure "M i" for i
hoelzl@40859
   833
  by (rule sigma_finite_measures)
hoelzl@40859
   834
ak2110@68833
   835
locale%unimportant finite_product_sigma_finite = product_sigma_finite M for M :: "'i \<Rightarrow> 'a measure" +
hoelzl@47694
   836
  fixes I :: "'i set"
hoelzl@47694
   837
  assumes finite_index: "finite I"
hoelzl@41689
   838
immler@69681
   839
proposition (in finite_product_sigma_finite) sigma_finite_pairs:
hoelzl@40859
   840
  "\<exists>F::'i \<Rightarrow> nat \<Rightarrow> 'a set.
hoelzl@40859
   841
    (\<forall>i\<in>I. range (F i) \<subseteq> sets (M i)) \<and>
wenzelm@53015
   842
    (\<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
   843
    (\<Union>k. \<Pi>\<^sub>E i\<in>I. F i k) = space (PiM I M)"
immler@69681
   844
proof -
hoelzl@47694
   845
  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
   846
    using M.sigma_finite_incseq by metis
hoelzl@40859
   847
  from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
hoelzl@47694
   848
  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
   849
    by auto
wenzelm@53015
   850
  let ?F = "\<lambda>k. \<Pi>\<^sub>E i\<in>I. F i k"
hoelzl@47694
   851
  note space_PiM[simp]
hoelzl@40859
   852
  show ?thesis
hoelzl@41981
   853
  proof (intro exI[of _ F] conjI allI incseq_SucI set_eqI iffI ballI)
hoelzl@40859
   854
    fix i show "range (F i) \<subseteq> sets (M i)" by fact
hoelzl@40859
   855
  next
hoelzl@47694
   856
    fix i k show "emeasure (M i) (F i k) \<noteq> \<infinity>" by fact
hoelzl@40859
   857
  next
hoelzl@50123
   858
    fix x assume "x \<in> (\<Union>i. ?F i)" with F(1) show "x \<in> space (PiM I M)"
immler@50244
   859
      by (auto simp: PiE_def dest!: sets.sets_into_space)
hoelzl@40859
   860
  next
hoelzl@47694
   861
    fix f assume "f \<in> space (PiM I M)"
hoelzl@41981
   862
    with Pi_UN[OF finite_index, of "\<lambda>k i. F i k"] F
hoelzl@50123
   863
    show "f \<in> (\<Union>i. ?F i)" by (auto simp: incseq_def PiE_def)
hoelzl@40859
   864
  next
hoelzl@40859
   865
    fix i show "?F i \<subseteq> ?F (Suc i)"
wenzelm@61808
   866
      using \<open>\<And>i. incseq (F i)\<close>[THEN incseq_SucD] by auto
hoelzl@40859
   867
  qed
hoelzl@40859
   868
qed
hoelzl@40859
   869
immler@69681
   870
lemma emeasure_PiM_empty[simp]: "emeasure (PiM {} M) {\<lambda>_. undefined} = 1"
hoelzl@49780
   871
proof -
hoelzl@62975
   872
  let ?\<mu> = "\<lambda>A. if A = {} then 0 else (1::ennreal)"
wenzelm@53015
   873
  have "emeasure (Pi\<^sub>M {} M) (prod_emb {} M {} (\<Pi>\<^sub>E i\<in>{}. {})) = 1"
hoelzl@49780
   874
  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
hoelzl@49780
   875
    show "positive (PiM {} M) ?\<mu>"
hoelzl@49780
   876
      by (auto simp: positive_def)
hoelzl@49780
   877
    show "countably_additive (PiM {} M) ?\<mu>"
immler@50244
   878
      by (rule sets.countably_additiveI_finite)
hoelzl@49780
   879
         (auto simp: additive_def positive_def sets_PiM_empty space_PiM_empty intro!: )
hoelzl@49780
   880
  qed (auto simp: prod_emb_def)
wenzelm@53015
   881
  also have "(prod_emb {} M {} (\<Pi>\<^sub>E i\<in>{}. {})) = {\<lambda>_. undefined}"
hoelzl@49780
   882
    by (auto simp: prod_emb_def)
hoelzl@49780
   883
  finally show ?thesis
hoelzl@49780
   884
    by simp
hoelzl@49780
   885
qed
hoelzl@49780
   886
immler@69681
   887
lemma PiM_empty: "PiM {} M = count_space {\<lambda>_. undefined}"
hoelzl@62975
   888
  by (rule measure_eqI) (auto simp add: sets_PiM_empty)
hoelzl@49780
   889
immler@69681
   890
lemma (in product_sigma_finite) emeasure_PiM:
wenzelm@53015
   891
  "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))"
immler@69681
   892
proof (induct I arbitrary: A rule: finite_induct)
hoelzl@40859
   893
  case (insert i I)
wenzelm@61169
   894
  interpret finite_product_sigma_finite M I by standard fact
wenzelm@61808
   895
  have "finite (insert i I)" using \<open>finite I\<close> by auto
wenzelm@61169
   896
  interpret I': finite_product_sigma_finite M "insert i I" by standard fact
hoelzl@41661
   897
  let ?h = "(\<lambda>(f, y). f(i := y))"
hoelzl@47694
   898
wenzelm@53015
   899
  let ?P = "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M) ?h"
hoelzl@47694
   900
  let ?\<mu> = "emeasure ?P"
hoelzl@47694
   901
  let ?I = "{j \<in> insert i I. emeasure (M j) (space (M j)) \<noteq> 1}"
hoelzl@47694
   902
  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
   903
wenzelm@53015
   904
  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
   905
    (\<Prod>i\<in>insert i I. emeasure (M i) (A i))"
hoelzl@49776
   906
  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
hoelzl@49776
   907
    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
   908
    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
   909
    let ?p = "prod_emb (insert i I) M J (Pi\<^sub>E J E)"
wenzelm@53015
   910
    let ?p' = "prod_emb I M (J - {i}) (\<Pi>\<^sub>E j\<in>J-{i}. E j)"
hoelzl@49776
   911
    have "?\<mu> ?p =
wenzelm@53015
   912
      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
   913
      by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
wenzelm@53015
   914
    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
   915
      using J E[rule_format, THEN sets.sets_into_space]
nipkow@62390
   916
      by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: if_split_asm)
wenzelm@53015
   917
    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
   918
      emeasure (Pi\<^sub>M I M) ?p' * emeasure (M i) (if i \<in> J then (E i) else space (M i))"
hoelzl@49776
   919
      using J E by (intro M.emeasure_pair_measure_Times sets_PiM_I) auto
wenzelm@53015
   920
    also have "?p' = (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j))"
immler@50244
   921
      using J E[rule_format, THEN sets.sets_into_space]
nipkow@62390
   922
      by (auto simp: prod_emb_iff PiE_def Pi_iff split: if_split_asm) blast+
wenzelm@53015
   923
    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
   924
      (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
nipkow@64272
   925
      using E by (subst insert) (auto intro!: prod.cong)
hoelzl@49776
   926
    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
   927
       emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
nipkow@69064
   928
      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
hoelzl@49776
   929
    also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
nipkow@64272
   930
      using insert(1,2) J E by (intro prod.mono_neutral_right) auto
hoelzl@49776
   931
    finally show "?\<mu> ?p = \<dots>" .
hoelzl@47694
   932
wenzelm@53015
   933
    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
   934
      using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
hoelzl@49776
   935
  next
wenzelm@53015
   936
    show "positive (sets (Pi\<^sub>M (insert i I) M)) ?\<mu>" "countably_additive (sets (Pi\<^sub>M (insert i I) M)) ?\<mu>"
hoelzl@49776
   937
      using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
hoelzl@49776
   938
  next
hoelzl@49776
   939
    show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
hoelzl@49776
   940
      insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
hoelzl@49776
   941
      using insert by auto
nipkow@64272
   942
  qed (auto intro!: prod.cong)
hoelzl@49776
   943
  with insert show ?case
immler@50244
   944
    by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
hoelzl@50003
   945
qed simp
hoelzl@47694
   946
immler@69681
   947
lemma (in product_sigma_finite) PiM_eqI:
hoelzl@61362
   948
  assumes I[simp]: "finite I" and P: "sets P = PiM I M"
hoelzl@61359
   949
  assumes eq: "\<And>A. (\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> P (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
hoelzl@61359
   950
  shows "P = PiM I M"
hoelzl@61359
   951
proof -
hoelzl@61359
   952
  interpret finite_product_sigma_finite M I
hoelzl@61359
   953
    proof qed fact
hoelzl@61359
   954
  from sigma_finite_pairs guess C .. note C = this
hoelzl@61359
   955
  show ?thesis
hoelzl@61362
   956
  proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric])
hoelzl@61362
   957
    show "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>M I M) (Pi\<^sub>E I A) = P (Pi\<^sub>E I A)" for A
hoelzl@61362
   958
      by (simp add: eq emeasure_PiM)
wenzelm@63040
   959
    define A where "A n = (\<Pi>\<^sub>E i\<in>I. C i n)" for n
hoelzl@61362
   960
    with C show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>" "(\<Union>i. A i) = space (PiM I M)"
nipkow@64272
   961
      by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_prod_eq_top)
hoelzl@61359
   962
  qed
hoelzl@61359
   963
qed
hoelzl@61359
   964
immler@69681
   965
lemma (in product_sigma_finite) sigma_finite:
hoelzl@49776
   966
  assumes "finite I"
hoelzl@49776
   967
  shows "sigma_finite_measure (PiM I M)"
hoelzl@57447
   968
proof
wenzelm@61169
   969
  interpret finite_product_sigma_finite M I by standard fact
hoelzl@49776
   970
hoelzl@57447
   971
  obtain F where F: "\<And>j. countable (F j)" "\<And>j f. f \<in> F j \<Longrightarrow> f \<in> sets (M j)"
hoelzl@57447
   972
    "\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
nipkow@69745
   973
    in_space: "\<And>j. space (M j) = \<Union>(F j)"
hoelzl@57447
   974
    using sigma_finite_countable by (metis subset_eq)
wenzelm@64910
   975
  moreover have "(\<Union>(Pi\<^sub>E I ` Pi\<^sub>E I F)) = space (Pi\<^sub>M I M)"
hoelzl@57447
   976
    using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
hoelzl@57447
   977
  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>)"
wenzelm@64910
   978
    by (intro exI[of _ "Pi\<^sub>E I ` Pi\<^sub>E I F"])
hoelzl@57447
   979
       (auto intro!: countable_PiE sets_PiM_I_finite
nipkow@64272
   980
             simp: PiE_iff emeasure_PiM finite_index ennreal_prod_eq_top)
hoelzl@40859
   981
qed
hoelzl@40859
   982
wenzelm@53015
   983
sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^sub>M I M"
hoelzl@47694
   984
  using sigma_finite[OF finite_index] .
hoelzl@40859
   985
immler@69681
   986
lemma (in finite_product_sigma_finite) measure_times:
wenzelm@53015
   987
  "(\<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
   988
  using emeasure_PiM[OF finite_index] by auto
hoelzl@41096
   989
immler@69681
   990
lemma (in product_sigma_finite) nn_integral_empty:
hoelzl@61359
   991
  "0 \<le> f (\<lambda>k. undefined) \<Longrightarrow> integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
hoelzl@61359
   992
  by (simp add: PiM_empty nn_integral_count_space_finite max.absorb2)
hoelzl@40859
   993
ak2110@68833
   994
lemma%important (in product_sigma_finite) distr_merge:
hoelzl@40859
   995
  assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
wenzelm@53015
   996
  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
   997
   (is "?D = ?P")
immler@69681
   998
proof (rule PiM_eqI)
wenzelm@61169
   999
  interpret I: finite_product_sigma_finite M I by standard fact
wenzelm@61169
  1000
  interpret J: finite_product_sigma_finite M J by standard fact
hoelzl@61359
  1001
  fix A assume A: "\<And>i. i \<in> I \<union> J \<Longrightarrow> A i \<in> sets (M i)"
wenzelm@64910
  1002
  have *: "(merge I J -` Pi\<^sub>E (I \<union> J) A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)) = Pi\<^sub>E I A \<times> Pi\<^sub>E J A"
hoelzl@61359
  1003
    using A[THEN sets.sets_into_space] by (auto simp: space_PiM space_pair_measure)
hoelzl@61359
  1004
  from A fin show "emeasure (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>E (I \<union> J) A) =
hoelzl@61359
  1005
      (\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
hoelzl@61359
  1006
    by (subst emeasure_distr)
nipkow@64272
  1007
       (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint)
hoelzl@61359
  1008
qed (insert fin, simp_all)
hoelzl@41026
  1009
immler@69681
  1010
proposition (in product_sigma_finite) product_nn_integral_fold:
hoelzl@47694
  1011
  assumes IJ: "I \<inter> J = {}" "finite I" "finite J"
hoelzl@62975
  1012
  and f[measurable]: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
hoelzl@56996
  1013
  shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
wenzelm@53015
  1014
    (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
immler@69681
  1015
proof -
wenzelm@61169
  1016
  interpret I: finite_product_sigma_finite M I by standard fact
wenzelm@61169
  1017
  interpret J: finite_product_sigma_finite M J by standard fact
wenzelm@61169
  1018
  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
wenzelm@53015
  1019
  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
  1020
    using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
hoelzl@41661
  1021
  show ?thesis
hoelzl@47694
  1022
    apply (subst distr_merge[OF IJ, symmetric])
hoelzl@62975
  1023
    apply (subst nn_integral_distr[OF measurable_merge])
hoelzl@62975
  1024
    apply measurable []
hoelzl@56996
  1025
    apply (subst J.nn_integral_fst[symmetric, OF P_borel])
hoelzl@47694
  1026
    apply simp
hoelzl@47694
  1027
    done
hoelzl@40859
  1028
qed
hoelzl@40859
  1029
immler@69681
  1030
lemma (in product_sigma_finite) distr_singleton:
wenzelm@53015
  1031
  "distr (Pi\<^sub>M {i} M) (M i) (\<lambda>x. x i) = M i" (is "?D = _")
hoelzl@47694
  1032
proof (intro measure_eqI[symmetric])
wenzelm@61169
  1033
  interpret I: finite_product_sigma_finite M "{i}" by standard simp
hoelzl@47694
  1034
  fix A assume A: "A \<in> sets (M i)"
wenzelm@53374
  1035
  then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
immler@50244
  1036
    using sets.sets_into_space by (auto simp: space_PiM)
wenzelm@53374
  1037
  then show "emeasure (M i) A = emeasure ?D A"
hoelzl@47694
  1038
    using A I.measure_times[of "\<lambda>_. A"]
hoelzl@47694
  1039
    by (simp add: emeasure_distr measurable_component_singleton)
hoelzl@47694
  1040
qed simp
hoelzl@41831
  1041
immler@69681
  1042
lemma (in product_sigma_finite) product_nn_integral_singleton:
hoelzl@40859
  1043
  assumes f: "f \<in> borel_measurable (M i)"
hoelzl@56996
  1044
  shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
hoelzl@40859
  1045
proof -
wenzelm@61169
  1046
  interpret I: finite_product_sigma_finite M "{i}" by standard simp
hoelzl@47694
  1047
  from f show ?thesis
hoelzl@47694
  1048
    apply (subst distr_singleton[symmetric])
hoelzl@56996
  1049
    apply (subst nn_integral_distr[OF measurable_component_singleton])
hoelzl@47694
  1050
    apply simp_all
hoelzl@47694
  1051
    done
hoelzl@40859
  1052
qed
hoelzl@40859
  1053
immler@69681
  1054
proposition (in product_sigma_finite) product_nn_integral_insert:
hoelzl@49780
  1055
  assumes I[simp]: "finite I" "i \<notin> I"
wenzelm@53015
  1056
    and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
hoelzl@56996
  1057
  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))"
immler@69681
  1058
proof -
wenzelm@61169
  1059
  interpret I: finite_product_sigma_finite M I by standard auto
wenzelm@61169
  1060
  interpret i: finite_product_sigma_finite M "{i}" by standard auto
hoelzl@41689
  1061
  have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
hoelzl@41689
  1062
    using f by auto
hoelzl@41096
  1063
  show ?thesis
hoelzl@56996
  1064
    unfolding product_nn_integral_fold[OF IJ, unfolded insert, OF I(1) i.finite_index f]
hoelzl@56996
  1065
  proof (rule nn_integral_cong, subst product_nn_integral_singleton[symmetric])
wenzelm@53015
  1066
    fix x assume x: "x \<in> space (Pi\<^sub>M I M)"
hoelzl@49780
  1067
    let ?f = "\<lambda>y. f (x(i := y))"
hoelzl@49780
  1068
    show "?f \<in> borel_measurable (M i)"
wenzelm@61808
  1069
      using measurable_comp[OF measurable_component_update f, OF x \<open>i \<notin> I\<close>]
hoelzl@47694
  1070
      unfolding comp_def .
wenzelm@53015
  1071
    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
  1072
      using x
hoelzl@56996
  1073
      by (auto intro!: nn_integral_cong arg_cong[where f=f]
hoelzl@50123
  1074
               simp add: space_PiM extensional_def PiE_def)
hoelzl@41096
  1075
  qed
hoelzl@41096
  1076
qed
hoelzl@41096
  1077
immler@69681
  1078
lemma (in product_sigma_finite) product_nn_integral_insert_rev:
hoelzl@59425
  1079
  assumes I[simp]: "finite I" "i \<notin> I"
hoelzl@59425
  1080
    and [measurable]: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
hoelzl@59425
  1081
  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
  1082
  apply (subst product_nn_integral_insert[OF assms])
hoelzl@59425
  1083
  apply (rule pair_sigma_finite.Fubini')
hoelzl@59425
  1084
  apply intro_locales []
hoelzl@59425
  1085
  apply (rule sigma_finite[OF I(1)])
hoelzl@59425
  1086
  apply measurable
hoelzl@59425
  1087
  done
hoelzl@59425
  1088
immler@69681
  1089
lemma (in product_sigma_finite) product_nn_integral_prod:
hoelzl@62975
  1090
  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
hoelzl@56996
  1091
  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@62975
  1092
using assms proof (induction I)
hoelzl@41096
  1093
  case (insert i I)
hoelzl@62975
  1094
  note insert.prems[measurable]
wenzelm@61808
  1095
  note \<open>finite I\<close>[intro, simp]
wenzelm@61169
  1096
  interpret I: finite_product_sigma_finite M I by standard auto
hoelzl@41096
  1097
  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))"
nipkow@64272
  1098
    using insert by (auto intro!: prod.cong)
wenzelm@53015
  1099
  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
  1100
    using sets.sets_into_space insert
nipkow@64272
  1101
    by (intro borel_measurable_prod_ennreal
hoelzl@41689
  1102
              measurable_comp[OF measurable_component_singleton, unfolded comp_def])
hoelzl@41096
  1103
       auto
hoelzl@41981
  1104
  then show ?case
hoelzl@62975
  1105
    apply (simp add: product_nn_integral_insert[OF insert(1,2)])
hoelzl@62975
  1106
    apply (simp add: insert(2-) * nn_integral_multc)
hoelzl@56996
  1107
    apply (subst nn_integral_cmult)
hoelzl@62975
  1108
    apply (auto simp add: insert(2-))
hoelzl@41981
  1109
    done
hoelzl@47694
  1110
qed (simp add: space_PiM)
hoelzl@41096
  1111
immler@69681
  1112
proposition (in product_sigma_finite) product_nn_integral_pair:
haftmann@61424
  1113
  assumes [measurable]: "case_prod f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
hoelzl@59425
  1114
  assumes xy: "x \<noteq> y"
hoelzl@59425
  1115
  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))"
immler@69681
  1116
proof -
hoelzl@59425
  1117
  interpret psm: pair_sigma_finite "M x" "M y"
hoelzl@59425
  1118
    unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all
hoelzl@59425
  1119
  have "{x, y} = {y, x}" by auto
hoelzl@59425
  1120
  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
  1121
    using xy by (subst product_nn_integral_insert_rev) simp_all
hoelzl@59425
  1122
  also have "... = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. f x y \<partial>M x \<partial>M y)"
hoelzl@59425
  1123
    by (intro nn_integral_cong, subst product_nn_integral_singleton) simp_all
hoelzl@59425
  1124
  also have "... = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
hoelzl@59425
  1125
    by (subst psm.nn_integral_snd[symmetric]) simp_all
hoelzl@59425
  1126
  finally show ?thesis .
hoelzl@59425
  1127
qed
hoelzl@59425
  1128
immler@69681
  1129
lemma (in product_sigma_finite) distr_component:
wenzelm@53015
  1130
  "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
hoelzl@61359
  1131
proof (intro PiM_eqI)
wenzelm@63540
  1132
  fix A assume A: "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
wenzelm@63540
  1133
  then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
lp15@65036
  1134
    by (fastforce dest: sets.sets_into_space)
wenzelm@63540
  1135
  with A show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x)) (Pi\<^sub>E {i} A) = (\<Prod>i\<in>{i}. emeasure (M i) (A i))"
hoelzl@61359
  1136
    by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
hoelzl@61359
  1137
qed simp_all
hoelzl@41026
  1138
immler@69681
  1139
lemma (in product_sigma_finite)
wenzelm@53015
  1140
  assumes IJ: "I \<inter> J = {}" "finite I" "finite J" and A: "A \<in> sets (Pi\<^sub>M (I \<union> J) M)"
hoelzl@49776
  1141
  shows emeasure_fold_integral:
wenzelm@53015
  1142
    "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
  1143
    and emeasure_fold_measurable:
wenzelm@53015
  1144
    "(\<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
  1145
proof -
wenzelm@61169
  1146
  interpret I: finite_product_sigma_finite M I by standard fact
wenzelm@61169
  1147
  interpret J: finite_product_sigma_finite M J by standard fact
wenzelm@53015
  1148
  interpret IJ: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
wenzelm@53015
  1149
  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
  1150
    by (intro measurable_sets[OF _ A] measurable_merge assms)
hoelzl@49776
  1151
hoelzl@49776
  1152
  show ?I
hoelzl@49776
  1153
    apply (subst distr_merge[symmetric, OF IJ])
hoelzl@49776
  1154
    apply (subst emeasure_distr[OF measurable_merge A])
hoelzl@49776
  1155
    apply (subst J.emeasure_pair_measure_alt[OF merge])
hoelzl@56996
  1156
    apply (auto intro!: nn_integral_cong arg_cong2[where f=emeasure] simp: space_pair_measure)
hoelzl@49776
  1157
    done
hoelzl@49776
  1158
hoelzl@49776
  1159
  show ?B
hoelzl@49776
  1160
    using IJ.measurable_emeasure_Pair1[OF merge]
haftmann@56154
  1161
    by (simp add: vimage_comp comp_def space_pair_measure cong: measurable_cong)
hoelzl@49776
  1162
qed
hoelzl@49776
  1163
immler@69681
  1164
lemma sets_Collect_single:
wenzelm@53015
  1165
  "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
  1166
  by simp
hoelzl@49776
  1167
immler@69681
  1168
lemma pair_measure_eq_distr_PiM:
hoelzl@50104
  1169
  fixes M1 :: "'a measure" and M2 :: "'a measure"
hoelzl@50104
  1170
  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
blanchet@55414
  1171
  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
  1172
    (is "?P = ?D")
hoelzl@50104
  1173
proof (rule pair_measure_eqI[OF assms])
blanchet@55414
  1174
  interpret B: product_sigma_finite "case_bool M1 M2"
hoelzl@50104
  1175
    unfolding product_sigma_finite_def using assms by (auto split: bool.split)
blanchet@55414
  1176
  let ?B = "Pi\<^sub>M UNIV (case_bool M1 M2)"
hoelzl@50104
  1177
hoelzl@50104
  1178
  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
  1179
    by auto
hoelzl@50104
  1180
  fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
blanchet@55414
  1181
  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (case_bool M1 M2 i) (case_bool A B i))"
hoelzl@50104
  1182
    by (simp add: UNIV_bool ac_simps)
blanchet@55414
  1183
  also have "\<dots> = emeasure ?B (Pi\<^sub>E UNIV (case_bool A B))"
hoelzl@50104
  1184
    using A B by (subst B.emeasure_PiM) (auto split: bool.split)
blanchet@55414
  1185
  also have "Pi\<^sub>E UNIV (case_bool A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
immler@50244
  1186
    using A[THEN sets.sets_into_space] B[THEN sets.sets_into_space]
hoelzl@50123
  1187
    by (auto simp: PiE_iff all_bool_eq space_PiM split: bool.split)
hoelzl@50104
  1188
  finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
hoelzl@50104
  1189
    using A B
blanchet@55414
  1190
      measurable_component_singleton[of True UNIV "case_bool M1 M2"]
blanchet@55414
  1191
      measurable_component_singleton[of False UNIV "case_bool M1 M2"]
hoelzl@50104
  1192
    by (subst emeasure_distr) (auto simp: measurable_pair_iff)
hoelzl@50104
  1193
qed simp
hoelzl@50104
  1194
immler@69681
  1195
lemma infprod_in_sets[intro]:
hoelzl@64008
  1196
  fixes E :: "nat \<Rightarrow> 'a set" assumes E: "\<And>i. E i \<in> sets (M i)"
hoelzl@64008
  1197
  shows "Pi UNIV E \<in> sets (\<Pi>\<^sub>M i\<in>UNIV::nat set. M i)"
hoelzl@64008
  1198
proof -
hoelzl@64008
  1199
  have "Pi UNIV E = (\<Inter>i. prod_emb UNIV M {..i} (\<Pi>\<^sub>E j\<in>{..i}. E j))"
hoelzl@64008
  1200
    using E E[THEN sets.sets_into_space]
hoelzl@64008
  1201
    by (auto simp: prod_emb_def Pi_iff extensional_def)
hoelzl@64008
  1202
  with E show ?thesis by auto
hoelzl@64008
  1203
qed
hoelzl@64008
  1204
lp15@69918
  1205
lp15@69918
  1206
lp15@69918
  1207
subsection \<open>Measurability\<close>
lp15@69918
  1208
lp15@69918
  1209
text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
lp15@69918
  1210
generated by open sets in the product, and the product sigma algebra, countably generated by
lp15@69918
  1211
products of measurable sets along finitely many coordinates. The second one is defined and studied
lp15@69918
  1212
in \<^file>\<open>Finite_Product_Measure.thy\<close>.
lp15@69918
  1213
lp15@69918
  1214
These sigma-algebra share a lot of natural properties (measurability of coordinates, for instance),
lp15@69918
  1215
but there is a fundamental difference: open sets are generated by arbitrary unions, not only
lp15@69918
  1216
countable ones, so typically many open sets will not be measurable with respect to the product sigma
lp15@69918
  1217
algebra (while all sets in the product sigma algebra are borel). The two sigma algebras coincide
lp15@69918
  1218
only when everything is countable (i.e., the product is countable, and the borel sigma algebra in
lp15@69918
  1219
the factor is countably generated).
lp15@69918
  1220
lp15@69918
  1221
In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
lp15@69918
  1222
compare it with the product sigma algebra as explained above.
lp15@69918
  1223
\<close>
lp15@69918
  1224
lp15@69918
  1225
lemma measurable_product_coordinates [measurable (raw)]:
lp15@69918
  1226
  "(\<lambda>x. x i) \<in> measurable borel borel"
lp15@69918
  1227
by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
lp15@69918
  1228
lp15@69918
  1229
lemma measurable_product_then_coordinatewise:
lp15@69918
  1230
  fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
lp15@69918
  1231
  assumes [measurable]: "f \<in> borel_measurable M"
lp15@69918
  1232
  shows "(\<lambda>x. f x i) \<in> borel_measurable M"
lp15@69918
  1233
proof -
lp15@69918
  1234
  have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f"
lp15@69918
  1235
    unfolding comp_def by auto
lp15@69918
  1236
  then show ?thesis by simp
lp15@69918
  1237
qed
lp15@69918
  1238
lp15@69918
  1239
text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
lp15@69918
  1240
of the product sigma algebra that is more similar to the one we used above for the product
lp15@69918
  1241
topology.\<close>
lp15@69918
  1242
lp15@69918
  1243
lemma sets_PiM_finite:
lp15@69918
  1244
  "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
lp15@69918
  1245
        {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
lp15@69918
  1246
proof
lp15@69918
  1247
  have "{(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}} \<subseteq> sets (Pi\<^sub>M I M)"
lp15@69918
  1248
  proof (auto)
lp15@69918
  1249
    fix X assume H: "\<forall>i. X i \<in> sets (M i)" "finite {i. X i \<noteq> space (M i)}"
lp15@69918
  1250
    then have *: "X i \<in> sets (M i)" for i by simp
lp15@69918
  1251
    define J where "J = {i \<in> I. X i \<noteq> space (M i)}"
lp15@69918
  1252
    have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
lp15@69918
  1253
    define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
lp15@69918
  1254
    have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
lp15@69918
  1255
      unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
lp15@69918
  1256
    moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
lp15@69918
  1257
      unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
lp15@69918
  1258
      by (auto simp add: PiE_iff, blast)
lp15@69918
  1259
    ultimately show "Pi\<^sub>E I X \<in> sets (Pi\<^sub>M I M)" by simp
lp15@69918
  1260
  qed
lp15@69918
  1261
  then show "sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}
lp15@69918
  1262
              \<subseteq> sets (Pi\<^sub>M I M)"
lp15@69918
  1263
    by (metis (mono_tags, lifting) sets.sigma_sets_subset' sets.top space_PiM)
lp15@69918
  1264
lp15@69918
  1265
  have *: "\<exists>X. {f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X \<and>
lp15@69918
  1266
                (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}"
lp15@69918
  1267
    if "i \<in> I" "A \<in> sets (M i)" for i A
lp15@69918
  1268
  proof -
lp15@69918
  1269
    define X where "X = (\<lambda>j. if j = i then A else space (M j))"
lp15@69918
  1270
    have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
lp15@69918
  1271
      unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
lp15@69918
  1272
      by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
lp15@69918
  1273
    moreover have "X j \<in> sets (M j)" for j
lp15@69918
  1274
      unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
lp15@69918
  1275
    moreover have "finite {j. X j \<noteq> space (M j)}"
lp15@69918
  1276
      unfolding X_def by simp
lp15@69918
  1277
    ultimately show ?thesis by auto
lp15@69918
  1278
  qed
lp15@69918
  1279
  show "sets (Pi\<^sub>M I M) \<subseteq> sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i)) {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. X i \<in> sets (M i)) \<and> finite {i. X i \<noteq> space (M i)}}"
lp15@69918
  1280
    unfolding sets_PiM_single
lp15@69918
  1281
    apply (rule sigma_sets_mono')
lp15@69918
  1282
    apply (auto simp add: PiE_iff *)
lp15@69918
  1283
    done
lp15@69918
  1284
qed
lp15@69918
  1285
lp15@69918
  1286
lemma sets_PiM_subset_borel:
lp15@69918
  1287
  "sets (Pi\<^sub>M UNIV (\<lambda>_. borel)) \<subseteq> sets borel"
lp15@69918
  1288
proof -
lp15@69918
  1289
  have *: "Pi\<^sub>E UNIV X \<in> sets borel" if [measurable]: "\<And>i. X i \<in> sets borel" "finite {i. X i \<noteq> UNIV}" for X::"'a \<Rightarrow> 'b set"
lp15@69918
  1290
  proof -
lp15@69918
  1291
    define I where "I = {i. X i \<noteq> UNIV}"
lp15@69918
  1292
    have "finite I" unfolding I_def using that by simp
lp15@69918
  1293
    have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
lp15@69918
  1294
      unfolding I_def by auto
lp15@69918
  1295
    also have "... \<in> sets borel"
lp15@69918
  1296
      using that \<open>finite I\<close> by measurable
lp15@69918
  1297
    finally show ?thesis by simp
lp15@69918
  1298
  qed
lp15@69918
  1299
  then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
lp15@69918
  1300
    by auto
lp15@69918
  1301
  then show ?thesis unfolding sets_PiM_finite space_borel
lp15@69918
  1302
    by (simp add: * sets.sigma_sets_subset')
lp15@69918
  1303
qed
lp15@69918
  1304
lp15@69918
  1305
proposition sets_PiM_equal_borel:
lp15@69918
  1306
  "sets (Pi\<^sub>M UNIV (\<lambda>i::('a::countable). borel::('b::second_countable_topology measure))) = sets borel"
lp15@69918
  1307
proof
lp15@69918
  1308
  obtain K::"('a \<Rightarrow> 'b) set set" where K: "topological_basis K" "countable K"
lp15@69918
  1309
            "\<And>k. k \<in> K \<Longrightarrow> \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
lp15@69918
  1310
    using product_topology_countable_basis by fast
lp15@69918
  1311
  have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
lp15@69918
  1312
  proof -
lp15@69918
  1313
    obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
lp15@69918
  1314
      using K(3)[OF \<open>k \<in> K\<close>] by blast
lp15@69918
  1315
    show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
lp15@69918
  1316
  qed
lp15@69918
  1317
  have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
lp15@69918
  1318
  proof -
lp15@69918
  1319
    obtain B where "B \<subseteq> K" "U = (\<Union>B)"
lp15@69918
  1320
      using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
lp15@69918
  1321
    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
lp15@69918
  1322
    moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
lp15@69918
  1323
      using \<open>B \<subseteq> K\<close> * that by auto
lp15@69918
  1324
    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
lp15@69918
  1325
  qed
lp15@69918
  1326
  have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
lp15@69918
  1327
    apply (rule sets.sigma_sets_subset') using ** by auto
lp15@69918
  1328
  then show "sets (borel::('a \<Rightarrow> 'b) measure) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))"
lp15@69918
  1329
    unfolding borel_def by auto
lp15@69918
  1330
qed (simp add: sets_PiM_subset_borel)
lp15@69918
  1331
lp15@69918
  1332
lemma measurable_coordinatewise_then_product:
lp15@69918
  1333
  fixes f::"'a \<Rightarrow> ('b::countable) \<Rightarrow> ('c::second_countable_topology)"
lp15@69918
  1334
  assumes [measurable]: "\<And>i. (\<lambda>x. f x i) \<in> borel_measurable M"
lp15@69918
  1335
  shows "f \<in> borel_measurable M"
lp15@69918
  1336
proof -
lp15@69918
  1337
  have "f \<in> measurable M (Pi\<^sub>M UNIV (\<lambda>_. borel))"
lp15@69918
  1338
    by (rule measurable_PiM_single', auto simp add: assms)
lp15@69918
  1339
  then show ?thesis using sets_PiM_equal_borel measurable_cong_sets by blast
lp15@69918
  1340
qed
lp15@69918
  1341
lp15@69918
  1342
hoelzl@47694
  1343
end