src/HOL/Probability/Complete_Measure.thy

-(*  Title:      HOL/Probability/Complete_Measure.thy
+(*  Title:      Complete_Measure.thy
     Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
 *)
-
 theory Complete_Measure
 imports Product_Measure
 begin
 
 locale completeable_measure_space = measure_space

 sublocale completeable_measure_space \<subseteq> completion!: measure_space completion
   where "measure completion = \<mu>'"
 proof -
   show "measure_space completion"
   proof
-    show "measure completion {} = 0" by (auto simp: completion_def)
+    show "positive completion (measure completion)"
+      by (auto simp: completion_def positive_def)
   next
     show "countably_additive completion (measure completion)"
     proof (intro countably_additiveI)
       fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
       have "disjoint_family (\<lambda>i. main_part (A i))"

         fix n m assume "A n \<inter> A m = {}"
         then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
           using A by (subst (1 2) main_part_null_part_Un) auto
         then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
       qed
-      then have "(\<Sum>\<^isub>\<infinity>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"
+      then have "(\<Sum>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"
         unfolding completion_def using A by (auto intro!: measure_countably_additive)
-      then show "(\<Sum>\<^isub>\<infinity>n. measure completion (A n)) = measure completion (UNION UNIV A)"
+      then show "(\<Sum>n. measure completion (A n)) = measure completion (UNION UNIV A)"
         by (simp add: completion_def \<mu>_main_part_UN[OF A(1)])
     qed
   qed
   show "measure completion = \<mu>'" unfolding completion_def by simp
 qed

     show "AE x. f x = ?f' x"
       by (rule AE_I', rule sets) auto
   qed
 qed
 
-lemma (in completeable_measure_space) completion_ex_borel_measurable:
-  fixes g :: "'a \<Rightarrow> pextreal"
-  assumes g: "g \<in> borel_measurable completion"
+lemma (in completeable_measure_space) completion_ex_borel_measurable_pos:
+  fixes g :: "'a \<Rightarrow> extreal"
+  assumes g: "g \<in> borel_measurable completion" and "\<And>x. 0 \<le> g x"
   shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
 proof -
-  from g[THEN completion.borel_measurable_implies_simple_function_sequence]
-  obtain f where "\<And>i. simple_function completion (f i)" "f \<up> g" by auto
-  then have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)"
-    using completion_ex_simple_function by auto
+  from g[THEN completion.borel_measurable_implies_simple_function_sequence'] guess f . note f = this
+  from this(1)[THEN completion_ex_simple_function]
+  have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)" ..
   from this[THEN choice] obtain f' where
     sf: "\<And>i. simple_function M (f' i)" and
     AE: "\<forall>i. AE x. f i x = f' i x" by auto
   show ?thesis
   proof (intro bexI)
-    from AE[unfolded all_AE_countable]
+    from AE[unfolded AE_all_countable[symmetric]]
     show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
     proof (elim AE_mp, safe intro!: AE_I2)
       fix x assume eq: "\<forall>i. f i x = f' i x"
-      moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
-      ultimately show "g x = ?f x" by (simp add: SUPR_apply)
+      moreover have "g x = (SUP i. f i x)"
+        unfolding f using `0 \<le> g x` by (auto split: split_max)
+      ultimately show "g x = ?f x" by auto
     qed
     show "?f \<in> borel_measurable M"
       using sf by (auto intro: borel_measurable_simple_function)
   qed
 qed
 
+lemma (in completeable_measure_space) completion_ex_borel_measurable:
+  fixes g :: "'a \<Rightarrow> extreal"
+  assumes g: "g \<in> borel_measurable completion"
+  shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
+proof -
+  have "(\<lambda>x. max 0 (g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (g x)" using g by auto
+  from completion_ex_borel_measurable_pos[OF this] guess g_pos ..
+  moreover
+  have "(\<lambda>x. max 0 (- g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (- g x)" using g by auto
+  from completion_ex_borel_measurable_pos[OF this] guess g_neg ..
+  ultimately
+  show ?thesis
+  proof (safe intro!: bexI[of _ "\<lambda>x. g_pos x - g_neg x"])
+    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"
+    proof (intro AE_I2 impI)
+      fix x assume g: "max 0 (- g x) = g_neg x" "max 0 (g x) = g_pos x"
+      show "g x = g_pos x - g_neg x" unfolding g[symmetric]
+        by (cases "g x") (auto split: split_max)
+    qed
+  qed auto
+qed
+
 end