src/HOL/Probability/Complete_Measure.thy
 changeset 41981 cdf7693bbe08 parent 41959 b460124855b8 child 41983 2dc6e382a58b
```     1.1 --- a/src/HOL/Probability/Complete_Measure.thy	Mon Mar 14 14:37:47 2011 +0100
1.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Mon Mar 14 14:37:49 2011 +0100
1.3 @@ -1,7 +1,6 @@
1.4 -(*  Title:      HOL/Probability/Complete_Measure.thy
1.5 +(*  Title:      Complete_Measure.thy
1.6      Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
1.7  *)
1.8 -
1.9  theory Complete_Measure
1.10  imports Product_Measure
1.11  begin
1.12 @@ -177,7 +176,8 @@
1.13  proof -
1.14    show "measure_space completion"
1.15    proof
1.16 -    show "measure completion {} = 0" by (auto simp: completion_def)
1.17 +    show "positive completion (measure completion)"
1.18 +      by (auto simp: completion_def positive_def)
1.19    next
1.20      show "countably_additive completion (measure completion)"
1.22 @@ -189,9 +189,9 @@
1.23            using A by (subst (1 2) main_part_null_part_Un) auto
1.24          then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
1.25        qed
1.26 -      then have "(\<Sum>\<^isub>\<infinity>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"
1.27 +      then have "(\<Sum>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"
1.28          unfolding completion_def using A by (auto intro!: measure_countably_additive)
1.29 -      then show "(\<Sum>\<^isub>\<infinity>n. measure completion (A n)) = measure completion (UNION UNIV A)"
1.30 +      then show "(\<Sum>n. measure completion (A n)) = measure completion (UNION UNIV A)"
1.31          by (simp add: completion_def \<mu>_main_part_UN[OF A(1)])
1.32      qed
1.33    qed
1.34 @@ -251,30 +251,52 @@
1.35    qed
1.36  qed
1.37
1.38 -lemma (in completeable_measure_space) completion_ex_borel_measurable:
1.39 -  fixes g :: "'a \<Rightarrow> pextreal"
1.40 -  assumes g: "g \<in> borel_measurable completion"
1.41 +lemma (in completeable_measure_space) completion_ex_borel_measurable_pos:
1.42 +  fixes g :: "'a \<Rightarrow> extreal"
1.43 +  assumes g: "g \<in> borel_measurable completion" and "\<And>x. 0 \<le> g x"
1.44    shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
1.45  proof -
1.46 -  from g[THEN completion.borel_measurable_implies_simple_function_sequence]
1.47 -  obtain f where "\<And>i. simple_function completion (f i)" "f \<up> g" by auto
1.48 -  then have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)"
1.49 -    using completion_ex_simple_function by auto
1.50 +  from g[THEN completion.borel_measurable_implies_simple_function_sequence'] guess f . note f = this
1.51 +  from this(1)[THEN completion_ex_simple_function]
1.52 +  have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)" ..
1.53    from this[THEN choice] obtain f' where
1.54      sf: "\<And>i. simple_function M (f' i)" and
1.55      AE: "\<forall>i. AE x. f i x = f' i x" by auto
1.56    show ?thesis
1.57    proof (intro bexI)
1.58 -    from AE[unfolded all_AE_countable]
1.59 +    from AE[unfolded AE_all_countable[symmetric]]
1.60      show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
1.61      proof (elim AE_mp, safe intro!: AE_I2)
1.62        fix x assume eq: "\<forall>i. f i x = f' i x"
1.63 -      moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
1.64 -      ultimately show "g x = ?f x" by (simp add: SUPR_apply)
1.65 +      moreover have "g x = (SUP i. f i x)"
1.66 +        unfolding f using `0 \<le> g x` by (auto split: split_max)
1.67 +      ultimately show "g x = ?f x" by auto
1.68      qed
1.69      show "?f \<in> borel_measurable M"
1.70        using sf by (auto intro: borel_measurable_simple_function)
1.71    qed
1.72  qed
1.73
1.74 +lemma (in completeable_measure_space) completion_ex_borel_measurable:
1.75 +  fixes g :: "'a \<Rightarrow> extreal"
1.76 +  assumes g: "g \<in> borel_measurable completion"
1.77 +  shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
1.78 +proof -
1.79 +  have "(\<lambda>x. max 0 (g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (g x)" using g by auto
1.80 +  from completion_ex_borel_measurable_pos[OF this] guess g_pos ..
1.81 +  moreover
1.82 +  have "(\<lambda>x. max 0 (- g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (- g x)" using g by auto
1.83 +  from completion_ex_borel_measurable_pos[OF this] guess g_neg ..
1.84 +  ultimately
1.85 +  show ?thesis
1.86 +  proof (safe intro!: bexI[of _ "\<lambda>x. g_pos x - g_neg x"])
1.87 +    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"
1.88 +    proof (intro AE_I2 impI)
1.89 +      fix x assume g: "max 0 (- g x) = g_neg x" "max 0 (g x) = g_pos x"
1.90 +      show "g x = g_pos x - g_neg x" unfolding g[symmetric]
1.91 +        by (cases "g x") (auto split: split_max)
1.92 +    qed
1.93 +  qed auto
1.94 +qed
1.95 +
1.96  end
```