src/HOL/Probability/Product_Measure.thy
 author hoelzl Tue Mar 16 16:27:28 2010 +0100 (2010-03-16) changeset 35833 7b7ae5aa396d child 35977 30d42bfd0174 permissions -rw-r--r--
```     1 theory Product_Measure
```
```     2 imports "~~/src/HOL/Probability/Lebesgue"
```
```     3 begin
```
```     4
```
```     5 definition
```
```     6   "prod_measure M M' = (\<lambda>a. measure_space.integral M (\<lambda>s0. measure M' ((\<lambda>s1. (s0, s1)) -` a)))"
```
```     7
```
```     8 definition
```
```     9   "prod_measure_space M M' \<equiv>
```
```    10     \<lparr> space = space M \<times> space M',
```
```    11       sets = sets (sigma (space M \<times> space M') (prod_sets (sets M) (sets M'))),
```
```    12       measure = prod_measure M M' \<rparr>"
```
```    13
```
```    14 lemma prod_measure_times:
```
```    15   assumes "measure_space M" and "measure_space M'" and a: "a \<in> sets M"
```
```    16   shows "prod_measure M M' (a \<times> a') = measure M a * measure M' a'"
```
```    17 proof -
```
```    18   interpret M: measure_space M by fact
```
```    19   interpret M': measure_space M' by fact
```
```    20
```
```    21   { fix \<omega>
```
```    22     have "(\<lambda>\<omega>'. (\<omega>, \<omega>')) -` (a \<times> a') = (if \<omega> \<in> a then a' else {})"
```
```    23       by auto
```
```    24     hence "measure M' ((\<lambda>\<omega>'. (\<omega>, \<omega>')) -` (a \<times> a')) =
```
```    25       measure M' a' * indicator_fn a \<omega>"
```
```    26       unfolding indicator_fn_def by auto }
```
```    27   note vimage_eq_indicator = this
```
```    28
```
```    29   show ?thesis
```
```    30     unfolding prod_measure_def vimage_eq_indicator
```
```    31       M.integral_cmul_indicator(1)[OF `a \<in> sets M`]
```
```    32     by simp
```
```    33 qed
```
```    34
```
```    35
```
```    36
```
```    37 lemma measure_space_finite_prod_measure:
```
```    38   fixes M :: "('a, 'b) measure_space_scheme"
```
```    39     and M' :: "('c, 'd) measure_space_scheme"
```
```    40   assumes "measure_space M" and "measure_space M'"
```
```    41   and finM: "finite (space M)" "Pow (space M) = sets M"
```
```    42   and finM': "finite (space M')" "Pow (space M') = sets M'"
```
```    43   shows "measure_space (prod_measure_space M M')"
```
```    44 proof (rule finite_additivity_sufficient)
```
```    45   interpret M: measure_space M by fact
```
```    46   interpret M': measure_space M' by fact
```
```    47
```
```    48   have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'"
```
```    49     unfolding prod_measure_space_def by simp
```
```    50
```
```    51   have prod_sets: "prod_sets (sets M) (sets M') \<subseteq> Pow (space M \<times> space M')"
```
```    52     using M.sets_into_space M'.sets_into_space unfolding prod_sets_def by auto
```
```    53   show sigma: "sigma_algebra (prod_measure_space M M')" unfolding prod_measure_space_def
```
```    54     by (rule sigma_algebra_sigma_sets[where a="prod_sets (sets M) (sets M')"])
```
```    55        (simp_all add: sigma_def prod_sets)
```
```    56
```
```    57   then interpret sa: sigma_algebra "prod_measure_space M M'" .
```
```    58
```
```    59   { fix x y assume "y \<in> sets (prod_measure_space M M')" and "x \<in> space M"
```
```    60     hence "y \<subseteq> space M \<times> space M'"
```
```    61       using sa.sets_into_space unfolding prod_measure_space_def by simp
```
```    62     hence "Pair x -` y \<in> sets M'"
```
```    63       using `x \<in> space M` unfolding finM'(2)[symmetric] by auto }
```
```    64   note Pair_in_sets = this
```
```    65
```
```    66   show "additive (prod_measure_space M M') (measure (prod_measure_space M M'))"
```
```    67     unfolding measure additive_def
```
```    68   proof safe
```
```    69     fix x y assume x: "x \<in> sets (prod_measure_space M M')" and y: "y \<in> sets (prod_measure_space M M')"
```
```    70       and disj_x_y: "x \<inter> y = {}"
```
```    71     { fix z have "Pair z -` x \<inter> Pair z -` y = {}" using disj_x_y by auto }
```
```    72     note Pair_disj = this
```
```    73
```
```    74     from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric]
```
```    75     show "prod_measure M M' (x \<union> y) = prod_measure M M' x + prod_measure M M' y"
```
```    76       unfolding prod_measure_def
```
```    77       apply (subst (1 2 3) M.integral_finite_singleton[OF finM])
```
```    78       by (simp_all add: setsum_addf[symmetric] field_simps)
```
```    79   qed
```
```    80
```
```    81   show "finite (space (prod_measure_space M M'))"
```
```    82     unfolding prod_measure_space_def using finM finM' by simp
```
```    83
```
```    84   have singletonM: "\<And>x. x \<in> space M \<Longrightarrow> {x} \<in> sets M"
```
```    85     unfolding finM(2)[symmetric] by simp
```
```    86
```
```    87   show "positive (prod_measure_space M M') (measure (prod_measure_space M M'))"
```
```    88     unfolding positive_def
```
```    89   proof (safe, simp add: M.integral_zero prod_measure_space_def prod_measure_def)
```
```    90     fix Q assume "Q \<in> sets (prod_measure_space M M')"
```
```    91     from Pair_in_sets[OF this]
```
```    92     show "0 \<le> measure (prod_measure_space M M') Q"
```
```    93       unfolding prod_measure_space_def prod_measure_def
```
```    94       apply (subst M.integral_finite_singleton[OF finM])
```
```    95       using M.positive M'.positive singletonM
```
```    96       by (auto intro!: setsum_nonneg mult_nonneg_nonneg)
```
```    97   qed
```
```    98 qed
```
```    99
```
```   100 lemma measure_space_finite_prod_measure_alterantive:
```
```   101   assumes "measure_space M" and "measure_space M'"
```
```   102   and finM: "finite (space M)" "Pow (space M) = sets M"
```
```   103   and finM': "finite (space M')" "Pow (space M') = sets M'"
```
```   104   shows "measure_space \<lparr> space = space M \<times> space M',
```
```   105                          sets = Pow (space M \<times> space M'),
```
```   106 		         measure = prod_measure M M' \<rparr>"
```
```   107   (is "measure_space ?space")
```
```   108 proof (rule finite_additivity_sufficient)
```
```   109   interpret M: measure_space M by fact
```
```   110   interpret M': measure_space M' by fact
```
```   111
```
```   112   show "sigma_algebra ?space"
```
```   113     using sigma_algebra.sigma_algebra_extend[where M="\<lparr> space = space M \<times> space M', sets = Pow (space M \<times> space M') \<rparr>"]
```
```   114     by (auto intro!: sigma_algebra_Pow)
```
```   115   then interpret sa: sigma_algebra ?space .
```
```   116
```
```   117   have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'"
```
```   118     unfolding prod_measure_space_def by simp
```
```   119
```
```   120   { fix x y assume "y \<in> sets ?space" and "x \<in> space M"
```
```   121     hence "y \<subseteq> space M \<times> space M'"
```
```   122       using sa.sets_into_space by simp
```
```   123     hence "Pair x -` y \<in> sets M'"
```
```   124       using `x \<in> space M` unfolding finM'(2)[symmetric] by auto }
```
```   125   note Pair_in_sets = this
```
```   126
```
```   127   show "additive ?space (measure ?space)"
```
```   128     unfolding measure additive_def
```
```   129   proof safe
```
```   130     fix x y assume x: "x \<in> sets ?space" and y: "y \<in> sets ?space"
```
```   131       and disj_x_y: "x \<inter> y = {}"
```
```   132     { fix z have "Pair z -` x \<inter> Pair z -` y = {}" using disj_x_y by auto }
```
```   133     note Pair_disj = this
```
```   134
```
```   135     from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric]
```
```   136     show "measure ?space (x \<union> y) = measure ?space x + measure ?space y"
```
```   137       apply (simp add: prod_measure_def)
```
```   138       apply (subst (1 2 3) M.integral_finite_singleton[OF finM])
```
```   139       by (simp_all add: setsum_addf[symmetric] field_simps)
```
```   140   qed
```
```   141
```
```   142   show "finite (space ?space)" using finM finM' by simp
```
```   143
```
```   144   have singletonM: "\<And>x. x \<in> space M \<Longrightarrow> {x} \<in> sets M"
```
```   145     unfolding finM(2)[symmetric] by simp
```
```   146
```
```   147   show "positive ?space (measure ?space)"
```
```   148     unfolding positive_def
```
```   149   proof (safe, simp add: M.integral_zero prod_measure_def)
```
```   150     fix Q assume "Q \<in> sets ?space"
```
```   151     from Pair_in_sets[OF this]
```
```   152     show "0 \<le> measure ?space Q"
```
```   153       unfolding prod_measure_space_def prod_measure_def
```
```   154       apply (subst M.integral_finite_singleton[OF finM])
```
```   155       using M.positive M'.positive singletonM
```
```   156       by (auto intro!: setsum_nonneg mult_nonneg_nonneg)
```
```   157   qed
```
```   158 qed
```
```   159
```
`   160 end`