1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:33 2012 +0200
     1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:34 2012 +0200
     1.3 @@ -388,53 +388,40 @@
     1.4  
     1.5  lemma simple_function_induct_nn[consumes 2, case_names cong set mult add]:
     1.6    fixes u :: "'a \<Rightarrow> ereal"
     1.7 -  assumes u: "simple_function M u" and nn: "AE x in M. 0 \<le> u x"
     1.8 -  assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
     1.9 +  assumes u: "simple_function M u" and nn: "\<And>x. 0 \<le> u x"
    1.10 +  assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
    1.11    assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
    1.12    assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
    1.13    assumes add: "\<And>u v. simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> simple_function M v \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
    1.14    shows "P u"
    1.15  proof -
    1.16 -  def v \<equiv> "max 0 \<circ> u"
    1.17 -  have v: "simple_function M v"
    1.18 -    unfolding v_def using u by (rule simple_function_compose)
    1.19 -  have v_nn: "\<And>x. 0 \<le> v x"
    1.20 -    unfolding v_def by (auto simp: max_def)
    1.21 -
    1.22    show ?thesis
    1.23    proof (rule cong)
    1.24 -    have "AE x in M. u x = v x"
    1.25 -      unfolding v_def using nn by eventually_elim (auto simp: max_def)
    1.26 -    with AE_space
    1.27 -    show "AE x in M. (\<Sum>y\<in>v ` space M. y * indicator (v -` {y} \<inter> space M) x) = u x"
    1.28 -    proof eventually_elim
    1.29 -      fix x assume x: "x \<in> space M" and "u x = v x"
    1.30 -      from simple_function_indicator_representation[OF v x]
    1.31 -      show "(\<Sum>y\<in>v ` space M. y * indicator (v -` {y} \<inter> space M) x) = u x"
    1.32 -        unfolding `u x = v x` ..
    1.33 -    qed
    1.34 +    fix x assume x: "x \<in> space M"
    1.35 +    from simple_function_indicator_representation[OF u x]
    1.36 +    show "(\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x) = u x" ..
    1.37    next
    1.38 -    show "simple_function M (\<lambda>x. (\<Sum>y\<in>v ` space M. y * indicator (v -` {y} \<inter> space M) x))"
    1.39 +    show "simple_function M (\<lambda>x. (\<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x))"
    1.40        apply (subst simple_function_cong)
    1.41        apply (rule simple_function_indicator_representation[symmetric])
    1.42 -      apply (auto intro: v)
    1.43 +      apply (auto intro: u)
    1.44        done
    1.45    next
    1.46 -    from v v_nn have "finite (v ` space M)" "\<And>x. x \<in> v ` space M \<Longrightarrow> 0 \<le> x"
    1.47 +    from u nn have "finite (u ` space M)" "\<And>x. x \<in> u ` space M \<Longrightarrow> 0 \<le> x"
    1.48        unfolding simple_function_def by auto
    1.49 -    then show "P (\<lambda>x. \<Sum>y\<in>v ` space M. y * indicator (v -` {y} \<inter> space M) x)"
    1.50 +    then show "P (\<lambda>x. \<Sum>y\<in>u ` space M. y * indicator (u -` {y} \<inter> space M) x)"
    1.51      proof induct
    1.52        case empty show ?case
    1.53          using set[of "{}"] by (simp add: indicator_def[abs_def])
    1.54 -    qed (auto intro!: add mult set simple_functionD v setsum_nonneg
    1.55 +    qed (auto intro!: add mult set simple_functionD u setsum_nonneg
    1.56         simple_function_setsum)
    1.57    qed fact
    1.58  qed
    1.59  
    1.60  lemma borel_measurable_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]:
    1.61    fixes u :: "'a \<Rightarrow> ereal"
    1.62 -  assumes u: "u \<in> borel_measurable M" "AE x in M. 0 \<le> u x"
    1.63 -  assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
    1.64 +  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
    1.65 +  assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f"
    1.66    assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
    1.67    assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
    1.68    assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
    1.69 @@ -444,26 +431,20 @@
    1.70  proof (induct rule: borel_measurable_implies_simple_function_sequence')
    1.71    fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
    1.72      sup: "\<And>x. (SUP i. U i x) = max 0 (u x)" and nn: "\<And>i x. 0 \<le> U i x"
    1.73 -  have u_eq: "max 0 \<circ> u = (SUP i. U i)" and "\<And>i. AE x in M. 0 \<le> U i x"
    1.74 +  have u_eq: "u = (SUP i. U i)"
    1.75      using nn u sup by (auto simp: max_def)
    1.76    
    1.77    from U have "\<And>i. U i \<in> borel_measurable M"
    1.78      by (simp add: borel_measurable_simple_function)
    1.79  
    1.80 -  have "max 0 \<circ> u \<in> borel_measurable M" "u \<in> borel_measurable M"
    1.81 -    by (auto intro!: measurable_comp u borel_measurable_ereal_max simp: id_def[symmetric])
    1.82 -  moreover have "AE x in M. (max 0 \<circ> u) x = u x"
    1.83 -    using u(2) by eventually_elim (auto simp: max_def)
    1.84 -  moreover have "P (max 0 \<circ> u)"
    1.85 +  show "P u"
    1.86      unfolding u_eq
    1.87    proof (rule seq)
    1.88      fix i show "P (U i)"
    1.89 -      using `simple_function M (U i)` `AE x in M. 0 \<le> U i x`
    1.90 +      using `simple_function M (U i)` nn
    1.91        by (induct rule: simple_function_induct_nn)
    1.92           (auto intro: set mult add cong dest!: borel_measurable_simple_function)
    1.93    qed fact+
    1.94 -  ultimately show "P u"
    1.95 -    by fact
    1.96  qed
    1.97  
    1.98  lemma simple_function_If_set:
    1.99 @@ -1427,23 +1408,21 @@
   1.100    by (auto intro!: positive_integral_0_iff_AE[THEN iffD2])
   1.101  
   1.102  lemma positive_integral_subalgebra:
   1.103 -  assumes f: "f \<in> borel_measurable N" "AE x in N. 0 \<le> f x"
   1.104 +  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
   1.105    and N: "sets N \<subseteq> sets M" "space N = space M" "\<And>A. A \<in> sets N \<Longrightarrow> emeasure N A = emeasure M A"
   1.106    shows "integral\<^isup>P N f = integral\<^isup>P M f"
   1.107  proof -
   1.108 -  from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess fs . note fs = this
   1.109 -  note sf = simple_function_subalgebra[OF fs(1) N(1,2)]
   1.110 -  from positive_integral_monotone_convergence_simple[OF fs(2,5,1), symmetric]
   1.111 -  have "integral\<^isup>P N f = (SUP i. \<Sum>x\<in>fs i ` space M. x * emeasure N (fs i -` {x} \<inter> space M))"
   1.112 -    unfolding fs(4) positive_integral_max_0
   1.113 -    unfolding simple_integral_def `space N = space M` by simp
   1.114 -  also have "\<dots> = (SUP i. \<Sum>x\<in>fs i ` space M. x * (emeasure M) (fs i -` {x} \<inter> space M))"
   1.115 -    using N simple_functionD(2)[OF fs(1)] unfolding `space N = space M` by auto
   1.116 -  also have "\<dots> = integral\<^isup>P M f"
   1.117 -    using positive_integral_monotone_convergence_simple[OF fs(2,5) sf, symmetric]
   1.118 -    unfolding fs(4) positive_integral_max_0
   1.119 -    unfolding simple_integral_def `space N = space M` by simp
   1.120 -  finally show ?thesis .
   1.121 +  have [simp]: "\<And>f :: 'a \<Rightarrow> ereal. f \<in> borel_measurable N \<Longrightarrow> f \<in> borel_measurable M"
   1.122 +    using N by (auto simp: measurable_def)
   1.123 +  have [simp]: "\<And>P. (AE x in N. P x) \<Longrightarrow> (AE x in M. P x)"
   1.124 +    using N by (auto simp add: eventually_ae_filter null_sets_def)
   1.125 +  have [simp]: "\<And>A. A \<in> sets N \<Longrightarrow> A \<in> sets M"
   1.126 +    using N by auto
   1.127 +  from f show ?thesis
   1.128 +    apply induct
   1.129 +    apply (simp_all add: positive_integral_add positive_integral_cmult positive_integral_monotone_convergence_SUP N)
   1.130 +    apply (auto intro!: positive_integral_cong cong: positive_integral_cong simp: N(2)[symmetric])
   1.131 +    done
   1.132  qed
   1.133  
   1.134  section "Lebesgue Integral"
   1.135 @@ -2310,17 +2289,17 @@
   1.136  
   1.137  lemma positive_integral_distr':
   1.138    assumes T: "T \<in> measurable M M'"
   1.139 -  and f: "f \<in> borel_measurable (distr M M' T)" "AE x in (distr M M' T). 0 \<le> f x"
   1.140 +  and f: "f \<in> borel_measurable (distr M M' T)" "\<And>x. 0 \<le> f x"
   1.141    shows "integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
   1.142    using f 
   1.143  proof induct
   1.144    case (cong f g)
   1.145 -  then have eq: "AE x in (distr M M' T). g x = f x" "AE x in M. g (T x) = f (T x)"
   1.146 -    by (auto dest: AE_distrD[OF T])
   1.147 -  show ?case
   1.148 -    apply (subst eq(1)[THEN positive_integral_cong_AE])
   1.149 -    apply (subst eq(2)[THEN positive_integral_cong_AE])
   1.150 -    apply fact
   1.151 +  with T show ?case
   1.152 +    apply (subst positive_integral_cong[of _ f g])
   1.153 +    apply simp
   1.154 +    apply (subst positive_integral_cong[of _ "\<lambda>x. f (T x)" "\<lambda>x. g (T x)"])
   1.155 +    apply (simp add: measurable_def Pi_iff)
   1.156 +    apply simp
   1.157      done
   1.158  next
   1.159    case (set A)
   1.160 @@ -2529,16 +2508,13 @@
   1.161  
   1.162  lemma positive_integral_density':
   1.163    assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   1.164 -  assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
   1.165 +  assumes g: "g \<in> borel_measurable M" "\<And>x. 0 \<le> g x"
   1.166    shows "integral\<^isup>P (density M f) g = (\<integral>\<^isup>+ x. f x * g x \<partial>M)"
   1.167  using g proof induct
   1.168    case (cong u v)
   1.169 -  then have eq: "AE x in density M f. v x = u x" "AE x in M. f x * v x = f x * u x"
   1.170 -    by (auto simp: AE_density f)
   1.171 -  show ?case
   1.172 -    apply (subst positive_integral_cong_AE[OF eq(1)])
   1.173 -    apply (subst positive_integral_cong_AE[OF eq(2)])
   1.174 -    apply fact
   1.175 +  then show ?case
   1.176 +    apply (subst positive_integral_cong[OF cong(3)])
   1.177 +    apply (simp_all cong: positive_integral_cong)
   1.178      done
   1.179  next
   1.180    case (set A) then show ?case