add induction rule for intersection-stable sigma-sets
authorhoelzl
Wed Oct 10 12:12:27 2012 +0200 (2012-10-10)
changeset 49789e0a4cb91a8a9
parent 49788 3c10763f5cb4
child 49790 6b9b9ebba47d
add induction rule for intersection-stable sigma-sets
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:26 2012 +0200
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Oct 10 12:12:27 2012 +0200
     1.3 @@ -33,15 +33,18 @@
     1.4        {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}
     1.5        (\<lambda>X. \<integral>\<^isup>+x. (\<integral>\<^isup>+y. indicator X (x,y) \<partial>B) \<partial>A)"
     1.6  
     1.7 +lemma pair_measure_closed: "{a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B} \<subseteq> Pow (space A \<times> space B)"
     1.8 +  using space_closed[of A] space_closed[of B] by auto
     1.9 +
    1.10  lemma space_pair_measure:
    1.11    "space (A \<Otimes>\<^isub>M B) = space A \<times> space B"
    1.12 -  unfolding pair_measure_def using space_closed[of A] space_closed[of B]
    1.13 -  by (intro space_measure_of) auto
    1.14 +  unfolding pair_measure_def using pair_measure_closed[of A B]
    1.15 +  by (rule space_measure_of)
    1.16  
    1.17  lemma sets_pair_measure:
    1.18    "sets (A \<Otimes>\<^isub>M B) = sigma_sets (space A \<times> space B) {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}"
    1.19 -  unfolding pair_measure_def using space_closed[of A] space_closed[of B]
    1.20 -  by (intro sets_measure_of) auto
    1.21 +  unfolding pair_measure_def using pair_measure_closed[of A B]
    1.22 +  by (rule sets_measure_of)
    1.23  
    1.24  lemma sets_pair_measure_cong[cong]:
    1.25    "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^isub>M M2) = sets (M1' \<Otimes>\<^isub>M M2')"
    1.26 @@ -162,40 +165,24 @@
    1.27    assumes "Q \<in> sets (N \<Otimes>\<^isub>M M)"
    1.28    shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N"
    1.29      (is "?s Q \<in> _")
    1.30 -proof -
    1.31 -  let ?\<Omega> = "space N \<times> space M" and ?D = "{A\<in>sets (N \<Otimes>\<^isub>M M). ?s A \<in> borel_measurable N}"
    1.32 -  note space_pair_measure[simp]
    1.33 -  interpret dynkin_system ?\<Omega> ?D
    1.34 -  proof (intro dynkin_systemI)
    1.35 -    fix A assume "A \<in> ?D" then show "A \<subseteq> ?\<Omega>"
    1.36 -      using sets_into_space[of A "N \<Otimes>\<^isub>M M"] by simp
    1.37 -  next
    1.38 -    from top show "?\<Omega> \<in> ?D"
    1.39 -      by (auto simp add: if_distrib intro!: measurable_If)
    1.40 -  next
    1.41 -    fix A assume "A \<in> ?D"
    1.42 -    with sets_into_space have "\<And>x. emeasure M (Pair x -` (?\<Omega> - A)) =
    1.43 -        (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
    1.44 -      by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
    1.45 -    with `A \<in> ?D` top show "?\<Omega> - A \<in> ?D"
    1.46 -      by (auto intro!: measurable_If)
    1.47 -  next
    1.48 -    fix F :: "nat \<Rightarrow> ('b\<times>'a) set" assume "disjoint_family F" "range F \<subseteq> ?D"
    1.49 -    moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
    1.50 -      by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
    1.51 -    ultimately show "(\<Union>i. F i) \<in> ?D"
    1.52 -      by (auto simp: vimage_UN intro!: borel_measurable_psuminf)
    1.53 -  qed
    1.54 -  let ?G = "{a \<times> b | a b. a \<in> sets N \<and> b \<in> sets M}"
    1.55 -  have "sigma_sets ?\<Omega> ?G = ?D"
    1.56 -  proof (rule dynkin_lemma)
    1.57 -    show "?G \<subseteq> ?D"
    1.58 -      by (auto simp: if_distrib Int_def[symmetric] intro!: measurable_If)
    1.59 -  qed (auto simp: sets_pair_measure  Int_stable_pair_measure_generator)
    1.60 -  with `Q \<in> sets (N \<Otimes>\<^isub>M M)` have "Q \<in> ?D"
    1.61 -    by (simp add: sets_pair_measure[symmetric])
    1.62 -  then show "?s Q \<in> borel_measurable N" by simp
    1.63 -qed
    1.64 +  using Int_stable_pair_measure_generator pair_measure_closed assms
    1.65 +  unfolding sets_pair_measure
    1.66 +proof (induct rule: sigma_sets_induct_disjoint)
    1.67 +  case (compl A)
    1.68 +  with sets_into_space have "\<And>x. emeasure M (Pair x -` ((space N \<times> space M) - A)) =
    1.69 +      (if x \<in> space N then emeasure M (space M) - ?s A x else 0)"
    1.70 +    unfolding sets_pair_measure[symmetric]
    1.71 +    by (auto intro!: emeasure_compl simp: vimage_Diff sets_Pair1)
    1.72 +  with compl top show ?case
    1.73 +    by (auto intro!: measurable_If simp: space_pair_measure)
    1.74 +next
    1.75 +  case (union F)
    1.76 +  moreover then have "\<And>x. emeasure M (\<Union>i. Pair x -` F i) = (\<Sum>i. ?s (F i) x)"
    1.77 +    unfolding sets_pair_measure[symmetric]
    1.78 +    by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def sets_Pair1)
    1.79 +  ultimately show ?case
    1.80 +    by (auto simp: vimage_UN)
    1.81 +qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
    1.82  
    1.83  lemma (in sigma_finite_measure) measurable_emeasure_Pair:
    1.84    assumes Q: "Q \<in> sets (N \<Otimes>\<^isub>M M)" shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" (is "?s Q \<in> _")
     2.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:26 2012 +0200
     2.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Oct 10 12:12:27 2012 +0200
     2.3 @@ -633,48 +633,45 @@
     2.4  proof -
     2.5    let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
     2.6    interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
     2.7 -  { fix F assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
     2.8 +  have "space M = \<Omega>"
     2.9 +    using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
    2.10 +
    2.11 +  { fix F D assume "F \<in> E" and "?\<mu> F \<noteq> \<infinity>"
    2.12      then have [intro]: "F \<in> sigma_sets \<Omega> E" by auto
    2.13 -    let ?D = "{D \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> D) = ?\<nu> (F \<inter> D)}"
    2.14      have "?\<nu> F \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` `F \<in> E` eq by simp
    2.15 -    interpret D: dynkin_system \<Omega> ?D
    2.16 -    proof (rule dynkin_systemI, simp_all)
    2.17 -      fix A assume "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
    2.18 -      then show "A \<subseteq> \<Omega>" using S.sets_into_space by auto
    2.19 +    assume "D \<in> sets M"
    2.20 +    with `Int_stable E` `E \<subseteq> Pow \<Omega>` have "emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
    2.21 +      unfolding M
    2.22 +    proof (induct rule: sigma_sets_induct_disjoint)
    2.23 +      case (basic A)
    2.24 +      then have "F \<inter> A \<in> E" using `Int_stable E` `F \<in> E` by (auto simp: Int_stable_def)
    2.25 +      then show ?case using eq by auto
    2.26      next
    2.27 -      have "F \<inter> \<Omega> = F" using `F \<in> E` `E \<subseteq> Pow \<Omega>` by auto
    2.28 -      then show "?\<mu> (F \<inter> \<Omega>) = ?\<nu> (F \<inter> \<Omega>)"
    2.29 -        using `F \<in> E` eq by (auto intro: sigma_sets_top)
    2.30 +      case empty then show ?case by simp
    2.31      next
    2.32 -      fix A assume *: "A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> A) = ?\<nu> (F \<inter> A)"
    2.33 +      case (compl A)
    2.34        then have **: "F \<inter> (\<Omega> - A) = F - (F \<inter> A)"
    2.35          and [intro]: "F \<inter> A \<in> sigma_sets \<Omega> E"
    2.36 -        using `F \<in> E` S.sets_into_space by auto
    2.37 +        using `F \<in> E` S.sets_into_space by (auto simp: M)
    2.38        have "?\<nu> (F \<inter> A) \<le> ?\<nu> F" by (auto intro!: emeasure_mono simp: M N)
    2.39        then have "?\<nu> (F \<inter> A) \<noteq> \<infinity>" using `?\<nu> F \<noteq> \<infinity>` by auto
    2.40        have "?\<mu> (F \<inter> A) \<le> ?\<mu> F" by (auto intro!: emeasure_mono simp: M N)
    2.41        then have "?\<mu> (F \<inter> A) \<noteq> \<infinity>" using `?\<mu> F \<noteq> \<infinity>` by auto
    2.42        then have "?\<mu> (F \<inter> (\<Omega> - A)) = ?\<mu> F - ?\<mu> (F \<inter> A)" unfolding **
    2.43          using `F \<inter> A \<in> sigma_sets \<Omega> E` by (auto intro!: emeasure_Diff simp: M N)
    2.44 -      also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` * by simp
    2.45 +      also have "\<dots> = ?\<nu> F - ?\<nu> (F \<inter> A)" using eq `F \<in> E` compl by simp
    2.46        also have "\<dots> = ?\<nu> (F \<inter> (\<Omega> - A))" unfolding **
    2.47          using `F \<inter> A \<in> sigma_sets \<Omega> E` `?\<nu> (F \<inter> A) \<noteq> \<infinity>`
    2.48          by (auto intro!: emeasure_Diff[symmetric] simp: M N)
    2.49 -      finally show "\<Omega> - A \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Omega> - A)) = ?\<nu> (F \<inter> (\<Omega> - A))"
    2.50 -        using * by auto
    2.51 +      finally show ?case
    2.52 +        using `space M = \<Omega>` by auto
    2.53      next
    2.54 -      fix A :: "nat \<Rightarrow> 'a set"
    2.55 -      assume "disjoint_family A" and A: "range A \<subseteq> {X \<in> sigma_sets \<Omega> E. ?\<mu> (F \<inter> X) = ?\<nu> (F \<inter> X)}"
    2.56 +      case (union A)
    2.57        then have "?\<mu> (\<Union>x. F \<inter> A x) = ?\<nu> (\<Union>x. F \<inter> A x)"
    2.58          by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N)
    2.59 -      with A show "(\<Union>x. A x) \<in> sigma_sets \<Omega> E \<and> ?\<mu> (F \<inter> (\<Union>x. A x)) = ?\<nu> (F \<inter> (\<Union>x. A x))"
    2.60 +      with A show ?case
    2.61          by auto
    2.62 -    qed
    2.63 -    have *: "sigma_sets \<Omega> E = ?D"
    2.64 -      using `F \<in> E` `Int_stable E`
    2.65 -      by (intro D.dynkin_lemma) (auto simp add: Int_stable_def eq)
    2.66 -    have "\<And>D. D \<in> sets M \<Longrightarrow> emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
    2.67 -      unfolding M by (subst (asm) *) auto }
    2.68 +    qed }
    2.69    note * = this
    2.70    show "M = N"
    2.71    proof (rule measure_eqI)
    2.72 @@ -684,9 +681,7 @@
    2.73        using A(1) by (auto simp: subset_eq M)
    2.74      fix F assume "F \<in> sets M"
    2.75      let ?D = "disjointed (\<lambda>i. F \<inter> A i)"
    2.76 -    have "space M = \<Omega>"
    2.77 -      using top[of M] space_closed[of M] S.top S.space_closed `sets M = sigma_sets \<Omega> E` by blast
    2.78 -    then have F_eq: "F = (\<Union>i. ?D i)"
    2.79 +    from `space M = \<Omega>` have F_eq: "F = (\<Union>i. ?D i)"
    2.80        using `F \<in> sets M`[THEN sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
    2.81      have [simp, intro]: "\<And>i. ?D i \<in> sets M"
    2.82        using range_disjointed_sets[of "\<lambda>i. F \<inter> A i" M] `F \<in> sets M`
     3.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 10 12:12:26 2012 +0200
     3.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Oct 10 12:12:27 2012 +0200
     3.3 @@ -2041,4 +2041,25 @@
     3.4      using assms by (auto simp: dynkin_def)
     3.5  qed
     3.6  
     3.7 +lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
     3.8 +  assumes "Int_stable G"
     3.9 +    and closed: "G \<subseteq> Pow \<Omega>"
    3.10 +    and A: "A \<in> sigma_sets \<Omega> G"
    3.11 +  assumes basic: "\<And>A. A \<in> G \<Longrightarrow> P A"
    3.12 +    and empty: "P {}"
    3.13 +    and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
    3.14 +    and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
    3.15 +  shows "P A"
    3.16 +proof -
    3.17 +  let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
    3.18 +  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
    3.19 +    using closed by (rule sigma_algebra_sigma_sets)
    3.20 +  from compl[OF _ empty] closed have space: "P \<Omega>" by simp
    3.21 +  interpret dynkin_system \<Omega> ?D
    3.22 +    by default (auto dest: sets_into_space intro!: space compl union)
    3.23 +  have "sigma_sets \<Omega> G = ?D"
    3.24 +    by (rule dynkin_lemma) (auto simp: basic `Int_stable G`)
    3.25 +  with A show ?thesis by auto
    3.26 +qed
    3.27 +
    3.28  end