src/HOL/Probability/Product_Measure.thy
author hoelzl
Fri Aug 27 14:05:16 2010 +0200 (2010-08-27)
changeset 39088 ca17017c10e6
parent 39082 54dbe0368dc6
child 39092 98de40859858
child 39095 f92b7e2877c2
permissions -rw-r--r--
Measurable on product space is equiv. to measurable components
hoelzl@35833
     1
theory Product_Measure
hoelzl@38656
     2
imports Lebesgue_Integration
hoelzl@35833
     3
begin
hoelzl@35833
     4
hoelzl@39082
     5
definition "dynkin M \<longleftrightarrow>
hoelzl@39082
     6
  space M \<in> sets M \<and>
hoelzl@39082
     7
  (\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
hoelzl@39082
     8
  (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
hoelzl@39082
     9
  (\<forall>A. disjoint_family A \<and> range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
hellerar@39080
    10
hellerar@39080
    11
lemma dynkinI:
hellerar@39080
    12
  assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
hellerar@39080
    13
  assumes "space M \<in> sets M" and "\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M"
hellerar@39080
    14
  assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
hellerar@39080
    15
          \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
hellerar@39080
    16
  shows "dynkin M"
hoelzl@39082
    17
using assms unfolding dynkin_def sorry
hellerar@39080
    18
hellerar@39080
    19
lemma dynkin_subset:
hellerar@39080
    20
  assumes "dynkin M"
hellerar@39080
    21
  shows "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
hellerar@39080
    22
using assms unfolding dynkin_def by auto
hellerar@39080
    23
hellerar@39080
    24
lemma dynkin_space:
hellerar@39080
    25
  assumes "dynkin M"
hellerar@39080
    26
  shows "space M \<in> sets M"
hellerar@39080
    27
using assms unfolding dynkin_def by auto
hellerar@39080
    28
hellerar@39080
    29
lemma dynkin_diff:
hellerar@39080
    30
  assumes "dynkin M"
hellerar@39080
    31
  shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
hellerar@39080
    32
using assms unfolding dynkin_def by auto
hellerar@39080
    33
hellerar@39080
    34
lemma dynkin_UN:
hellerar@39080
    35
  assumes "dynkin M"
hellerar@39080
    36
  assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
hellerar@39080
    37
  assumes "\<forall> i :: nat. a i \<in> sets M"
hellerar@39080
    38
  shows "UNION UNIV a \<in> sets M"
hoelzl@39082
    39
using assms unfolding dynkin_def sorry
hellerar@39080
    40
hoelzl@39082
    41
definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
hellerar@39080
    42
hellerar@39080
    43
lemma dynkin_trivial:
hellerar@39080
    44
  shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
hellerar@39080
    45
by (rule dynkinI) auto
hellerar@39080
    46
hellerar@39080
    47
lemma
hoelzl@39082
    48
  fixes D :: "'a algebra"
hellerar@39080
    49
  assumes stab: "Int_stable E"
hellerar@39080
    50
  and spac: "space E = space D"
hellerar@39080
    51
  and subsED: "sets E \<subseteq> sets D"
hellerar@39080
    52
  and subsDE: "sets D \<subseteq> sigma_sets (space E) (sets E)"
hellerar@39080
    53
  and dyn: "dynkin D"
hellerar@39080
    54
  shows "sigma (space E) (sets E) = D"
hellerar@39080
    55
proof -
hellerar@39080
    56
  def sets_\<delta>E == "\<Inter> {sets d | d :: 'a algebra. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
hellerar@39080
    57
  def \<delta>E == "\<lparr> space = space E, sets = sets_\<delta>E \<rparr>"
hellerar@39080
    58
  have "\<lparr> space = space E, sets = Pow (space E) \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
hellerar@39080
    59
    using dynkin_trivial spac subsED dynkin_subset[OF dyn] by fastsimp
hellerar@39080
    60
  hence not_empty: "{sets (d :: 'a algebra) | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}"
hellerar@39080
    61
    using exI[of "\<lambda> x. space x = space E \<and> dynkin x \<and> sets E \<subseteq> sets x" "\<lparr> space = space E, sets = Pow (space E) \<rparr>", simplified]
hellerar@39080
    62
    by auto
hellerar@39080
    63
hellerar@39080
    64
  have "sets_\<delta>E \<subseteq> sets D"
hellerar@39080
    65
    unfolding sets_\<delta>E_def using assms by auto
hellerar@39080
    66
hellerar@39080
    67
  have \<delta>ynkin: "dynkin \<delta>E"
hellerar@39080
    68
  proof (rule dynkinI, safe)
hellerar@39080
    69
    fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
hellerar@39080
    70
    { fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E"
hoelzl@39082
    71
      hence "A \<subseteq> space d" using dynkin_subset by auto }
hoelzl@39082
    72
    show "x \<in> space \<delta>E" using asm unfolding \<delta>E_def sets_\<delta>E_def using not_empty
hoelzl@39082
    73
      by simp (metis dynkin_subset in_mono mem_def)
hellerar@39080
    74
  next
hellerar@39080
    75
    show "space \<delta>E \<in> sets \<delta>E"
hellerar@39080
    76
      unfolding \<delta>E_def sets_\<delta>E_def
hellerar@39080
    77
      using dynkin_space by fastsimp
hellerar@39080
    78
  next
hellerar@39080
    79
    fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
hellerar@39080
    80
    thus "b - a \<in> sets \<delta>E"
hellerar@39080
    81
      unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff)
hellerar@39080
    82
  next
hellerar@39080
    83
    fix a assume asm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> sets \<delta>E"
hellerar@39080
    84
    thus "UNION UNIV a \<in> sets \<delta>E"
hellerar@39080
    85
      unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)])
hellerar@39080
    86
      by blast
hellerar@39080
    87
  qed
hoelzl@39082
    88
hellerar@39080
    89
  def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}"
hellerar@39080
    90
  { fix d assume dasm: "d \<in> sets_\<delta>E"
hellerar@39080
    91
    have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>"
hoelzl@39082
    92
    proof (rule dynkinI, safe, simp_all)
hellerar@39080
    93
      fix A x assume "A \<in> Dy d" "x \<in> A"
hellerar@39080
    94
      thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty
hoelzl@39082
    95
        by simp (metis dynkin_subset in_mono mem_def)
hellerar@39080
    96
    next
hellerar@39080
    97
      show "space E \<in> Dy d"
hellerar@39080
    98
        unfolding Dy_def \<delta>E_def sets_\<delta>E_def
hellerar@39080
    99
      proof auto
hellerar@39080
   100
        fix d assume asm: "dynkin d" "space d = space E" "sets E \<subseteq> sets d"
hellerar@39080
   101
        hence "space d \<in> sets d" using dynkin_space[OF asm(1)] by auto
hellerar@39080
   102
        thus "space E \<in> sets d" using asm by auto
hellerar@39080
   103
      next
hellerar@39080
   104
        fix da :: "'a algebra" assume asm: "dynkin da" "space da = space E" "sets E \<subseteq> sets da"
hellerar@39080
   105
        have d: "d = space E \<inter> d"
hellerar@39080
   106
          using dasm dynkin_subset[OF asm(1)] asm(2) dynkin_subset[OF \<delta>ynkin]
hellerar@39080
   107
          unfolding \<delta>E_def by auto
hellerar@39080
   108
        hence "space E \<inter> d \<in> sets \<delta>E" unfolding \<delta>E_def
hellerar@39080
   109
          using dasm by auto
hellerar@39080
   110
        have "sets \<delta>E \<subseteq> sets da" unfolding \<delta>E_def sets_\<delta>E_def using asm
hellerar@39080
   111
          by auto
hellerar@39080
   112
        thus "space E \<inter> d \<in> sets da" using dasm asm d dynkin_subset[OF \<delta>ynkin]
hellerar@39080
   113
          unfolding \<delta>E_def by auto
hellerar@39080
   114
      qed
hellerar@39080
   115
    next
hellerar@39080
   116
      fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d"
hellerar@39080
   117
      hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
hellerar@39080
   118
        unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   119
      hence *: "b - a \<in> sets \<delta>E"
hellerar@39080
   120
        using dynkin_diff[OF \<delta>ynkin] by auto
hellerar@39080
   121
      have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E"
hellerar@39080
   122
        using absm unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   123
      hence "(b \<inter> d) - (a \<inter> d) \<in> sets \<delta>E"
hellerar@39080
   124
        using dynkin_diff[OF \<delta>ynkin] by auto
hellerar@39080
   125
      hence **: "(b - a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2)
hellerar@39080
   126
      thus "b - a \<in> Dy d"
hellerar@39080
   127
        using * ** unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   128
    next
hellerar@39080
   129
      fix a assume aasm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> Dy d"
hellerar@39080
   130
      hence "\<forall> i. a i \<in> sets \<delta>E"
hellerar@39080
   131
        unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   132
      from dynkin_UN[OF \<delta>ynkin aasm(1) this]
hellerar@39080
   133
      have *: "UNION UNIV a \<in> sets \<delta>E" by auto
hellerar@39080
   134
      from aasm
hellerar@39080
   135
      have aE: "\<forall> i. a i \<inter> d \<in> sets \<delta>E"
hellerar@39080
   136
        unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   137
      from aasm
hellerar@39080
   138
      have "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> (a i \<inter> d) \<inter> (a j \<inter> d) = {}" by auto
hellerar@39080
   139
      from dynkin_UN[OF \<delta>ynkin this]
hellerar@39080
   140
      have "UNION UNIV (\<lambda> i. a i \<inter> d) \<in> sets \<delta>E"
hellerar@39080
   141
        using aE by auto
hellerar@39080
   142
      hence **: "UNION UNIV a \<inter> d \<in> sets \<delta>E" by auto
hellerar@39080
   143
      from * ** show "UNION UNIV a \<in> Dy d" unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   144
    qed } note Dy_nkin = this
hellerar@39080
   145
  have E_\<delta>E: "sets E \<subseteq> sets \<delta>E"
hellerar@39080
   146
    unfolding \<delta>E_def sets_\<delta>E_def by auto
hellerar@39080
   147
  { fix d assume dasm: "d \<in> sets \<delta>E"
hellerar@39080
   148
    { fix e assume easm: "e \<in> sets E"
hellerar@39080
   149
      hence deasm: "e \<in> sets \<delta>E"
hellerar@39080
   150
        unfolding \<delta>E_def sets_\<delta>E_def by auto
hellerar@39080
   151
      have subset: "Dy e \<subseteq> sets \<delta>E"
hellerar@39080
   152
        unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   153
      { fix e' assume e'asm: "e' \<in> sets E"
hellerar@39080
   154
        have "e' \<inter> e \<in> sets E"
hellerar@39080
   155
          using easm e'asm stab unfolding Int_stable_def by auto
hellerar@39080
   156
        hence "e' \<inter> e \<in> sets \<delta>E"
hellerar@39080
   157
          unfolding \<delta>E_def sets_\<delta>E_def by auto
hellerar@39080
   158
        hence "e' \<in> Dy e" using e'asm unfolding Dy_def \<delta>E_def sets_\<delta>E_def by auto }
hellerar@39080
   159
      hence E_Dy: "sets E \<subseteq> Dy e" by auto
hellerar@39080
   160
      have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
hellerar@39080
   161
        using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto
hellerar@39080
   162
      hence "sets_\<delta>E \<subseteq> Dy e"
hoelzl@39082
   163
        unfolding sets_\<delta>E_def by auto (metis E_Dy simps(1) simps(2) spac)
hellerar@39080
   164
      hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto
hellerar@39080
   165
      hence "d \<inter> e \<in> sets \<delta>E"
hellerar@39080
   166
        using dasm easm deasm unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   167
      hence "e \<in> Dy d" using deasm
hellerar@39080
   168
        unfolding Dy_def \<delta>E_def
hellerar@39080
   169
        by (auto simp add:Int_commute) }
hellerar@39080
   170
    hence "sets E \<subseteq> Dy d" by auto
hellerar@39080
   171
    hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]]
hoelzl@39082
   172
      unfolding \<delta>E_def sets_\<delta>E_def
hoelzl@39082
   173
      by auto (metis `sets E <= Dy d` simps(1) simps(2) spac)
hellerar@39080
   174
    hence *: "sets \<delta>E = Dy d"
hellerar@39080
   175
      unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   176
    fix a assume aasm: "a \<in> sets \<delta>E"
hellerar@39080
   177
    hence "a \<inter> d \<in> sets \<delta>E"
hellerar@39080
   178
      using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this
hellerar@39080
   179
  have "sigma_algebra D"
hellerar@39080
   180
    apply unfold_locales
hellerar@39080
   181
    using dynkin_subset[OF dyn]
hellerar@39080
   182
    using dynkin_diff[OF dyn, of _ "space D", OF _ dynkin_space[OF dyn]]
hellerar@39080
   183
    using dynkin_diff[OF dyn, of "space D" "space D", OF dynkin_space[OF dyn] dynkin_space[OF dyn]]
hellerar@39080
   184
    using dynkin_space[OF dyn]
hoelzl@39082
   185
    sorry
hoelzl@39082
   186
(*
hellerar@39080
   187
  proof auto
hellerar@39080
   188
    fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets D" "\<And>A. A \<in> sets D \<Longrightarrow> A \<subseteq> space D"
hellerar@39080
   189
      "\<And>a. a \<in> sets D \<Longrightarrow> space D - a \<in> sets D"
hellerar@39080
   190
    "{} \<in> sets D" "space D \<in> sets D"
hellerar@39080
   191
    let "?A i" = "A i - (\<Inter> j \<in> {..< i}. A j)"
hellerar@39080
   192
    { fix i :: nat assume "i > 0"
hoelzl@39082
   193
      have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E" sorry }
hoelzl@39082
   194
      oops
hellerar@39080
   195
  qed
hoelzl@39082
   196
*)
hoelzl@39082
   197
hoelzl@39082
   198
  show ?thesis sorry
hellerar@39080
   199
qed
hellerar@39080
   200
hoelzl@38656
   201
definition prod_sets where
hoelzl@38656
   202
  "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
hoelzl@38656
   203
hoelzl@35833
   204
definition
hoelzl@39088
   205
  "prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"
hoelzl@39088
   206
hoelzl@39088
   207
lemma
hoelzl@39088
   208
  fixes M1 :: "'a algebra" and M2 :: "'b algebra"
hoelzl@39088
   209
  assumes "algebra M1" "algebra M2"
hoelzl@39088
   210
  shows measureable_fst[intro!, simp]:
hoelzl@39088
   211
    "fst \<in> measurable (prod_measure_space M1 M2) M1" (is ?fst)
hoelzl@39088
   212
  and measureable_snd[intro!, simp]:
hoelzl@39088
   213
    "snd \<in> measurable (prod_measure_space M1 M2) M2" (is ?snd)
hoelzl@39088
   214
proof -
hoelzl@39088
   215
  interpret M1: algebra M1 by fact
hoelzl@39088
   216
  interpret M2: algebra M2 by fact
hoelzl@39088
   217
hoelzl@39088
   218
  { fix X assume "X \<in> sets M1"
hoelzl@39088
   219
    then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. fst -` X \<inter> space M1 \<times> space M2 = X1 \<times> X2"
hoelzl@39088
   220
      apply - apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"])
hoelzl@39088
   221
      using M1.sets_into_space by force+ }
hoelzl@39088
   222
  moreover
hoelzl@39088
   223
  { fix X assume "X \<in> sets M2"
hoelzl@39088
   224
    then have "\<exists>X1\<in>sets M1. \<exists>X2\<in>sets M2. snd -` X \<inter> space M1 \<times> space M2 = X1 \<times> X2"
hoelzl@39088
   225
      apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])
hoelzl@39088
   226
      using M2.sets_into_space by force+ }
hoelzl@39088
   227
  ultimately show ?fst ?snd
hoelzl@39088
   228
    by (force intro!: sigma_sets.Basic
hoelzl@39088
   229
              simp: measurable_def prod_measure_space_def prod_sets_def sets_sigma)+
hoelzl@39088
   230
qed
hoelzl@39088
   231
hoelzl@39088
   232
lemma (in sigma_algebra) measureable_prod:
hoelzl@39088
   233
  fixes M1 :: "'a algebra" and M2 :: "'b algebra"
hoelzl@39088
   234
  assumes "algebra M1" "algebra M2"
hoelzl@39088
   235
  shows "f \<in> measurable M (prod_measure_space M1 M2) \<longleftrightarrow>
hoelzl@39088
   236
    (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
hoelzl@39088
   237
using assms proof (safe intro!: measurable_comp[where b="prod_measure_space M1 M2"])
hoelzl@39088
   238
  interpret M1: algebra M1 by fact
hoelzl@39088
   239
  interpret M2: algebra M2 by fact
hoelzl@39088
   240
  assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2"
hoelzl@39088
   241
hoelzl@39088
   242
  show "f \<in> measurable M (prod_measure_space M1 M2)" unfolding prod_measure_space_def
hoelzl@39088
   243
  proof (rule measurable_sigma)
hoelzl@39088
   244
    show "prod_sets (sets M1) (sets M2) \<subseteq> Pow (space M1 \<times> space M2)"
hoelzl@39088
   245
      unfolding prod_sets_def using M1.sets_into_space M2.sets_into_space by auto
hoelzl@39088
   246
    show "f \<in> space M \<rightarrow> space M1 \<times> space M2"
hoelzl@39088
   247
      using f s by (auto simp: mem_Times_iff measurable_def comp_def)
hoelzl@39088
   248
    fix A assume "A \<in> prod_sets (sets M1) (sets M2)"
hoelzl@39088
   249
    then obtain B C where "B \<in> sets M1" "C \<in> sets M2" "A = B \<times> C"
hoelzl@39088
   250
      unfolding prod_sets_def by auto
hoelzl@39088
   251
    moreover have "(fst \<circ> f) -` B \<inter> space M \<in> sets M"
hoelzl@39088
   252
      using f `B \<in> sets M1` unfolding measurable_def by auto
hoelzl@39088
   253
    moreover have "(snd \<circ> f) -` C \<inter> space M \<in> sets M"
hoelzl@39088
   254
      using s `C \<in> sets M2` unfolding measurable_def by auto
hoelzl@39088
   255
    moreover have "f -` A \<inter> space M = ((fst \<circ> f) -` B \<inter> space M) \<inter> ((snd \<circ> f) -` C \<inter> space M)"
hoelzl@39088
   256
      unfolding `A = B \<times> C` by (auto simp: vimage_Times)
hoelzl@39088
   257
    ultimately show "f -` A \<inter> space M \<in> sets M" by auto
hoelzl@39088
   258
  qed
hoelzl@39088
   259
qed
hoelzl@35833
   260
hoelzl@35833
   261
definition
hoelzl@39088
   262
  "prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))"
hoelzl@38656
   263
hoelzl@38656
   264
lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
hoelzl@38656
   265
  by (auto simp add: prod_sets_def)
hoelzl@35833
   266
hoelzl@38656
   267
lemma sigma_prod_sets_finite:
hoelzl@38656
   268
  assumes "finite A" and "finite B"
hoelzl@38656
   269
  shows "sigma_sets (A \<times> B) (prod_sets (Pow A) (Pow B)) = Pow (A \<times> B)"
hoelzl@38656
   270
proof safe
hoelzl@38656
   271
  have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product)
hoelzl@35833
   272
hoelzl@38656
   273
  fix x assume subset: "x \<subseteq> A \<times> B"
hoelzl@38656
   274
  hence "finite x" using fin by (rule finite_subset)
hoelzl@38656
   275
  from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))"
hoelzl@38656
   276
    (is "x \<in> sigma_sets ?prod ?sets")
hoelzl@38656
   277
  proof (induct x)
hoelzl@38656
   278
    case empty show ?case by (rule sigma_sets.Empty)
hoelzl@38656
   279
  next
hoelzl@38656
   280
    case (insert a x)
hoelzl@38656
   281
    hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic)
hoelzl@38656
   282
    moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto
hoelzl@38656
   283
    ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)
hoelzl@38656
   284
  qed
hoelzl@38656
   285
next
hoelzl@38656
   286
  fix x a b
hoelzl@38656
   287
  assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x"
hoelzl@38656
   288
  from sigma_sets_into_sp[OF _ this(1)] this(2)
hoelzl@38656
   289
  show "a \<in> A" and "b \<in> B"
hoelzl@38656
   290
    by (auto simp: prod_sets_def)
hoelzl@35833
   291
qed
hoelzl@35833
   292
hoelzl@38656
   293
lemma (in sigma_algebra) measurable_prod_sigma:
hoelzl@38656
   294
  assumes sa1: "sigma_algebra a1" and sa2: "sigma_algebra a2"
hoelzl@38656
   295
  assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
hoelzl@38656
   296
  shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2))
hoelzl@38656
   297
                          (prod_sets (sets a1) (sets a2)))"
hoelzl@35977
   298
proof -
hoelzl@38656
   299
  from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
hoelzl@38656
   300
     and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
hoelzl@38656
   301
    by (auto simp add: measurable_def)
hoelzl@38656
   302
  from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
hoelzl@38656
   303
     and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
hoelzl@38656
   304
    by (auto simp add: measurable_def)
hoelzl@38656
   305
  show ?thesis
hoelzl@38656
   306
    proof (rule measurable_sigma)
hoelzl@38656
   307
      show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
hoelzl@38656
   308
        by (auto simp add: prod_sets_def sigma_algebra_iff dest: algebra.space_closed)
hoelzl@38656
   309
    next
hoelzl@38656
   310
      show "f \<in> space M \<rightarrow> space a1 \<times> space a2"
hoelzl@38656
   311
        by (rule prod_final [OF fn1 fn2])
hoelzl@38656
   312
    next
hoelzl@38656
   313
      fix z
hoelzl@38656
   314
      assume z: "z \<in> prod_sets (sets a1) (sets a2)"
hoelzl@38656
   315
      thus "f -` z \<inter> space M \<in> sets M"
hoelzl@38656
   316
        proof (auto simp add: prod_sets_def vimage_Times)
hoelzl@38656
   317
          fix x y
hoelzl@38656
   318
          assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
hoelzl@38656
   319
          have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
hoelzl@38656
   320
                ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
hoelzl@38656
   321
            by blast
hoelzl@38656
   322
          also have "...  \<in> sets M" using x y q1 q2
hoelzl@38656
   323
            by blast
hoelzl@38656
   324
          finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
hoelzl@38656
   325
        qed
hoelzl@38656
   326
    qed
hoelzl@35977
   327
qed
hoelzl@35833
   328
hoelzl@38656
   329
lemma (in sigma_finite_measure) prod_measure_times:
hoelzl@38656
   330
  assumes "sigma_finite_measure N \<nu>"
hoelzl@38656
   331
  and "A1 \<in> sets M" "A2 \<in> sets N"
hoelzl@38656
   332
  shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"
hoelzl@38656
   333
  oops
hoelzl@35833
   334
hoelzl@38656
   335
lemma (in sigma_finite_measure) sigma_finite_prod_measure_space:
hoelzl@38656
   336
  assumes "sigma_finite_measure N \<nu>"
hoelzl@38656
   337
  shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   338
  oops
hoelzl@38656
   339
hoelzl@38656
   340
lemma (in finite_measure_space) finite_prod_measure_times:
hoelzl@38656
   341
  assumes "finite_measure_space N \<nu>"
hoelzl@38656
   342
  and "A1 \<in> sets M" "A2 \<in> sets N"
hoelzl@38656
   343
  shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"
hoelzl@38656
   344
proof -
hoelzl@38656
   345
  interpret N: finite_measure_space N \<nu> by fact
hoelzl@38656
   346
  have *: "\<And>x. \<nu> (Pair x -` (A1 \<times> A2)) * \<mu> {x} = (if x \<in> A1 then \<nu> A2 * \<mu> {x} else 0)"
hoelzl@38656
   347
    by (auto simp: vimage_Times comp_def)
hoelzl@38656
   348
  have "finite A1"
hoelzl@38656
   349
    using `A1 \<in> sets M` finite_space by (auto simp: sets_eq_Pow intro: finite_subset)
hoelzl@38656
   350
  then have "\<mu> A1 = (\<Sum>x\<in>A1. \<mu> {x})" using `A1 \<in> sets M`
hoelzl@38656
   351
    by (auto intro!: measure_finite_singleton simp: sets_eq_Pow)
hoelzl@38656
   352
  then show ?thesis using `A1 \<in> sets M`
hoelzl@38656
   353
    unfolding prod_measure_def positive_integral_finite_eq_setsum *
hoelzl@38656
   354
    by (auto simp add: sets_eq_Pow setsum_right_distrib[symmetric] mult_commute setsum_cases[OF finite_space])
hoelzl@35833
   355
qed
hoelzl@35833
   356
hoelzl@38656
   357
lemma (in finite_measure_space) finite_prod_measure_space:
hoelzl@38656
   358
  assumes "finite_measure_space N \<nu>"
hoelzl@38656
   359
  shows "prod_measure_space M N = \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr>"
hoelzl@35977
   360
proof -
hoelzl@38656
   361
  interpret N: finite_measure_space N \<nu> by fact
hoelzl@38656
   362
  show ?thesis using finite_space N.finite_space
hoelzl@38656
   363
    by (simp add: sigma_def prod_measure_space_def sigma_prod_sets_finite sets_eq_Pow N.sets_eq_Pow)
hoelzl@35833
   364
qed
hoelzl@35833
   365
hoelzl@38656
   366
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure:
hoelzl@38656
   367
  assumes "finite_measure_space N \<nu>"
hoelzl@38656
   368
  shows "finite_measure_space (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   369
  unfolding finite_prod_measure_space[OF assms]
hoelzl@38656
   370
proof (rule finite_measure_spaceI)
hoelzl@38656
   371
  interpret N: finite_measure_space N \<nu> by fact
hoelzl@38656
   372
hoelzl@38656
   373
  let ?P = "\<lparr>space = space M \<times> space N, sets = Pow (space M \<times> space N)\<rparr>"
hoelzl@38656
   374
  show "measure_space ?P (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   375
  proof (rule sigma_algebra.finite_additivity_sufficient)
hoelzl@38656
   376
    show "sigma_algebra ?P" by (rule sigma_algebra_Pow)
hoelzl@38656
   377
    show "finite (space ?P)" using finite_space N.finite_space by auto
hoelzl@38656
   378
    from finite_prod_measure_times[OF assms, of "{}" "{}"]
hoelzl@38656
   379
    show "positive (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   380
      unfolding positive_def by simp
hoelzl@38656
   381
hoelzl@38656
   382
    show "additive ?P (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   383
      unfolding additive_def
hoelzl@38656
   384
      apply (auto simp add: sets_eq_Pow prod_measure_def positive_integral_add[symmetric]
hoelzl@38656
   385
                  intro!: positive_integral_cong)
hoelzl@38656
   386
      apply (subst N.measure_additive[symmetric])
hoelzl@38656
   387
      by (auto simp: N.sets_eq_Pow sets_eq_Pow)
hoelzl@38656
   388
  qed
hoelzl@38656
   389
  show "finite (space ?P)" using finite_space N.finite_space by auto
hoelzl@38656
   390
  show "sets ?P = Pow (space ?P)" by simp
hoelzl@38656
   391
hoelzl@38656
   392
  fix x assume "x \<in> space ?P"
hoelzl@38656
   393
  with finite_prod_measure_times[OF assms, of "{fst x}" "{snd x}"]
hoelzl@38656
   394
    finite_measure[of "{fst x}"] N.finite_measure[of "{snd x}"]
hoelzl@38656
   395
  show "prod_measure M \<mu> N \<nu> {x} \<noteq> \<omega>"
hoelzl@38656
   396
    by (auto simp add: sets_eq_Pow N.sets_eq_Pow elim!: SigmaE)
hoelzl@38656
   397
qed
hoelzl@38656
   398
hoelzl@38656
   399
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure_alterantive:
hoelzl@38656
   400
  assumes N: "finite_measure_space N \<nu>"
hoelzl@38656
   401
  shows "finite_measure_space \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr> (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   402
    (is "finite_measure_space ?M ?m")
hoelzl@38656
   403
  unfolding finite_prod_measure_space[OF N, symmetric]
hoelzl@38656
   404
  using finite_measure_space_finite_prod_measure[OF N] .
hoelzl@38656
   405
hoelzl@35833
   406
end