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