src/HOL/Probability/Product_Measure.thy
author hoelzl
Mon, 23 Aug 2010 19:35:57 +0200
changeset 38656 d5d342611edb
parent 36649 bfd8c550faa6
child 38705 aaee86c0e237
permissions -rw-r--r--
Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
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
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
     5
definition prod_sets where
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
     6
  "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
     7
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
     8
definition
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
     9
  "prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))"
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    10
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    11
definition
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    12
  "prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    13
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    14
lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    15
  by (auto simp add: prod_sets_def)
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    16
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    17
lemma sigma_prod_sets_finite:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    18
  assumes "finite A" and "finite B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    19
  shows "sigma_sets (A \<times> B) (prod_sets (Pow A) (Pow B)) = Pow (A \<times> B)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    20
proof safe
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    21
  have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product)
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    22
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    23
  fix x assume subset: "x \<subseteq> A \<times> B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    24
  hence "finite x" using fin by (rule finite_subset)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    25
  from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    26
    (is "x \<in> sigma_sets ?prod ?sets")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    27
  proof (induct x)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    28
    case empty show ?case by (rule sigma_sets.Empty)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    29
  next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    30
    case (insert a x)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    31
    hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    32
    moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    33
    ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    34
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    35
next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    36
  fix x a b
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    37
  assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    38
  from sigma_sets_into_sp[OF _ this(1)] this(2)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    39
  show "a \<in> A" and "b \<in> B"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    40
    by (auto simp: prod_sets_def)
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    41
qed
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    42
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    43
lemma (in sigma_algebra) measurable_prod_sigma:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    44
  assumes sa1: "sigma_algebra a1" and sa2: "sigma_algebra a2"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    45
  assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    46
  shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2))
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    47
                          (prod_sets (sets a1) (sets a2)))"
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35833
diff changeset
    48
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    49
  from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    50
     and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    51
    by (auto simp add: measurable_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    52
  from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    53
     and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    54
    by (auto simp add: measurable_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    55
  show ?thesis
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    56
    proof (rule measurable_sigma)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    57
      show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    58
        by (auto simp add: prod_sets_def sigma_algebra_iff dest: algebra.space_closed)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    59
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    60
      show "f \<in> space M \<rightarrow> space a1 \<times> space a2"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    61
        by (rule prod_final [OF fn1 fn2])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    62
    next
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    63
      fix z
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    64
      assume z: "z \<in> prod_sets (sets a1) (sets a2)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    65
      thus "f -` z \<inter> space M \<in> sets M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    66
        proof (auto simp add: prod_sets_def vimage_Times)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    67
          fix x y
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    68
          assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    69
          have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    70
                ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    71
            by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    72
          also have "...  \<in> sets M" using x y q1 q2
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    73
            by blast
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    74
          finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    75
        qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    76
    qed
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35833
diff changeset
    77
qed
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    78
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    79
lemma (in sigma_finite_measure) prod_measure_times:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    80
  assumes "sigma_finite_measure N \<nu>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    81
  and "A1 \<in> sets M" "A2 \<in> sets N"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    82
  shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    83
  oops
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    84
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    85
lemma (in sigma_finite_measure) sigma_finite_prod_measure_space:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    86
  assumes "sigma_finite_measure N \<nu>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    87
  shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    88
  oops
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    89
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    90
lemma (in finite_measure_space) simple_function_finite:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    91
  "simple_function f"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    92
  unfolding simple_function_def sets_eq_Pow using finite_space by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    93
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    94
lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \<in> borel_measurable M"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    95
  unfolding measurable_def sets_eq_Pow by auto
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
    96
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    97
lemma (in finite_measure_space) positive_integral_finite_eq_setsum:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    98
  "positive_integral f = (\<Sum>x \<in> space M. f x * \<mu> {x})"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    99
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   100
  have *: "positive_integral f = positive_integral (\<lambda>x. \<Sum>y\<in>space M. f y * indicator {y} x)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   101
    by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   102
  show ?thesis unfolding * using borel_measurable_finite[of f]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   103
    by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   104
qed
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
   105
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   106
lemma (in finite_measure_space) finite_prod_measure_times:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   107
  assumes "finite_measure_space N \<nu>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   108
  and "A1 \<in> sets M" "A2 \<in> sets N"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   109
  shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   110
proof -
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   111
  interpret N: finite_measure_space N \<nu> by fact
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   112
  have *: "\<And>x. \<nu> (Pair x -` (A1 \<times> A2)) * \<mu> {x} = (if x \<in> A1 then \<nu> A2 * \<mu> {x} else 0)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   113
    by (auto simp: vimage_Times comp_def)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   114
  have "finite A1"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   115
    using `A1 \<in> sets M` finite_space by (auto simp: sets_eq_Pow intro: finite_subset)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   116
  then have "\<mu> A1 = (\<Sum>x\<in>A1. \<mu> {x})" using `A1 \<in> sets M`
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   117
    by (auto intro!: measure_finite_singleton simp: sets_eq_Pow)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   118
  then show ?thesis using `A1 \<in> sets M`
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   119
    unfolding prod_measure_def positive_integral_finite_eq_setsum *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   120
    by (auto simp add: sets_eq_Pow setsum_right_distrib[symmetric] mult_commute setsum_cases[OF finite_space])
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
   121
qed
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
   122
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   123
lemma (in finite_measure_space) finite_prod_measure_space:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   124
  assumes "finite_measure_space N \<nu>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   125
  shows "prod_measure_space M N = \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr>"
35977
30d42bfd0174 Added finite measure space.
hoelzl
parents: 35833
diff changeset
   126
proof -
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   127
  interpret N: finite_measure_space N \<nu> by fact
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   128
  show ?thesis using finite_space N.finite_space
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   129
    by (simp add: sigma_def prod_measure_space_def sigma_prod_sets_finite sets_eq_Pow N.sets_eq_Pow)
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
   130
qed
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
   131
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   132
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   133
  assumes "finite_measure_space N \<nu>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   134
  shows "finite_measure_space (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   135
  unfolding finite_prod_measure_space[OF assms]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   136
proof (rule finite_measure_spaceI)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   137
  interpret N: finite_measure_space N \<nu> by fact
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   138
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   139
  let ?P = "\<lparr>space = space M \<times> space N, sets = Pow (space M \<times> space N)\<rparr>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   140
  show "measure_space ?P (prod_measure M \<mu> N \<nu>)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   141
  proof (rule sigma_algebra.finite_additivity_sufficient)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   142
    show "sigma_algebra ?P" by (rule sigma_algebra_Pow)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   143
    show "finite (space ?P)" using finite_space N.finite_space by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   144
    from finite_prod_measure_times[OF assms, of "{}" "{}"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   145
    show "positive (prod_measure M \<mu> N \<nu>)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   146
      unfolding positive_def by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   147
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   148
    show "additive ?P (prod_measure M \<mu> N \<nu>)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   149
      unfolding additive_def
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   150
      apply (auto simp add: sets_eq_Pow prod_measure_def positive_integral_add[symmetric]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   151
                  intro!: positive_integral_cong)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   152
      apply (subst N.measure_additive[symmetric])
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   153
      by (auto simp: N.sets_eq_Pow sets_eq_Pow)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   154
  qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   155
  show "finite (space ?P)" using finite_space N.finite_space by auto
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   156
  show "sets ?P = Pow (space ?P)" by simp
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   157
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   158
  fix x assume "x \<in> space ?P"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   159
  with finite_prod_measure_times[OF assms, of "{fst x}" "{snd x}"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   160
    finite_measure[of "{fst x}"] N.finite_measure[of "{snd x}"]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   161
  show "prod_measure M \<mu> N \<nu> {x} \<noteq> \<omega>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   162
    by (auto simp add: sets_eq_Pow N.sets_eq_Pow elim!: SigmaE)
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   163
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   164
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   165
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure_alterantive:
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   166
  assumes N: "finite_measure_space N \<nu>"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   167
  shows "finite_measure_space \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr> (prod_measure M \<mu> N \<nu>)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   168
    (is "finite_measure_space ?M ?m")
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   169
  unfolding finite_prod_measure_space[OF N, symmetric]
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   170
  using finite_measure_space_finite_prod_measure[OF N] .
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   171
35833
7b7ae5aa396d Added product measure space
hoelzl
parents:
diff changeset
   172
end