src/HOL/Probability/Complete_Measure.thy
author hoelzl
Mon Mar 14 14:37:49 2011 +0100 (2011-03-14)
changeset 41981 cdf7693bbe08
parent 41959 b460124855b8
child 41983 2dc6e382a58b
permissions -rw-r--r--
reworked Probability theory: measures are not type restricted to positive extended reals
     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)
    11   "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
    12     fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
    13 
    14 definition (in completeable_measure_space)
    15   "main_part A = fst (Eps (split_completion A))"
    16 
    17 definition (in completeable_measure_space)
    18   "null_part A = snd (Eps (split_completion A))"
    19 
    20 abbreviation (in completeable_measure_space) "\<mu>' A \<equiv> \<mu> (main_part A)"
    21 
    22 definition (in completeable_measure_space) completion :: "('a, 'b) measure_space_scheme" where
    23   "completion = \<lparr> space = space M,
    24                   sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' },
    25                   measure = \<mu>',
    26                   \<dots> = more M \<rparr>"
    27 
    28 
    29 lemma (in completeable_measure_space) space_completion[simp]:
    30   "space completion = space M" unfolding completion_def by simp
    31 
    32 lemma (in completeable_measure_space) sets_completionE:
    33   assumes "A \<in> sets completion"
    34   obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
    35   using assms unfolding completion_def by auto
    36 
    37 lemma (in completeable_measure_space) sets_completionI:
    38   assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
    39   shows "A \<in> sets completion"
    40   using assms unfolding completion_def by auto
    41 
    42 lemma (in completeable_measure_space) sets_completionI_sets[intro]:
    43   "A \<in> sets M \<Longrightarrow> A \<in> sets completion"
    44   unfolding completion_def by force
    45 
    46 lemma (in completeable_measure_space) null_sets_completion:
    47   assumes "N' \<in> null_sets" "N \<subseteq> N'" shows "N \<in> sets completion"
    48   apply(rule sets_completionI[of N "{}" N N'])
    49   using assms by auto
    50 
    51 sublocale completeable_measure_space \<subseteq> completion!: sigma_algebra completion
    52 proof (unfold sigma_algebra_iff2, safe)
    53   fix A x assume "A \<in> sets completion" "x \<in> A"
    54   with sets_into_space show "x \<in> space completion"
    55     by (auto elim!: sets_completionE)
    56 next
    57   fix A assume "A \<in> sets completion"
    58   from this[THEN sets_completionE] guess S N N' . note A = this
    59   let ?C = "space completion"
    60   show "?C - A \<in> sets completion" using A
    61     by (intro sets_completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"])
    62        auto
    63 next
    64   fix A ::"nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion"
    65   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'"
    66     unfolding completion_def by (auto simp: image_subset_iff)
    67   from choice[OF this] guess S ..
    68   from choice[OF this] guess N ..
    69   from choice[OF this] guess N' ..
    70   then show "UNION UNIV A \<in> sets completion"
    71     using null_sets_UN[of N']
    72     by (intro sets_completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"])
    73        auto
    74 qed auto
    75 
    76 lemma (in completeable_measure_space) split_completion:
    77   assumes "A \<in> sets completion"
    78   shows "split_completion A (main_part A, null_part A)"
    79   unfolding main_part_def null_part_def
    80 proof (rule someI2_ex)
    81   from assms[THEN sets_completionE] guess S N N' . note A = this
    82   let ?P = "(S, N - S)"
    83   show "\<exists>p. split_completion A p"
    84     unfolding split_completion_def using A
    85   proof (intro exI conjI)
    86     show "A = fst ?P \<union> snd ?P" using A by auto
    87     show "snd ?P \<subseteq> N'" using A by auto
    88   qed auto
    89 qed auto
    90 
    91 lemma (in completeable_measure_space)
    92   assumes "S \<in> sets completion"
    93   shows main_part_sets[intro, simp]: "main_part S \<in> sets M"
    94     and main_part_null_part_Un[simp]: "main_part S \<union> null_part S = S"
    95     and main_part_null_part_Int[simp]: "main_part S \<inter> null_part S = {}"
    96   using split_completion[OF assms] by (auto simp: split_completion_def)
    97 
    98 lemma (in completeable_measure_space) null_part:
    99   assumes "S \<in> sets completion" shows "\<exists>N. N\<in>null_sets \<and> null_part S \<subseteq> N"
   100   using split_completion[OF assms] by (auto simp: split_completion_def)
   101 
   102 lemma (in completeable_measure_space) null_part_sets[intro, simp]:
   103   assumes "S \<in> sets M" shows "null_part S \<in> sets M" "\<mu> (null_part S) = 0"
   104 proof -
   105   have S: "S \<in> sets completion" using assms by auto
   106   have "S - main_part S \<in> sets M" using assms by auto
   107   moreover
   108   from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
   109   have "S - main_part S = null_part S" by auto
   110   ultimately show sets: "null_part S \<in> sets M" by auto
   111   from null_part[OF S] guess N ..
   112   with measure_eq_0[of N "null_part S"] sets
   113   show "\<mu> (null_part S) = 0" by auto
   114 qed
   115 
   116 lemma (in completeable_measure_space) \<mu>'_set[simp]:
   117   assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"
   118 proof -
   119   have S: "S \<in> sets completion" using assms by auto
   120   then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp
   121   also have "\<dots> = \<mu>' S"
   122     using S assms measure_additive[of "main_part S" "null_part S"]
   123     by (auto simp: measure_additive)
   124   finally show ?thesis by simp
   125 qed
   126 
   127 lemma (in completeable_measure_space) sets_completionI_sub:
   128   assumes N: "N' \<in> null_sets" "N \<subseteq> N'"
   129   shows "N \<in> sets completion"
   130   using assms by (intro sets_completionI[of _ "{}" N N']) auto
   131 
   132 lemma (in completeable_measure_space) \<mu>_main_part_UN:
   133   fixes S :: "nat \<Rightarrow> 'a set"
   134   assumes "range S \<subseteq> sets completion"
   135   shows "\<mu>' (\<Union>i. (S i)) = \<mu> (\<Union>i. main_part (S i))"
   136 proof -
   137   have S: "\<And>i. S i \<in> sets completion" using assms by auto
   138   then have UN: "(\<Union>i. S i) \<in> sets completion" by auto
   139   have "\<forall>i. \<exists>N. N \<in> null_sets \<and> null_part (S i) \<subseteq> N"
   140     using null_part[OF S] by auto
   141   from choice[OF this] guess N .. note N = this
   142   then have UN_N: "(\<Union>i. N i) \<in> null_sets" by (intro null_sets_UN) auto
   143   have "(\<Union>i. S i) \<in> sets completion" using S by auto
   144   from null_part[OF this] guess N' .. note N' = this
   145   let ?N = "(\<Union>i. N i) \<union> N'"
   146   have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
   147   have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"
   148     using N' by auto
   149   also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
   150     unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
   151   also have "\<dots> = (\<Union>i. main_part (S i)) \<union> ?N"
   152     using N by auto
   153   finally have *: "main_part (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part (S i)) \<union> ?N" .
   154   have "\<mu> (main_part (\<Union>i. S i)) = \<mu> (main_part (\<Union>i. S i) \<union> ?N)"
   155     using null_set UN by (intro measure_Un_null_set[symmetric]) auto
   156   also have "\<dots> = \<mu> ((\<Union>i. main_part (S i)) \<union> ?N)"
   157     unfolding * ..
   158   also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"
   159     using null_set S by (intro measure_Un_null_set) auto
   160   finally show ?thesis .
   161 qed
   162 
   163 lemma (in completeable_measure_space) \<mu>_main_part_Un:
   164   assumes S: "S \<in> sets completion" and T: "T \<in> sets completion"
   165   shows "\<mu>' (S \<union> T) = \<mu> (main_part S \<union> main_part T)"
   166 proof -
   167   have UN: "(\<Union>i. binary (main_part S) (main_part T) i) = (\<Union>i. main_part (binary S T i))"
   168     unfolding binary_def by (auto split: split_if_asm)
   169   show ?thesis
   170     using \<mu>_main_part_UN[of "binary S T"] assms
   171     unfolding range_binary_eq Un_range_binary UN by auto
   172 qed
   173 
   174 sublocale completeable_measure_space \<subseteq> completion!: measure_space completion
   175   where "measure completion = \<mu>'"
   176 proof -
   177   show "measure_space completion"
   178   proof
   179     show "positive completion (measure completion)"
   180       by (auto simp: completion_def positive_def)
   181   next
   182     show "countably_additive completion (measure completion)"
   183     proof (intro countably_additiveI)
   184       fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
   185       have "disjoint_family (\<lambda>i. main_part (A i))"
   186       proof (intro disjoint_family_on_bisimulation[OF A(2)])
   187         fix n m assume "A n \<inter> A m = {}"
   188         then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
   189           using A by (subst (1 2) main_part_null_part_Un) auto
   190         then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
   191       qed
   192       then have "(\<Sum>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"
   193         unfolding completion_def using A by (auto intro!: measure_countably_additive)
   194       then show "(\<Sum>n. measure completion (A n)) = measure completion (UNION UNIV A)"
   195         by (simp add: completion_def \<mu>_main_part_UN[OF A(1)])
   196     qed
   197   qed
   198   show "measure completion = \<mu>'" unfolding completion_def by simp
   199 qed
   200 
   201 lemma (in completeable_measure_space) completion_ex_simple_function:
   202   assumes f: "simple_function completion f"
   203   shows "\<exists>f'. simple_function M f' \<and> (AE x. f x = f' x)"
   204 proof -
   205   let "?F x" = "f -` {x} \<inter> space M"
   206   have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
   207     using completion.simple_functionD[OF f]
   208       completion.simple_functionD[OF f] by simp_all
   209   have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"
   210     using F null_part by auto
   211   from choice[OF this] obtain N where
   212     N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
   213   let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
   214   have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
   215   show ?thesis unfolding simple_function_def
   216   proof (safe intro!: exI[of _ ?f'])
   217     have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
   218     from finite_subset[OF this] completion.simple_functionD(1)[OF f]
   219     show "finite (?f' ` space M)" by auto
   220   next
   221     fix x assume "x \<in> space M"
   222     have "?f' -` {?f' x} \<inter> space M =
   223       (if x \<in> ?N then ?F undefined \<union> ?N
   224        else if f x = undefined then ?F (f x) \<union> ?N
   225        else ?F (f x) - ?N)"
   226       using N(2) sets_into_space by (auto split: split_if_asm)
   227     moreover { fix y have "?F y \<union> ?N \<in> sets M"
   228       proof cases
   229         assume y: "y \<in> f`space M"
   230         have "?F y \<union> ?N = (main_part (?F y) \<union> null_part (?F y)) \<union> ?N"
   231           using main_part_null_part_Un[OF F] by auto
   232         also have "\<dots> = main_part (?F y) \<union> ?N"
   233           using y N by auto
   234         finally show ?thesis
   235           using F sets by auto
   236       next
   237         assume "y \<notin> f`space M" then have "?F y = {}" by auto
   238         then show ?thesis using sets by auto
   239       qed }
   240     moreover {
   241       have "?F (f x) - ?N = main_part (?F (f x)) \<union> null_part (?F (f x)) - ?N"
   242         using main_part_null_part_Un[OF F] by auto
   243       also have "\<dots> = main_part (?F (f x)) - ?N"
   244         using N `x \<in> space M` by auto
   245       finally have "?F (f x) - ?N \<in> sets M"
   246         using F sets by auto }
   247     ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
   248   next
   249     show "AE x. f x = ?f' x"
   250       by (rule AE_I', rule sets) auto
   251   qed
   252 qed
   253 
   254 lemma (in completeable_measure_space) completion_ex_borel_measurable_pos:
   255   fixes g :: "'a \<Rightarrow> extreal"
   256   assumes g: "g \<in> borel_measurable completion" and "\<And>x. 0 \<le> g x"
   257   shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
   258 proof -
   259   from g[THEN completion.borel_measurable_implies_simple_function_sequence'] guess f . note f = this
   260   from this(1)[THEN completion_ex_simple_function]
   261   have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)" ..
   262   from this[THEN choice] obtain f' where
   263     sf: "\<And>i. simple_function M (f' i)" and
   264     AE: "\<forall>i. AE x. f i x = f' i x" by auto
   265   show ?thesis
   266   proof (intro bexI)
   267     from AE[unfolded AE_all_countable[symmetric]]
   268     show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
   269     proof (elim AE_mp, safe intro!: AE_I2)
   270       fix x assume eq: "\<forall>i. f i x = f' i x"
   271       moreover have "g x = (SUP i. f i x)"
   272         unfolding f using `0 \<le> g x` by (auto split: split_max)
   273       ultimately show "g x = ?f x" by auto
   274     qed
   275     show "?f \<in> borel_measurable M"
   276       using sf by (auto intro: borel_measurable_simple_function)
   277   qed
   278 qed
   279 
   280 lemma (in completeable_measure_space) completion_ex_borel_measurable:
   281   fixes g :: "'a \<Rightarrow> extreal"
   282   assumes g: "g \<in> borel_measurable completion"
   283   shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
   284 proof -
   285   have "(\<lambda>x. max 0 (g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (g x)" using g by auto
   286   from completion_ex_borel_measurable_pos[OF this] guess g_pos ..
   287   moreover
   288   have "(\<lambda>x. max 0 (- g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (- g x)" using g by auto
   289   from completion_ex_borel_measurable_pos[OF this] guess g_neg ..
   290   ultimately
   291   show ?thesis
   292   proof (safe intro!: bexI[of _ "\<lambda>x. g_pos x - g_neg x"])
   293     show "AE x. max 0 (- g x) = g_neg x \<longrightarrow> max 0 (g x) = g_pos x \<longrightarrow> g x = g_pos x - g_neg x"
   294     proof (intro AE_I2 impI)
   295       fix x assume g: "max 0 (- g x) = g_neg x" "max 0 (g x) = g_pos x"
   296       show "g x = g_pos x - g_neg x" unfolding g[symmetric]
   297         by (cases "g x") (auto split: split_max)
   298     qed
   299   qed auto
   300 qed
   301 
   302 end