src/HOL/Probability/Product_Measure.thy
author hellerar
Thu Sep 02 15:31:38 2010 +0200 (2010-09-02)
changeset 39094 67da17aced5a
parent 39080 cae59dc0a094
child 39095 f92b7e2877c2
permissions -rw-r--r--
measure unique
hoelzl@35833
     1
theory Product_Measure
hoelzl@38656
     2
imports Lebesgue_Integration
hoelzl@35833
     3
begin
hoelzl@35833
     4
hellerar@39080
     5
definition dynkin
hellerar@39080
     6
where "dynkin M =
hellerar@39080
     7
      ((\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
hellerar@39094
     8
       space M \<in> sets M \<and> (\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M) \<and>
hellerar@39080
     9
       (\<forall> a. (\<forall> i j :: nat. i \<noteq> j \<longrightarrow> a i \<inter> a j = {}) \<and>
hellerar@39080
    10
             (\<forall> i :: nat. a i \<in> sets M) \<longrightarrow> UNION UNIV a \<in> sets M))"
hellerar@39080
    11
hellerar@39080
    12
lemma dynkinI:
hellerar@39080
    13
  assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
hellerar@39094
    14
  assumes "space M \<in> sets M" and "\<forall> b \<in> sets M. \<forall> a \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M"
hellerar@39080
    15
  assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
hellerar@39080
    16
          \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
hellerar@39080
    17
  shows "dynkin M"
hellerar@39080
    18
using assms unfolding dynkin_def by auto
hellerar@39080
    19
hellerar@39080
    20
lemma dynkin_subset:
hellerar@39080
    21
  assumes "dynkin M"
hellerar@39080
    22
  shows "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
hellerar@39080
    23
using assms unfolding dynkin_def by auto
hellerar@39080
    24
hellerar@39080
    25
lemma dynkin_space:
hellerar@39080
    26
  assumes "dynkin M"
hellerar@39080
    27
  shows "space M \<in> sets M"
hellerar@39080
    28
using assms unfolding dynkin_def by auto
hellerar@39080
    29
hellerar@39080
    30
lemma dynkin_diff:
hellerar@39080
    31
  assumes "dynkin M"
hellerar@39094
    32
  shows "\<And> a b. \<lbrakk> a \<in> sets M ; b \<in> sets M ; a \<subseteq> b \<rbrakk> \<Longrightarrow> b - a \<in> sets M"
hellerar@39080
    33
using assms unfolding dynkin_def by auto
hellerar@39080
    34
hellerar@39094
    35
lemma dynkin_empty:
hellerar@39094
    36
  assumes "dynkin M"
hellerar@39094
    37
  shows "{} \<in> sets M"
hellerar@39094
    38
using dynkin_diff[OF assms dynkin_space[OF assms] dynkin_space[OF assms]] by auto
hellerar@39094
    39
hellerar@39080
    40
lemma dynkin_UN:
hellerar@39080
    41
  assumes "dynkin M"
hellerar@39080
    42
  assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
hellerar@39094
    43
  assumes "\<And> i :: nat. a i \<in> sets M"
hellerar@39080
    44
  shows "UNION UNIV a \<in> sets M"
hellerar@39080
    45
using assms unfolding dynkin_def by auto
hellerar@39080
    46
hellerar@39080
    47
definition Int_stable
hellerar@39080
    48
where "Int_stable M = (\<forall> a \<in> sets M. (\<forall> b \<in> sets M. a \<inter> b \<in> sets M))"
hellerar@39080
    49
hellerar@39080
    50
lemma dynkin_trivial:
hellerar@39080
    51
  shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
hellerar@39080
    52
by (rule dynkinI) auto
hellerar@39080
    53
hellerar@39094
    54
lemma dynkin_lemma:
hellerar@39080
    55
  assumes stab: "Int_stable E"
hellerar@39080
    56
  and spac: "space E = space D"
hellerar@39080
    57
  and subsED: "sets E \<subseteq> sets D"
hellerar@39080
    58
  and subsDE: "sets D \<subseteq> sigma_sets (space E) (sets E)"
hellerar@39080
    59
  and dyn: "dynkin D"
hellerar@39080
    60
  shows "sigma (space E) (sets E) = D"
hellerar@39080
    61
proof -
hellerar@39080
    62
  def sets_\<delta>E == "\<Inter> {sets d | d :: 'a algebra. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
hellerar@39080
    63
  def \<delta>E == "\<lparr> space = space E, sets = sets_\<delta>E \<rparr>"
hellerar@39080
    64
  have "\<lparr> space = space E, sets = Pow (space E) \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
hellerar@39080
    65
    using dynkin_trivial spac subsED dynkin_subset[OF dyn] by fastsimp
hellerar@39080
    66
  hence not_empty: "{sets (d :: 'a algebra) | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d} \<noteq> {}"
hellerar@39080
    67
    using exI[of "\<lambda> x. space x = space E \<and> dynkin x \<and> sets E \<subseteq> sets x" "\<lparr> space = space E, sets = Pow (space E) \<rparr>", simplified]
hellerar@39080
    68
    by auto
hellerar@39094
    69
  have \<delta>E_D: "sets_\<delta>E \<subseteq> sets D"
hellerar@39080
    70
    unfolding sets_\<delta>E_def using assms by auto
hellerar@39080
    71
  have \<delta>ynkin: "dynkin \<delta>E"
hellerar@39080
    72
  proof (rule dynkinI, safe)
hellerar@39080
    73
    fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
hellerar@39080
    74
    { fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E"
hellerar@39080
    75
      hence "A \<subseteq> space d"
hellerar@39080
    76
        using dynkin_subset by auto }
hellerar@39080
    77
    show "x \<in> space \<delta>E" using asm
hellerar@39080
    78
      unfolding \<delta>E_def sets_\<delta>E_def using not_empty
hellerar@39080
    79
    proof auto
hellerar@39080
    80
      fix x A fix d :: "'a algebra"
hellerar@39080
    81
      assume asm: "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
hellerar@39080
    82
        dynkin d \<and>
hellerar@39080
    83
        space d = space E \<and>
hellerar@39080
    84
        sets E \<subseteq> sets d) \<longrightarrow>
hellerar@39080
    85
        A \<in> x" "x \<in> A"
hellerar@39080
    86
        and asm': "space d = space E" "dynkin d" "sets E \<subseteq> sets d"
hellerar@39080
    87
      have "A \<in> sets d"
hellerar@39080
    88
        apply (rule impE[OF spec[OF asm(1), of "sets d"]])
hellerar@39080
    89
        using exI[of _ d] asm' by auto
hellerar@39080
    90
      thus "x \<in> space E" using asm' dynkin_subset[OF asm'(2), of A] asm(2) by auto
hellerar@39080
    91
    qed
hellerar@39080
    92
  next
hellerar@39080
    93
    show "space \<delta>E \<in> sets \<delta>E"
hellerar@39080
    94
      unfolding \<delta>E_def sets_\<delta>E_def
hellerar@39080
    95
      using dynkin_space by fastsimp
hellerar@39080
    96
  next
hellerar@39094
    97
    fix a b assume "a \<in> sets \<delta>E" "b \<in> sets \<delta>E" "a \<subseteq> b"
hellerar@39080
    98
    thus "b - a \<in> sets \<delta>E"
hellerar@39080
    99
      unfolding \<delta>E_def sets_\<delta>E_def by (auto intro:dynkin_diff)
hellerar@39080
   100
  next
hellerar@39080
   101
    fix a assume asm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> sets \<delta>E"
hellerar@39080
   102
    thus "UNION UNIV a \<in> sets \<delta>E"
hellerar@39080
   103
      unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)])
hellerar@39080
   104
      by blast
hellerar@39080
   105
  qed
hellerar@39080
   106
  def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}"
hellerar@39080
   107
  { fix d assume dasm: "d \<in> sets_\<delta>E"
hellerar@39080
   108
    have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>"
hellerar@39080
   109
    proof (rule dynkinI, auto)
hellerar@39080
   110
      fix A x assume "A \<in> Dy d" "x \<in> A"
hellerar@39080
   111
      thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty
hellerar@39080
   112
      proof auto fix x A fix da :: "'a algebra"
hellerar@39080
   113
        assume asm: "x \<in> A"
hellerar@39080
   114
          "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
hellerar@39080
   115
          dynkin d \<and> space d = space E \<and>
hellerar@39080
   116
          sets E \<subseteq> sets d) \<longrightarrow> A \<in> x"
hellerar@39080
   117
          "\<forall>x. (\<exists>d. x = sets d \<and>
hellerar@39080
   118
          dynkin d \<and> space d = space E \<and>
hellerar@39080
   119
          sets E \<subseteq> sets d) \<longrightarrow> A \<inter> d \<in> x"
hellerar@39080
   120
          "space da = space E" "dynkin da"
hellerar@39080
   121
          "sets E \<subseteq> sets da"
hellerar@39080
   122
        have "A \<in> sets da"
hellerar@39080
   123
          apply (rule impE[OF spec[OF asm(2)], of "sets da"])
hellerar@39080
   124
          apply (rule exI[of _ da])
hellerar@39080
   125
          using exI[of _ da] asm(4,5,6) by auto
hellerar@39080
   126
        thus "x \<in> space E" using dynkin_subset[OF asm(5)] asm by auto
hellerar@39080
   127
      qed
hellerar@39080
   128
    next
hellerar@39080
   129
      show "space E \<in> Dy d"
hellerar@39080
   130
        unfolding Dy_def \<delta>E_def sets_\<delta>E_def
hellerar@39080
   131
      proof auto
hellerar@39080
   132
        fix d assume asm: "dynkin d" "space d = space E" "sets E \<subseteq> sets d"
hellerar@39080
   133
        hence "space d \<in> sets d" using dynkin_space[OF asm(1)] by auto
hellerar@39080
   134
        thus "space E \<in> sets d" using asm by auto
hellerar@39080
   135
      next
hellerar@39080
   136
        fix da :: "'a algebra" assume asm: "dynkin da" "space da = space E" "sets E \<subseteq> sets da"
hellerar@39080
   137
        have d: "d = space E \<inter> d"
hellerar@39080
   138
          using dasm dynkin_subset[OF asm(1)] asm(2) dynkin_subset[OF \<delta>ynkin]
hellerar@39080
   139
          unfolding \<delta>E_def by auto
hellerar@39080
   140
        hence "space E \<inter> d \<in> sets \<delta>E" unfolding \<delta>E_def
hellerar@39080
   141
          using dasm by auto
hellerar@39080
   142
        have "sets \<delta>E \<subseteq> sets da" unfolding \<delta>E_def sets_\<delta>E_def using asm
hellerar@39080
   143
          by auto
hellerar@39080
   144
        thus "space E \<inter> d \<in> sets da" using dasm asm d dynkin_subset[OF \<delta>ynkin]
hellerar@39080
   145
          unfolding \<delta>E_def by auto
hellerar@39080
   146
      qed
hellerar@39080
   147
    next
hellerar@39094
   148
      fix a b assume absm: "a \<in> Dy d" "b \<in> Dy d" "a \<subseteq> b"
hellerar@39080
   149
      hence "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
hellerar@39080
   150
        unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   151
      hence *: "b - a \<in> sets \<delta>E"
hellerar@39094
   152
        using dynkin_diff[OF \<delta>ynkin] `a \<subseteq> b` by auto
hellerar@39080
   153
      have "a \<inter> d \<in> sets \<delta>E" "b \<inter> d \<in> sets \<delta>E"
hellerar@39080
   154
        using absm unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   155
      hence "(b \<inter> d) - (a \<inter> d) \<in> sets \<delta>E"
hellerar@39094
   156
        using dynkin_diff[OF \<delta>ynkin] `a \<subseteq> b` by auto
hellerar@39080
   157
      hence **: "(b - a) \<inter> d \<in> sets \<delta>E" by (auto simp add:Diff_Int_distrib2)
hellerar@39080
   158
      thus "b - a \<in> Dy d"
hellerar@39080
   159
        using * ** unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   160
    next
hellerar@39080
   161
      fix a assume aasm: "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}" "\<And>i. a i \<in> Dy d"
hellerar@39094
   162
      hence "\<And> i. a i \<in> sets \<delta>E"
hellerar@39080
   163
        unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   164
      from dynkin_UN[OF \<delta>ynkin aasm(1) this]
hellerar@39080
   165
      have *: "UNION UNIV a \<in> sets \<delta>E" by auto
hellerar@39080
   166
      from aasm
hellerar@39080
   167
      have aE: "\<forall> i. a i \<inter> d \<in> sets \<delta>E"
hellerar@39080
   168
        unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   169
      from aasm
hellerar@39080
   170
      have "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> (a i \<inter> d) \<inter> (a j \<inter> d) = {}" by auto
hellerar@39080
   171
      from dynkin_UN[OF \<delta>ynkin this]
hellerar@39080
   172
      have "UNION UNIV (\<lambda> i. a i \<inter> d) \<in> sets \<delta>E"
hellerar@39080
   173
        using aE by auto
hellerar@39080
   174
      hence **: "UNION UNIV a \<inter> d \<in> sets \<delta>E" by auto
hellerar@39080
   175
      from * ** show "UNION UNIV a \<in> Dy d" unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   176
    qed } note Dy_nkin = this
hellerar@39080
   177
  have E_\<delta>E: "sets E \<subseteq> sets \<delta>E"
hellerar@39080
   178
    unfolding \<delta>E_def sets_\<delta>E_def by auto
hellerar@39080
   179
  { fix d assume dasm: "d \<in> sets \<delta>E"
hellerar@39080
   180
    { fix e assume easm: "e \<in> sets E"
hellerar@39080
   181
      hence deasm: "e \<in> sets \<delta>E"
hellerar@39080
   182
        unfolding \<delta>E_def sets_\<delta>E_def by auto
hellerar@39080
   183
      have subset: "Dy e \<subseteq> sets \<delta>E"
hellerar@39080
   184
        unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   185
      { fix e' assume e'asm: "e' \<in> sets E"
hellerar@39080
   186
        have "e' \<inter> e \<in> sets E"
hellerar@39080
   187
          using easm e'asm stab unfolding Int_stable_def by auto
hellerar@39080
   188
        hence "e' \<inter> e \<in> sets \<delta>E"
hellerar@39080
   189
          unfolding \<delta>E_def sets_\<delta>E_def by auto
hellerar@39080
   190
        hence "e' \<in> Dy e" using e'asm unfolding Dy_def \<delta>E_def sets_\<delta>E_def by auto }
hellerar@39080
   191
      hence E_Dy: "sets E \<subseteq> Dy e" by auto
hellerar@39080
   192
      have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
hellerar@39080
   193
        using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto
hellerar@39080
   194
      hence "sets_\<delta>E \<subseteq> Dy e"
hellerar@39080
   195
        unfolding sets_\<delta>E_def
hellerar@39080
   196
      proof auto fix x
hellerar@39080
   197
        assume asm: "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and>
hellerar@39080
   198
          dynkin d \<and>
hellerar@39080
   199
          space d = space E \<and>
hellerar@39080
   200
          sets E \<subseteq> sets d) \<longrightarrow>
hellerar@39080
   201
          x \<in> xa"
hellerar@39080
   202
          "dynkin \<lparr>space = space E, sets = Dy e\<rparr>"
hellerar@39080
   203
          "sets E \<subseteq> Dy e"
hellerar@39080
   204
        show "x \<in> Dy e"
hellerar@39080
   205
          apply (rule impE[OF spec[OF asm(1), of "Dy e"]])
hellerar@39080
   206
          apply (rule exI[of _ "\<lparr>space = space E, sets = Dy e\<rparr>"])
hellerar@39080
   207
          using asm by auto
hellerar@39080
   208
      qed
hellerar@39080
   209
      hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto
hellerar@39080
   210
      hence "d \<inter> e \<in> sets \<delta>E"
hellerar@39080
   211
        using dasm easm deasm unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   212
      hence "e \<in> Dy d" using deasm
hellerar@39080
   213
        unfolding Dy_def \<delta>E_def
hellerar@39080
   214
        by (auto simp add:Int_commute) }
hellerar@39080
   215
    hence "sets E \<subseteq> Dy d" by auto
hellerar@39080
   216
    hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]]
hellerar@39080
   217
      unfolding \<delta>E_def sets_\<delta>E_def 
hellerar@39080
   218
    proof auto
hellerar@39080
   219
      fix x
hellerar@39080
   220
      assume asm: "sets E \<subseteq> Dy d"
hellerar@39080
   221
        "dynkin \<lparr>space = space E, sets = Dy d\<rparr>"
hellerar@39080
   222
        "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and> dynkin d \<and>
hellerar@39080
   223
            space d = space E \<and> sets E \<subseteq> sets d) \<longrightarrow> x \<in> xa"
hellerar@39080
   224
      show "x \<in> Dy d"
hellerar@39080
   225
        apply (rule impE[OF spec[OF asm(3), of "Dy d"]])
hellerar@39080
   226
        apply (rule exI[of _ "\<lparr>space = space E, sets = Dy d\<rparr>"])
hellerar@39080
   227
        using asm by auto
hellerar@39080
   228
    qed
hellerar@39080
   229
    hence *: "sets \<delta>E = Dy d"
hellerar@39080
   230
      unfolding Dy_def \<delta>E_def by auto
hellerar@39080
   231
    fix a assume aasm: "a \<in> sets \<delta>E"
hellerar@39080
   232
    hence "a \<inter> d \<in> sets \<delta>E"
hellerar@39080
   233
      using * dasm unfolding Dy_def \<delta>E_def by auto } note \<delta>E_stab = this
hellerar@39094
   234
  { fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets \<delta>E" "\<And>A. A \<in> sets \<delta>E \<Longrightarrow> A \<subseteq> space \<delta>E"
hellerar@39094
   235
      "\<And>a. a \<in> sets \<delta>E \<Longrightarrow> space \<delta>E - a \<in> sets \<delta>E"
hellerar@39094
   236
    "{} \<in> sets \<delta>E" "space \<delta>E \<in> sets \<delta>E"
hellerar@39094
   237
    let "?A i" = "A i \<inter> (\<Inter> j \<in> {..< i}. space \<delta>E - A j)"
hellerar@39094
   238
    { fix i :: nat
hellerar@39094
   239
      have *: "(\<Inter> j \<in> {..< i}. space \<delta>E - A j) \<inter> space \<delta>E \<in> sets \<delta>E"
hellerar@39094
   240
        apply (induct i)
hellerar@39094
   241
        using lessThan_Suc Asm \<delta>E_stab apply fastsimp
hellerar@39094
   242
        apply (subst lessThan_Suc)
hellerar@39094
   243
        apply (subst INT_insert)
hellerar@39094
   244
        apply (subst Int_assoc)
hellerar@39094
   245
        apply (subst \<delta>E_stab)
hellerar@39094
   246
        using lessThan_Suc Asm \<delta>E_stab Asm
hellerar@39094
   247
        apply (fastsimp simp add:Int_assoc dynkin_diff[OF \<delta>ynkin])
hellerar@39094
   248
        prefer 2 apply simp
hellerar@39094
   249
        apply (rule dynkin_diff[OF \<delta>ynkin, of _ "space \<delta>E", OF _ dynkin_space[OF \<delta>ynkin]])
hellerar@39094
   250
        using Asm by auto
hellerar@39094
   251
      have **: "\<And> i. A i \<subseteq> space \<delta>E" using Asm by auto
hellerar@39094
   252
      have "(\<Inter> j \<in> {..< i}. space \<delta>E - A j) \<subseteq> space \<delta>E \<or> (\<Inter> j \<in> {..< i}. A j) = UNIV \<and> i = 0"
hellerar@39094
   253
        apply (cases i)
hellerar@39094
   254
        using Asm ** dynkin_subset[OF \<delta>ynkin, of "A (i - 1)"]
hellerar@39094
   255
        by auto
hellerar@39094
   256
      hence Aisets: "?A i \<in> sets \<delta>E"
hellerar@39094
   257
        apply (cases i)
hellerar@39094
   258
        using Asm * apply fastsimp
hellerar@39094
   259
        apply (rule \<delta>E_stab)
hellerar@39094
   260
        using Asm * **
hellerar@39094
   261
        by (auto simp add:Int_absorb2)
hellerar@39094
   262
      have "?A i = disjointed A i" unfolding disjointed_def
hellerar@39094
   263
      atLeast0LessThan using Asm by auto
hellerar@39094
   264
      hence "?A i = disjointed A i" "?A i \<in> sets \<delta>E"
hellerar@39094
   265
        using Aisets by auto
hellerar@39094
   266
    } note Ai = this
hellerar@39094
   267
    from dynkin_UN[OF \<delta>ynkin _ this(2)] this disjoint_family_disjointed[of A]
hellerar@39094
   268
    have "(\<Union> i. ?A i) \<in> sets \<delta>E"
hellerar@39094
   269
      by (auto simp add:disjoint_family_on_def disjointed_def)
hellerar@39094
   270
    hence "(\<Union> i. A i) \<in> sets \<delta>E"
hellerar@39094
   271
      using Ai(1) UN_disjointed_eq[of A] by auto } note \<delta>E_UN = this
hellerar@39094
   272
  { fix a b assume asm: "a \<in> sets \<delta>E" "b \<in> sets \<delta>E"
hellerar@39094
   273
    let ?ab = "\<lambda> i. if (i::nat) = 0 then a else if i = 1 then b else {}"
hellerar@39094
   274
    have *: "(\<Union> i. ?ab i) \<in> sets \<delta>E"
hellerar@39094
   275
      apply (rule \<delta>E_UN)
hellerar@39094
   276
      using asm \<delta>E_UN dynkin_empty[OF \<delta>ynkin] 
hellerar@39094
   277
      dynkin_subset[OF \<delta>ynkin] 
hellerar@39094
   278
      dynkin_space[OF \<delta>ynkin]
hellerar@39094
   279
      dynkin_diff[OF \<delta>ynkin] by auto
hellerar@39094
   280
    have "(\<Union> i. ?ab i) = a \<union> b" apply auto
hellerar@39094
   281
      apply (case_tac "i = 0")
hellerar@39094
   282
      apply auto
hellerar@39094
   283
      apply (case_tac "i = 1")
hellerar@39094
   284
      by auto
hellerar@39094
   285
    hence "a \<union> b \<in> sets \<delta>E" using * by auto} note \<delta>E_Un = this
hellerar@39094
   286
  have "sigma_algebra \<delta>E"
hellerar@39080
   287
    apply unfold_locales
hellerar@39094
   288
    using dynkin_subset[OF \<delta>ynkin]
hellerar@39094
   289
    using dynkin_diff[OF \<delta>ynkin, of _ "space \<delta>E", OF _ dynkin_space[OF \<delta>ynkin]]
hellerar@39094
   290
    using dynkin_diff[OF \<delta>ynkin, of "space \<delta>E" "space \<delta>E", OF dynkin_space[OF \<delta>ynkin] dynkin_space[OF \<delta>ynkin]]
hellerar@39094
   291
    using dynkin_space[OF \<delta>ynkin]
hellerar@39094
   292
    using \<delta>E_UN \<delta>E_Un
hellerar@39094
   293
    by auto
hellerar@39094
   294
  from sigma_algebra.sigma_subset[OF this E_\<delta>E] \<delta>E_D subsDE spac
hellerar@39094
   295
  show ?thesis by (auto simp add:\<delta>E_def sigma_def)
hellerar@39094
   296
qed
hellerar@39094
   297
hellerar@39094
   298
lemma measure_eq:
hellerar@39094
   299
  assumes fin: "\<mu> (space M) = \<nu> (space M)" "\<nu> (space M) < \<omega>" 
hellerar@39094
   300
  assumes E: "M = sigma (space E) (sets E)" "Int_stable E"
hellerar@39094
   301
  assumes eq: "\<And> e. e \<in> sets E \<Longrightarrow> \<mu> e = \<nu> e"
hellerar@39094
   302
  assumes ms: "measure_space M \<mu>" "measure_space M \<nu>"
hellerar@39094
   303
  assumes A: "A \<in> sets M"
hellerar@39094
   304
  shows "\<mu> A = \<nu> A"
hellerar@39094
   305
proof -
hellerar@39094
   306
  interpret M: measure_space M \<mu>
hellerar@39094
   307
    using ms by simp
hellerar@39094
   308
  interpret M': measure_space M \<nu>
hellerar@39094
   309
    using ms by simp
hellerar@39094
   310
hellerar@39094
   311
  let ?D_sets = "{A. A \<in> sets M \<and> \<mu> A = \<nu> A}"
hellerar@39094
   312
  have \<delta>: "dynkin \<lparr> space = space M , sets = ?D_sets \<rparr>"
hellerar@39094
   313
  proof (rule dynkinI, safe, simp_all)
hellerar@39094
   314
    fix A x assume "A \<in> sets M \<and> \<mu> A = \<nu> A" "x \<in> A"
hellerar@39094
   315
    thus "x \<in> space M" using assms M.sets_into_space by auto
hellerar@39094
   316
  next
hellerar@39094
   317
    show "\<mu> (space M) = \<nu> (space M)"
hellerar@39094
   318
      using fin by auto
hellerar@39094
   319
  next
hellerar@39094
   320
    fix a b
hellerar@39094
   321
    assume asm: "a \<in> sets M \<and> \<mu> a = \<nu> a"
hellerar@39094
   322
      "b \<in> sets M \<and> \<mu> b = \<nu> b" "a \<subseteq> b"
hellerar@39094
   323
    hence "a \<subseteq> space M"
hellerar@39094
   324
      using M.sets_into_space by auto
hellerar@39094
   325
    from M.measure_mono[OF this]
hellerar@39094
   326
    have "\<mu> a \<le> \<mu> (space M)"
hellerar@39094
   327
      using asm by auto
hellerar@39094
   328
    hence afin: "\<mu> a < \<omega>"
hellerar@39094
   329
      using fin by auto
hellerar@39094
   330
    have *: "b = b - a \<union> a" using asm by auto
hellerar@39094
   331
    have **: "(b - a) \<inter> a = {}" using asm by auto
hellerar@39094
   332
    have iv: "\<mu> (b - a) + \<mu> a = \<mu> b"
hellerar@39094
   333
      using M.measure_additive[of "b - a" a]
hellerar@39094
   334
        conjunct1[OF asm(1)] conjunct1[OF asm(2)] * **
hellerar@39094
   335
      by auto
hellerar@39094
   336
    have v: "\<nu> (b - a) + \<nu> a = \<nu> b"
hellerar@39094
   337
      using M'.measure_additive[of "b - a" a]
hellerar@39094
   338
        conjunct1[OF asm(1)] conjunct1[OF asm(2)] * **
hellerar@39094
   339
      by auto
hellerar@39094
   340
    from iv v have "\<mu> (b - a) = \<nu> (b - a)" using asm afin
hellerar@39094
   341
      pinfreal_add_cancel_right[of "\<mu> (b - a)" "\<nu> a" "\<nu> (b - a)"]
hellerar@39094
   342
      by auto
hellerar@39094
   343
    thus "b - a \<in> sets M \<and> \<mu> (b - a) = \<nu> (b - a)"
hellerar@39094
   344
      using asm by auto
hellerar@39094
   345
  next
hellerar@39094
   346
    fix a assume "\<And>i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
hellerar@39094
   347
      "\<And>i. a i \<in> sets M \<and> \<mu> (a i) = \<nu> (a i)"
hellerar@39094
   348
    thus "(\<Union>x. a x) \<in> sets M \<and> \<mu> (\<Union>x. a x) = \<nu> (\<Union>x. a x)"
hellerar@39094
   349
      using M.measure_countably_additive
hellerar@39094
   350
        M'.measure_countably_additive
hellerar@39094
   351
        M.countable_UN
hellerar@39094
   352
      apply (auto simp add:disjoint_family_on_def image_def)
hellerar@39094
   353
      apply (subst M.measure_countably_additive[symmetric])
hellerar@39094
   354
      apply (auto simp add:disjoint_family_on_def)
hellerar@39094
   355
      apply (subst M'.measure_countably_additive[symmetric])
hellerar@39094
   356
      by (auto simp add:disjoint_family_on_def)
hellerar@39080
   357
  qed
hellerar@39094
   358
  have *: "sets E \<subseteq> ?D_sets"
hellerar@39094
   359
    using eq E sigma_sets.Basic[of _ "sets E"]
hellerar@39094
   360
    by (auto simp add:sigma_def)
hellerar@39094
   361
  have **: "?D_sets \<subseteq> sets M" by auto
hellerar@39094
   362
  have "M = \<lparr> space = space M , sets = ?D_sets \<rparr>"
hellerar@39094
   363
    unfolding E(1)
hellerar@39094
   364
    apply (rule dynkin_lemma[OF E(2)])
hellerar@39094
   365
    using eq E space_sigma \<delta> sigma_sets.Basic
hellerar@39094
   366
    by (auto simp add:sigma_def)
hellerar@39094
   367
  from subst[OF this, of "\<lambda> M. A \<in> sets M", OF A]
hellerar@39094
   368
  show ?thesis by auto
hellerar@39094
   369
qed
hellerar@39094
   370
hellerar@39094
   371
lemma
hellerar@39094
   372
  assumes sfin: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And> i :: nat. \<nu> (A i) < \<omega>"
hellerar@39094
   373
  assumes A: "\<And>  i. \<mu> (A i) = \<nu> (A i)" "\<And> i. A i \<subseteq> A (Suc i)"
hellerar@39094
   374
  assumes E: "M = sigma (space E) (sets E)" "Int_stable E"
hellerar@39094
   375
  assumes eq: "\<And> e. e \<in> sets E \<Longrightarrow> \<mu> e = \<nu> e"
hellerar@39094
   376
  assumes ms: "measure_space (M :: 'a algebra) \<mu>" "measure_space M \<nu>"
hellerar@39094
   377
  assumes B: "B \<in> sets M"
hellerar@39094
   378
  shows "\<mu> B = \<nu> B"
hellerar@39094
   379
proof -
hellerar@39094
   380
  interpret M: measure_space M \<mu> by (rule ms)
hellerar@39094
   381
  interpret M': measure_space M \<nu> by (rule ms)
hellerar@39094
   382
  have *: "M = \<lparr> space = space M, sets = sets M \<rparr>" by auto
hellerar@39094
   383
  { fix i :: nat
hellerar@39094
   384
    have **: "M\<lparr> space := A i, sets := op \<inter> (A i) ` sets M \<rparr> =
hellerar@39094
   385
      \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr>"
hellerar@39094
   386
      by auto
hellerar@39094
   387
    have mu_i: "measure_space \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr> \<mu>"
hellerar@39094
   388
      using M.restricted_measure_space[of "A i", simplified **]
hellerar@39094
   389
        sfin by auto
hellerar@39094
   390
    have nu_i: "measure_space \<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr> \<nu>"
hellerar@39094
   391
      using M'.restricted_measure_space[of "A i", simplified **]
hellerar@39094
   392
        sfin by auto
hellerar@39094
   393
    let ?M = "\<lparr> space = A i, sets = op \<inter> (A i) ` sets M \<rparr>"
hellerar@39094
   394
    have "\<mu> (A i \<inter> B) = \<nu> (A i \<inter> B)"
hellerar@39094
   395
      apply (rule measure_eq[of \<mu> ?M \<nu> "\<lparr> space = space E \<inter> A i, sets = op \<inter> (A i) ` sets E\<rparr>" "A i \<inter> B", simplified])
hellerar@39094
   396
      using assms nu_i mu_i
hellerar@39094
   397
      apply (auto simp add:image_def) (* TODO *)
hellerar@39080
   398
qed
hellerar@39080
   399
hellerar@39080
   400
lemma
hellerar@39080
   401
(*
hoelzl@38656
   402
definition prod_sets where
hoelzl@38656
   403
  "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
hoelzl@38656
   404
hoelzl@35833
   405
definition
hoelzl@38656
   406
  "prod_measure M \<mu> N \<nu> = (\<lambda>A. measure_space.positive_integral M \<mu> (\<lambda>s0. \<nu> ((\<lambda>s1. (s0, s1)) -` A)))"
hoelzl@35833
   407
hoelzl@35833
   408
definition
hoelzl@38656
   409
  "prod_measure_space M1 M2 = sigma (space M1 \<times> space M2) (prod_sets (sets M1) (sets M2))"
hoelzl@38656
   410
hoelzl@38656
   411
lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
hoelzl@38656
   412
  by (auto simp add: prod_sets_def)
hoelzl@35833
   413
hoelzl@38656
   414
lemma sigma_prod_sets_finite:
hoelzl@38656
   415
  assumes "finite A" and "finite B"
hoelzl@38656
   416
  shows "sigma_sets (A \<times> B) (prod_sets (Pow A) (Pow B)) = Pow (A \<times> B)"
hoelzl@38656
   417
proof safe
hoelzl@38656
   418
  have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product)
hoelzl@35833
   419
hoelzl@38656
   420
  fix x assume subset: "x \<subseteq> A \<times> B"
hoelzl@38656
   421
  hence "finite x" using fin by (rule finite_subset)
hoelzl@38656
   422
  from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))"
hoelzl@38656
   423
    (is "x \<in> sigma_sets ?prod ?sets")
hoelzl@38656
   424
  proof (induct x)
hoelzl@38656
   425
    case empty show ?case by (rule sigma_sets.Empty)
hoelzl@38656
   426
  next
hoelzl@38656
   427
    case (insert a x)
hoelzl@38656
   428
    hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic)
hoelzl@38656
   429
    moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto
hoelzl@38656
   430
    ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un)
hoelzl@38656
   431
  qed
hoelzl@38656
   432
next
hoelzl@38656
   433
  fix x a b
hoelzl@38656
   434
  assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x"
hoelzl@38656
   435
  from sigma_sets_into_sp[OF _ this(1)] this(2)
hoelzl@38656
   436
  show "a \<in> A" and "b \<in> B"
hoelzl@38656
   437
    by (auto simp: prod_sets_def)
hoelzl@35833
   438
qed
hoelzl@35833
   439
hoelzl@38656
   440
lemma (in sigma_algebra) measurable_prod_sigma:
hoelzl@38656
   441
  assumes sa1: "sigma_algebra a1" and sa2: "sigma_algebra a2"
hoelzl@38656
   442
  assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
hoelzl@38656
   443
  shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2))
hoelzl@38656
   444
                          (prod_sets (sets a1) (sets a2)))"
hoelzl@35977
   445
proof -
hoelzl@38656
   446
  from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
hoelzl@38656
   447
     and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
hoelzl@38656
   448
    by (auto simp add: measurable_def)
hoelzl@38656
   449
  from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
hoelzl@38656
   450
     and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
hoelzl@38656
   451
    by (auto simp add: measurable_def)
hoelzl@38656
   452
  show ?thesis
hoelzl@38656
   453
    proof (rule measurable_sigma)
hoelzl@38656
   454
      show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
hoelzl@38656
   455
        by (auto simp add: prod_sets_def sigma_algebra_iff dest: algebra.space_closed)
hoelzl@38656
   456
    next
hoelzl@38656
   457
      show "f \<in> space M \<rightarrow> space a1 \<times> space a2"
hoelzl@38656
   458
        by (rule prod_final [OF fn1 fn2])
hoelzl@38656
   459
    next
hoelzl@38656
   460
      fix z
hoelzl@38656
   461
      assume z: "z \<in> prod_sets (sets a1) (sets a2)"
hoelzl@38656
   462
      thus "f -` z \<inter> space M \<in> sets M"
hoelzl@38656
   463
        proof (auto simp add: prod_sets_def vimage_Times)
hoelzl@38656
   464
          fix x y
hoelzl@38656
   465
          assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
hoelzl@38656
   466
          have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
hoelzl@38656
   467
                ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
hoelzl@38656
   468
            by blast
hoelzl@38656
   469
          also have "...  \<in> sets M" using x y q1 q2
hoelzl@38656
   470
            by blast
hoelzl@38656
   471
          finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
hoelzl@38656
   472
        qed
hoelzl@38656
   473
    qed
hoelzl@35977
   474
qed
hoelzl@35833
   475
hoelzl@38656
   476
lemma (in sigma_finite_measure) prod_measure_times:
hoelzl@38656
   477
  assumes "sigma_finite_measure N \<nu>"
hoelzl@38656
   478
  and "A1 \<in> sets M" "A2 \<in> sets N"
hoelzl@38656
   479
  shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"
hoelzl@38656
   480
  oops
hoelzl@35833
   481
hoelzl@38656
   482
lemma (in sigma_finite_measure) sigma_finite_prod_measure_space:
hoelzl@38656
   483
  assumes "sigma_finite_measure N \<nu>"
hoelzl@38656
   484
  shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   485
  oops
hoelzl@38656
   486
hoelzl@38656
   487
lemma (in finite_measure_space) finite_prod_measure_times:
hoelzl@38656
   488
  assumes "finite_measure_space N \<nu>"
hoelzl@38656
   489
  and "A1 \<in> sets M" "A2 \<in> sets N"
hoelzl@38656
   490
  shows "prod_measure M \<mu> N \<nu> (A1 \<times> A2) = \<mu> A1 * \<nu> A2"
hoelzl@38656
   491
proof -
hoelzl@38656
   492
  interpret N: finite_measure_space N \<nu> by fact
hoelzl@38656
   493
  have *: "\<And>x. \<nu> (Pair x -` (A1 \<times> A2)) * \<mu> {x} = (if x \<in> A1 then \<nu> A2 * \<mu> {x} else 0)"
hoelzl@38656
   494
    by (auto simp: vimage_Times comp_def)
hoelzl@38656
   495
  have "finite A1"
hoelzl@38656
   496
    using `A1 \<in> sets M` finite_space by (auto simp: sets_eq_Pow intro: finite_subset)
hoelzl@38656
   497
  then have "\<mu> A1 = (\<Sum>x\<in>A1. \<mu> {x})" using `A1 \<in> sets M`
hoelzl@38656
   498
    by (auto intro!: measure_finite_singleton simp: sets_eq_Pow)
hoelzl@38656
   499
  then show ?thesis using `A1 \<in> sets M`
hoelzl@38656
   500
    unfolding prod_measure_def positive_integral_finite_eq_setsum *
hoelzl@38656
   501
    by (auto simp add: sets_eq_Pow setsum_right_distrib[symmetric] mult_commute setsum_cases[OF finite_space])
hoelzl@35833
   502
qed
hoelzl@35833
   503
hoelzl@38656
   504
lemma (in finite_measure_space) finite_prod_measure_space:
hoelzl@38656
   505
  assumes "finite_measure_space N \<nu>"
hoelzl@38656
   506
  shows "prod_measure_space M N = \<lparr> space = space M \<times> space N, sets = Pow (space M \<times> space N) \<rparr>"
hoelzl@35977
   507
proof -
hoelzl@38656
   508
  interpret N: finite_measure_space N \<nu> by fact
hoelzl@38656
   509
  show ?thesis using finite_space N.finite_space
hoelzl@38656
   510
    by (simp add: sigma_def prod_measure_space_def sigma_prod_sets_finite sets_eq_Pow N.sets_eq_Pow)
hoelzl@35833
   511
qed
hoelzl@35833
   512
hoelzl@38656
   513
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure:
hoelzl@38656
   514
  assumes "finite_measure_space N \<nu>"
hoelzl@38656
   515
  shows "finite_measure_space (prod_measure_space M N) (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   516
  unfolding finite_prod_measure_space[OF assms]
hoelzl@38656
   517
proof (rule finite_measure_spaceI)
hoelzl@38656
   518
  interpret N: finite_measure_space N \<nu> by fact
hoelzl@38656
   519
hoelzl@38656
   520
  let ?P = "\<lparr>space = space M \<times> space N, sets = Pow (space M \<times> space N)\<rparr>"
hoelzl@38656
   521
  show "measure_space ?P (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   522
  proof (rule sigma_algebra.finite_additivity_sufficient)
hoelzl@38656
   523
    show "sigma_algebra ?P" by (rule sigma_algebra_Pow)
hoelzl@38656
   524
    show "finite (space ?P)" using finite_space N.finite_space by auto
hoelzl@38656
   525
    from finite_prod_measure_times[OF assms, of "{}" "{}"]
hoelzl@38656
   526
    show "positive (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   527
      unfolding positive_def by simp
hoelzl@38656
   528
hoelzl@38656
   529
    show "additive ?P (prod_measure M \<mu> N \<nu>)"
hoelzl@38656
   530
      unfolding additive_def
hoelzl@38656
   531
      apply (auto simp add: sets_eq_Pow prod_measure_def positive_integral_add[symmetric]
hoelzl@38656
   532
                  intro!: positive_integral_cong)
hoelzl@38656
   533
      apply (subst N.measure_additive[symmetric])
hoelzl@38656
   534
      by (auto simp: N.sets_eq_Pow sets_eq_Pow)
hoelzl@38656
   535
  qed
hoelzl@38656
   536
  show "finite (space ?P)" using finite_space N.finite_space by auto
hoelzl@38656
   537
  show "sets ?P = Pow (space ?P)" by simp
hoelzl@38656
   538
hoelzl@38656
   539
  fix x assume "x \<in> space ?P"
hoelzl@38656
   540
  with finite_prod_measure_times[OF assms, of "{fst x}" "{snd x}"]
hoelzl@38656
   541
    finite_measure[of "{fst x}"] N.finite_measure[of "{snd x}"]
hoelzl@38656
   542
  show "prod_measure M \<mu> N \<nu> {x} \<noteq> \<omega>"
hoelzl@38656
   543
    by (auto simp add: sets_eq_Pow N.sets_eq_Pow elim!: SigmaE)
hoelzl@38656
   544
qed
hoelzl@38656
   545
hoelzl@38656
   546
lemma (in finite_measure_space) finite_measure_space_finite_prod_measure_alterantive:
hoelzl@38656
   547
  assumes N: "finite_measure_space N \<nu>"
hoelzl@38656
   548
  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
   549
    (is "finite_measure_space ?M ?m")
hoelzl@38656
   550
  unfolding finite_prod_measure_space[OF N, symmetric]
hoelzl@38656
   551
  using finite_measure_space_finite_prod_measure[OF N] .
hoelzl@38656
   552
hellerar@39080
   553
*)
hoelzl@35833
   554
end