src/HOL/Probability/Complete_Measure.thy
author hoelzl
Wed Dec 08 19:32:11 2010 +0100 (2010-12-08)
changeset 41097 a1abfa4e2b44
parent 41023 9118eb4eb8dc
child 41689 3e39b0e730d6
permissions -rw-r--r--
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
     1 (*  Title:      Complete_Measure.thy
     2     Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
     3 *)
     4 theory Complete_Measure
     5 imports Product_Measure
     6 begin
     7 
     8 locale completeable_measure_space = measure_space
     9 
    10 definition (in completeable_measure_space) completion :: "'a algebra" where
    11   "completion = \<lparr> space = space M,
    12     sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' } \<rparr>"
    13 
    14 lemma (in completeable_measure_space) space_completion[simp]:
    15   "space completion = space M" unfolding completion_def by simp
    16 
    17 lemma (in completeable_measure_space) sets_completionE:
    18   assumes "A \<in> sets completion"
    19   obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
    20   using assms unfolding completion_def by auto
    21 
    22 lemma (in completeable_measure_space) sets_completionI:
    23   assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
    24   shows "A \<in> sets completion"
    25   using assms unfolding completion_def by auto
    26 
    27 lemma (in completeable_measure_space) sets_completionI_sets[intro]:
    28   "A \<in> sets M \<Longrightarrow> A \<in> sets completion"
    29   unfolding completion_def by force
    30 
    31 lemma (in completeable_measure_space) null_sets_completion:
    32   assumes "N' \<in> null_sets" "N \<subseteq> N'" shows "N \<in> sets completion"
    33   apply(rule sets_completionI[of N "{}" N N'])
    34   using assms by auto
    35 
    36 sublocale completeable_measure_space \<subseteq> completion!: sigma_algebra completion
    37 proof (unfold sigma_algebra_iff2, safe)
    38   fix A x assume "A \<in> sets completion" "x \<in> A"
    39   with sets_into_space show "x \<in> space completion"
    40     by (auto elim!: sets_completionE)
    41 next
    42   fix A assume "A \<in> sets completion"
    43   from this[THEN sets_completionE] guess S N N' . note A = this
    44   let ?C = "space completion"
    45   show "?C - A \<in> sets completion" using A
    46     by (intro sets_completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"])
    47        auto
    48 next
    49   fix A ::"nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion"
    50   then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N'"
    51     unfolding completion_def by (auto simp: image_subset_iff)
    52   from choice[OF this] guess S ..
    53   from choice[OF this] guess N ..
    54   from choice[OF this] guess N' ..
    55   then show "UNION UNIV A \<in> sets completion"
    56     using null_sets_UN[of N']
    57     by (intro sets_completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"])
    58        auto
    59 qed auto
    60 
    61 definition (in completeable_measure_space)
    62   "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
    63     fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
    64 
    65 definition (in completeable_measure_space)
    66   "main_part A = fst (Eps (split_completion A))"
    67 
    68 definition (in completeable_measure_space)
    69   "null_part A = snd (Eps (split_completion A))"
    70 
    71 lemma (in completeable_measure_space) split_completion:
    72   assumes "A \<in> sets completion"
    73   shows "split_completion A (main_part A, null_part A)"
    74   unfolding main_part_def null_part_def
    75 proof (rule someI2_ex)
    76   from assms[THEN sets_completionE] guess S N N' . note A = this
    77   let ?P = "(S, N - S)"
    78   show "\<exists>p. split_completion A p"
    79     unfolding split_completion_def using A
    80   proof (intro exI conjI)
    81     show "A = fst ?P \<union> snd ?P" using A by auto
    82     show "snd ?P \<subseteq> N'" using A by auto
    83   qed auto
    84 qed auto
    85 
    86 lemma (in completeable_measure_space)
    87   assumes "S \<in> sets completion"
    88   shows main_part_sets[intro, simp]: "main_part S \<in> sets M"
    89     and main_part_null_part_Un[simp]: "main_part S \<union> null_part S = S"
    90     and main_part_null_part_Int[simp]: "main_part S \<inter> null_part S = {}"
    91   using split_completion[OF assms] by (auto simp: split_completion_def)
    92 
    93 lemma (in completeable_measure_space) null_part:
    94   assumes "S \<in> sets completion" shows "\<exists>N. N\<in>null_sets \<and> null_part S \<subseteq> N"
    95   using split_completion[OF assms] by (auto simp: split_completion_def)
    96 
    97 lemma (in completeable_measure_space) null_part_sets[intro, simp]:
    98   assumes "S \<in> sets M" shows "null_part S \<in> sets M" "\<mu> (null_part S) = 0"
    99 proof -
   100   have S: "S \<in> sets completion" using assms by auto
   101   have "S - main_part S \<in> sets M" using assms by auto
   102   moreover
   103   from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
   104   have "S - main_part S = null_part S" by auto
   105   ultimately show sets: "null_part S \<in> sets M" by auto
   106   from null_part[OF S] guess N ..
   107   with measure_eq_0[of N "null_part S"] sets
   108   show "\<mu> (null_part S) = 0" by auto
   109 qed
   110 
   111 definition (in completeable_measure_space) "\<mu>' A = \<mu> (main_part A)"
   112 
   113 lemma (in completeable_measure_space) \<mu>'_set[simp]:
   114   assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"
   115 proof -
   116   have S: "S \<in> sets completion" using assms by auto
   117   then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp
   118   also have "\<dots> = \<mu> (main_part S)"
   119     using S assms measure_additive[of "main_part S" "null_part S"]
   120     by (auto simp: measure_additive)
   121   finally show ?thesis unfolding \<mu>'_def by simp
   122 qed
   123 
   124 lemma (in completeable_measure_space) sets_completionI_sub:
   125   assumes N: "N' \<in> null_sets" "N \<subseteq> N'"
   126   shows "N \<in> sets completion"
   127   using assms by (intro sets_completionI[of _ "{}" N N']) auto
   128 
   129 lemma (in completeable_measure_space) \<mu>_main_part_UN:
   130   fixes S :: "nat \<Rightarrow> 'a set"
   131   assumes "range S \<subseteq> sets completion"
   132   shows "\<mu>' (\<Union>i. (S i)) = \<mu> (\<Union>i. main_part (S i))"
   133 proof -
   134   have S: "\<And>i. S i \<in> sets completion" using assms by auto
   135   then have UN: "(\<Union>i. S i) \<in> sets completion" by auto
   136   have "\<forall>i. \<exists>N. N \<in> null_sets \<and> null_part (S i) \<subseteq> N"
   137     using null_part[OF S] by auto
   138   from choice[OF this] guess N .. note N = this
   139   then have UN_N: "(\<Union>i. N i) \<in> null_sets" by (intro null_sets_UN) auto
   140   have "(\<Union>i. S i) \<in> sets completion" using S by auto
   141   from null_part[OF this] guess N' .. note N' = this
   142   let ?N = "(\<Union>i. N i) \<union> N'"
   143   have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
   144   have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"
   145     using N' by auto
   146   also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
   147     unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
   148   also have "\<dots> = (\<Union>i. main_part (S i)) \<union> ?N"
   149     using N by auto
   150   finally have *: "main_part (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part (S i)) \<union> ?N" .
   151   have "\<mu> (main_part (\<Union>i. S i)) = \<mu> (main_part (\<Union>i. S i) \<union> ?N)"
   152     using null_set UN by (intro measure_Un_null_set[symmetric]) auto
   153   also have "\<dots> = \<mu> ((\<Union>i. main_part (S i)) \<union> ?N)"
   154     unfolding * ..
   155   also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"
   156     using null_set S by (intro measure_Un_null_set) auto
   157   finally show ?thesis unfolding \<mu>'_def .
   158 qed
   159 
   160 lemma (in completeable_measure_space) \<mu>_main_part_Un:
   161   assumes S: "S \<in> sets completion" and T: "T \<in> sets completion"
   162   shows "\<mu>' (S \<union> T) = \<mu> (main_part S \<union> main_part T)"
   163 proof -
   164   have UN: "(\<Union>i. binary (main_part S) (main_part T) i) = (\<Union>i. main_part (binary S T i))"
   165     unfolding binary_def by (auto split: split_if_asm)
   166   show ?thesis
   167     using \<mu>_main_part_UN[of "binary S T"] assms
   168     unfolding range_binary_eq Un_range_binary UN by auto
   169 qed
   170 
   171 sublocale completeable_measure_space \<subseteq> completion!: measure_space completion \<mu>'
   172 proof
   173   show "\<mu>' {} = 0" by auto
   174 next
   175   show "countably_additive completion \<mu>'"
   176   proof (unfold countably_additive_def, intro allI conjI impI)
   177     fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
   178     have "disjoint_family (\<lambda>i. main_part (A i))"
   179     proof (intro disjoint_family_on_bisimulation[OF A(2)])
   180       fix n m assume "A n \<inter> A m = {}"
   181       then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
   182         using A by (subst (1 2) main_part_null_part_Un) auto
   183       then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
   184     qed
   185     then have "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu> (\<Union>i. main_part (A i))"
   186       unfolding \<mu>'_def using A by (intro measure_countably_additive) auto
   187     then show "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu>' (UNION UNIV A)"
   188       unfolding \<mu>_main_part_UN[OF A(1)] .
   189   qed
   190 qed
   191 
   192 lemma (in completeable_measure_space) completion_ex_simple_function:
   193   assumes f: "completion.simple_function f"
   194   shows "\<exists>f'. simple_function f' \<and> (AE x. f x = f' x)"
   195 proof -
   196   let "?F x" = "f -` {x} \<inter> space M"
   197   have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
   198     using completion.simple_functionD[OF f]
   199       completion.simple_functionD[OF f] by simp_all
   200   have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"
   201     using F null_part by auto
   202   from choice[OF this] obtain N where
   203     N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
   204   let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
   205   have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
   206   show ?thesis unfolding simple_function_def
   207   proof (safe intro!: exI[of _ ?f'])
   208     have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
   209     from finite_subset[OF this] completion.simple_functionD(1)[OF f]
   210     show "finite (?f' ` space M)" by auto
   211   next
   212     fix x assume "x \<in> space M"
   213     have "?f' -` {?f' x} \<inter> space M =
   214       (if x \<in> ?N then ?F undefined \<union> ?N
   215        else if f x = undefined then ?F (f x) \<union> ?N
   216        else ?F (f x) - ?N)"
   217       using N(2) sets_into_space by (auto split: split_if_asm)
   218     moreover { fix y have "?F y \<union> ?N \<in> sets M"
   219       proof cases
   220         assume y: "y \<in> f`space M"
   221         have "?F y \<union> ?N = (main_part (?F y) \<union> null_part (?F y)) \<union> ?N"
   222           using main_part_null_part_Un[OF F] by auto
   223         also have "\<dots> = main_part (?F y) \<union> ?N"
   224           using y N by auto
   225         finally show ?thesis
   226           using F sets by auto
   227       next
   228         assume "y \<notin> f`space M" then have "?F y = {}" by auto
   229         then show ?thesis using sets by auto
   230       qed }
   231     moreover {
   232       have "?F (f x) - ?N = main_part (?F (f x)) \<union> null_part (?F (f x)) - ?N"
   233         using main_part_null_part_Un[OF F] by auto
   234       also have "\<dots> = main_part (?F (f x)) - ?N"
   235         using N `x \<in> space M` by auto
   236       finally have "?F (f x) - ?N \<in> sets M"
   237         using F sets by auto }
   238     ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
   239   next
   240     show "AE x. f x = ?f' x"
   241       by (rule AE_I', rule sets) auto
   242   qed
   243 qed
   244 
   245 lemma (in completeable_measure_space) completion_ex_borel_measurable:
   246   fixes g :: "'a \<Rightarrow> pextreal"
   247   assumes g: "g \<in> borel_measurable completion"
   248   shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
   249 proof -
   250   from g[THEN completion.borel_measurable_implies_simple_function_sequence]
   251   obtain f where "\<And>i. completion.simple_function (f i)" "f \<up> g" by auto
   252   then have "\<forall>i. \<exists>f'. simple_function f' \<and> (AE x. f i x = f' x)"
   253     using completion_ex_simple_function by auto
   254   from this[THEN choice] obtain f' where
   255     sf: "\<And>i. simple_function (f' i)" and
   256     AE: "\<forall>i. AE x. f i x = f' i x" by auto
   257   show ?thesis
   258   proof (intro bexI)
   259     from AE[unfolded all_AE_countable]
   260     show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
   261     proof (rule AE_mp, safe intro!: AE_cong)
   262       fix x assume eq: "\<forall>i. f i x = f' i x"
   263       moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
   264       ultimately show "g x = ?f x" by (simp add: SUPR_apply)
   265     qed
   266     show "?f \<in> borel_measurable M"
   267       using sf by (auto intro: borel_measurable_simple_function)
   268   qed
   269 qed
   270 
   271 end