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