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
```