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