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.21      proof (intro countably_additiveI)
    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