src/HOL/Probability/Complete_Measure.thy
 author haftmann Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) changeset 60517 f16e4fb20652 parent 58587 5484f6079bcd child 61808 fc1556774cfe permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
```     1 (*  Title:      HOL/Probability/Complete_Measure.thy
```
```     2     Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 theory Complete_Measure
```
```     6   imports Bochner_Integration Probability_Measure
```
```     7 begin
```
```     8
```
```     9 definition
```
```    10   "split_completion M A p = (if A \<in> sets M then p = (A, {}) else
```
```    11    \<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and> fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets M)"
```
```    12
```
```    13 definition
```
```    14   "main_part M A = fst (Eps (split_completion M A))"
```
```    15
```
```    16 definition
```
```    17   "null_part M A = snd (Eps (split_completion M A))"
```
```    18
```
```    19 definition completion :: "'a measure \<Rightarrow> 'a measure" where
```
```    20   "completion M = measure_of (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }
```
```    21     (emeasure M \<circ> main_part M)"
```
```    22
```
```    23 lemma completion_into_space:
```
```    24   "{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)"
```
```    25   using sets.sets_into_space by auto
```
```    26
```
```    27 lemma space_completion[simp]: "space (completion M) = space M"
```
```    28   unfolding completion_def using space_measure_of[OF completion_into_space] by simp
```
```    29
```
```    30 lemma completionI:
```
```    31   assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
```
```    32   shows "A \<in> { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
```
```    33   using assms by auto
```
```    34
```
```    35 lemma completionE:
```
```    36   assumes "A \<in> { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
```
```    37   obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
```
```    38   using assms by auto
```
```    39
```
```    40 lemma sigma_algebra_completion:
```
```    41   "sigma_algebra (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
```
```    42     (is "sigma_algebra _ ?A")
```
```    43   unfolding sigma_algebra_iff2
```
```    44 proof (intro conjI ballI allI impI)
```
```    45   show "?A \<subseteq> Pow (space M)"
```
```    46     using sets.sets_into_space by auto
```
```    47 next
```
```    48   show "{} \<in> ?A" by auto
```
```    49 next
```
```    50   let ?C = "space M"
```
```    51   fix A assume "A \<in> ?A" from completionE[OF this] guess S N N' .
```
```    52   then show "space M - A \<in> ?A"
```
```    53     by (intro completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"]) auto
```
```    54 next
```
```    55   fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> ?A"
```
```    56   then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N'"
```
```    57     by (auto simp: image_subset_iff)
```
```    58   from choice[OF this] guess S ..
```
```    59   from choice[OF this] guess N ..
```
```    60   from choice[OF this] guess N' ..
```
```    61   then show "UNION UNIV A \<in> ?A"
```
```    62     using null_sets_UN[of N']
```
```    63     by (intro completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"]) auto
```
```    64 qed
```
```    65
```
```    66 lemma sets_completion:
```
```    67   "sets (completion M) = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
```
```    68   using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion] by (simp add: completion_def)
```
```    69
```
```    70 lemma sets_completionE:
```
```    71   assumes "A \<in> sets (completion M)"
```
```    72   obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
```
```    73   using assms unfolding sets_completion by auto
```
```    74
```
```    75 lemma sets_completionI:
```
```    76   assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
```
```    77   shows "A \<in> sets (completion M)"
```
```    78   using assms unfolding sets_completion by auto
```
```    79
```
```    80 lemma sets_completionI_sets[intro, simp]:
```
```    81   "A \<in> sets M \<Longrightarrow> A \<in> sets (completion M)"
```
```    82   unfolding sets_completion by force
```
```    83
```
```    84 lemma null_sets_completion:
```
```    85   assumes "N' \<in> null_sets M" "N \<subseteq> N'" shows "N \<in> sets (completion M)"
```
```    86   using assms by (intro sets_completionI[of N "{}" N N']) auto
```
```    87
```
```    88 lemma split_completion:
```
```    89   assumes "A \<in> sets (completion M)"
```
```    90   shows "split_completion M A (main_part M A, null_part M A)"
```
```    91 proof cases
```
```    92   assume "A \<in> sets M" then show ?thesis
```
```    93     by (simp add: split_completion_def[abs_def] main_part_def null_part_def)
```
```    94 next
```
```    95   assume nA: "A \<notin> sets M"
```
```    96   show ?thesis
```
```    97     unfolding main_part_def null_part_def if_not_P[OF nA]
```
```    98   proof (rule someI2_ex)
```
```    99     from assms[THEN sets_completionE] guess S N N' . note A = this
```
```   100     let ?P = "(S, N - S)"
```
```   101     show "\<exists>p. split_completion M A p"
```
```   102       unfolding split_completion_def if_not_P[OF nA] using A
```
```   103     proof (intro exI conjI)
```
```   104       show "A = fst ?P \<union> snd ?P" using A by auto
```
```   105       show "snd ?P \<subseteq> N'" using A by auto
```
```   106    qed auto
```
```   107   qed auto
```
```   108 qed
```
```   109
```
```   110 lemma
```
```   111   assumes "S \<in> sets (completion M)"
```
```   112   shows main_part_sets[intro, simp]: "main_part M S \<in> sets M"
```
```   113     and main_part_null_part_Un[simp]: "main_part M S \<union> null_part M S = S"
```
```   114     and main_part_null_part_Int[simp]: "main_part M S \<inter> null_part M S = {}"
```
```   115   using split_completion[OF assms]
```
```   116   by (auto simp: split_completion_def split: split_if_asm)
```
```   117
```
```   118 lemma main_part[simp]: "S \<in> sets M \<Longrightarrow> main_part M S = S"
```
```   119   using split_completion[of S M]
```
```   120   by (auto simp: split_completion_def split: split_if_asm)
```
```   121
```
```   122 lemma null_part:
```
```   123   assumes "S \<in> sets (completion M)" shows "\<exists>N. N\<in>null_sets M \<and> null_part M S \<subseteq> N"
```
```   124   using split_completion[OF assms] by (auto simp: split_completion_def split: split_if_asm)
```
```   125
```
```   126 lemma null_part_sets[intro, simp]:
```
```   127   assumes "S \<in> sets M" shows "null_part M S \<in> sets M" "emeasure M (null_part M S) = 0"
```
```   128 proof -
```
```   129   have S: "S \<in> sets (completion M)" using assms by auto
```
```   130   have "S - main_part M S \<in> sets M" using assms by auto
```
```   131   moreover
```
```   132   from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
```
```   133   have "S - main_part M S = null_part M S" by auto
```
```   134   ultimately show sets: "null_part M S \<in> sets M" by auto
```
```   135   from null_part[OF S] guess N ..
```
```   136   with emeasure_eq_0[of N _ "null_part M S"] sets
```
```   137   show "emeasure M (null_part M S) = 0" by auto
```
```   138 qed
```
```   139
```
```   140 lemma emeasure_main_part_UN:
```
```   141   fixes S :: "nat \<Rightarrow> 'a set"
```
```   142   assumes "range S \<subseteq> sets (completion M)"
```
```   143   shows "emeasure M (main_part M (\<Union>i. (S i))) = emeasure M (\<Union>i. main_part M (S i))"
```
```   144 proof -
```
```   145   have S: "\<And>i. S i \<in> sets (completion M)" using assms by auto
```
```   146   then have UN: "(\<Union>i. S i) \<in> sets (completion M)" by auto
```
```   147   have "\<forall>i. \<exists>N. N \<in> null_sets M \<and> null_part M (S i) \<subseteq> N"
```
```   148     using null_part[OF S] by auto
```
```   149   from choice[OF this] guess N .. note N = this
```
```   150   then have UN_N: "(\<Union>i. N i) \<in> null_sets M" by (intro null_sets_UN) auto
```
```   151   have "(\<Union>i. S i) \<in> sets (completion M)" using S by auto
```
```   152   from null_part[OF this] guess N' .. note N' = this
```
```   153   let ?N = "(\<Union>i. N i) \<union> N'"
```
```   154   have null_set: "?N \<in> null_sets M" using N' UN_N by (intro null_sets.Un) auto
```
```   155   have "main_part M (\<Union>i. S i) \<union> ?N = (main_part M (\<Union>i. S i) \<union> null_part M (\<Union>i. S i)) \<union> ?N"
```
```   156     using N' by auto
```
```   157   also have "\<dots> = (\<Union>i. main_part M (S i) \<union> null_part M (S i)) \<union> ?N"
```
```   158     unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
```
```   159   also have "\<dots> = (\<Union>i. main_part M (S i)) \<union> ?N"
```
```   160     using N by auto
```
```   161   finally have *: "main_part M (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part M (S i)) \<union> ?N" .
```
```   162   have "emeasure M (main_part M (\<Union>i. S i)) = emeasure M (main_part M (\<Union>i. S i) \<union> ?N)"
```
```   163     using null_set UN by (intro emeasure_Un_null_set[symmetric]) auto
```
```   164   also have "\<dots> = emeasure M ((\<Union>i. main_part M (S i)) \<union> ?N)"
```
```   165     unfolding * ..
```
```   166   also have "\<dots> = emeasure M (\<Union>i. main_part M (S i))"
```
```   167     using null_set S by (intro emeasure_Un_null_set) auto
```
```   168   finally show ?thesis .
```
```   169 qed
```
```   170
```
```   171 lemma emeasure_completion[simp]:
```
```   172   assumes S: "S \<in> sets (completion M)" shows "emeasure (completion M) S = emeasure M (main_part M S)"
```
```   173 proof (subst emeasure_measure_of[OF completion_def completion_into_space])
```
```   174   let ?\<mu> = "emeasure M \<circ> main_part M"
```
```   175   show "S \<in> sets (completion M)" "?\<mu> S = emeasure M (main_part M S) " using S by simp_all
```
```   176   show "positive (sets (completion M)) ?\<mu>"
```
```   177     by (simp add: positive_def emeasure_nonneg)
```
```   178   show "countably_additive (sets (completion M)) ?\<mu>"
```
```   179   proof (intro countably_additiveI)
```
```   180     fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (completion M)" "disjoint_family A"
```
```   181     have "disjoint_family (\<lambda>i. main_part M (A i))"
```
```   182     proof (intro disjoint_family_on_bisimulation[OF A(2)])
```
```   183       fix n m assume "A n \<inter> A m = {}"
```
```   184       then have "(main_part M (A n) \<union> null_part M (A n)) \<inter> (main_part M (A m) \<union> null_part M (A m)) = {}"
```
```   185         using A by (subst (1 2) main_part_null_part_Un) auto
```
```   186       then show "main_part M (A n) \<inter> main_part M (A m) = {}" by auto
```
```   187     qed
```
```   188     then have "(\<Sum>n. emeasure M (main_part M (A n))) = emeasure M (\<Union>i. main_part M (A i))"
```
```   189       using A by (auto intro!: suminf_emeasure)
```
```   190     then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (UNION UNIV A)"
```
```   191       by (simp add: completion_def emeasure_main_part_UN[OF A(1)])
```
```   192   qed
```
```   193 qed
```
```   194
```
```   195 lemma emeasure_completion_UN:
```
```   196   "range S \<subseteq> sets (completion M) \<Longrightarrow>
```
```   197     emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))"
```
```   198   by (subst emeasure_completion) (auto simp add: emeasure_main_part_UN)
```
```   199
```
```   200 lemma emeasure_completion_Un:
```
```   201   assumes S: "S \<in> sets (completion M)" and T: "T \<in> sets (completion M)"
```
```   202   shows "emeasure (completion M) (S \<union> T) = emeasure M (main_part M S \<union> main_part M T)"
```
```   203 proof (subst emeasure_completion)
```
```   204   have UN: "(\<Union>i. binary (main_part M S) (main_part M T) i) = (\<Union>i. main_part M (binary S T i))"
```
```   205     unfolding binary_def by (auto split: split_if_asm)
```
```   206   show "emeasure M (main_part M (S \<union> T)) = emeasure M (main_part M S \<union> main_part M T)"
```
```   207     using emeasure_main_part_UN[of "binary S T" M] assms
```
```   208     unfolding range_binary_eq Un_range_binary UN by auto
```
```   209 qed (auto intro: S T)
```
```   210
```
```   211 lemma sets_completionI_sub:
```
```   212   assumes N: "N' \<in> null_sets M" "N \<subseteq> N'"
```
```   213   shows "N \<in> sets (completion M)"
```
```   214   using assms by (intro sets_completionI[of _ "{}" N N']) auto
```
```   215
```
```   216 lemma completion_ex_simple_function:
```
```   217   assumes f: "simple_function (completion M) f"
```
```   218   shows "\<exists>f'. simple_function M f' \<and> (AE x in M. f x = f' x)"
```
```   219 proof -
```
```   220   let ?F = "\<lambda>x. f -` {x} \<inter> space M"
```
```   221   have F: "\<And>x. ?F x \<in> sets (completion M)" and fin: "finite (f`space M)"
```
```   222     using simple_functionD[OF f] simple_functionD[OF f] by simp_all
```
```   223   have "\<forall>x. \<exists>N. N \<in> null_sets M \<and> null_part M (?F x) \<subseteq> N"
```
```   224     using F null_part by auto
```
```   225   from choice[OF this] obtain N where
```
```   226     N: "\<And>x. null_part M (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets M" by auto
```
```   227   let ?N = "\<Union>x\<in>f`space M. N x"
```
```   228   let ?f' = "\<lambda>x. if x \<in> ?N then undefined else f x"
```
```   229   have sets: "?N \<in> null_sets M" using N fin by (intro null_sets.finite_UN) auto
```
```   230   show ?thesis unfolding simple_function_def
```
```   231   proof (safe intro!: exI[of _ ?f'])
```
```   232     have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
```
```   233     from finite_subset[OF this] simple_functionD(1)[OF f]
```
```   234     show "finite (?f' ` space M)" by auto
```
```   235   next
```
```   236     fix x assume "x \<in> space M"
```
```   237     have "?f' -` {?f' x} \<inter> space M =
```
```   238       (if x \<in> ?N then ?F undefined \<union> ?N
```
```   239        else if f x = undefined then ?F (f x) \<union> ?N
```
```   240        else ?F (f x) - ?N)"
```
```   241       using N(2) sets.sets_into_space by (auto split: split_if_asm simp: null_sets_def)
```
```   242     moreover { fix y have "?F y \<union> ?N \<in> sets M"
```
```   243       proof cases
```
```   244         assume y: "y \<in> f`space M"
```
```   245         have "?F y \<union> ?N = (main_part M (?F y) \<union> null_part M (?F y)) \<union> ?N"
```
```   246           using main_part_null_part_Un[OF F] by auto
```
```   247         also have "\<dots> = main_part M (?F y) \<union> ?N"
```
```   248           using y N by auto
```
```   249         finally show ?thesis
```
```   250           using F sets by auto
```
```   251       next
```
```   252         assume "y \<notin> f`space M" then have "?F y = {}" by auto
```
```   253         then show ?thesis using sets by auto
```
```   254       qed }
```
```   255     moreover {
```
```   256       have "?F (f x) - ?N = main_part M (?F (f x)) \<union> null_part M (?F (f x)) - ?N"
```
```   257         using main_part_null_part_Un[OF F] by auto
```
```   258       also have "\<dots> = main_part M (?F (f x)) - ?N"
```
```   259         using N `x \<in> space M` by auto
```
```   260       finally have "?F (f x) - ?N \<in> sets M"
```
```   261         using F sets by auto }
```
```   262     ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
```
```   263   next
```
```   264     show "AE x in M. f x = ?f' x"
```
```   265       by (rule AE_I', rule sets) auto
```
```   266   qed
```
```   267 qed
```
```   268
```
```   269 lemma completion_ex_borel_measurable_pos:
```
```   270   fixes g :: "'a \<Rightarrow> ereal"
```
```   271   assumes g: "g \<in> borel_measurable (completion M)" and "\<And>x. 0 \<le> g x"
```
```   272   shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)"
```
```   273 proof -
```
```   274   from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this
```
```   275   from this(1)[THEN completion_ex_simple_function]
```
```   276   have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x in M. f i x = f' x)" ..
```
```   277   from this[THEN choice] obtain f' where
```
```   278     sf: "\<And>i. simple_function M (f' i)" and
```
```   279     AE: "\<forall>i. AE x in M. f i x = f' i x" by auto
```
```   280   show ?thesis
```
```   281   proof (intro bexI)
```
```   282     from AE[unfolded AE_all_countable[symmetric]]
```
```   283     show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x")
```
```   284     proof (elim AE_mp, safe intro!: AE_I2)
```
```   285       fix x assume eq: "\<forall>i. f i x = f' i x"
```
```   286       moreover have "g x = (SUP i. f i x)"
```
```   287         unfolding f using `0 \<le> g x` by (auto split: split_max)
```
```   288       ultimately show "g x = ?f x" by auto
```
```   289     qed
```
```   290     show "?f \<in> borel_measurable M"
```
```   291       using sf[THEN borel_measurable_simple_function] by auto
```
```   292   qed
```
```   293 qed
```
```   294
```
```   295 lemma completion_ex_borel_measurable:
```
```   296   fixes g :: "'a \<Rightarrow> ereal"
```
```   297   assumes g: "g \<in> borel_measurable (completion M)"
```
```   298   shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)"
```
```   299 proof -
```
```   300   have "(\<lambda>x. max 0 (g x)) \<in> borel_measurable (completion M)" "\<And>x. 0 \<le> max 0 (g x)" using g by auto
```
```   301   from completion_ex_borel_measurable_pos[OF this] guess g_pos ..
```
```   302   moreover
```
```   303   have "(\<lambda>x. max 0 (- g x)) \<in> borel_measurable (completion M)" "\<And>x. 0 \<le> max 0 (- g x)" using g by auto
```
```   304   from completion_ex_borel_measurable_pos[OF this] guess g_neg ..
```
```   305   ultimately
```
```   306   show ?thesis
```
```   307   proof (safe intro!: bexI[of _ "\<lambda>x. g_pos x - g_neg x"])
```
```   308     show "AE x in M. max 0 (- g x) = g_neg x \<longrightarrow> max 0 (g x) = g_pos x \<longrightarrow> g x = g_pos x - g_neg x"
```
```   309     proof (intro AE_I2 impI)
```
```   310       fix x assume g: "max 0 (- g x) = g_neg x" "max 0 (g x) = g_pos x"
```
```   311       show "g x = g_pos x - g_neg x" unfolding g[symmetric]
```
```   312         by (cases "g x") (auto split: split_max)
```
```   313     qed
```
```   314   qed auto
```
```   315 qed
```
```   316
```
```   317 lemma (in prob_space) prob_space_completion: "prob_space (completion M)"
```
```   318   by (rule prob_spaceI) (simp add: emeasure_space_1)
```
```   319
```
```   320 lemma null_sets_completionI: "N \<in> null_sets M \<Longrightarrow> N \<in> null_sets (completion M)"
```
```   321   by (auto simp: null_sets_def)
```
```   322
```
```   323 lemma AE_completion: "(AE x in M. P x) \<Longrightarrow> (AE x in completion M. P x)"
```
```   324   unfolding eventually_ae_filter by (auto intro: null_sets_completionI)
```
```   325
```
```   326 lemma null_sets_completion_iff: "N \<in> sets M \<Longrightarrow> N \<in> null_sets (completion M) \<longleftrightarrow> N \<in> null_sets M"
```
```   327   by (auto simp: null_sets_def)
```
```   328
```
```   329 lemma AE_completion_iff: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in completion M. P x)"
```
```   330   by (simp add: AE_iff_null null_sets_completion_iff)
```
```   331
```
```   332 end
```