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