src/HOL/Probability/Complete_Measure.thy
author hoelzl
Wed Dec 01 19:20:30 2010 +0100 (2010-12-01)
changeset 40859 de0b30e6c2d2
child 40871 688f6ff859e1
permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
     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 sigma_algebra) simple_functionD':
   193   assumes "simple_function f"
   194   shows "f -` {x} \<inter> space M \<in> sets M"
   195 proof cases
   196   assume "x \<in> f`space M" from simple_functionD(2)[OF assms this] show ?thesis .
   197 next
   198   assume "x \<notin> f`space M" then have "f -` {x} \<inter> space M = {}" by auto
   199   then show ?thesis by auto
   200 qed
   201 
   202 lemma (in sigma_algebra) simple_function_If:
   203   assumes sf: "simple_function f" "simple_function g" and A: "A \<in> sets M"
   204   shows "simple_function (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function ?IF")
   205 proof -
   206   def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M"
   207   show ?thesis unfolding simple_function_def
   208   proof safe
   209     have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto
   210     from finite_subset[OF this] assms
   211     show "finite (?IF ` space M)" unfolding simple_function_def by auto
   212   next
   213     fix x assume "x \<in> space M"
   214     then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
   215       then ((F (f x) \<inter> A) \<union> (G (f x) - (G (f x) \<inter> A)))
   216       else ((F (g x) \<inter> A) \<union> (G (g x) - (G (g x) \<inter> A))))"
   217       using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
   218     have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
   219       unfolding F_def G_def using sf[THEN simple_functionD'] by auto
   220     show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
   221   qed
   222 qed
   223 
   224 lemma (in measure_space) null_sets_finite_UN:
   225   assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets"
   226   shows "(\<Union>i\<in>S. A i) \<in> null_sets"
   227 proof (intro CollectI conjI)
   228   show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto
   229   have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))"
   230     using assms by (intro measure_finitely_subadditive) auto
   231   then show "\<mu> (\<Union>i\<in>S. A i) = 0"
   232     using assms by auto
   233 qed
   234 
   235 lemma (in completeable_measure_space) completion_ex_simple_function:
   236   assumes f: "completion.simple_function f"
   237   shows "\<exists>f'. simple_function f' \<and> (AE x. f x = f' x)"
   238 proof -
   239   let "?F x" = "f -` {x} \<inter> space M"
   240   have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
   241     using completion.simple_functionD'[OF f]
   242       completion.simple_functionD[OF f] by simp_all
   243   have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"
   244     using F null_part by auto
   245   from choice[OF this] obtain N where
   246     N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
   247   let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
   248   have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
   249   show ?thesis unfolding simple_function_def
   250   proof (safe intro!: exI[of _ ?f'])
   251     have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
   252     from finite_subset[OF this] completion.simple_functionD(1)[OF f]
   253     show "finite (?f' ` space M)" by auto
   254   next
   255     fix x assume "x \<in> space M"
   256     have "?f' -` {?f' x} \<inter> space M =
   257       (if x \<in> ?N then ?F undefined \<union> ?N
   258        else if f x = undefined then ?F (f x) \<union> ?N
   259        else ?F (f x) - ?N)"
   260       using N(2) sets_into_space by (auto split: split_if_asm)
   261     moreover { fix y have "?F y \<union> ?N \<in> sets M"
   262       proof cases
   263         assume y: "y \<in> f`space M"
   264         have "?F y \<union> ?N = (main_part (?F y) \<union> null_part (?F y)) \<union> ?N"
   265           using main_part_null_part_Un[OF F] by auto
   266         also have "\<dots> = main_part (?F y) \<union> ?N"
   267           using y N by auto
   268         finally show ?thesis
   269           using F sets by auto
   270       next
   271         assume "y \<notin> f`space M" then have "?F y = {}" by auto
   272         then show ?thesis using sets by auto
   273       qed }
   274     moreover {
   275       have "?F (f x) - ?N = main_part (?F (f x)) \<union> null_part (?F (f x)) - ?N"
   276         using main_part_null_part_Un[OF F] by auto
   277       also have "\<dots> = main_part (?F (f x)) - ?N"
   278         using N `x \<in> space M` by auto
   279       finally have "?F (f x) - ?N \<in> sets M"
   280         using F sets by auto }
   281     ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
   282   next
   283     show "AE x. f x = ?f' x"
   284       by (rule AE_I', rule sets) auto
   285   qed
   286 qed
   287 
   288 lemma (in completeable_measure_space) completion_ex_borel_measurable:
   289   fixes g :: "'a \<Rightarrow> pinfreal"
   290   assumes g: "g \<in> borel_measurable completion"
   291   shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
   292 proof -
   293   from g[THEN completion.borel_measurable_implies_simple_function_sequence]
   294   obtain f where "\<And>i. completion.simple_function (f i)" "f \<up> g" by auto
   295   then have "\<forall>i. \<exists>f'. simple_function f' \<and> (AE x. f i x = f' x)"
   296     using completion_ex_simple_function by auto
   297   from this[THEN choice] obtain f' where
   298     sf: "\<And>i. simple_function (f' i)" and
   299     AE: "\<forall>i. AE x. f i x = f' i x" by auto
   300   show ?thesis
   301   proof (intro bexI)
   302     from AE[unfolded all_AE_countable]
   303     show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
   304     proof (rule AE_mp, safe intro!: AE_cong)
   305       fix x assume eq: "\<forall>i. f i x = f' i x"
   306       have "g x = (SUP i. f i x)"
   307         using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
   308       then show "g x = ?f x"
   309         using eq unfolding SUPR_fun_expand by auto
   310     qed
   311     show "?f \<in> borel_measurable M"
   312       using sf by (auto intro!: borel_measurable_SUP
   313         intro: borel_measurable_simple_function)
   314   qed
   315 qed
   316 
   317 end