src/HOL/Probability/Product_Measure.thy
author hoelzl
Wed Dec 01 19:20:30 2010 +0100 (2010-12-01)
changeset 40859 de0b30e6c2d2
parent 39098 21e9bd6cf0a8
child 40871 688f6ff859e1
permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
hoelzl@35833
     1
theory Product_Measure
hoelzl@38656
     2
imports Lebesgue_Integration
hoelzl@35833
     3
begin
hoelzl@35833
     4
hoelzl@40859
     5
lemma in_sigma[intro, simp]: "A \<in> sets M \<Longrightarrow> A \<in> sets (sigma M)"
hoelzl@40859
     6
  unfolding sigma_def by (auto intro!: sigma_sets.Basic)
hellerar@39080
     7
hoelzl@40859
     8
lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
hoelzl@40859
     9
  unfolding sigma_def sigma_sets_eq by simp
hoelzl@39082
    10
hoelzl@40859
    11
lemma vimage_algebra_sigma:
hoelzl@40859
    12
  assumes E: "sets E \<subseteq> Pow (space E)"
hoelzl@40859
    13
    and f: "f \<in> space F \<rightarrow> space E"
hoelzl@40859
    14
    and "\<And>A. A \<in> sets F \<Longrightarrow> A \<in> (\<lambda>X. f -` X \<inter> space F) ` sets E"
hoelzl@40859
    15
    and "\<And>A. A \<in> sets E \<Longrightarrow> f -` A \<inter> space F \<in> sets F"
hoelzl@40859
    16
  shows "sigma_algebra.vimage_algebra (sigma E) (space F) f = sigma F"
hoelzl@40859
    17
proof -
hoelzl@40859
    18
  interpret sigma_algebra "sigma E"
hoelzl@40859
    19
    using assms by (intro sigma_algebra_sigma) auto
hoelzl@40859
    20
  have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
hoelzl@40859
    21
    using assms by auto
hoelzl@40859
    22
  show "vimage_algebra (space F) f = sigma F"
hoelzl@40859
    23
    unfolding vimage_algebra_def using assms
hoelzl@40859
    24
    by (simp add: sigma_def eq sigma_sets_vimage)
hellerar@39094
    25
qed
hellerar@39094
    26
hoelzl@40859
    27
lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
hoelzl@40859
    28
  by auto
hoelzl@40859
    29
hoelzl@40859
    30
lemma Pair_vimage_times[simp]: "\<And>A B x. Pair x -` (A \<times> B) = (if x \<in> A then B else {})"
hoelzl@40859
    31
  by auto
hoelzl@40859
    32
hoelzl@40859
    33
lemma rev_Pair_vimage_times[simp]: "\<And>A B y. (\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
hoelzl@40859
    34
  by auto
hoelzl@40859
    35
hoelzl@40859
    36
lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
hoelzl@40859
    37
  by (cases x) simp
hoelzl@40859
    38
hoelzl@40859
    39
abbreviation
hoelzl@40859
    40
  "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
hellerar@39094
    41
hoelzl@40859
    42
abbreviation
hoelzl@40859
    43
  funcset_extensional :: "['a set, 'b set] => ('a => 'b) set"
hoelzl@40859
    44
    (infixr "->\<^isub>E" 60) where
hoelzl@40859
    45
  "A ->\<^isub>E B \<equiv> Pi\<^isub>E A (%_. B)"
hoelzl@40859
    46
hoelzl@40859
    47
notation (xsymbols)
hoelzl@40859
    48
  funcset_extensional  (infixr "\<rightarrow>\<^isub>E" 60)
hoelzl@40859
    49
hoelzl@40859
    50
lemma extensional_empty[simp]: "extensional {} = {\<lambda>x. undefined}"
hoelzl@40859
    51
  by safe (auto simp add: extensional_def fun_eq_iff)
hoelzl@40859
    52
hoelzl@40859
    53
lemma extensional_insert[intro, simp]:
hoelzl@40859
    54
  assumes "a \<in> extensional (insert i I)"
hoelzl@40859
    55
  shows "a(i := b) \<in> extensional (insert i I)"
hoelzl@40859
    56
  using assms unfolding extensional_def by auto
hoelzl@40859
    57
hoelzl@40859
    58
lemma extensional_Int[simp]:
hoelzl@40859
    59
  "extensional I \<inter> extensional I' = extensional (I \<inter> I')"
hoelzl@40859
    60
  unfolding extensional_def by auto
hoelzl@38656
    61
hoelzl@35833
    62
definition
hoelzl@40859
    63
  "merge I x J y = (\<lambda>i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
hoelzl@40859
    64
hoelzl@40859
    65
lemma merge_apply[simp]:
hoelzl@40859
    66
  "I \<inter> J = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
hoelzl@40859
    67
  "I \<inter> J = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
hoelzl@40859
    68
  "J \<inter> I = {} \<Longrightarrow> i \<in> I \<Longrightarrow> merge I x J y i = x i"
hoelzl@40859
    69
  "J \<inter> I = {} \<Longrightarrow> i \<in> J \<Longrightarrow> merge I x J y i = y i"
hoelzl@40859
    70
  "i \<notin> I \<Longrightarrow> i \<notin> J \<Longrightarrow> merge I x J y i = undefined"
hoelzl@40859
    71
  unfolding merge_def by auto
hoelzl@40859
    72
hoelzl@40859
    73
lemma merge_commute:
hoelzl@40859
    74
  "I \<inter> J = {} \<Longrightarrow> merge I x J y = merge J y I x"
hoelzl@40859
    75
  by (auto simp: merge_def intro!: ext)
hoelzl@40859
    76
hoelzl@40859
    77
lemma Pi_cancel_merge_range[simp]:
hoelzl@40859
    78
  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
hoelzl@40859
    79
  "I \<inter> J = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
hoelzl@40859
    80
  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge I A J B) \<longleftrightarrow> x \<in> Pi I A"
hoelzl@40859
    81
  "J \<inter> I = {} \<Longrightarrow> x \<in> Pi I (merge J B I A) \<longleftrightarrow> x \<in> Pi I A"
hoelzl@40859
    82
  by (auto simp: Pi_def)
hoelzl@40859
    83
hoelzl@40859
    84
lemma Pi_cancel_merge[simp]:
hoelzl@40859
    85
  "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
hoelzl@40859
    86
  "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
hoelzl@40859
    87
  "I \<inter> J = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
hoelzl@40859
    88
  "J \<inter> I = {} \<Longrightarrow> merge I x J y \<in> Pi J B \<longleftrightarrow> y \<in> Pi J B"
hoelzl@40859
    89
  by (auto simp: Pi_def)
hoelzl@40859
    90
hoelzl@40859
    91
lemma extensional_merge[simp]: "merge I x J y \<in> extensional (I \<union> J)"
hoelzl@40859
    92
  by (auto simp: extensional_def)
hoelzl@40859
    93
hoelzl@40859
    94
lemma restrict_Pi_cancel: "restrict x I \<in> Pi I A \<longleftrightarrow> x \<in> Pi I A"
hoelzl@40859
    95
  by (auto simp: restrict_def Pi_def)
hoelzl@40859
    96
hoelzl@40859
    97
lemma restrict_merge[simp]:
hoelzl@40859
    98
  "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
hoelzl@40859
    99
  "I \<inter> J = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
hoelzl@40859
   100
  "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) I = restrict x I"
hoelzl@40859
   101
  "J \<inter> I = {} \<Longrightarrow> restrict (merge I x J y) J = restrict y J"
hoelzl@40859
   102
  by (auto simp: restrict_def intro!: ext)
hoelzl@40859
   103
hoelzl@40859
   104
lemma extensional_insert_undefined[intro, simp]:
hoelzl@40859
   105
  assumes "a \<in> extensional (insert i I)"
hoelzl@40859
   106
  shows "a(i := undefined) \<in> extensional I"
hoelzl@40859
   107
  using assms unfolding extensional_def by auto
hoelzl@40859
   108
hoelzl@40859
   109
lemma extensional_insert_cancel[intro, simp]:
hoelzl@40859
   110
  assumes "a \<in> extensional I"
hoelzl@40859
   111
  shows "a \<in> extensional (insert i I)"
hoelzl@40859
   112
  using assms unfolding extensional_def by auto
hoelzl@40859
   113
hoelzl@40859
   114
lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
hoelzl@40859
   115
  by auto
hoelzl@40859
   116
hoelzl@40859
   117
lemma Pi_cancel_fupd_range[simp]: "i \<notin> I \<Longrightarrow> x \<in> Pi I (B(i := b)) \<longleftrightarrow> x \<in> Pi I B"
hoelzl@40859
   118
  by (auto simp: Pi_def)
hoelzl@40859
   119
hoelzl@40859
   120
lemma Pi_split_insert_domain[simp]: "x \<in> Pi (insert i I) X \<longleftrightarrow> x \<in> Pi I X \<and> x i \<in> X i"
hoelzl@40859
   121
  by (auto simp: Pi_def)
hoelzl@39088
   122
hoelzl@40859
   123
lemma Pi_split_domain[simp]: "x \<in> Pi (I \<union> J) X \<longleftrightarrow> x \<in> Pi I X \<and> x \<in> Pi J X"
hoelzl@40859
   124
  by (auto simp: Pi_def)
hoelzl@40859
   125
hoelzl@40859
   126
lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
hoelzl@40859
   127
  by (auto simp: Pi_def)
hoelzl@40859
   128
hoelzl@40859
   129
section "Binary products"
hoelzl@40859
   130
hoelzl@40859
   131
definition
hoelzl@40859
   132
  "pair_algebra A B = \<lparr> space = space A \<times> space B,
hoelzl@40859
   133
                           sets = {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<rparr>"
hoelzl@40859
   134
hoelzl@40859
   135
locale pair_sigma_algebra = M1: sigma_algebra M1 + M2: sigma_algebra M2
hoelzl@40859
   136
  for M1 M2
hoelzl@40859
   137
hoelzl@40859
   138
abbreviation (in pair_sigma_algebra)
hoelzl@40859
   139
  "E \<equiv> pair_algebra M1 M2"
hoelzl@40859
   140
hoelzl@40859
   141
abbreviation (in pair_sigma_algebra)
hoelzl@40859
   142
  "P \<equiv> sigma E"
hoelzl@40859
   143
hoelzl@40859
   144
sublocale pair_sigma_algebra \<subseteq> sigma_algebra P
hoelzl@40859
   145
  using M1.sets_into_space M2.sets_into_space
hoelzl@40859
   146
  by (force simp: pair_algebra_def intro!: sigma_algebra_sigma)
hoelzl@40859
   147
hoelzl@40859
   148
lemma pair_algebraI[intro, simp]:
hoelzl@40859
   149
  "x \<in> sets A \<Longrightarrow> y \<in> sets B \<Longrightarrow> x \<times> y \<in> sets (pair_algebra A B)"
hoelzl@40859
   150
  by (auto simp add: pair_algebra_def)
hoelzl@40859
   151
hoelzl@40859
   152
lemma space_pair_algebra:
hoelzl@40859
   153
  "space (pair_algebra A B) = space A \<times> space B"
hoelzl@40859
   154
  by (simp add: pair_algebra_def)
hoelzl@40859
   155
hoelzl@40859
   156
lemma pair_algebra_Int_snd:
hoelzl@40859
   157
  assumes "sets S1 \<subseteq> Pow (space S1)"
hoelzl@40859
   158
  shows "pair_algebra S1 (algebra.restricted_space S2 A) =
hoelzl@40859
   159
         algebra.restricted_space (pair_algebra S1 S2) (space S1 \<times> A)"
hoelzl@40859
   160
  (is "?L = ?R")
hoelzl@40859
   161
proof (intro algebra.equality set_eqI iffI)
hoelzl@40859
   162
  fix X assume "X \<in> sets ?L"
hoelzl@40859
   163
  then obtain A1 A2 where X: "X = A1 \<times> (A \<inter> A2)" and "A1 \<in> sets S1" "A2 \<in> sets S2"
hoelzl@40859
   164
    by (auto simp: pair_algebra_def)
hoelzl@40859
   165
  then show "X \<in> sets ?R" unfolding pair_algebra_def
hoelzl@40859
   166
    using assms apply simp by (intro image_eqI[of _ _ "A1 \<times> A2"]) auto
hoelzl@40859
   167
next
hoelzl@40859
   168
  fix X assume "X \<in> sets ?R"
hoelzl@40859
   169
  then obtain A1 A2 where "X = space S1 \<times> A \<inter> A1 \<times> A2" "A1 \<in> sets S1" "A2 \<in> sets S2"
hoelzl@40859
   170
    by (auto simp: pair_algebra_def)
hoelzl@40859
   171
  moreover then have "X = A1 \<times> (A \<inter> A2)"
hoelzl@40859
   172
    using assms by auto
hoelzl@40859
   173
  ultimately show "X \<in> sets ?L"
hoelzl@40859
   174
    unfolding pair_algebra_def by auto
hoelzl@40859
   175
qed (auto simp add: pair_algebra_def)
hoelzl@40859
   176
hoelzl@40859
   177
lemma (in pair_sigma_algebra)
hoelzl@40859
   178
  shows measurable_fst[intro!, simp]:
hoelzl@40859
   179
    "fst \<in> measurable P M1" (is ?fst)
hoelzl@40859
   180
  and measurable_snd[intro!, simp]:
hoelzl@40859
   181
    "snd \<in> measurable P M2" (is ?snd)
hoelzl@39088
   182
proof -
hoelzl@39088
   183
  { fix X assume "X \<in> sets M1"
hoelzl@39088
   184
    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
   185
      apply - apply (rule bexI[of _ X]) apply (rule bexI[of _ "space M2"])
hoelzl@39088
   186
      using M1.sets_into_space by force+ }
hoelzl@39088
   187
  moreover
hoelzl@39088
   188
  { fix X assume "X \<in> sets M2"
hoelzl@39088
   189
    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
   190
      apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])
hoelzl@39088
   191
      using M2.sets_into_space by force+ }
hoelzl@40859
   192
  ultimately have "?fst \<and> ?snd"
hoelzl@40859
   193
    by (fastsimp simp: measurable_def sets_sigma space_pair_algebra
hoelzl@40859
   194
                 intro!: sigma_sets.Basic)
hoelzl@40859
   195
  then show ?fst ?snd by auto
hoelzl@40859
   196
qed
hoelzl@40859
   197
hoelzl@40859
   198
lemma (in pair_sigma_algebra) measurable_pair:
hoelzl@40859
   199
  assumes "sigma_algebra M"
hoelzl@40859
   200
  shows "f \<in> measurable M P \<longleftrightarrow>
hoelzl@40859
   201
    (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
hoelzl@40859
   202
proof -
hoelzl@40859
   203
  interpret M: sigma_algebra M by fact
hoelzl@40859
   204
  from assms show ?thesis
hoelzl@40859
   205
  proof (safe intro!: measurable_comp[where b=P])
hoelzl@40859
   206
    assume f: "(fst \<circ> f) \<in> measurable M M1" and s: "(snd \<circ> f) \<in> measurable M M2"
hoelzl@40859
   207
    show "f \<in> measurable M P"
hoelzl@40859
   208
    proof (rule M.measurable_sigma)
hoelzl@40859
   209
      show "sets (pair_algebra M1 M2) \<subseteq> Pow (space E)"
hoelzl@40859
   210
        unfolding pair_algebra_def using M1.sets_into_space M2.sets_into_space by auto
hoelzl@40859
   211
      show "f \<in> space M \<rightarrow> space E"
hoelzl@40859
   212
        using f s by (auto simp: mem_Times_iff measurable_def comp_def space_sigma space_pair_algebra)
hoelzl@40859
   213
      fix A assume "A \<in> sets E"
hoelzl@40859
   214
      then obtain B C where "B \<in> sets M1" "C \<in> sets M2" "A = B \<times> C"
hoelzl@40859
   215
        unfolding pair_algebra_def by auto
hoelzl@40859
   216
      moreover have "(fst \<circ> f) -` B \<inter> space M \<in> sets M"
hoelzl@40859
   217
        using f `B \<in> sets M1` unfolding measurable_def by auto
hoelzl@40859
   218
      moreover have "(snd \<circ> f) -` C \<inter> space M \<in> sets M"
hoelzl@40859
   219
        using s `C \<in> sets M2` unfolding measurable_def by auto
hoelzl@40859
   220
      moreover have "f -` A \<inter> space M = ((fst \<circ> f) -` B \<inter> space M) \<inter> ((snd \<circ> f) -` C \<inter> space M)"
hoelzl@40859
   221
        unfolding `A = B \<times> C` by (auto simp: vimage_Times)
hoelzl@40859
   222
      ultimately show "f -` A \<inter> space M \<in> sets M" by auto
hoelzl@40859
   223
    qed
hoelzl@40859
   224
  qed
hoelzl@40859
   225
qed
hoelzl@40859
   226
hoelzl@40859
   227
lemma (in pair_sigma_algebra) measurable_prod_sigma:
hoelzl@40859
   228
  assumes "sigma_algebra M"
hoelzl@40859
   229
  assumes 1: "(fst \<circ> f) \<in> measurable M M1" and 2: "(snd \<circ> f) \<in> measurable M M2"
hoelzl@40859
   230
  shows "f \<in> measurable M P"
hoelzl@40859
   231
proof -
hoelzl@40859
   232
  interpret M: sigma_algebra M by fact
hoelzl@40859
   233
  from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space M1"
hoelzl@40859
   234
     and q1: "\<forall>y\<in>sets M1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
hoelzl@40859
   235
    by (auto simp add: measurable_def)
hoelzl@40859
   236
  from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space M2"
hoelzl@40859
   237
     and q2: "\<forall>y\<in>sets M2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
hoelzl@40859
   238
    by (auto simp add: measurable_def)
hoelzl@40859
   239
  show ?thesis
hoelzl@40859
   240
  proof (rule M.measurable_sigma)
hoelzl@40859
   241
    show "sets E \<subseteq> Pow (space E)"
hoelzl@40859
   242
      using M1.space_closed M2.space_closed
hoelzl@40859
   243
      by (auto simp add: sigma_algebra_iff pair_algebra_def)
hoelzl@40859
   244
  next
hoelzl@40859
   245
    show "f \<in> space M \<rightarrow> space E"
hoelzl@40859
   246
      by (simp add: space_pair_algebra) (rule prod_final [OF fn1 fn2])
hoelzl@40859
   247
  next
hoelzl@40859
   248
    fix z
hoelzl@40859
   249
    assume z: "z \<in> sets E"
hoelzl@40859
   250
    thus "f -` z \<inter> space M \<in> sets M"
hoelzl@40859
   251
    proof (auto simp add: pair_algebra_def vimage_Times)
hoelzl@40859
   252
      fix x y
hoelzl@40859
   253
      assume x: "x \<in> sets M1" and y: "y \<in> sets M2"
hoelzl@40859
   254
      have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
hoelzl@40859
   255
            ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
hoelzl@40859
   256
        by blast
hoelzl@40859
   257
      also have "...  \<in> sets M" using x y q1 q2
hoelzl@40859
   258
        by blast
hoelzl@40859
   259
      finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
hoelzl@40859
   260
    qed
hoelzl@40859
   261
  qed
hoelzl@40859
   262
qed
hoelzl@40859
   263
hoelzl@40859
   264
lemma pair_algebraE:
hoelzl@40859
   265
  assumes "X \<in> sets (pair_algebra M1 M2)"
hoelzl@40859
   266
  obtains A B where "X = A \<times> B" "A \<in> sets M1" "B \<in> sets M2"
hoelzl@40859
   267
  using assms unfolding pair_algebra_def by auto
hoelzl@40859
   268
hoelzl@40859
   269
lemma (in pair_sigma_algebra) pair_algebra_swap:
hoelzl@40859
   270
  "(\<lambda>X. (\<lambda>(x,y). (y,x)) -` X \<inter> space M2 \<times> space M1) ` sets E = sets (pair_algebra M2 M1)"
hoelzl@40859
   271
proof (safe elim!: pair_algebraE)
hoelzl@40859
   272
  fix A B assume "A \<in> sets M1" "B \<in> sets M2"
hoelzl@40859
   273
  moreover then have "(\<lambda>(x, y). (y, x)) -` (A \<times> B) \<inter> space M2 \<times> space M1 = B \<times> A"
hoelzl@40859
   274
    using M1.sets_into_space M2.sets_into_space by auto
hoelzl@40859
   275
  ultimately show "(\<lambda>(x, y). (y, x)) -` (A \<times> B) \<inter> space M2 \<times> space M1 \<in> sets (pair_algebra M2 M1)"
hoelzl@40859
   276
    by (auto intro: pair_algebraI)
hoelzl@40859
   277
next
hoelzl@40859
   278
  fix A B assume "A \<in> sets M1" "B \<in> sets M2"
hoelzl@40859
   279
  then show "B \<times> A \<in> (\<lambda>X. (\<lambda>(x, y). (y, x)) -` X \<inter> space M2 \<times> space M1) ` sets E"
hoelzl@40859
   280
    using M1.sets_into_space M2.sets_into_space
hoelzl@40859
   281
    by (auto intro!: image_eqI[where x="A \<times> B"] pair_algebraI)
hoelzl@40859
   282
qed
hoelzl@40859
   283
hoelzl@40859
   284
lemma (in pair_sigma_algebra) sets_pair_sigma_algebra_swap:
hoelzl@40859
   285
  assumes Q: "Q \<in> sets P"
hoelzl@40859
   286
  shows "(\<lambda>(x,y). (y, x)) ` Q \<in> sets (sigma (pair_algebra M2 M1))" (is "_ \<in> sets ?Q")
hoelzl@40859
   287
proof -
hoelzl@40859
   288
  have *: "(\<lambda>(x,y). (y, x)) \<in> space M2 \<times> space M1 \<rightarrow> (space M1 \<times> space M2)"
hoelzl@40859
   289
       "sets (pair_algebra M1 M2) \<subseteq> Pow (space M1 \<times> space M2)"
hoelzl@40859
   290
    using M1.sets_into_space M2.sets_into_space by (auto elim!: pair_algebraE)
hoelzl@40859
   291
  from Q sets_into_space show ?thesis
hoelzl@40859
   292
    by (auto intro!: image_eqI[where x=Q]
hoelzl@40859
   293
             simp: pair_algebra_swap[symmetric] sets_sigma
hoelzl@40859
   294
                   sigma_sets_vimage[OF *] space_pair_algebra)
hoelzl@40859
   295
qed
hoelzl@40859
   296
hoelzl@40859
   297
lemma (in pair_sigma_algebra) pair_sigma_algebra_swap_measurable:
hoelzl@40859
   298
  shows "(\<lambda>(x,y). (y, x)) \<in> measurable P (sigma (pair_algebra M2 M1))"
hoelzl@40859
   299
    (is "?f \<in> measurable ?P ?Q")
hoelzl@40859
   300
  unfolding measurable_def
hoelzl@40859
   301
proof (intro CollectI conjI Pi_I ballI)
hoelzl@40859
   302
  fix x assume "x \<in> space ?P" then show "(case x of (x, y) \<Rightarrow> (y, x)) \<in> space ?Q"
hoelzl@40859
   303
    unfolding pair_algebra_def by auto
hoelzl@40859
   304
next
hoelzl@40859
   305
  fix A assume "A \<in> sets ?Q"
hoelzl@40859
   306
  interpret Q: pair_sigma_algebra M2 M1 by default
hoelzl@40859
   307
  have "?f -` A \<inter> space ?P = (\<lambda>(x,y). (y, x)) ` A"
hoelzl@40859
   308
    using Q.sets_into_space `A \<in> sets ?Q` by (auto simp: pair_algebra_def)
hoelzl@40859
   309
  with Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets ?Q`]
hoelzl@40859
   310
  show "?f -` A \<inter> space ?P \<in> sets ?P" by simp
hoelzl@40859
   311
qed
hoelzl@40859
   312
hoelzl@40859
   313
lemma (in pair_sigma_algebra) measurable_cut_fst:
hoelzl@40859
   314
  assumes "Q \<in> sets P" shows "Pair x -` Q \<in> sets M2"
hoelzl@40859
   315
proof -
hoelzl@40859
   316
  let ?Q' = "{Q. Q \<subseteq> space P \<and> Pair x -` Q \<in> sets M2}"
hoelzl@40859
   317
  let ?Q = "\<lparr> space = space P, sets = ?Q' \<rparr>"
hoelzl@40859
   318
  interpret Q: sigma_algebra ?Q
hoelzl@40859
   319
    proof qed (auto simp: vimage_UN vimage_Diff space_pair_algebra)
hoelzl@40859
   320
  have "sets E \<subseteq> sets ?Q"
hoelzl@40859
   321
    using M1.sets_into_space M2.sets_into_space
hoelzl@40859
   322
    by (auto simp: pair_algebra_def space_pair_algebra)
hoelzl@40859
   323
  then have "sets P \<subseteq> sets ?Q"
hoelzl@40859
   324
    by (subst pair_algebra_def, intro Q.sets_sigma_subset)
hoelzl@40859
   325
       (simp_all add: pair_algebra_def)
hoelzl@40859
   326
  with assms show ?thesis by auto
hoelzl@40859
   327
qed
hoelzl@40859
   328
hoelzl@40859
   329
lemma (in pair_sigma_algebra) measurable_cut_snd:
hoelzl@40859
   330
  assumes Q: "Q \<in> sets P" shows "(\<lambda>x. (x, y)) -` Q \<in> sets M1" (is "?cut Q \<in> sets M1")
hoelzl@40859
   331
proof -
hoelzl@40859
   332
  interpret Q: pair_sigma_algebra M2 M1 by default
hoelzl@40859
   333
  have "Pair y -` (\<lambda>(x, y). (y, x)) ` Q = (\<lambda>x. (x, y)) -` Q" by auto
hoelzl@40859
   334
  with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]
hoelzl@40859
   335
  show ?thesis by simp
hoelzl@40859
   336
qed
hoelzl@40859
   337
hoelzl@40859
   338
lemma (in pair_sigma_algebra) measurable_pair_image_snd:
hoelzl@40859
   339
  assumes m: "f \<in> measurable P M" and "x \<in> space M1"
hoelzl@40859
   340
  shows "(\<lambda>y. f (x, y)) \<in> measurable M2 M"
hoelzl@40859
   341
  unfolding measurable_def
hoelzl@40859
   342
proof (intro CollectI conjI Pi_I ballI)
hoelzl@40859
   343
  fix y assume "y \<in> space M2" with `f \<in> measurable P M` `x \<in> space M1`
hoelzl@40859
   344
  show "f (x, y) \<in> space M" unfolding measurable_def pair_algebra_def by auto
hoelzl@40859
   345
next
hoelzl@40859
   346
  fix A assume "A \<in> sets M"
hoelzl@40859
   347
  then have "Pair x -` (f -` A \<inter> space P) \<in> sets M2" (is "?C \<in> _")
hoelzl@40859
   348
    using `f \<in> measurable P M`
hoelzl@40859
   349
    by (intro measurable_cut_fst) (auto simp: measurable_def)
hoelzl@40859
   350
  also have "?C = (\<lambda>y. f (x, y)) -` A \<inter> space M2"
hoelzl@40859
   351
    using `x \<in> space M1` by (auto simp: pair_algebra_def)
hoelzl@40859
   352
  finally show "(\<lambda>y. f (x, y)) -` A \<inter> space M2 \<in> sets M2" .
hoelzl@40859
   353
qed
hoelzl@40859
   354
hoelzl@40859
   355
lemma (in pair_sigma_algebra) measurable_pair_image_fst:
hoelzl@40859
   356
  assumes m: "f \<in> measurable P M" and "y \<in> space M2"
hoelzl@40859
   357
  shows "(\<lambda>x. f (x, y)) \<in> measurable M1 M"
hoelzl@40859
   358
proof -
hoelzl@40859
   359
  interpret Q: pair_sigma_algebra M2 M1 by default
hoelzl@40859
   360
  from Q.measurable_pair_image_snd[OF measurable_comp `y \<in> space M2`,
hoelzl@40859
   361
                                      OF Q.pair_sigma_algebra_swap_measurable m]
hoelzl@40859
   362
  show ?thesis by simp
hoelzl@40859
   363
qed
hoelzl@40859
   364
hoelzl@40859
   365
lemma (in pair_sigma_algebra) Int_stable_pair_algebra: "Int_stable E"
hoelzl@40859
   366
  unfolding Int_stable_def
hoelzl@40859
   367
proof (intro ballI)
hoelzl@40859
   368
  fix A B assume "A \<in> sets E" "B \<in> sets E"
hoelzl@40859
   369
  then obtain A1 A2 B1 B2 where "A = A1 \<times> A2" "B = B1 \<times> B2"
hoelzl@40859
   370
    "A1 \<in> sets M1" "A2 \<in> sets M2" "B1 \<in> sets M1" "B2 \<in> sets M2"
hoelzl@40859
   371
    unfolding pair_algebra_def by auto
hoelzl@40859
   372
  then show "A \<inter> B \<in> sets E"
hoelzl@40859
   373
    by (auto simp add: times_Int_times pair_algebra_def)
hoelzl@40859
   374
qed
hoelzl@40859
   375
hoelzl@40859
   376
lemma finite_measure_cut_measurable:
hoelzl@40859
   377
  fixes M1 :: "'a algebra" and M2 :: "'b algebra"
hoelzl@40859
   378
  assumes "sigma_finite_measure M1 \<mu>1" "finite_measure M2 \<mu>2"
hoelzl@40859
   379
  assumes "Q \<in> sets (sigma (pair_algebra M1 M2))"
hoelzl@40859
   380
  shows "(\<lambda>x. \<mu>2 (Pair x -` Q)) \<in> borel_measurable M1"
hoelzl@40859
   381
    (is "?s Q \<in> _")
hoelzl@40859
   382
proof -
hoelzl@40859
   383
  interpret M1: sigma_finite_measure M1 \<mu>1 by fact
hoelzl@40859
   384
  interpret M2: finite_measure M2 \<mu>2 by fact
hoelzl@40859
   385
  interpret pair_sigma_algebra M1 M2 by default
hoelzl@40859
   386
  have [intro]: "sigma_algebra M1" by fact
hoelzl@40859
   387
  have [intro]: "sigma_algebra M2" by fact
hoelzl@40859
   388
  let ?D = "\<lparr> space = space P, sets = {A\<in>sets P. ?s A \<in> borel_measurable M1}  \<rparr>"
hoelzl@40859
   389
  note space_pair_algebra[simp]
hoelzl@40859
   390
  interpret dynkin_system ?D
hoelzl@40859
   391
  proof (intro dynkin_systemI)
hoelzl@40859
   392
    fix A assume "A \<in> sets ?D" then show "A \<subseteq> space ?D"
hoelzl@40859
   393
      using sets_into_space by simp
hoelzl@40859
   394
  next
hoelzl@40859
   395
    from top show "space ?D \<in> sets ?D"
hoelzl@40859
   396
      by (auto simp add: if_distrib intro!: M1.measurable_If)
hoelzl@40859
   397
  next
hoelzl@40859
   398
    fix A assume "A \<in> sets ?D"
hoelzl@40859
   399
    with sets_into_space have "\<And>x. \<mu>2 (Pair x -` (space M1 \<times> space M2 - A)) =
hoelzl@40859
   400
        (if x \<in> space M1 then \<mu>2 (space M2) - ?s A x else 0)"
hoelzl@40859
   401
      by (auto intro!: M2.finite_measure_compl measurable_cut_fst
hoelzl@40859
   402
               simp: vimage_Diff)
hoelzl@40859
   403
    with `A \<in> sets ?D` top show "space ?D - A \<in> sets ?D"
hoelzl@40859
   404
      by (auto intro!: Diff M1.measurable_If M1.borel_measurable_pinfreal_diff)
hoelzl@40859
   405
  next
hoelzl@40859
   406
    fix F :: "nat \<Rightarrow> ('a\<times>'b) set" assume "disjoint_family F" "range F \<subseteq> sets ?D"
hoelzl@40859
   407
    moreover then have "\<And>x. \<mu>2 (\<Union>i. Pair x -` F i) = (\<Sum>\<^isub>\<infinity> i. ?s (F i) x)"
hoelzl@40859
   408
      by (intro M2.measure_countably_additive[symmetric])
hoelzl@40859
   409
         (auto intro!: measurable_cut_fst simp: disjoint_family_on_def)
hoelzl@40859
   410
    ultimately show "(\<Union>i. F i) \<in> sets ?D"
hoelzl@40859
   411
      by (auto simp: vimage_UN intro!: M1.borel_measurable_psuminf)
hoelzl@40859
   412
  qed
hoelzl@40859
   413
  have "P = ?D"
hoelzl@40859
   414
  proof (intro dynkin_lemma)
hoelzl@40859
   415
    show "Int_stable E" by (rule Int_stable_pair_algebra)
hoelzl@40859
   416
    from M1.sets_into_space have "\<And>A. A \<in> sets M1 \<Longrightarrow> {x \<in> space M1. x \<in> A} = A"
hoelzl@40859
   417
      by auto
hoelzl@40859
   418
    then show "sets E \<subseteq> sets ?D"
hoelzl@40859
   419
      by (auto simp: pair_algebra_def sets_sigma if_distrib
hoelzl@40859
   420
               intro: sigma_sets.Basic intro!: M1.measurable_If)
hoelzl@40859
   421
  qed auto
hoelzl@40859
   422
  with `Q \<in> sets P` have "Q \<in> sets ?D" by simp
hoelzl@40859
   423
  then show "?s Q \<in> borel_measurable M1" by simp
hoelzl@40859
   424
qed
hoelzl@40859
   425
hoelzl@40859
   426
subsection {* Binary products of $\sigma$-finite measure spaces *}
hoelzl@40859
   427
hoelzl@40859
   428
locale pair_sigma_finite = M1: sigma_finite_measure M1 \<mu>1 + M2: sigma_finite_measure M2 \<mu>2
hoelzl@40859
   429
  for M1 \<mu>1 M2 \<mu>2
hoelzl@40859
   430
hoelzl@40859
   431
sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2
hoelzl@40859
   432
  by default
hoelzl@40859
   433
hoelzl@40859
   434
lemma (in pair_sigma_finite) measure_cut_measurable_fst:
hoelzl@40859
   435
  assumes "Q \<in> sets P" shows "(\<lambda>x. \<mu>2 (Pair x -` Q)) \<in> borel_measurable M1" (is "?s Q \<in> _")
hoelzl@40859
   436
proof -
hoelzl@40859
   437
  have [intro]: "sigma_algebra M1" and [intro]: "sigma_algebra M2" by default+
hoelzl@40859
   438
  have M1: "sigma_finite_measure M1 \<mu>1" by default
hoelzl@40859
   439
hoelzl@40859
   440
  from M2.disjoint_sigma_finite guess F .. note F = this
hoelzl@40859
   441
  let "?C x i" = "F i \<inter> Pair x -` Q"
hoelzl@40859
   442
  { fix i
hoelzl@40859
   443
    let ?R = "M2.restricted_space (F i)"
hoelzl@40859
   444
    have [simp]: "space M1 \<times> F i \<inter> space M1 \<times> space M2 = space M1 \<times> F i"
hoelzl@40859
   445
      using F M2.sets_into_space by auto
hoelzl@40859
   446
    have "(\<lambda>x. \<mu>2 (Pair x -` (space M1 \<times> F i \<inter> Q))) \<in> borel_measurable M1"
hoelzl@40859
   447
    proof (intro finite_measure_cut_measurable[OF M1])
hoelzl@40859
   448
      show "finite_measure (M2.restricted_space (F i)) \<mu>2"
hoelzl@40859
   449
        using F by (intro M2.restricted_to_finite_measure) auto
hoelzl@40859
   450
      have "space M1 \<times> F i \<in> sets P"
hoelzl@40859
   451
        using M1.top F by blast
hoelzl@40859
   452
      from sigma_sets_Int[symmetric,
hoelzl@40859
   453
        OF this[unfolded pair_sigma_algebra_def sets_sigma]]
hoelzl@40859
   454
      show "(space M1 \<times> F i) \<inter> Q \<in> sets (sigma (pair_algebra M1 ?R))"
hoelzl@40859
   455
        using `Q \<in> sets P`
hoelzl@40859
   456
        using pair_algebra_Int_snd[OF M1.space_closed, of "F i" M2]
hoelzl@40859
   457
        by (auto simp: pair_algebra_def sets_sigma)
hoelzl@40859
   458
    qed
hoelzl@40859
   459
    moreover have "\<And>x. Pair x -` (space M1 \<times> F i \<inter> Q) = ?C x i"
hoelzl@40859
   460
      using `Q \<in> sets P` sets_into_space by (auto simp: space_pair_algebra)
hoelzl@40859
   461
    ultimately have "(\<lambda>x. \<mu>2 (?C x i)) \<in> borel_measurable M1"
hoelzl@40859
   462
      by simp }
hoelzl@40859
   463
  moreover
hoelzl@40859
   464
  { fix x
hoelzl@40859
   465
    have "(\<Sum>\<^isub>\<infinity>i. \<mu>2 (?C x i)) = \<mu>2 (\<Union>i. ?C x i)"
hoelzl@40859
   466
    proof (intro M2.measure_countably_additive)
hoelzl@40859
   467
      show "range (?C x) \<subseteq> sets M2"
hoelzl@40859
   468
        using F `Q \<in> sets P` by (auto intro!: M2.Int measurable_cut_fst)
hoelzl@40859
   469
      have "disjoint_family F" using F by auto
hoelzl@40859
   470
      show "disjoint_family (?C x)"
hoelzl@40859
   471
        by (rule disjoint_family_on_bisimulation[OF `disjoint_family F`]) auto
hoelzl@40859
   472
    qed
hoelzl@40859
   473
    also have "(\<Union>i. ?C x i) = Pair x -` Q"
hoelzl@40859
   474
      using F sets_into_space `Q \<in> sets P`
hoelzl@40859
   475
      by (auto simp: space_pair_algebra)
hoelzl@40859
   476
    finally have "\<mu>2 (Pair x -` Q) = (\<Sum>\<^isub>\<infinity>i. \<mu>2 (?C x i))"
hoelzl@40859
   477
      by simp }
hoelzl@40859
   478
  ultimately show ?thesis
hoelzl@40859
   479
    by (auto intro!: M1.borel_measurable_psuminf)
hoelzl@40859
   480
qed
hoelzl@40859
   481
hoelzl@40859
   482
lemma (in pair_sigma_finite) measure_cut_measurable_snd:
hoelzl@40859
   483
  assumes "Q \<in> sets P" shows "(\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` Q)) \<in> borel_measurable M2"
hoelzl@40859
   484
proof -
hoelzl@40859
   485
  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
hoelzl@40859
   486
  have [simp]: "\<And>y. (Pair y -` (\<lambda>(x, y). (y, x)) ` Q) = (\<lambda>x. (x, y)) -` Q"
hoelzl@40859
   487
    by auto
hoelzl@40859
   488
  note sets_pair_sigma_algebra_swap[OF assms]
hoelzl@40859
   489
  from Q.measure_cut_measurable_fst[OF this]
hoelzl@40859
   490
  show ?thesis by simp
hoelzl@40859
   491
qed
hoelzl@40859
   492
hoelzl@40859
   493
lemma (in pair_sigma_algebra) pair_sigma_algebra_measurable:
hoelzl@40859
   494
  assumes "f \<in> measurable P M"
hoelzl@40859
   495
  shows "(\<lambda>(x,y). f (y, x)) \<in> measurable (sigma (pair_algebra M2 M1)) M"
hoelzl@40859
   496
proof -
hoelzl@40859
   497
  interpret Q: pair_sigma_algebra M2 M1 by default
hoelzl@40859
   498
  have *: "(\<lambda>(x,y). f (y, x)) = f \<circ> (\<lambda>(x,y). (y, x))" by (simp add: fun_eq_iff)
hoelzl@40859
   499
  show ?thesis
hoelzl@40859
   500
    using Q.pair_sigma_algebra_swap_measurable assms
hoelzl@40859
   501
    unfolding * by (rule measurable_comp)
hoelzl@39088
   502
qed
hoelzl@39088
   503
hoelzl@40859
   504
lemma (in pair_sigma_algebra) pair_sigma_algebra_swap:
hoelzl@40859
   505
  "sigma (pair_algebra M2 M1) = (vimage_algebra (space M2 \<times> space M1) (\<lambda>(x, y). (y, x)))"
hoelzl@40859
   506
  unfolding vimage_algebra_def
hoelzl@40859
   507
  apply (simp add: sets_sigma)
hoelzl@40859
   508
  apply (subst sigma_sets_vimage[symmetric])
hoelzl@40859
   509
  apply (fastsimp simp: pair_algebra_def)
hoelzl@40859
   510
  using M1.sets_into_space M2.sets_into_space apply (fastsimp simp: pair_algebra_def)
hoelzl@40859
   511
proof -
hoelzl@40859
   512
  have "(\<lambda>X. (\<lambda>(x, y). (y, x)) -` X \<inter> space M2 \<times> space M1) ` sets E
hoelzl@40859
   513
    = sets (pair_algebra M2 M1)" (is "?S = _")
hoelzl@40859
   514
    by (rule pair_algebra_swap)
hoelzl@40859
   515
  then show "sigma (pair_algebra M2 M1) = \<lparr>space = space M2 \<times> space M1,
hoelzl@40859
   516
       sets = sigma_sets (space M2 \<times> space M1) ?S\<rparr>"
hoelzl@40859
   517
    by (simp add: pair_algebra_def sigma_def)
hoelzl@40859
   518
qed
hoelzl@40859
   519
hoelzl@40859
   520
definition (in pair_sigma_finite)
hoelzl@40859
   521
  "pair_measure A = M1.positive_integral (\<lambda>x.
hoelzl@40859
   522
    M2.positive_integral (\<lambda>y. indicator A (x, y)))"
hoelzl@40859
   523
hoelzl@40859
   524
lemma (in pair_sigma_finite) pair_measure_alt:
hoelzl@40859
   525
  assumes "A \<in> sets P"
hoelzl@40859
   526
  shows "pair_measure A = M1.positive_integral (\<lambda>x. \<mu>2 (Pair x -` A))"
hoelzl@40859
   527
  unfolding pair_measure_def
hoelzl@40859
   528
proof (rule M1.positive_integral_cong)
hoelzl@40859
   529
  fix x assume "x \<in> space M1"
hoelzl@40859
   530
  have *: "\<And>y. indicator A (x, y) = (indicator (Pair x -` A) y :: pinfreal)"
hoelzl@40859
   531
    unfolding indicator_def by auto
hoelzl@40859
   532
  show "M2.positive_integral (\<lambda>y. indicator A (x, y)) = \<mu>2 (Pair x -` A)"
hoelzl@40859
   533
    unfolding *
hoelzl@40859
   534
    apply (subst M2.positive_integral_indicator)
hoelzl@40859
   535
    apply (rule measurable_cut_fst[OF assms])
hoelzl@40859
   536
    by simp
hoelzl@40859
   537
qed
hoelzl@40859
   538
hoelzl@40859
   539
lemma (in pair_sigma_finite) pair_measure_times:
hoelzl@40859
   540
  assumes A: "A \<in> sets M1" and "B \<in> sets M2"
hoelzl@40859
   541
  shows "pair_measure (A \<times> B) = \<mu>1 A * \<mu>2 B"
hoelzl@40859
   542
proof -
hoelzl@40859
   543
  from assms have "pair_measure (A \<times> B) =
hoelzl@40859
   544
      M1.positive_integral (\<lambda>x. \<mu>2 B * indicator A x)"
hoelzl@40859
   545
    by (auto intro!: M1.positive_integral_cong simp: pair_measure_alt)
hoelzl@40859
   546
  with assms show ?thesis
hoelzl@40859
   547
    by (simp add: M1.positive_integral_cmult_indicator ac_simps)
hoelzl@40859
   548
qed
hoelzl@40859
   549
hoelzl@40859
   550
lemma (in pair_sigma_finite) sigma_finite_up_in_pair_algebra:
hoelzl@40859
   551
  "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets E \<and> F \<up> space E \<and>
hoelzl@40859
   552
    (\<forall>i. pair_measure (F i) \<noteq> \<omega>)"
hoelzl@40859
   553
proof -
hoelzl@40859
   554
  obtain F1 :: "nat \<Rightarrow> 'a set" and F2 :: "nat \<Rightarrow> 'b set" where
hoelzl@40859
   555
    F1: "range F1 \<subseteq> sets M1" "F1 \<up> space M1" "\<And>i. \<mu>1 (F1 i) \<noteq> \<omega>" and
hoelzl@40859
   556
    F2: "range F2 \<subseteq> sets M2" "F2 \<up> space M2" "\<And>i. \<mu>2 (F2 i) \<noteq> \<omega>"
hoelzl@40859
   557
    using M1.sigma_finite_up M2.sigma_finite_up by auto
hoelzl@40859
   558
  then have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)"
hoelzl@40859
   559
    unfolding isoton_def by auto
hoelzl@40859
   560
  let ?F = "\<lambda>i. F1 i \<times> F2 i"
hoelzl@40859
   561
  show ?thesis unfolding isoton_def space_pair_algebra
hoelzl@40859
   562
  proof (intro exI[of _ ?F] conjI allI)
hoelzl@40859
   563
    show "range ?F \<subseteq> sets E" using F1 F2
hoelzl@40859
   564
      by (fastsimp intro!: pair_algebraI)
hoelzl@40859
   565
  next
hoelzl@40859
   566
    have "space M1 \<times> space M2 \<subseteq> (\<Union>i. ?F i)"
hoelzl@40859
   567
    proof (intro subsetI)
hoelzl@40859
   568
      fix x assume "x \<in> space M1 \<times> space M2"
hoelzl@40859
   569
      then obtain i j where "fst x \<in> F1 i" "snd x \<in> F2 j"
hoelzl@40859
   570
        by (auto simp: space)
hoelzl@40859
   571
      then have "fst x \<in> F1 (max i j)" "snd x \<in> F2 (max j i)"
hoelzl@40859
   572
        using `F1 \<up> space M1` `F2 \<up> space M2`
hoelzl@40859
   573
        by (auto simp: max_def dest: isoton_mono_le)
hoelzl@40859
   574
      then have "(fst x, snd x) \<in> F1 (max i j) \<times> F2 (max i j)"
hoelzl@40859
   575
        by (intro SigmaI) (auto simp add: min_max.sup_commute)
hoelzl@40859
   576
      then show "x \<in> (\<Union>i. ?F i)" by auto
hoelzl@40859
   577
    qed
hoelzl@40859
   578
    then show "(\<Union>i. ?F i) = space M1 \<times> space M2"
hoelzl@40859
   579
      using space by (auto simp: space)
hoelzl@40859
   580
  next
hoelzl@40859
   581
    fix i show "F1 i \<times> F2 i \<subseteq> F1 (Suc i) \<times> F2 (Suc i)"
hoelzl@40859
   582
      using `F1 \<up> space M1` `F2 \<up> space M2` unfolding isoton_def
hoelzl@40859
   583
      by auto
hoelzl@40859
   584
  next
hoelzl@40859
   585
    fix i
hoelzl@40859
   586
    from F1 F2 have "F1 i \<in> sets M1" "F2 i \<in> sets M2" by auto
hoelzl@40859
   587
    with F1 F2 show "pair_measure (F1 i \<times> F2 i) \<noteq> \<omega>"
hoelzl@40859
   588
      by (simp add: pair_measure_times)
hoelzl@40859
   589
  qed
hoelzl@40859
   590
qed
hoelzl@40859
   591
hoelzl@40859
   592
sublocale pair_sigma_finite \<subseteq> sigma_finite_measure P pair_measure
hoelzl@40859
   593
proof
hoelzl@40859
   594
  show "pair_measure {} = 0"
hoelzl@40859
   595
    unfolding pair_measure_def by auto
hoelzl@40859
   596
hoelzl@40859
   597
  show "countably_additive P pair_measure"
hoelzl@40859
   598
    unfolding countably_additive_def
hoelzl@40859
   599
  proof (intro allI impI)
hoelzl@40859
   600
    fix F :: "nat \<Rightarrow> ('a \<times> 'b) set"
hoelzl@40859
   601
    assume F: "range F \<subseteq> sets P" "disjoint_family F"
hoelzl@40859
   602
    from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto
hoelzl@40859
   603
    moreover from F have "\<And>i. (\<lambda>x. \<mu>2 (Pair x -` F i)) \<in> borel_measurable M1"
hoelzl@40859
   604
      by (intro measure_cut_measurable_fst) auto
hoelzl@40859
   605
    moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x -` F i)"
hoelzl@40859
   606
      by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
hoelzl@40859
   607
    moreover have "\<And>x. x \<in> space M1 \<Longrightarrow> range (\<lambda>i. Pair x -` F i) \<subseteq> sets M2"
hoelzl@40859
   608
      using F by (auto intro!: measurable_cut_fst)
hoelzl@40859
   609
    ultimately show "(\<Sum>\<^isub>\<infinity>n. pair_measure (F n)) = pair_measure (\<Union>i. F i)"
hoelzl@40859
   610
      by (simp add: pair_measure_alt vimage_UN M1.positive_integral_psuminf[symmetric]
hoelzl@40859
   611
                    M2.measure_countably_additive
hoelzl@40859
   612
               cong: M1.positive_integral_cong)
hoelzl@40859
   613
  qed
hoelzl@40859
   614
hoelzl@40859
   615
  from sigma_finite_up_in_pair_algebra guess F :: "nat \<Rightarrow> ('a \<times> 'c) set" .. note F = this
hoelzl@40859
   616
  show "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> sets P \<and> (\<Union>i. F i) = space P \<and> (\<forall>i. pair_measure (F i) \<noteq> \<omega>)"
hoelzl@40859
   617
  proof (rule exI[of _ F], intro conjI)
hoelzl@40859
   618
    show "range F \<subseteq> sets P" using F by auto
hoelzl@40859
   619
    show "(\<Union>i. F i) = space P"
hoelzl@40859
   620
      using F by (auto simp: space_pair_algebra isoton_def)
hoelzl@40859
   621
    show "\<forall>i. pair_measure (F i) \<noteq> \<omega>" using F by auto
hoelzl@40859
   622
  qed
hoelzl@40859
   623
qed
hoelzl@39088
   624
hoelzl@40859
   625
lemma (in pair_sigma_finite) pair_measure_alt2:
hoelzl@40859
   626
  assumes "A \<in> sets P"
hoelzl@40859
   627
  shows "pair_measure A = M2.positive_integral (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` A))"
hoelzl@40859
   628
    (is "_ = ?\<nu> A")
hoelzl@40859
   629
proof -
hoelzl@40859
   630
  from sigma_finite_up_in_pair_algebra guess F :: "nat \<Rightarrow> ('a \<times> 'c) set" .. note F = this
hoelzl@40859
   631
  show ?thesis
hoelzl@40859
   632
  proof (rule measure_unique_Int_stable[where \<nu>="?\<nu>", OF Int_stable_pair_algebra],
hoelzl@40859
   633
         simp_all add: pair_sigma_algebra_def[symmetric])
hoelzl@40859
   634
    show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. pair_measure (F i) \<noteq> \<omega>"
hoelzl@40859
   635
      using F by auto
hoelzl@40859
   636
    show "measure_space P pair_measure" by default
hoelzl@40859
   637
  next
hoelzl@40859
   638
    show "measure_space P ?\<nu>"
hoelzl@40859
   639
    proof
hoelzl@40859
   640
      show "?\<nu> {} = 0" by auto
hoelzl@40859
   641
      show "countably_additive P ?\<nu>"
hoelzl@40859
   642
        unfolding countably_additive_def
hoelzl@40859
   643
      proof (intro allI impI)
hoelzl@40859
   644
        fix F :: "nat \<Rightarrow> ('a \<times> 'b) set"
hoelzl@40859
   645
        assume F: "range F \<subseteq> sets P" "disjoint_family F"
hoelzl@40859
   646
        from F have *: "\<And>i. F i \<in> sets P" "(\<Union>i. F i) \<in> sets P" by auto
hoelzl@40859
   647
        moreover from F have "\<And>i. (\<lambda>y. \<mu>1 ((\<lambda>x. (x, y)) -` F i)) \<in> borel_measurable M2"
hoelzl@40859
   648
          by (intro measure_cut_measurable_snd) auto
hoelzl@40859
   649
        moreover have "\<And>y. disjoint_family (\<lambda>i. (\<lambda>x. (x, y)) -` F i)"
hoelzl@40859
   650
          by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
hoelzl@40859
   651
        moreover have "\<And>y. y \<in> space M2 \<Longrightarrow> range (\<lambda>i. (\<lambda>x. (x, y)) -` F i) \<subseteq> sets M1"
hoelzl@40859
   652
          using F by (auto intro!: measurable_cut_snd)
hoelzl@40859
   653
        ultimately show "(\<Sum>\<^isub>\<infinity>n. ?\<nu> (F n)) = ?\<nu> (\<Union>i. F i)"
hoelzl@40859
   654
          by (simp add: vimage_UN M2.positive_integral_psuminf[symmetric]
hoelzl@40859
   655
                        M1.measure_countably_additive
hoelzl@40859
   656
                   cong: M2.positive_integral_cong)
hoelzl@40859
   657
      qed
hoelzl@40859
   658
    qed
hoelzl@40859
   659
  next
hoelzl@40859
   660
    fix X assume "X \<in> sets E"
hoelzl@40859
   661
    then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
hoelzl@40859
   662
      unfolding pair_algebra_def by auto
hoelzl@40859
   663
    show "pair_measure X = ?\<nu> X"
hoelzl@40859
   664
    proof -
hoelzl@40859
   665
      from AB have "?\<nu> (A \<times> B) =
hoelzl@40859
   666
          M2.positive_integral (\<lambda>y. \<mu>1 A * indicator B y)"
hoelzl@40859
   667
        by (auto intro!: M2.positive_integral_cong)
hoelzl@40859
   668
      with AB show ?thesis
hoelzl@40859
   669
        unfolding pair_measure_times[OF AB] X
hoelzl@40859
   670
        by (simp add: M2.positive_integral_cmult_indicator ac_simps)
hoelzl@40859
   671
    qed
hoelzl@40859
   672
  qed fact
hoelzl@40859
   673
qed
hoelzl@40859
   674
hoelzl@40859
   675
section "Fubinis theorem"
hoelzl@40859
   676
hoelzl@40859
   677
lemma (in pair_sigma_finite) simple_function_cut:
hoelzl@40859
   678
  assumes f: "simple_function f"
hoelzl@40859
   679
  shows "(\<lambda>x. M2.positive_integral (\<lambda> y. f (x, y))) \<in> borel_measurable M1"
hoelzl@40859
   680
    and "M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. f (x, y)))
hoelzl@40859
   681
      = positive_integral f"
hoelzl@40859
   682
proof -
hoelzl@40859
   683
  have f_borel: "f \<in> borel_measurable P"
hoelzl@40859
   684
    using f by (rule borel_measurable_simple_function)
hoelzl@40859
   685
  let "?F z" = "f -` {z} \<inter> space P"
hoelzl@40859
   686
  let "?F' x z" = "Pair x -` ?F z"
hoelzl@40859
   687
  { fix x assume "x \<in> space M1"
hoelzl@40859
   688
    have [simp]: "\<And>z y. indicator (?F z) (x, y) = indicator (?F' x z) y"
hoelzl@40859
   689
      by (auto simp: indicator_def)
hoelzl@40859
   690
    have "\<And>y. y \<in> space M2 \<Longrightarrow> (x, y) \<in> space P" using `x \<in> space M1`
hoelzl@40859
   691
      by (simp add: space_pair_algebra)
hoelzl@40859
   692
    moreover have "\<And>x z. ?F' x z \<in> sets M2" using f_borel
hoelzl@40859
   693
      by (intro borel_measurable_vimage measurable_cut_fst)
hoelzl@40859
   694
    ultimately have "M2.simple_function (\<lambda> y. f (x, y))"
hoelzl@40859
   695
      apply (rule_tac M2.simple_function_cong[THEN iffD2, OF _])
hoelzl@40859
   696
      apply (rule simple_function_indicator_representation[OF f])
hoelzl@40859
   697
      using `x \<in> space M1` by (auto simp del: space_sigma) }
hoelzl@40859
   698
  note M2_sf = this
hoelzl@40859
   699
  { fix x assume x: "x \<in> space M1"
hoelzl@40859
   700
    then have "M2.positive_integral (\<lambda> y. f (x, y)) =
hoelzl@40859
   701
        (\<Sum>z\<in>f ` space P. z * \<mu>2 (?F' x z))"
hoelzl@40859
   702
      unfolding M2.positive_integral_eq_simple_integral[OF M2_sf[OF x]]
hoelzl@40859
   703
      unfolding M2.simple_integral_def
hoelzl@40859
   704
    proof (safe intro!: setsum_mono_zero_cong_left)
hoelzl@40859
   705
      from f show "finite (f ` space P)" by (rule simple_functionD)
hoelzl@40859
   706
    next
hoelzl@40859
   707
      fix y assume "y \<in> space M2" then show "f (x, y) \<in> f ` space P"
hoelzl@40859
   708
        using `x \<in> space M1` by (auto simp: space_pair_algebra)
hoelzl@40859
   709
    next
hoelzl@40859
   710
      fix x' y assume "(x', y) \<in> space P"
hoelzl@40859
   711
        "f (x', y) \<notin> (\<lambda>y. f (x, y)) ` space M2"
hoelzl@40859
   712
      then have *: "?F' x (f (x', y)) = {}"
hoelzl@40859
   713
        by (force simp: space_pair_algebra)
hoelzl@40859
   714
      show  "f (x', y) * \<mu>2 (?F' x (f (x', y))) = 0"
hoelzl@40859
   715
        unfolding * by simp
hoelzl@40859
   716
    qed (simp add: vimage_compose[symmetric] comp_def
hoelzl@40859
   717
                   space_pair_algebra) }
hoelzl@40859
   718
  note eq = this
hoelzl@40859
   719
  moreover have "\<And>z. ?F z \<in> sets P"
hoelzl@40859
   720
    by (auto intro!: f_borel borel_measurable_vimage simp del: space_sigma)
hoelzl@40859
   721
  moreover then have "\<And>z. (\<lambda>x. \<mu>2 (?F' x z)) \<in> borel_measurable M1"
hoelzl@40859
   722
    by (auto intro!: measure_cut_measurable_fst simp del: vimage_Int)
hoelzl@40859
   723
  ultimately
hoelzl@40859
   724
  show "(\<lambda> x. M2.positive_integral (\<lambda> y. f (x, y))) \<in> borel_measurable M1"
hoelzl@40859
   725
    and "M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. f (x, y)))
hoelzl@40859
   726
    = positive_integral f"
hoelzl@40859
   727
    by (auto simp del: vimage_Int cong: measurable_cong
hoelzl@40859
   728
             intro!: M1.borel_measurable_pinfreal_setsum
hoelzl@40859
   729
             simp add: M1.positive_integral_setsum simple_integral_def
hoelzl@40859
   730
                       M1.positive_integral_cmult
hoelzl@40859
   731
                       M1.positive_integral_cong[OF eq]
hoelzl@40859
   732
                       positive_integral_eq_simple_integral[OF f]
hoelzl@40859
   733
                       pair_measure_alt[symmetric])
hoelzl@40859
   734
qed
hoelzl@40859
   735
hoelzl@40859
   736
lemma (in pair_sigma_finite) positive_integral_fst_measurable:
hoelzl@40859
   737
  assumes f: "f \<in> borel_measurable P"
hoelzl@40859
   738
  shows "(\<lambda> x. M2.positive_integral (\<lambda> y. f (x, y))) \<in> borel_measurable M1"
hoelzl@40859
   739
      (is "?C f \<in> borel_measurable M1")
hoelzl@40859
   740
    and "M1.positive_integral (\<lambda> x. M2.positive_integral (\<lambda> y. f (x, y))) =
hoelzl@40859
   741
      positive_integral f"
hoelzl@40859
   742
proof -
hoelzl@40859
   743
  from borel_measurable_implies_simple_function_sequence[OF f]
hoelzl@40859
   744
  obtain F where F: "\<And>i. simple_function (F i)" "F \<up> f" by auto
hoelzl@40859
   745
  then have F_borel: "\<And>i. F i \<in> borel_measurable P"
hoelzl@40859
   746
    and F_mono: "\<And>i x. F i x \<le> F (Suc i) x"
hoelzl@40859
   747
    and F_SUPR: "\<And>x. (SUP i. F i x) = f x"
hoelzl@40859
   748
    unfolding isoton_def le_fun_def SUPR_fun_expand
hoelzl@40859
   749
    by (auto intro: borel_measurable_simple_function)
hoelzl@40859
   750
  note sf = simple_function_cut[OF F(1)]
hoelzl@40859
   751
  then have "(SUP i. ?C (F i)) \<in> borel_measurable M1"
hoelzl@40859
   752
    using F(1) by (auto intro!: M1.borel_measurable_SUP)
hoelzl@40859
   753
  moreover
hoelzl@40859
   754
  { fix x assume "x \<in> space M1"
hoelzl@40859
   755
    have isotone: "(\<lambda> i y. F i (x, y)) \<up> (\<lambda>y. f (x, y))"
hoelzl@40859
   756
      using `F \<up> f` unfolding isoton_fun_expand
hoelzl@40859
   757
      by (auto simp: isoton_def)
hoelzl@40859
   758
    note measurable_pair_image_snd[OF F_borel`x \<in> space M1`]
hoelzl@40859
   759
    from M2.positive_integral_isoton[OF isotone this]
hoelzl@40859
   760
    have "(SUP i. ?C (F i) x) = ?C f x"
hoelzl@40859
   761
      by (simp add: isoton_def) }
hoelzl@40859
   762
  note SUPR_C = this
hoelzl@40859
   763
  ultimately show "?C f \<in> borel_measurable M1"
hoelzl@40859
   764
    unfolding SUPR_fun_expand by (simp cong: measurable_cong)
hoelzl@40859
   765
  have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))"
hoelzl@40859
   766
    using F_borel F_mono
hoelzl@40859
   767
    by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])
hoelzl@40859
   768
  also have "(SUP i. positive_integral (F i)) =
hoelzl@40859
   769
    (SUP i. M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. F i (x, y))))"
hoelzl@40859
   770
    unfolding sf(2) by simp
hoelzl@40859
   771
  also have "\<dots> = M1.positive_integral (\<lambda>x. SUP i. M2.positive_integral (\<lambda>y. F i (x, y)))"
hoelzl@40859
   772
    by (auto intro!: M1.positive_integral_monotone_convergence_SUP[OF _ sf(1)]
hoelzl@40859
   773
                     M2.positive_integral_mono F_mono)
hoelzl@40859
   774
  also have "\<dots> = M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. SUP i. F i (x, y)))"
hoelzl@40859
   775
    using F_borel F_mono
hoelzl@40859
   776
    by (auto intro!: M2.positive_integral_monotone_convergence_SUP
hoelzl@40859
   777
                     M1.positive_integral_cong measurable_pair_image_snd)
hoelzl@40859
   778
  finally show "M1.positive_integral (\<lambda> x. M2.positive_integral (\<lambda> y. f (x, y))) =
hoelzl@40859
   779
      positive_integral f"
hoelzl@40859
   780
    unfolding F_SUPR by simp
hoelzl@40859
   781
qed
hoelzl@40859
   782
hoelzl@40859
   783
lemma (in pair_sigma_finite) positive_integral_snd_measurable:
hoelzl@40859
   784
  assumes f: "f \<in> borel_measurable P"
hoelzl@40859
   785
  shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
hoelzl@40859
   786
      positive_integral f"
hoelzl@40859
   787
proof -
hoelzl@40859
   788
  interpret Q: pair_sigma_finite M2 \<mu>2 M1 \<mu>1 by default
hoelzl@40859
   789
hoelzl@40859
   790
  have s: "\<And>x y. (case (x, y) of (x, y) \<Rightarrow> f (y, x)) = f (y, x)" by simp
hoelzl@40859
   791
  have t: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> (y, x))) = (\<lambda>(x, y). f (y, x))" by (auto simp: fun_eq_iff)
hoelzl@40859
   792
hoelzl@40859
   793
  have bij: "bij_betw (\<lambda>(x, y). (y, x)) (space M2 \<times> space M1) (space P)"
hoelzl@40859
   794
    by (auto intro!: inj_onI simp: space_pair_algebra bij_betw_def)
hoelzl@40859
   795
hoelzl@40859
   796
  note pair_sigma_algebra_measurable[OF f]
hoelzl@40859
   797
  from Q.positive_integral_fst_measurable[OF this]
hoelzl@40859
   798
  have "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
hoelzl@40859
   799
    Q.positive_integral (\<lambda>(x, y). f (y, x))"
hoelzl@40859
   800
    by simp
hoelzl@40859
   801
  also have "\<dots> = positive_integral f"
hoelzl@40859
   802
    unfolding positive_integral_vimage[OF bij, of f] t
hoelzl@40859
   803
    unfolding pair_sigma_algebra_swap[symmetric]
hoelzl@40859
   804
  proof (rule Q.positive_integral_cong_measure[symmetric])
hoelzl@40859
   805
    fix A assume "A \<in> sets Q.P"
hoelzl@40859
   806
    from this Q.sets_pair_sigma_algebra_swap[OF this]
hoelzl@40859
   807
    show "pair_measure ((\<lambda>(x, y). (y, x)) ` A) = Q.pair_measure A"
hoelzl@40859
   808
      by (auto intro!: M1.positive_integral_cong arg_cong[where f=\<mu>2]
hoelzl@40859
   809
               simp: pair_measure_alt Q.pair_measure_alt2)
hoelzl@40859
   810
  qed
hoelzl@40859
   811
  finally show ?thesis .
hoelzl@40859
   812
qed
hoelzl@40859
   813
hoelzl@40859
   814
lemma (in pair_sigma_finite) Fubini:
hoelzl@40859
   815
  assumes f: "f \<in> borel_measurable P"
hoelzl@40859
   816
  shows "M2.positive_integral (\<lambda>y. M1.positive_integral (\<lambda>x. f (x, y))) =
hoelzl@40859
   817
      M1.positive_integral (\<lambda>x. M2.positive_integral (\<lambda>y. f (x, y)))"
hoelzl@40859
   818
  unfolding positive_integral_snd_measurable[OF assms]
hoelzl@40859
   819
  unfolding positive_integral_fst_measurable[OF assms] ..
hoelzl@40859
   820
hoelzl@40859
   821
lemma (in pair_sigma_finite) AE_pair:
hoelzl@40859
   822
  assumes "almost_everywhere (\<lambda>x. Q x)"
hoelzl@40859
   823
  shows "M1.almost_everywhere (\<lambda>x. M2.almost_everywhere (\<lambda>y. Q (x, y)))"
hoelzl@40859
   824
proof -
hoelzl@40859
   825
  obtain N where N: "N \<in> sets P" "pair_measure N = 0" "{x\<in>space P. \<not> Q x} \<subseteq> N"
hoelzl@40859
   826
    using assms unfolding almost_everywhere_def by auto
hoelzl@40859
   827
  show ?thesis
hoelzl@40859
   828
  proof (rule M1.AE_I)
hoelzl@40859
   829
    from N measure_cut_measurable_fst[OF `N \<in> sets P`]
hoelzl@40859
   830
    show "\<mu>1 {x\<in>space M1. \<mu>2 (Pair x -` N) \<noteq> 0} = 0"
hoelzl@40859
   831
      by (simp add: M1.positive_integral_0_iff pair_measure_alt vimage_def)
hoelzl@40859
   832
    show "{x \<in> space M1. \<mu>2 (Pair x -` N) \<noteq> 0} \<in> sets M1"
hoelzl@40859
   833
      by (intro M1.borel_measurable_pinfreal_neq_const measure_cut_measurable_fst N)
hoelzl@40859
   834
    { fix x assume "x \<in> space M1" "\<mu>2 (Pair x -` N) = 0"
hoelzl@40859
   835
      have "M2.almost_everywhere (\<lambda>y. Q (x, y))"
hoelzl@40859
   836
      proof (rule M2.AE_I)
hoelzl@40859
   837
        show "\<mu>2 (Pair x -` N) = 0" by fact
hoelzl@40859
   838
        show "Pair x -` N \<in> sets M2" by (intro measurable_cut_fst N)
hoelzl@40859
   839
        show "{y \<in> space M2. \<not> Q (x, y)} \<subseteq> Pair x -` N"
hoelzl@40859
   840
          using N `x \<in> space M1` unfolding space_sigma space_pair_algebra by auto
hoelzl@40859
   841
      qed }
hoelzl@40859
   842
    then show "{x \<in> space M1. \<not> M2.almost_everywhere (\<lambda>y. Q (x, y))} \<subseteq> {x \<in> space M1. \<mu>2 (Pair x -` N) \<noteq> 0}"
hoelzl@40859
   843
      by auto
hoelzl@39088
   844
  qed
hoelzl@39088
   845
qed
hoelzl@35833
   846
hoelzl@40859
   847
section "Finite product spaces"
hoelzl@40859
   848
hoelzl@40859
   849
section "Products"
hoelzl@40859
   850
hoelzl@40859
   851
locale product_sigma_algebra =
hoelzl@40859
   852
  fixes M :: "'i \<Rightarrow> 'a algebra"
hoelzl@40859
   853
  assumes sigma_algebras: "\<And>i. sigma_algebra (M i)"
hoelzl@40859
   854
hoelzl@40859
   855
locale finite_product_sigma_algebra = product_sigma_algebra M for M :: "'i \<Rightarrow> 'a algebra" +
hoelzl@40859
   856
  fixes I :: "'i set"
hoelzl@40859
   857
  assumes finite_index: "finite I"
hoelzl@40859
   858
hoelzl@40859
   859
syntax
hoelzl@40859
   860
  "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
hoelzl@40859
   861
hoelzl@40859
   862
syntax (xsymbols)
hoelzl@40859
   863
  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
hoelzl@40859
   864
hoelzl@40859
   865
syntax (HTML output)
hoelzl@40859
   866
  "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)"   10)
hoelzl@40859
   867
hoelzl@40859
   868
translations
hoelzl@40859
   869
  "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
hoelzl@40859
   870
hoelzl@35833
   871
definition
hoelzl@40859
   872
  "product_algebra M I = \<lparr> space = (\<Pi>\<^isub>E i\<in>I. space (M i)), sets = Pi\<^isub>E I ` (\<Pi> i \<in> I. sets (M i)) \<rparr>"
hoelzl@40859
   873
hoelzl@40859
   874
abbreviation (in finite_product_sigma_algebra) "G \<equiv> product_algebra M I"
hoelzl@40859
   875
abbreviation (in finite_product_sigma_algebra) "P \<equiv> sigma G"
hoelzl@40859
   876
hoelzl@40859
   877
sublocale product_sigma_algebra \<subseteq> M: sigma_algebra "M i" for i by (rule sigma_algebras)
hoelzl@40859
   878
hoelzl@40859
   879
lemma (in finite_product_sigma_algebra) product_algebra_into_space:
hoelzl@40859
   880
  "sets G \<subseteq> Pow (space G)"
hoelzl@40859
   881
  using M.sets_into_space unfolding product_algebra_def
hoelzl@40859
   882
  by auto blast
hoelzl@40859
   883
hoelzl@40859
   884
sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P
hoelzl@40859
   885
  using product_algebra_into_space by (rule sigma_algebra_sigma)
hoelzl@40859
   886
hoelzl@40859
   887
lemma space_product_algebra[simp]:
hoelzl@40859
   888
  "space (product_algebra M I) = Pi\<^isub>E I (\<lambda>i. space (M i))"
hoelzl@40859
   889
  unfolding product_algebra_def by simp
hoelzl@40859
   890
hoelzl@40859
   891
lemma (in finite_product_sigma_algebra) P_empty:
hoelzl@40859
   892
  "I = {} \<Longrightarrow> P = \<lparr> space = {\<lambda>k. undefined}, sets = { {}, {\<lambda>k. undefined} }\<rparr>"
hoelzl@40859
   893
  unfolding product_algebra_def by (simp add: sigma_def)
hoelzl@40859
   894
hoelzl@40859
   895
lemma (in finite_product_sigma_algebra) in_P[simp, intro]:
hoelzl@40859
   896
  "\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
hoelzl@40859
   897
  by (auto simp: product_algebra_def sets_sigma intro!: sigma_sets.Basic)
hoelzl@40859
   898
hoelzl@40859
   899
lemma bij_betw_prod_fold:
hoelzl@40859
   900
  assumes "i \<notin> I"
hoelzl@40859
   901
  shows "bij_betw (\<lambda>x. (x(i:=undefined), x i)) (\<Pi>\<^isub>E j\<in>insert i I. space (M j)) ((\<Pi>\<^isub>E j\<in>I. space (M j)) \<times> space (M i))"
hoelzl@40859
   902
    (is "bij_betw ?f ?P ?F")
hoelzl@40859
   903
    using `i \<notin> I`
hoelzl@40859
   904
proof (unfold bij_betw_def, intro conjI set_eqI iffI)
hoelzl@40859
   905
  show "inj_on ?f ?P"
hoelzl@40859
   906
  proof (safe intro!: inj_onI ext)
hoelzl@40859
   907
    fix a b x assume "a(i:=undefined) = b(i:=undefined)" "a i = b i"
hoelzl@40859
   908
    then show "a x = b x"
hoelzl@40859
   909
      by (cases "x = i") (auto simp: fun_eq_iff split: split_if_asm)
hoelzl@40859
   910
  qed
hoelzl@40859
   911
next
hoelzl@40859
   912
  fix X assume *: "X \<in> ?F" show "X \<in> ?f ` ?P"
hoelzl@40859
   913
  proof (cases X)
hoelzl@40859
   914
    case (Pair a b) with * `i \<notin> I` show ?thesis
hoelzl@40859
   915
      by (auto intro!: image_eqI[where x="a (i := b)"] ext simp: extensional_def)
hoelzl@40859
   916
  qed
hoelzl@40859
   917
qed auto
hoelzl@40859
   918
hoelzl@40859
   919
section "Generating set generates also product algebra"
hoelzl@40859
   920
hoelzl@40859
   921
lemma pair_sigma_algebra_sigma:
hoelzl@40859
   922
  assumes 1: "S1 \<up> (space E1)" "range S1 \<subseteq> sets E1" and E1: "sets E1 \<subseteq> Pow (space E1)"
hoelzl@40859
   923
  assumes 2: "S2 \<up> (space E2)" "range S2 \<subseteq> sets E2" and E2: "sets E2 \<subseteq> Pow (space E2)"
hoelzl@40859
   924
  shows "sigma (pair_algebra (sigma E1) (sigma E2)) = sigma (pair_algebra E1 E2)"
hoelzl@40859
   925
    (is "?S = ?E")
hoelzl@40859
   926
proof -
hoelzl@40859
   927
  interpret M1: sigma_algebra "sigma E1" using E1 by (rule sigma_algebra_sigma)
hoelzl@40859
   928
  interpret M2: sigma_algebra "sigma E2" using E2 by (rule sigma_algebra_sigma)
hoelzl@40859
   929
  have P: "sets (pair_algebra E1 E2) \<subseteq> Pow (space E1 \<times> space E2)"
hoelzl@40859
   930
    using E1 E2 by (auto simp add: pair_algebra_def)
hoelzl@40859
   931
  interpret E: sigma_algebra ?E unfolding pair_algebra_def
hoelzl@40859
   932
    using E1 E2 by (intro sigma_algebra_sigma) auto
hoelzl@40859
   933
hoelzl@40859
   934
  { fix A assume "A \<in> sets E1"
hoelzl@40859
   935
    then have "fst -` A \<inter> space ?E = A \<times> (\<Union>i. S2 i)"
hoelzl@40859
   936
      using E1 2 unfolding isoton_def pair_algebra_def by auto
hoelzl@40859
   937
    also have "\<dots> = (\<Union>i. A \<times> S2 i)" by auto
hoelzl@40859
   938
    also have "\<dots> \<in> sets ?E" unfolding pair_algebra_def sets_sigma
hoelzl@40859
   939
      using 2 `A \<in> sets E1`
hoelzl@40859
   940
      by (intro sigma_sets.Union)
hoelzl@40859
   941
         (auto simp: image_subset_iff intro!: sigma_sets.Basic)
hoelzl@40859
   942
    finally have "fst -` A \<inter> space ?E \<in> sets ?E" . }
hoelzl@40859
   943
  moreover
hoelzl@40859
   944
  { fix B assume "B \<in> sets E2"
hoelzl@40859
   945
    then have "snd -` B \<inter> space ?E = (\<Union>i. S1 i) \<times> B"
hoelzl@40859
   946
      using E2 1 unfolding isoton_def pair_algebra_def by auto
hoelzl@40859
   947
    also have "\<dots> = (\<Union>i. S1 i \<times> B)" by auto
hoelzl@40859
   948
    also have "\<dots> \<in> sets ?E"
hoelzl@40859
   949
      using 1 `B \<in> sets E2` unfolding pair_algebra_def sets_sigma
hoelzl@40859
   950
      by (intro sigma_sets.Union)
hoelzl@40859
   951
         (auto simp: image_subset_iff intro!: sigma_sets.Basic)
hoelzl@40859
   952
    finally have "snd -` B \<inter> space ?E \<in> sets ?E" . }
hoelzl@40859
   953
  ultimately have proj:
hoelzl@40859
   954
    "fst \<in> measurable ?E (sigma E1) \<and> snd \<in> measurable ?E (sigma E2)"
hoelzl@40859
   955
    using E1 E2 by (subst (1 2) E.measurable_iff_sigma)
hoelzl@40859
   956
                   (auto simp: pair_algebra_def sets_sigma)
hoelzl@40859
   957
hoelzl@40859
   958
  { fix A B assume A: "A \<in> sets (sigma E1)" and B: "B \<in> sets (sigma E2)"
hoelzl@40859
   959
    with proj have "fst -` A \<inter> space ?E \<in> sets ?E" "snd -` B \<inter> space ?E \<in> sets ?E"
hoelzl@40859
   960
      unfolding measurable_def by simp_all
hoelzl@40859
   961
    moreover have "A \<times> B = (fst -` A \<inter> space ?E) \<inter> (snd -` B \<inter> space ?E)"
hoelzl@40859
   962
      using A B M1.sets_into_space M2.sets_into_space
hoelzl@40859
   963
      by (auto simp: pair_algebra_def)
hoelzl@40859
   964
    ultimately have "A \<times> B \<in> sets ?E" by auto }
hoelzl@40859
   965
  then have "sigma_sets (space ?E) (sets (pair_algebra (sigma E1) (sigma E2))) \<subseteq> sets ?E"
hoelzl@40859
   966
    by (intro E.sigma_sets_subset) (auto simp add: pair_algebra_def sets_sigma)
hoelzl@40859
   967
  then have subset: "sets ?S \<subseteq> sets ?E"
hoelzl@40859
   968
    by (simp add: sets_sigma pair_algebra_def)
hoelzl@40859
   969
hoelzl@40859
   970
  have "sets ?S = sets ?E"
hoelzl@40859
   971
  proof (intro set_eqI iffI)
hoelzl@40859
   972
    fix A assume "A \<in> sets ?E" then show "A \<in> sets ?S"
hoelzl@40859
   973
      unfolding sets_sigma
hoelzl@40859
   974
    proof induct
hoelzl@40859
   975
      case (Basic A) then show ?case
hoelzl@40859
   976
        by (auto simp: pair_algebra_def sets_sigma intro: sigma_sets.Basic)
hoelzl@40859
   977
    qed (auto intro: sigma_sets.intros simp: pair_algebra_def)
hoelzl@40859
   978
  next
hoelzl@40859
   979
    fix A assume "A \<in> sets ?S" then show "A \<in> sets ?E" using subset by auto
hoelzl@40859
   980
  qed
hoelzl@40859
   981
  then show ?thesis
hoelzl@40859
   982
    by (simp add: pair_algebra_def sigma_def)
hoelzl@40859
   983
qed
hoelzl@40859
   984
hoelzl@40859
   985
lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
hoelzl@40859
   986
  apply auto
hoelzl@40859
   987
  apply (drule_tac x=x in Pi_mem)
hoelzl@40859
   988
  apply (simp_all split: split_if_asm)
hoelzl@40859
   989
  apply (drule_tac x=i in Pi_mem)
hoelzl@40859
   990
  apply (auto dest!: Pi_mem)
hoelzl@40859
   991
  done
hoelzl@40859
   992
hoelzl@40859
   993
lemma Pi_UN:
hoelzl@40859
   994
  fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
hoelzl@40859
   995
  assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
hoelzl@40859
   996
  shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
hoelzl@40859
   997
proof (intro set_eqI iffI)
hoelzl@40859
   998
  fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
hoelzl@40859
   999
  then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
hoelzl@40859
  1000
  from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
hoelzl@40859
  1001
  obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"