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