src/HOL/Probability/Complete_Measure.thy
changeset 41689 3e39b0e730d6
parent 41097 a1abfa4e2b44
child 41705 1100512e16d8
     1.1 --- a/src/HOL/Probability/Complete_Measure.thy	Wed Feb 02 10:35:41 2011 +0100
     1.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Wed Feb 02 12:34:45 2011 +0100
     1.3 @@ -7,9 +7,24 @@
     1.4  
     1.5  locale completeable_measure_space = measure_space
     1.6  
     1.7 -definition (in completeable_measure_space) completion :: "'a algebra" where
     1.8 +definition (in completeable_measure_space)
     1.9 +  "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
    1.10 +    fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
    1.11 +
    1.12 +definition (in completeable_measure_space)
    1.13 +  "main_part A = fst (Eps (split_completion A))"
    1.14 +
    1.15 +definition (in completeable_measure_space)
    1.16 +  "null_part A = snd (Eps (split_completion A))"
    1.17 +
    1.18 +abbreviation (in completeable_measure_space) "\<mu>' A \<equiv> \<mu> (main_part A)"
    1.19 +
    1.20 +definition (in completeable_measure_space) completion :: "('a, 'b) measure_space_scheme" where
    1.21    "completion = \<lparr> space = space M,
    1.22 -    sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' } \<rparr>"
    1.23 +                  sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' },
    1.24 +                  measure = \<mu>',
    1.25 +                  \<dots> = more M \<rparr>"
    1.26 +
    1.27  
    1.28  lemma (in completeable_measure_space) space_completion[simp]:
    1.29    "space completion = space M" unfolding completion_def by simp
    1.30 @@ -58,16 +73,6 @@
    1.31         auto
    1.32  qed auto
    1.33  
    1.34 -definition (in completeable_measure_space)
    1.35 -  "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
    1.36 -    fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
    1.37 -
    1.38 -definition (in completeable_measure_space)
    1.39 -  "main_part A = fst (Eps (split_completion A))"
    1.40 -
    1.41 -definition (in completeable_measure_space)
    1.42 -  "null_part A = snd (Eps (split_completion A))"
    1.43 -
    1.44  lemma (in completeable_measure_space) split_completion:
    1.45    assumes "A \<in> sets completion"
    1.46    shows "split_completion A (main_part A, null_part A)"
    1.47 @@ -108,17 +113,15 @@
    1.48    show "\<mu> (null_part S) = 0" by auto
    1.49  qed
    1.50  
    1.51 -definition (in completeable_measure_space) "\<mu>' A = \<mu> (main_part A)"
    1.52 -
    1.53  lemma (in completeable_measure_space) \<mu>'_set[simp]:
    1.54    assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"
    1.55  proof -
    1.56    have S: "S \<in> sets completion" using assms by auto
    1.57    then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp
    1.58 -  also have "\<dots> = \<mu> (main_part S)"
    1.59 +  also have "\<dots> = \<mu>' S"
    1.60      using S assms measure_additive[of "main_part S" "null_part S"]
    1.61      by (auto simp: measure_additive)
    1.62 -  finally show ?thesis unfolding \<mu>'_def by simp
    1.63 +  finally show ?thesis by simp
    1.64  qed
    1.65  
    1.66  lemma (in completeable_measure_space) sets_completionI_sub:
    1.67 @@ -154,7 +157,7 @@
    1.68      unfolding * ..
    1.69    also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"
    1.70      using null_set S by (intro measure_Un_null_set) auto
    1.71 -  finally show ?thesis unfolding \<mu>'_def .
    1.72 +  finally show ?thesis .
    1.73  qed
    1.74  
    1.75  lemma (in completeable_measure_space) \<mu>_main_part_Un:
    1.76 @@ -168,30 +171,35 @@
    1.77      unfolding range_binary_eq Un_range_binary UN by auto
    1.78  qed
    1.79  
    1.80 -sublocale completeable_measure_space \<subseteq> completion!: measure_space completion \<mu>'
    1.81 -proof
    1.82 -  show "\<mu>' {} = 0" by auto
    1.83 -next
    1.84 -  show "countably_additive completion \<mu>'"
    1.85 -  proof (unfold countably_additive_def, intro allI conjI impI)
    1.86 -    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
    1.87 -    have "disjoint_family (\<lambda>i. main_part (A i))"
    1.88 -    proof (intro disjoint_family_on_bisimulation[OF A(2)])
    1.89 -      fix n m assume "A n \<inter> A m = {}"
    1.90 -      then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
    1.91 -        using A by (subst (1 2) main_part_null_part_Un) auto
    1.92 -      then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
    1.93 +sublocale completeable_measure_space \<subseteq> completion!: measure_space completion
    1.94 +  where "measure completion = \<mu>'"
    1.95 +proof -
    1.96 +  show "measure_space completion"
    1.97 +  proof
    1.98 +    show "measure completion {} = 0" by (auto simp: completion_def)
    1.99 +  next
   1.100 +    show "countably_additive completion (measure completion)"
   1.101 +    proof (intro countably_additiveI)
   1.102 +      fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
   1.103 +      have "disjoint_family (\<lambda>i. main_part (A i))"
   1.104 +      proof (intro disjoint_family_on_bisimulation[OF A(2)])
   1.105 +        fix n m assume "A n \<inter> A m = {}"
   1.106 +        then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
   1.107 +          using A by (subst (1 2) main_part_null_part_Un) auto
   1.108 +        then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
   1.109 +      qed
   1.110 +      then have "(\<Sum>\<^isub>\<infinity>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"
   1.111 +        unfolding completion_def using A by (auto intro!: measure_countably_additive)
   1.112 +      then show "(\<Sum>\<^isub>\<infinity>n. measure completion (A n)) = measure completion (UNION UNIV A)"
   1.113 +        by (simp add: completion_def \<mu>_main_part_UN[OF A(1)])
   1.114      qed
   1.115 -    then have "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu> (\<Union>i. main_part (A i))"
   1.116 -      unfolding \<mu>'_def using A by (intro measure_countably_additive) auto
   1.117 -    then show "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu>' (UNION UNIV A)"
   1.118 -      unfolding \<mu>_main_part_UN[OF A(1)] .
   1.119    qed
   1.120 +  show "measure completion = \<mu>'" unfolding completion_def by simp
   1.121  qed
   1.122  
   1.123  lemma (in completeable_measure_space) completion_ex_simple_function:
   1.124 -  assumes f: "completion.simple_function f"
   1.125 -  shows "\<exists>f'. simple_function f' \<and> (AE x. f x = f' x)"
   1.126 +  assumes f: "simple_function completion f"
   1.127 +  shows "\<exists>f'. simple_function M f' \<and> (AE x. f x = f' x)"
   1.128  proof -
   1.129    let "?F x" = "f -` {x} \<inter> space M"
   1.130    have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
   1.131 @@ -248,11 +256,11 @@
   1.132    shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
   1.133  proof -
   1.134    from g[THEN completion.borel_measurable_implies_simple_function_sequence]
   1.135 -  obtain f where "\<And>i. completion.simple_function (f i)" "f \<up> g" by auto
   1.136 -  then have "\<forall>i. \<exists>f'. simple_function f' \<and> (AE x. f i x = f' x)"
   1.137 +  obtain f where "\<And>i. simple_function completion (f i)" "f \<up> g" by auto
   1.138 +  then have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)"
   1.139      using completion_ex_simple_function by auto
   1.140    from this[THEN choice] obtain f' where
   1.141 -    sf: "\<And>i. simple_function (f' i)" and
   1.142 +    sf: "\<And>i. simple_function M (f' i)" and
   1.143      AE: "\<forall>i. AE x. f i x = f' i x" by auto
   1.144    show ?thesis
   1.145    proof (intro bexI)