Add Lebesgue integral and probability space.
authorhoelzl
Thu Mar 04 21:52:26 2010 +0100 (2010-03-04)
changeset 35582b16d99a72dc9
parent 35581 a25e51e2d64d
child 35583 c7ddb7105dde
Add Lebesgue integral and probability space.
src/HOL/IsaMakefile
src/HOL/Probability/Borel.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Lebesgue.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Probability.thy
src/HOL/Probability/Probability_Space.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Mar 04 19:50:45 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Mar 04 21:52:26 2010 +0100
     1.3 @@ -1086,13 +1086,15 @@
     1.4  
     1.5  HOL-Probability: HOL $(LOG)/HOL-Probability.gz
     1.6  
     1.7 -$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML \
     1.8 -  Probability/Probability.thy \
     1.9 -  Probability/Sigma_Algebra.thy \
    1.10 -  Probability/SeriesPlus.thy \
    1.11 -  Probability/Caratheodory.thy \
    1.12 -  Probability/Measure.thy \
    1.13 -  Probability/Borel.thy
    1.14 +$(LOG)/HOL-Probability.gz: $(OUT)/HOL Probability/ROOT.ML	\
    1.15 +  Probability/Probability.thy					\
    1.16 +  Probability/Sigma_Algebra.thy					\
    1.17 +  Probability/SeriesPlus.thy					\
    1.18 +  Probability/Caratheodory.thy					\
    1.19 +  Probability/Borel.thy						\
    1.20 +  Probability/Measure.thy					\
    1.21 +  Probability/Lebesgue.thy					\
    1.22 +  Probability/Probability_Space.thy
    1.23  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
    1.24  
    1.25  
     2.1 --- a/src/HOL/Probability/Borel.thy	Thu Mar 04 19:50:45 2010 +0100
     2.2 +++ b/src/HOL/Probability/Borel.thy	Thu Mar 04 21:52:26 2010 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4  
     2.5  definition mono_convergent where
     2.6    "mono_convergent u f s \<equiv>
     2.7 -        (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
     2.8 +        (\<forall>x\<in>s. incseq (\<lambda>n. u n x)) \<and>
     2.9          (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
    2.10  
    2.11  lemma in_borel_measurable:
    2.12 @@ -355,7 +355,7 @@
    2.13                      borel_measurable_add_borel_measurable f g) 
    2.14    have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) = 
    2.15          (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
    2.16 -    by (simp add: minus_divide_right) 
    2.17 +    by (simp add: minus_divide_right)
    2.18    also have "... \<in> borel_measurable M" 
    2.19      by (fast intro: affine_borel_measurable borel_measurable_square 
    2.20                      borel_measurable_add_borel_measurable 
    2.21 @@ -388,7 +388,7 @@
    2.22          assume w: "w \<in> space M" and f: "f w \<le> a"
    2.23          hence "u i w \<le> f w"
    2.24            by (auto intro: SEQ.incseq_le
    2.25 -                   simp add: incseq_def mc [unfolded mono_convergent_def])
    2.26 +                   simp add: mc [unfolded mono_convergent_def])
    2.27          thus "u i w \<le> a" using f
    2.28            by auto
    2.29        next
    2.30 @@ -422,4 +422,143 @@
    2.31      by (auto simp add: borel_measurable_add_borel_measurable) 
    2.32  qed
    2.33  
    2.34 +section "Monotone convergence"
    2.35 +
    2.36 +lemma mono_convergentD:
    2.37 +  assumes "mono_convergent u f s" and "x \<in> s"
    2.38 +  shows "incseq (\<lambda>n. u n x)" and "(\<lambda>i. u i x) ----> f x"
    2.39 +  using assms unfolding mono_convergent_def by auto
    2.40 +
    2.41 +
    2.42 +lemma mono_convergentI:
    2.43 +  assumes "\<And>x. x \<in> s \<Longrightarrow> incseq (\<lambda>n. u n x)"
    2.44 +  assumes "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>i. u i x) ----> f x"
    2.45 +  shows "mono_convergent u f s"
    2.46 +  using assms unfolding mono_convergent_def by auto
    2.47 +
    2.48 +lemma mono_convergent_le:
    2.49 +  assumes "mono_convergent u f s" and "t \<in> s"
    2.50 +  shows "u n t \<le> f t"
    2.51 +using mono_convergentD[OF assms] by (auto intro!: incseq_le)
    2.52 +
    2.53 +definition "upclose f g x = max (f x) (g x)"
    2.54 +
    2.55 +primrec mon_upclose where
    2.56 +"mon_upclose 0 u = u 0" |
    2.57 +"mon_upclose (Suc n) u = upclose (u (Suc n)) (mon_upclose n u)"
    2.58 +
    2.59 +lemma mon_upclose_ex:
    2.60 +  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
    2.61 +  shows "\<exists>n \<le> m. mon_upclose m u x = u n x"
    2.62 +proof (induct m)
    2.63 +  case (Suc m)
    2.64 +  then obtain n where "n \<le> m" and *: "mon_upclose m u x = u n x" by blast
    2.65 +  thus ?case
    2.66 +  proof (cases "u n x \<le> u (Suc m) x")
    2.67 +    case True with min_max.sup_absorb1 show ?thesis
    2.68 +      by (auto simp: * upclose_def intro!: exI[of _ "Suc m"])
    2.69 +  next
    2.70 +    case False
    2.71 +     with min_max.sup_absorb2 `n \<le> m` show ?thesis
    2.72 +       by (auto simp: * upclose_def intro!: exI[of _ n] min_max.sup_absorb2)
    2.73 +  qed
    2.74 +qed simp
    2.75 +
    2.76 +lemma mon_upclose_all:
    2.77 +  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ('b\<Colon>linorder)"
    2.78 +  assumes "m \<le> n"
    2.79 +  shows "u m x \<le> mon_upclose n u x"
    2.80 +using assms proof (induct n)
    2.81 +  case 0 thus ?case by auto
    2.82 +next
    2.83 +  case (Suc n)
    2.84 +  show ?case
    2.85 +  proof (cases "m = Suc n")
    2.86 +    case True thus ?thesis by (simp add: upclose_def)
    2.87 +  next
    2.88 +    case False
    2.89 +    hence "m \<le> n" using `m \<le> Suc n` by simp
    2.90 +    from Suc.hyps[OF this]
    2.91 +    show ?thesis by (auto simp: upclose_def intro!: min_max.le_supI2)
    2.92 +  qed
    2.93 +qed
    2.94 +
    2.95 +lemma mono_convergent_limit:
    2.96 +  fixes f :: "'a \<Rightarrow> real"
    2.97 +  assumes "mono_convergent u f s" and "x \<in> s" and "0 < r"
    2.98 +  shows "\<exists>N. \<forall>n\<ge>N. f x - u n x < r"
    2.99 +proof -
   2.100 +  from LIMSEQ_D[OF mono_convergentD(2)[OF assms(1,2)] `0 < r`]
   2.101 +  obtain N where "\<And>n. N \<le> n \<Longrightarrow> \<bar> u n x - f x \<bar> < r" by auto
   2.102 +  with mono_convergent_le[OF assms(1,2)] `0 < r`
   2.103 +  show ?thesis by (auto intro!: exI[of _ N])
   2.104 +qed
   2.105 +
   2.106 +lemma mon_upclose_le_mono_convergent:
   2.107 +  assumes mc: "\<And>n. mono_convergent (\<lambda>m. u m n) (f n) s" and "x \<in> s"
   2.108 +  and "incseq (\<lambda>n. f n x)"
   2.109 +  shows "mon_upclose n (u n) x <= f n x"
   2.110 +proof -
   2.111 +  obtain m where *: "mon_upclose n (u n) x = u n m x" and "m \<le> n"
   2.112 +    using mon_upclose_ex[of n "u n" x] by auto
   2.113 +  note this(1)
   2.114 +  also have "u n m x \<le> f m x" using mono_convergent_le[OF assms(1,2)] .
   2.115 +  also have "... \<le> f n x" using assms(3) `m \<le> n` unfolding incseq_def by auto
   2.116 +  finally show ?thesis .
   2.117 +qed
   2.118 +
   2.119 +lemma mon_upclose_mono_convergent:
   2.120 +  assumes mc_u: "\<And>n. mono_convergent (\<lambda>m. u m n) (f n) s"
   2.121 +  and mc_f: "mono_convergent f h s"
   2.122 +  shows "mono_convergent (\<lambda>n. mon_upclose n (u n)) h s"
   2.123 +proof (rule mono_convergentI)
   2.124 +  fix x assume "x \<in> s"
   2.125 +  show "incseq (\<lambda>n. mon_upclose n (u n) x)" unfolding incseq_def
   2.126 +  proof safe
   2.127 +    fix m n :: nat assume "m \<le> n"
   2.128 +    obtain i where mon: "mon_upclose m (u m) x = u m i x" and "i \<le> m"
   2.129 +      using mon_upclose_ex[of m "u m" x] by auto
   2.130 +    hence "i \<le> n" using `m \<le> n` by auto
   2.131 +
   2.132 +    note mon
   2.133 +    also have "u m i x \<le> u n i x"
   2.134 +      using mono_convergentD(1)[OF mc_u `x \<in> s`] `m \<le> n`
   2.135 +      unfolding incseq_def by auto
   2.136 +    also have "u n i x \<le> mon_upclose n (u n) x"
   2.137 +      using mon_upclose_all[OF `i \<le> n`, of "u n" x] .
   2.138 +    finally show "mon_upclose m (u m) x \<le> mon_upclose n (u n) x" .
   2.139 +  qed
   2.140 +
   2.141 +  show "(\<lambda>i. mon_upclose i (u i) x) ----> h x"
   2.142 +  proof (rule LIMSEQ_I)
   2.143 +    fix r :: real assume "0 < r"
   2.144 +    hence "0 < r / 2" by auto
   2.145 +    from mono_convergent_limit[OF mc_f `x \<in> s` this]
   2.146 +    obtain N where f_h: "\<And>n. N \<le> n \<Longrightarrow> h x - f n x < r / 2" by auto
   2.147 +
   2.148 +    from mono_convergent_limit[OF mc_u `x \<in> s` `0 < r / 2`]
   2.149 +    obtain N' where u_f: "\<And>n. N' \<le> n \<Longrightarrow> f N x - u n N x < r / 2" by auto
   2.150 +
   2.151 +    show "\<exists>N. \<forall>n\<ge>N. norm (mon_upclose n (u n) x - h x) < r"
   2.152 +    proof (rule exI[of _ "max N N'"], safe)
   2.153 +      fix n assume "max N N' \<le> n"
   2.154 +      hence "N \<le> n" and "N' \<le> n" by auto
   2.155 +      hence "u n N x \<le> mon_upclose n (u n) x"
   2.156 +        using mon_upclose_all[of N n "u n" x] by auto
   2.157 +      moreover
   2.158 +      from add_strict_mono[OF u_f[OF `N' \<le> n`] f_h[OF order_refl]]
   2.159 +      have "h x - u n N x < r" by auto
   2.160 +      ultimately have "h x - mon_upclose n (u n) x < r" by auto
   2.161 +      moreover
   2.162 +      obtain i where "mon_upclose n (u n) x = u n i x"
   2.163 +        using mon_upclose_ex[of n "u n"] by blast
   2.164 +      with mono_convergent_le[OF mc_u `x \<in> s`, of n i]
   2.165 +           mono_convergent_le[OF mc_f `x \<in> s`, of i]
   2.166 +      have "mon_upclose n (u n) x \<le> h x" by auto
   2.167 +      ultimately
   2.168 +      show "norm (mon_upclose n (u n) x - h x) < r" by auto
   2.169 +     qed
   2.170 +  qed
   2.171 +qed
   2.172 +
   2.173  end
     3.1 --- a/src/HOL/Probability/Caratheodory.thy	Thu Mar 04 19:50:45 2010 +0100
     3.2 +++ b/src/HOL/Probability/Caratheodory.thy	Thu Mar 04 21:52:26 2010 +0100
     3.3 @@ -15,8 +15,11 @@
     3.4    measure:: "'a set \<Rightarrow> real"
     3.5  
     3.6  definition
     3.7 -  disjoint_family  where
     3.8 -  "disjoint_family A \<longleftrightarrow> (\<forall>m n. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
     3.9 +  disjoint_family_on  where
    3.10 +  "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
    3.11 +
    3.12 +abbreviation
    3.13 +  "disjoint_family A \<equiv> disjoint_family_on A UNIV"
    3.14  
    3.15  definition
    3.16    positive  where
    3.17 @@ -99,9 +102,9 @@
    3.18    by (auto simp add: additive_def)
    3.19  
    3.20  lemma countably_additiveD:
    3.21 -  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A 
    3.22 +  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
    3.23     \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n))  sums  f (\<Union>i. A i)"
    3.24 -  by (simp add: countably_additive_def) 
    3.25 +  by (simp add: countably_additive_def)
    3.26  
    3.27  lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
    3.28    by blast
    3.29 @@ -111,7 +114,7 @@
    3.30  
    3.31  lemma disjoint_family_subset:
    3.32       "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
    3.33 -  by (force simp add: disjoint_family_def) 
    3.34 +  by (force simp add: disjoint_family_on_def)
    3.35  
    3.36  subsection {* A Two-Element Series *}
    3.37  
    3.38 @@ -119,28 +122,28 @@
    3.39    where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
    3.40  
    3.41  lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
    3.42 -  apply (simp add: binaryset_def) 
    3.43 -  apply (rule set_ext) 
    3.44 -  apply (auto simp add: image_iff) 
    3.45 +  apply (simp add: binaryset_def)
    3.46 +  apply (rule set_ext)
    3.47 +  apply (auto simp add: image_iff)
    3.48    done
    3.49  
    3.50  lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
    3.51 -  by (simp add: UNION_eq_Union_image range_binaryset_eq) 
    3.52 +  by (simp add: UNION_eq_Union_image range_binaryset_eq)
    3.53  
    3.54 -lemma LIMSEQ_binaryset: 
    3.55 +lemma LIMSEQ_binaryset:
    3.56    assumes f: "f {} = 0"
    3.57    shows  "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
    3.58  proof -
    3.59    have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
    3.60 -    proof 
    3.61 +    proof
    3.62        fix n
    3.63        show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
    3.64 -        by (induct n)  (auto simp add: binaryset_def f) 
    3.65 +        by (induct n)  (auto simp add: binaryset_def f)
    3.66      qed
    3.67    moreover
    3.68 -  have "... ----> f A + f B" by (rule LIMSEQ_const) 
    3.69 +  have "... ----> f A + f B" by (rule LIMSEQ_const)
    3.70    ultimately
    3.71 -  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" 
    3.72 +  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
    3.73      by metis
    3.74    hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
    3.75      by simp
    3.76 @@ -285,23 +288,23 @@
    3.77  lemma (in algebra) countably_subadditive_subadditive:
    3.78    assumes f: "positive M f" and cs: "countably_subadditive M f"
    3.79    shows  "subadditive M f"
    3.80 -proof (auto simp add: subadditive_def) 
    3.81 +proof (auto simp add: subadditive_def)
    3.82    fix x y
    3.83    assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
    3.84    hence "disjoint_family (binaryset x y)"
    3.85 -    by (auto simp add: disjoint_family_def binaryset_def) 
    3.86 -  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 
    3.87 -         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> 
    3.88 +    by (auto simp add: disjoint_family_on_def binaryset_def)
    3.89 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
    3.90 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
    3.91           summable (f o (binaryset x y)) \<longrightarrow>
    3.92           f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))"
    3.93 -    using cs by (simp add: countably_subadditive_def) 
    3.94 -  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 
    3.95 +    using cs by (simp add: countably_subadditive_def)
    3.96 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
    3.97           summable (f o (binaryset x y)) \<longrightarrow>
    3.98           f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))"
    3.99      by (simp add: range_binaryset_eq UN_binaryset_eq)
   3.100    thus "f (x \<union> y) \<le>  f x + f y" using f x y binaryset_sums
   3.101 -    by (auto simp add: Un sums_iff positive_def o_def) 
   3.102 -qed 
   3.103 +    by (auto simp add: Un sums_iff positive_def o_def)
   3.104 +qed
   3.105  
   3.106  
   3.107  definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
   3.108 @@ -312,19 +315,19 @@
   3.109    case 0 show ?case by simp
   3.110  next
   3.111    case (Suc n)
   3.112 -  thus ?case by (simp add: atLeastLessThanSuc disjointed_def) 
   3.113 +  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
   3.114  qed
   3.115  
   3.116  lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
   3.117 -  apply (rule UN_finite2_eq [where k=0]) 
   3.118 -  apply (simp add: finite_UN_disjointed_eq) 
   3.119 +  apply (rule UN_finite2_eq [where k=0])
   3.120 +  apply (simp add: finite_UN_disjointed_eq)
   3.121    done
   3.122  
   3.123  lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
   3.124    by (auto simp add: disjointed_def)
   3.125  
   3.126  lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
   3.127 -  by (simp add: disjoint_family_def) 
   3.128 +  by (simp add: disjoint_family_on_def)
   3.129       (metis neq_iff Int_commute less_disjoint_disjointed)
   3.130  
   3.131  lemma disjointed_subset: "disjointed A n \<subseteq> A n"
   3.132 @@ -383,7 +386,7 @@
   3.133  next
   3.134    case (Suc n) 
   3.135    have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj 
   3.136 -    by (auto simp add: disjoint_family_def neq_iff) blast
   3.137 +    by (auto simp add: disjoint_family_on_def neq_iff) blast
   3.138    moreover 
   3.139    have "A n \<in> sets M" using A by blast 
   3.140    moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   3.141 @@ -440,7 +443,7 @@
   3.142  next
   3.143    case (Suc n) 
   3.144    have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
   3.145 -    by (force simp add: disjoint_family_def neq_iff) 
   3.146 +    by (force simp add: disjoint_family_on_def neq_iff) 
   3.147    have 3: "A n \<in> lambda_system M f" using A
   3.148      by blast
   3.149    have 4: "UNION {0..<n} A \<in> lambda_system M f"
   3.150 @@ -505,7 +508,7 @@
   3.151            by blast
   3.152          moreover 
   3.153          have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   3.154 -          by (auto simp add: disjoint_family_def) 
   3.155 +          by (auto simp add: disjoint_family_on_def) 
   3.156          moreover 
   3.157          have "a \<inter> (\<Union>i. A i) \<in> sets M"
   3.158            by (metis Int U_in a)
   3.159 @@ -584,7 +587,7 @@
   3.160    finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" .
   3.161    thus ?thesis using a
   3.162      by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"] 
   3.163 -             simp add: measure_set_def disjoint_family_def b split_if_mem2) 
   3.164 +             simp add: measure_set_def disjoint_family_on_def b split_if_mem2) 
   3.165  qed  
   3.166  
   3.167  lemma (in algebra) inf_measure_pos0:
   3.168 @@ -622,7 +625,7 @@
   3.169    fix x y
   3.170    assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   3.171    hence "disjoint_family (binaryset x y)"
   3.172 -    by (auto simp add: disjoint_family_def binaryset_def) 
   3.173 +    by (auto simp add: disjoint_family_on_def binaryset_def) 
   3.174    hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 
   3.175           (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> 
   3.176           f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
   3.177 @@ -655,7 +658,7 @@
   3.178        show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
   3.179          by blast
   3.180        show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
   3.181 -        by (auto simp add: disjoint_family_def)
   3.182 +        by (auto simp add: disjoint_family_on_def)
   3.183        show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
   3.184          by (metis UN_extend_simps(4) s seq)
   3.185      qed
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Probability/Lebesgue.thy	Thu Mar 04 21:52:26 2010 +0100
     4.3 @@ -0,0 +1,1790 @@
     4.4 +header {*Lebesgue Integration*}
     4.5 +
     4.6 +theory Lebesgue
     4.7 +imports Measure Borel
     4.8 +begin
     4.9 +
    4.10 +text{*From the HOL4 Hurd/Coble Lebesgue integration, translated by Armin Heller and Johannes Hoelzl.*}
    4.11 +
    4.12 +definition
    4.13 +  "pos_part f = (\<lambda>x. max 0 (f x))"
    4.14 +
    4.15 +definition
    4.16 +  "neg_part f = (\<lambda>x. - min 0 (f x))"
    4.17 +
    4.18 +definition
    4.19 +  "nonneg f = (\<forall>x. 0 \<le> f x)"
    4.20 +
    4.21 +lemma nonneg_pos_part[intro!]:
    4.22 +  fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,zero}"
    4.23 +  shows "nonneg (pos_part f)"
    4.24 +  unfolding nonneg_def pos_part_def by auto
    4.25 +
    4.26 +lemma nonneg_neg_part[intro!]:
    4.27 +  fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,ordered_ab_group_add}"
    4.28 +  shows "nonneg (neg_part f)"
    4.29 +  unfolding nonneg_def neg_part_def min_def by auto
    4.30 +
    4.31 +context measure_space
    4.32 +begin
    4.33 +
    4.34 +definition
    4.35 + "pos_simple f =
    4.36 +  { (s :: nat set, a, x).
    4.37 +    finite s \<and> nonneg f \<and> nonneg x \<and> a ` s \<subseteq> sets M \<and>
    4.38 +    (\<forall>t \<in> space M. (\<exists>!i\<in>s. t\<in>a i) \<and> (\<forall>i\<in>s. t \<in> a i \<longrightarrow> f t = x i)) }"
    4.39 +
    4.40 +definition
    4.41 +  "pos_simple_integral \<equiv> \<lambda>(s, a, x). \<Sum> i \<in> s. x i * measure M (a i)"
    4.42 +
    4.43 +definition
    4.44 +  "psfis f = pos_simple_integral ` (pos_simple f)"
    4.45 +
    4.46 +definition
    4.47 +  "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
    4.48 +                        (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
    4.49 +
    4.50 +definition
    4.51 +  "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
    4.52 +
    4.53 +definition
    4.54 +  "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
    4.55 +
    4.56 +definition
    4.57 +  "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
    4.58 +
    4.59 +definition
    4.60 +  "countable_space_integral f \<equiv>
    4.61 +    let e = enumerate (f ` space M) in
    4.62 +      suminf (\<lambda>r. e r * measure M (f -` {e r} \<inter> space M))"
    4.63 +
    4.64 +definition
    4.65 +  "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
    4.66 +    f \<in> borel_measurable M \<and>
    4.67 +    (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
    4.68 +
    4.69 +lemma pos_simpleE[consumes 1]:
    4.70 +  assumes ps: "(s, a, x) \<in> pos_simple f"
    4.71 +  obtains "finite s" and "nonneg f" and "nonneg x"
    4.72 +    and "a ` s \<subseteq> sets M" and "(\<Union>i\<in>s. a i) = space M"
    4.73 +    and "disjoint_family_on a s"
    4.74 +    and "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
    4.75 +    and "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
    4.76 +proof
    4.77 +  show "finite s" and "nonneg f" and "nonneg x"
    4.78 +    and as_in_M: "a ` s \<subseteq> sets M"
    4.79 +    and *: "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
    4.80 +    and **: "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
    4.81 +    using ps unfolding pos_simple_def by auto
    4.82 +
    4.83 +  thus t: "(\<Union>i\<in>s. a i) = space M"
    4.84 +  proof safe
    4.85 +    fix x assume "x \<in> space M"
    4.86 +    from *[OF this] show "x \<in> (\<Union>i\<in>s. a i)" by auto
    4.87 +  next
    4.88 +    fix t i assume "i \<in> s"
    4.89 +    hence "a i \<in> sets M" using as_in_M by auto
    4.90 +    moreover assume "t \<in> a i"
    4.91 +    ultimately show "t \<in> space M" using sets_into_space by blast
    4.92 +  qed
    4.93 +
    4.94 +  show "disjoint_family_on a s" unfolding disjoint_family_on_def
    4.95 +  proof safe
    4.96 +    fix i j and t assume "i \<in> s" "t \<in> a i" and "j \<in> s" "t \<in> a j" and "i \<noteq> j"
    4.97 +    with t * show "t \<in> {}" by auto
    4.98 +  qed
    4.99 +qed
   4.100 +
   4.101 +lemma pos_simple_cong:
   4.102 +  assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
   4.103 +  shows "pos_simple f = pos_simple g"
   4.104 +  unfolding pos_simple_def using assms by auto
   4.105 +
   4.106 +lemma psfis_cong:
   4.107 +  assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
   4.108 +  shows "psfis f = psfis g"
   4.109 +  unfolding psfis_def using pos_simple_cong[OF assms] by simp
   4.110 +
   4.111 +lemma pos_simple_setsum_indicator_fn:
   4.112 +  assumes ps: "(s, a, x) \<in> pos_simple f"
   4.113 +  and "t \<in> space M"
   4.114 +  shows "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) = f t"
   4.115 +proof -
   4.116 +  from assms obtain i where *: "i \<in> s" "t \<in> a i"
   4.117 +    and "finite s" and xi: "x i = f t" by (auto elim!: pos_simpleE)
   4.118 +
   4.119 +  have **: "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) =
   4.120 +    (\<Sum>j\<in>s. if j \<in> {i} then x i else 0)"
   4.121 +    unfolding indicator_fn_def using assms *
   4.122 +    by (auto intro!: setsum_cong elim!: pos_simpleE)
   4.123 +  show ?thesis unfolding ** setsum_cases[OF `finite s`] xi
   4.124 +    using `i \<in> s` by simp
   4.125 +qed
   4.126 +
   4.127 +lemma (in measure_space) measure_setsum_split:
   4.128 +  assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
   4.129 +  assumes "(\<Union>i \<in> r. b i) = space M"
   4.130 +  assumes "disjoint_family_on b r"
   4.131 +  shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
   4.132 +proof -
   4.133 +  have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
   4.134 +    using assms by auto
   4.135 +  show ?thesis unfolding *
   4.136 +  proof (rule measure_finitely_additive''[symmetric])
   4.137 +    show "finite r" using `finite r` by auto
   4.138 +    { fix i assume "i \<in> r"
   4.139 +      hence "b i \<in> sets M" using br_in_M by auto
   4.140 +      thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
   4.141 +    }
   4.142 +    show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
   4.143 +      using `disjoint_family_on b r`
   4.144 +      unfolding disjoint_family_on_def by auto
   4.145 +  qed
   4.146 +qed
   4.147 +
   4.148 +lemma (in measure_space) pos_simple_common_partition:
   4.149 +  assumes psf: "(s, a, x) \<in> pos_simple f"
   4.150 +  assumes psg: "(s', b, y) \<in> pos_simple g"
   4.151 +  obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"
   4.152 +proof -
   4.153 +  (* definitions *)
   4.154 +
   4.155 +  def k == "{0 ..< card (s \<times> s')}"
   4.156 +  have fs: "finite s" "finite s'" "finite k" unfolding k_def
   4.157 +    using psf psg unfolding pos_simple_def by auto
   4.158 +  hence "finite (s \<times> s')" by simp
   4.159 +  then obtain p where p: "p ` k = s \<times> s'" "inj_on p k"
   4.160 +    using ex_bij_betw_nat_finite[of "s \<times> s'"] unfolding bij_betw_def k_def by blast
   4.161 +  def c == "\<lambda> i. a (fst (p i)) \<inter> b (snd (p i))"
   4.162 +  def z == "\<lambda> i. x (fst (p i))"
   4.163 +  def z' == "\<lambda> i. y (snd (p i))"
   4.164 +
   4.165 +  have "finite k" unfolding k_def by simp
   4.166 +
   4.167 +  have "nonneg z" and "nonneg z'"
   4.168 +    using psf psg unfolding z_def z'_def pos_simple_def nonneg_def by auto
   4.169 +
   4.170 +  have ck_subset_M: "c ` k \<subseteq> sets M"
   4.171 +  proof
   4.172 +    fix x assume "x \<in> c ` k"
   4.173 +    then obtain j where "j \<in> k" and "x = c j" by auto
   4.174 +    hence "p j \<in> s \<times> s'" using p(1) by auto
   4.175 +    hence "a (fst (p j)) \<in> sets M" (is "?a \<in> _")
   4.176 +      and "b (snd (p j)) \<in> sets M" (is "?b \<in> _")
   4.177 +      using psf psg unfolding pos_simple_def by auto
   4.178 +    thus "x \<in> sets M" unfolding `x = c j` c_def using Int by simp
   4.179 +  qed
   4.180 +
   4.181 +  { fix t assume "t \<in> space M"
   4.182 +    hence ex1s: "\<exists>!i\<in>s. t \<in> a i" and ex1s': "\<exists>!i\<in>s'. t \<in> b i"
   4.183 +      using psf psg unfolding pos_simple_def by auto
   4.184 +    then obtain j j' where j: "j \<in> s" "t \<in> a j" and j': "j' \<in> s'" "t \<in> b j'"
   4.185 +      by auto
   4.186 +    then obtain i :: nat where i: "(j,j') = p i" and "i \<in> k" using p by auto
   4.187 +    have "\<exists>!i\<in>k. t \<in> c i"
   4.188 +    proof (rule ex1I[of _ i])
   4.189 +      show "\<And>x. x \<in> k \<Longrightarrow> t \<in> c x \<Longrightarrow> x = i"
   4.190 +      proof -
   4.191 +        fix l assume "l \<in> k" "t \<in> c l"
   4.192 +        hence "p l \<in> s \<times> s'" and t_in: "t \<in> a (fst (p l))" "t \<in> b (snd (p l))"
   4.193 +          using p unfolding c_def by auto
   4.194 +        hence "fst (p l) \<in> s" and "snd (p l) \<in> s'" by auto
   4.195 +        with t_in j j' ex1s ex1s' have "p l = (j, j')" by (cases "p l", auto)
   4.196 +        thus "l = i"
   4.197 +          using `(j, j') = p i` p(2)[THEN inj_onD] `l \<in> k` `i \<in> k` by auto
   4.198 +      qed
   4.199 +
   4.200 +      show "i \<in> k \<and> t \<in> c i"
   4.201 +        using `i \<in> k` `t \<in> a j` `t \<in> b j'` c_def i[symmetric] by auto
   4.202 +    qed auto
   4.203 +  } note ex1 = this
   4.204 +
   4.205 +  show thesis
   4.206 +  proof (rule that)
   4.207 +    { fix t i assume "t \<in> space M" and "i \<in> k"
   4.208 +      hence "p i \<in> s \<times> s'" using p(1) by auto
   4.209 +      hence "fst (p i) \<in> s" by auto
   4.210 +      moreover
   4.211 +      assume "t \<in> c i"
   4.212 +      hence "t \<in> a (fst (p i))" unfolding c_def by auto
   4.213 +      ultimately have "f t = z i" using psf `t \<in> space M`
   4.214 +        unfolding z_def pos_simple_def by auto
   4.215 +    }
   4.216 +    thus "(k, c, z) \<in> pos_simple f"
   4.217 +      using psf `finite k` `nonneg z` ck_subset_M ex1
   4.218 +      unfolding pos_simple_def by auto
   4.219 +
   4.220 +    { fix t i assume "t \<in> space M" and "i \<in> k"
   4.221 +      hence "p i \<in> s \<times> s'" using p(1) by auto
   4.222 +      hence "snd (p i) \<in> s'" by auto
   4.223 +      moreover
   4.224 +      assume "t \<in> c i"
   4.225 +      hence "t \<in> b (snd (p i))" unfolding c_def by auto
   4.226 +      ultimately have "g t = z' i" using psg `t \<in> space M`
   4.227 +        unfolding z'_def pos_simple_def by auto
   4.228 +    }
   4.229 +    thus "(k, c, z') \<in> pos_simple g"
   4.230 +      using psg `finite k` `nonneg z'` ck_subset_M ex1
   4.231 +      unfolding pos_simple_def by auto
   4.232 +  qed
   4.233 +qed
   4.234 +
   4.235 +lemma (in measure_space) pos_simple_integral_equal:
   4.236 +  assumes psx: "(s, a, x) \<in> pos_simple f"
   4.237 +  assumes psy: "(s', b, y) \<in> pos_simple f"
   4.238 +  shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
   4.239 +  unfolding pos_simple_integral_def
   4.240 +proof simp
   4.241 +  have "(\<Sum>i\<in>s. x i * measure M (a i)) =
   4.242 +    (\<Sum>i\<in>s. (\<Sum>j \<in> s'. x i * measure M (a i \<inter> b j)))" (is "?left = _")
   4.243 +    using psy psx unfolding setsum_right_distrib[symmetric]
   4.244 +    by (auto intro!: setsum_cong measure_setsum_split elim!: pos_simpleE)
   4.245 +  also have "... = (\<Sum>i\<in>s. (\<Sum>j \<in> s'. y j * measure M (a i \<inter> b j)))"
   4.246 +  proof (rule setsum_cong, simp, rule setsum_cong, simp_all)
   4.247 +    fix i j assume i: "i \<in> s" and j: "j \<in> s'"
   4.248 +    hence "a i \<in> sets M" using psx by (auto elim!: pos_simpleE)
   4.249 +
   4.250 +    show "measure M (a i \<inter> b j) = 0 \<or> x i = y j"
   4.251 +    proof (cases "a i \<inter> b j = {}")
   4.252 +      case True thus ?thesis using empty_measure by simp
   4.253 +    next
   4.254 +      case False then obtain t where t: "t \<in> a i" "t \<in> b j" by auto
   4.255 +      hence "t \<in> space M" using `a i \<in> sets M` sets_into_space by auto
   4.256 +      with psx psy t i j have "x i = f t" and "y j = f t"
   4.257 +        unfolding pos_simple_def by auto
   4.258 +      thus ?thesis by simp
   4.259 +    qed
   4.260 +  qed
   4.261 +  also have "... = (\<Sum>j\<in>s'. (\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)))"
   4.262 +    by (subst setsum_commute) simp
   4.263 +  also have "... = (\<Sum>i\<in>s'. y i * measure M (b i))" (is "?sum_sum = ?right")
   4.264 +  proof (rule setsum_cong)
   4.265 +    fix j assume "j \<in> s'"
   4.266 +    have "y j * measure M (b j) = (\<Sum>i\<in>s. y j * measure M (b j \<inter> a i))"
   4.267 +      using psx psy `j \<in> s'` unfolding setsum_right_distrib[symmetric]
   4.268 +      by (auto intro!: measure_setsum_split elim!: pos_simpleE)
   4.269 +    thus "(\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)) = y j * measure M (b j)"
   4.270 +      by (auto intro!: setsum_cong arg_cong[where f="measure M"])
   4.271 +  qed simp
   4.272 +  finally show "?left = ?right" .
   4.273 +qed
   4.274 +
   4.275 +lemma (in measure_space)psfis_present:
   4.276 +  assumes "A \<in> psfis f"
   4.277 +  assumes "B \<in> psfis g"
   4.278 +  obtains z z' c k where
   4.279 +  "A = pos_simple_integral (k, c, z)"
   4.280 +  "B = pos_simple_integral (k, c, z')"
   4.281 +  "(k, c, z) \<in> pos_simple f"
   4.282 +  "(k, c, z') \<in> pos_simple g"
   4.283 +using assms
   4.284 +proof -
   4.285 +  from assms obtain s a x s' b y where
   4.286 +    ps: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g" and
   4.287 +    A: "A = pos_simple_integral (s, a, x)" and
   4.288 +    B: "B = pos_simple_integral (s', b, y)"
   4.289 +    unfolding psfis_def pos_simple_integral_def by auto
   4.290 +
   4.291 +  guess z z' c k using pos_simple_common_partition[OF ps] . note part = this
   4.292 +  show thesis
   4.293 +  proof (rule that[of k c z z', OF _ _ part])
   4.294 +    show "A = pos_simple_integral (k, c, z)"
   4.295 +      unfolding A by (rule pos_simple_integral_equal[OF ps(1) part(1)])
   4.296 +    show "B = pos_simple_integral (k, c, z')"
   4.297 +      unfolding B by (rule pos_simple_integral_equal[OF ps(2) part(2)])
   4.298 +  qed
   4.299 +qed
   4.300 +
   4.301 +lemma (in measure_space) pos_simple_integral_add:
   4.302 +  assumes "(s, a, x) \<in> pos_simple f"
   4.303 +  assumes "(s', b, y) \<in> pos_simple g"
   4.304 +  obtains s'' c z where
   4.305 +    "(s'', c, z) \<in> pos_simple (\<lambda>x. f x + g x)"
   4.306 +    "(pos_simple_integral (s, a, x) +
   4.307 +      pos_simple_integral (s', b, y) =
   4.308 +      pos_simple_integral (s'', c, z))"
   4.309 +using assms
   4.310 +proof -
   4.311 +  guess z z' c k
   4.312 +    by (rule pos_simple_common_partition[OF `(s, a, x) \<in> pos_simple f ` `(s', b, y) \<in> pos_simple g`])
   4.313 +  note kczz' = this
   4.314 +  have x: "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
   4.315 +    by (rule pos_simple_integral_equal) (fact, fact)
   4.316 +  have y: "pos_simple_integral (s', b, y) = pos_simple_integral (k, c, z')"
   4.317 +    by (rule pos_simple_integral_equal) (fact, fact)
   4.318 +
   4.319 +  have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))
   4.320 +    = (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"
   4.321 +    unfolding pos_simple_integral_def by auto
   4.322 +  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto
   4.323 +  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x)) + (\<Sum> x \<in> k. z' x * measure M (c x))" using setsum_addf by auto
   4.324 +  also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto
   4.325 +  finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =
   4.326 +    pos_simple_integral (k, c, (\<lambda> x. z x + z' x))" using x y by auto
   4.327 +  show ?thesis
   4.328 +    apply (rule that[of k c "(\<lambda> x. z x + z' x)", OF _ ths])
   4.329 +    using kczz' unfolding pos_simple_def nonneg_def by (auto intro!: add_nonneg_nonneg)
   4.330 +qed
   4.331 +
   4.332 +lemma psfis_add:
   4.333 +  assumes "a \<in> psfis f" "b \<in> psfis g"
   4.334 +  shows "a + b \<in> psfis (\<lambda>x. f x + g x)"
   4.335 +using assms pos_simple_integral_add
   4.336 +unfolding psfis_def by auto blast
   4.337 +
   4.338 +lemma pos_simple_integral_mono_on_mspace:
   4.339 +  assumes f: "(s, a, x) \<in> pos_simple f"
   4.340 +  assumes g: "(s', b, y) \<in> pos_simple g"
   4.341 +  assumes mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
   4.342 +  shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
   4.343 +using assms
   4.344 +proof -
   4.345 +  guess z z' c k by (rule pos_simple_common_partition[OF f g])
   4.346 +  note kczz' = this
   4.347 +  (* w = z and w' = z'  except where c _ = {} or undef *)
   4.348 +  def w == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z i"
   4.349 +  def w' == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z' i"
   4.350 +  { fix i
   4.351 +    have "w i \<le> w' i"
   4.352 +    proof (cases "i \<notin> k \<or> c i = {}")
   4.353 +      case False hence "i \<in> k" "c i \<noteq> {}" by auto
   4.354 +      then obtain v where v: "v \<in> c i" and "c i \<in> sets M"
   4.355 +        using kczz'(1) unfolding pos_simple_def by blast
   4.356 +      hence "v \<in> space M" using sets_into_space by blast
   4.357 +      with mono[OF `v \<in> space M`] kczz' `i \<in> k` `v \<in> c i`
   4.358 +      have "z i \<le> z' i" unfolding pos_simple_def by simp
   4.359 +      thus ?thesis unfolding w_def w'_def using False by auto
   4.360 +    next
   4.361 +      case True thus ?thesis unfolding w_def w'_def by auto
   4.362 +   qed
   4.363 +  } note w_mn = this
   4.364 +
   4.365 +  (* some technical stuff for the calculation*)
   4.366 +  have "\<And> i. i \<in> k \<Longrightarrow> c i \<in> sets M" using kczz' unfolding pos_simple_def by auto
   4.367 +  hence "\<And> i. i \<in> k \<Longrightarrow> measure M (c i) \<ge> 0" using positive by auto
   4.368 +  hence w_mono: "\<And> i. i \<in> k \<Longrightarrow> w i * measure M (c i) \<le> w' i * measure M (c i)"
   4.369 +    using mult_right_mono w_mn by blast
   4.370 +
   4.371 +  { fix i have "\<lbrakk>i \<in> k ; z i \<noteq> w i\<rbrakk> \<Longrightarrow> measure M (c i) = 0"
   4.372 +      unfolding w_def by (cases "c i = {}") auto }
   4.373 +  hence zw: "\<And> i. i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)" by auto
   4.374 +
   4.375 +  { fix i have "i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)"
   4.376 +      unfolding w_def by (cases "c i = {}") simp_all }
   4.377 +  note zw = this
   4.378 +
   4.379 +  { fix i have "i \<in> k \<Longrightarrow> z' i * measure M (c i) = w' i * measure M (c i)"
   4.380 +      unfolding w'_def by (cases "c i = {}") simp_all }
   4.381 +  note z'w' = this
   4.382 +
   4.383 +  (* the calculation *)
   4.384 +  have "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
   4.385 +    using f kczz'(1) by (rule pos_simple_integral_equal)
   4.386 +  also have "\<dots> = (\<Sum> i \<in> k. z i * measure M (c i))"
   4.387 +    unfolding pos_simple_integral_def by auto
   4.388 +  also have "\<dots> = (\<Sum> i \<in> k. w i * measure M (c i))"
   4.389 +    using setsum_cong2[of k, OF zw] by auto
   4.390 +  also have "\<dots> \<le> (\<Sum> i \<in> k. w' i * measure M (c i))"
   4.391 +    using setsum_mono[OF w_mono, of k] by auto
   4.392 +  also have "\<dots> = (\<Sum> i \<in> k. z' i * measure M (c i))"
   4.393 +    using setsum_cong2[of k, OF z'w'] by auto
   4.394 +  also have "\<dots> = pos_simple_integral (k, c, z')"
   4.395 +    unfolding pos_simple_integral_def by auto
   4.396 +  also have "\<dots> = pos_simple_integral (s', b, y)"
   4.397 +    using kczz'(2) g by (rule pos_simple_integral_equal)
   4.398 +  finally show "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
   4.399 +    by simp
   4.400 +qed
   4.401 +
   4.402 +lemma pos_simple_integral_mono:
   4.403 +  assumes a: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g"
   4.404 +  assumes "\<And> z. f z \<le> g z"
   4.405 +  shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
   4.406 +using assms pos_simple_integral_mono_on_mspace by auto
   4.407 +
   4.408 +lemma psfis_mono:
   4.409 +  assumes "a \<in> psfis f" "b \<in> psfis g"
   4.410 +  assumes "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
   4.411 +  shows "a \<le> b"
   4.412 +using assms pos_simple_integral_mono_on_mspace unfolding psfis_def by auto
   4.413 +
   4.414 +lemma pos_simple_fn_integral_unique:
   4.415 +  assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"
   4.416 +  shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
   4.417 +using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis
   4.418 +
   4.419 +lemma psfis_unique:
   4.420 +  assumes "a \<in> psfis f" "b \<in> psfis f"
   4.421 +  shows "a = b"
   4.422 +using assms real_le_antisym real_le_refl psfis_mono by metis
   4.423 +
   4.424 +lemma pos_simple_integral_indicator:
   4.425 +  assumes "A \<in> sets M"
   4.426 +  obtains s a x where
   4.427 +  "(s, a, x) \<in> pos_simple (indicator_fn A)"
   4.428 +  "measure M A = pos_simple_integral (s, a, x)"
   4.429 +using assms
   4.430 +proof -
   4.431 +  def s == "{0, 1} :: nat set"
   4.432 +  def a == "\<lambda> i :: nat. if i = 0 then A else space M - A"
   4.433 +  def x == "\<lambda> i :: nat. if i = 0 then 1 else (0 :: real)"
   4.434 +  have eq: "pos_simple_integral (s, a, x) = measure M A"
   4.435 +    unfolding s_def a_def x_def pos_simple_integral_def by auto
   4.436 +  have "(s, a, x) \<in> pos_simple (indicator_fn A)"
   4.437 +    unfolding pos_simple_def indicator_fn_def s_def a_def x_def nonneg_def
   4.438 +    using assms sets_into_space by auto
   4.439 +   from that[OF this] eq show thesis by auto
   4.440 +qed
   4.441 +
   4.442 +lemma psfis_indicator:
   4.443 +  assumes "A \<in> sets M"
   4.444 +  shows "measure M A \<in> psfis (indicator_fn A)"
   4.445 +using pos_simple_integral_indicator[OF assms]
   4.446 +  unfolding psfis_def image_def by auto
   4.447 +
   4.448 +lemma pos_simple_integral_mult:
   4.449 +  assumes f: "(s, a, x) \<in> pos_simple f"
   4.450 +  assumes "0 \<le> z"
   4.451 +  obtains s' b y where
   4.452 +  "(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
   4.453 +  "pos_simple_integral (s', b, y) = z * pos_simple_integral (s, a, x)"
   4.454 +  using assms that[of s a "\<lambda>i. z * x i"]
   4.455 +  by (simp add: pos_simple_def pos_simple_integral_def setsum_right_distrib algebra_simps nonneg_def mult_nonneg_nonneg)
   4.456 +
   4.457 +lemma psfis_mult:
   4.458 +  assumes "r \<in> psfis f"
   4.459 +  assumes "0 \<le> z"
   4.460 +  shows "z * r \<in> psfis (\<lambda>x. z * f x)"
   4.461 +using assms
   4.462 +proof -
   4.463 +  from assms obtain s a x
   4.464 +    where sax: "(s, a, x) \<in> pos_simple f"
   4.465 +    and r: "r = pos_simple_integral (s, a, x)"
   4.466 +    unfolding psfis_def image_def by auto
   4.467 +  obtain s' b y where
   4.468 +    "(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
   4.469 +    "z * pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
   4.470 +    using pos_simple_integral_mult[OF sax `0 \<le> z`, of thesis] by auto
   4.471 +  thus ?thesis using r unfolding psfis_def image_def by auto
   4.472 +qed
   4.473 +
   4.474 +lemma pos_simple_integral_setsum_image:
   4.475 +  assumes "finite P"
   4.476 +  assumes "\<And> i. i \<in> P \<Longrightarrow> (s i, a i, x i) \<in> pos_simple (f i)"
   4.477 +  obtains s' a' x' where
   4.478 +  "(s', a', x') \<in> pos_simple (\<lambda>t. (\<Sum> i \<in> P. f i t))"
   4.479 +  "pos_simple_integral (s', a', x') = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))"
   4.480 +using assms that
   4.481 +proof (induct P arbitrary:thesis rule:finite.induct)
   4.482 +  case emptyI note asms = this
   4.483 +  def s' == "{0 :: nat}"
   4.484 +  def a' == "\<lambda> x. if x = (0 :: nat) then space M else {}"
   4.485 +  def x' == "\<lambda> x :: nat. (0 :: real)"
   4.486 +  have "(s', a', x') \<in> pos_simple (\<lambda> t. 0)"
   4.487 +    unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto
   4.488 +  moreover have "pos_simple_integral (s', a', x') = 0"
   4.489 +    unfolding s'_def a'_def x'_def pos_simple_integral_def by auto
   4.490 +  ultimately show ?case using asms by auto
   4.491 +next
   4.492 +
   4.493 +  case (insertI P c) note asms = this
   4.494 +  then obtain s' a' x' where
   4.495 +    sax: "(s', a', x') \<in> pos_simple (\<lambda>t. \<Sum>i\<in>P. f i t)"
   4.496 +         "pos_simple_integral (s', a', x') =
   4.497 +             (\<Sum>i\<in>P. pos_simple_integral (s i, a i, x i))"
   4.498 +    by auto
   4.499 +
   4.500 +  { assume "c \<in> P"
   4.501 +    hence "P = insert c P" by auto
   4.502 +    hence thesis using asms sax by auto
   4.503 +  }
   4.504 +  moreover
   4.505 +  { assume "c \<notin> P"
   4.506 +    from asms obtain s'' a'' x'' where
   4.507 +      sax': "s'' = s c" "a'' = a c" "x'' = x c"
   4.508 +            "(s'', a'', x'') \<in> pos_simple (f c)" by auto
   4.509 +    from sax sax' obtain k :: "nat \<Rightarrow> bool" and b :: "nat \<Rightarrow> 'a \<Rightarrow> bool" and z :: "nat \<Rightarrow> real" where
   4.510 +      tybbie:
   4.511 +      "(k, b, z) \<in> pos_simple (\<lambda>t. ((\<Sum>i\<in>P. f i t) + f c t))"
   4.512 +      "(pos_simple_integral (s', a', x') +
   4.513 +      pos_simple_integral (s'', a'', x'') =
   4.514 +      pos_simple_integral (k, b, z))"
   4.515 +      using pos_simple_integral_add by blast
   4.516 +
   4.517 +    from tybbie have
   4.518 +      "pos_simple_integral (k, b, z) =
   4.519 +      pos_simple_integral (s', a', x') +
   4.520 +      pos_simple_integral (s'', a'', x'')" by simp
   4.521 +    also have "\<dots> = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))
   4.522 +                  + pos_simple_integral (s c, a c, x c)"
   4.523 +      using sax sax' by auto
   4.524 +    also have "\<dots> = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
   4.525 +      using asms `c \<notin> P` by auto
   4.526 +    finally have A: "pos_simple_integral (k, b, z) = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
   4.527 +      by simp
   4.528 +
   4.529 +    have "\<And> t. (\<Sum> i \<in> P. f i t) + f c t = (\<Sum> i \<in> insert c P. f i t)"
   4.530 +      using `c \<notin> P` `finite P` by auto
   4.531 +    hence B: "(k, b, z) \<in> pos_simple (\<lambda> t. (\<Sum> i \<in> insert c P. f i t))"
   4.532 +      using tybbie by simp
   4.533 +
   4.534 +    from A B have thesis using asms by auto
   4.535 +    } ultimately show thesis by blast
   4.536 +qed
   4.537 +
   4.538 +lemma psfis_setsum_image:
   4.539 +  assumes "finite P"
   4.540 +  assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"
   4.541 +  shows "(setsum a P) \<in> psfis (\<lambda>t. \<Sum>i \<in> P. f i t)"
   4.542 +using assms
   4.543 +proof (induct P)
   4.544 +  case empty
   4.545 +  let ?s = "{0 :: nat}"
   4.546 +  let ?a = "\<lambda> i. if i = (0 :: nat) then space M else {}"
   4.547 +  let ?x = "\<lambda> (i :: nat). (0 :: real)"
   4.548 +  have "(?s, ?a, ?x) \<in> pos_simple (\<lambda> t. (0 :: real))"
   4.549 +    unfolding pos_simple_def image_def nonneg_def by auto
   4.550 +  moreover have "(\<Sum> i \<in> ?s. ?x i * measure M (?a i)) = 0" by auto
   4.551 +  ultimately have "0 \<in> psfis (\<lambda> t. 0)"
   4.552 +    unfolding psfis_def image_def pos_simple_integral_def nonneg_def
   4.553 +    by (auto intro!:bexI[of _ "(?s, ?a, ?x)"])
   4.554 +  thus ?case by auto
   4.555 +next
   4.556 +  case (insert x P) note asms = this
   4.557 +  have "finite P" by fact
   4.558 +  have "x \<notin> P" by fact
   4.559 +  have "(\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)) \<Longrightarrow>
   4.560 +    setsum a P \<in> psfis (\<lambda>t. \<Sum>i\<in>P. f i t)" by fact
   4.561 +  have "setsum a (insert x P) = a x + setsum a P" using `finite P` `x \<notin> P` by auto
   4.562 +  also have "\<dots> \<in> psfis (\<lambda> t. f x t + (\<Sum> i \<in> P. f i t))"
   4.563 +    using asms psfis_add by auto
   4.564 +  also have "\<dots> = psfis (\<lambda> t. \<Sum> i \<in> insert x P. f i t)"
   4.565 +    using `x \<notin> P` `finite P` by auto
   4.566 +  finally show ?case by simp
   4.567 +qed
   4.568 +
   4.569 +lemma psfis_intro:
   4.570 +  assumes "a ` P \<subseteq> sets M" and "nonneg x" and "finite P"
   4.571 +  shows "(\<Sum>i\<in>P. x i * measure M (a i)) \<in> psfis (\<lambda>t. \<Sum>i\<in>P. x i * indicator_fn (a i) t)"
   4.572 +using assms psfis_mult psfis_indicator
   4.573 +unfolding image_def nonneg_def
   4.574 +by (auto intro!:psfis_setsum_image)
   4.575 +
   4.576 +lemma psfis_nonneg: "a \<in> psfis f \<Longrightarrow> nonneg f"
   4.577 +unfolding psfis_def pos_simple_def by auto
   4.578 +
   4.579 +lemma pos_psfis: "r \<in> psfis f \<Longrightarrow> 0 \<le> r"
   4.580 +unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def
   4.581 +using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)
   4.582 +
   4.583 +lemma pos_part_neg_part_borel_measurable:
   4.584 +  assumes "f \<in> borel_measurable M"
   4.585 +  shows "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M"
   4.586 +using assms
   4.587 +proof -
   4.588 +  { fix a :: real
   4.589 +    { assume asm: "0 \<le> a"
   4.590 +      from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
   4.591 +      have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
   4.592 +        unfolding pos_part_def using assms borel_measurable_le_iff by auto
   4.593 +      hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
   4.594 +    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
   4.595 +      unfolding pos_part_def using empty_sets by auto
   4.596 +    ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
   4.597 +      using le_less_linear by auto
   4.598 +  } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
   4.599 +  { fix a :: real
   4.600 +    { assume asm: "0 \<le> a"
   4.601 +      from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
   4.602 +      have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
   4.603 +        unfolding neg_part_def using assms borel_measurable_ge_iff by auto
   4.604 +      hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
   4.605 +    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
   4.606 +    moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
   4.607 +    ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
   4.608 +      using le_less_linear by auto
   4.609 +  } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
   4.610 +  from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
   4.611 +qed
   4.612 +
   4.613 +lemma pos_part_neg_part_borel_measurable_iff:
   4.614 +  "f \<in> borel_measurable M \<longleftrightarrow>
   4.615 +  pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
   4.616 +proof -
   4.617 +  { fix x
   4.618 +    have "f x = pos_part f x - neg_part f x"
   4.619 +      unfolding pos_part_def neg_part_def unfolding max_def min_def
   4.620 +      by auto }
   4.621 +  hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
   4.622 +  hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
   4.623 +  from pos_part_neg_part_borel_measurable[of f]
   4.624 +    borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
   4.625 +    this
   4.626 +  show ?thesis by auto
   4.627 +qed
   4.628 +
   4.629 +lemma borel_measurable_cong:
   4.630 +  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
   4.631 +  shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
   4.632 +using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
   4.633 +
   4.634 +lemma psfis_borel_measurable:
   4.635 +  assumes "a \<in> psfis f"
   4.636 +  shows "f \<in> borel_measurable M"
   4.637 +using assms
   4.638 +proof -
   4.639 +  from assms obtain s a' x where sa'x: "(s, a', x) \<in> pos_simple f" and sa'xa: "pos_simple_integral (s, a', x) = a"
   4.640 +    and fs: "finite s"
   4.641 +    unfolding psfis_def pos_simple_integral_def image_def
   4.642 +    by (auto elim:pos_simpleE)
   4.643 +  { fix w assume "w \<in> space M"
   4.644 +    hence "(f w \<le> a) = ((\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
   4.645 +      using pos_simple_setsum_indicator_fn[OF sa'x, of w] by simp
   4.646 +  } hence "\<And> w. (w \<in> space M \<and> f w \<le> a) = (w \<in> space M \<and> (\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
   4.647 +    by auto
   4.648 +  { fix i assume "i \<in> s"
   4.649 +    hence "indicator_fn (a' i) \<in> borel_measurable M"
   4.650 +      using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto
   4.651 +    hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"
   4.652 +      using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]
   4.653 +        real_mult_commute by auto }
   4.654 +  from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable
   4.655 +  have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto
   4.656 +  from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this
   4.657 +  show ?thesis by simp
   4.658 +qed
   4.659 +
   4.660 +lemma mono_conv_outgrow:
   4.661 +  assumes "incseq x" "x ----> y" "z < y"
   4.662 +  shows "\<exists>b. \<forall> a \<ge> b. z < x a"
   4.663 +using assms
   4.664 +proof -
   4.665 +  from assms have "y - z > 0" by simp
   4.666 +  hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
   4.667 +    unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
   4.668 +    by simp
   4.669 +  have "\<forall>m. x m \<le> y" using incseq_le assms by auto
   4.670 +  hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
   4.671 +    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
   4.672 +  from A B show ?thesis by auto
   4.673 +qed
   4.674 +
   4.675 +lemma psfis_mono_conv_mono:
   4.676 +  assumes mono: "mono_convergent u f (space M)"
   4.677 +  and ps_u: "\<And>n. x n \<in> psfis (u n)"
   4.678 +  and "x ----> y"
   4.679 +  and "r \<in> psfis s"
   4.680 +  and f_upper_bound: "\<And>t. t \<in> space M \<Longrightarrow> s t \<le> f t"
   4.681 +  shows "r <= y"
   4.682 +proof (rule field_le_mult_one_interval)
   4.683 +  fix z :: real assume "0 < z" and "z < 1"
   4.684 +  hence "0 \<le> z" by auto
   4.685 +(*  def B' \<equiv> "\<lambda>n. {w \<in> space M. z * s w <= u n w}" *)
   4.686 +  let "?B' n" = "{w \<in> space M. z * s w <= u n w}"
   4.687 +
   4.688 +  have "incseq x" unfolding incseq_def
   4.689 +  proof safe
   4.690 +    fix m n :: nat assume "m \<le> n"
   4.691 +    show "x m \<le> x n"
   4.692 +    proof (rule psfis_mono[OF `x m \<in> psfis (u m)` `x n \<in> psfis (u n)`])
   4.693 +      fix t assume "t \<in> space M"
   4.694 +      with mono_convergentD[OF mono this] `m \<le> n` show "u m t \<le> u n t"
   4.695 +        unfolding incseq_def by auto
   4.696 +    qed
   4.697 +  qed
   4.698 +
   4.699 +  from `r \<in> psfis s`
   4.700 +  obtain s' a x' where r: "r = pos_simple_integral (s', a, x')"
   4.701 +    and ps_s: "(s', a, x') \<in> pos_simple s"
   4.702 +    unfolding psfis_def by auto
   4.703 +
   4.704 +  { fix t i assume "i \<in> s'" "t \<in> a i"
   4.705 +    hence "t \<in> space M" using ps_s by (auto elim!: pos_simpleE) }
   4.706 +  note t_in_space = this
   4.707 +
   4.708 +  { fix n
   4.709 +    from psfis_borel_measurable[OF `r \<in> psfis s`]
   4.710 +       psfis_borel_measurable[OF ps_u]
   4.711 +    have "?B' n \<in> sets M"
   4.712 +      by (auto intro!:
   4.713 +        borel_measurable_leq_borel_measurable
   4.714 +        borel_measurable_times_borel_measurable
   4.715 +        borel_measurable_const) }
   4.716 +  note B'_in_M = this
   4.717 +
   4.718 +  { fix n have "(\<lambda>i. a i \<inter> ?B' n) ` s' \<subseteq> sets M" using B'_in_M ps_s
   4.719 +      by (auto intro!: Int elim!: pos_simpleE) }
   4.720 +  note B'_inter_a_in_M = this
   4.721 +
   4.722 +  let "?sum n" = "(\<Sum>i\<in>s'. x' i * measure M (a i \<inter> ?B' n))"
   4.723 +  { fix n
   4.724 +    have "z * ?sum n \<le> x n"
   4.725 +    proof (rule psfis_mono[OF _ ps_u])
   4.726 +      have *: "\<And>i t. indicator_fn (?B' n) t * (x' i * indicator_fn (a i) t) =
   4.727 +        x' i * indicator_fn (a i \<inter> ?B' n) t" unfolding indicator_fn_def by auto
   4.728 +      have ps': "?sum n \<in> psfis (\<lambda>t. indicator_fn (?B' n) t * (\<Sum>i\<in>s'. x' i * indicator_fn (a i) t))"
   4.729 +        unfolding setsum_right_distrib * using B'_in_M ps_s
   4.730 +        by (auto intro!: psfis_intro Int elim!: pos_simpleE)
   4.731 +      also have "... = psfis (\<lambda>t. indicator_fn (?B' n) t * s t)" (is "psfis ?l = psfis ?r")
   4.732 +      proof (rule psfis_cong)
   4.733 +        show "nonneg ?l" using psfis_nonneg[OF ps'] .
   4.734 +        show "nonneg ?r" using psfis_nonneg[OF `r \<in> psfis s`] unfolding nonneg_def indicator_fn_def by auto
   4.735 +        fix t assume "t \<in> space M"
   4.736 +        show "?l t = ?r t" unfolding pos_simple_setsum_indicator_fn[OF ps_s `t \<in> space M`] ..
   4.737 +      qed
   4.738 +      finally show "z * ?sum n \<in> psfis (\<lambda>t. z * ?r t)" using psfis_mult[OF _ `0 \<le> z`] by simp
   4.739 +    next
   4.740 +      fix t assume "t \<in> space M"
   4.741 +      show "z * (indicator_fn (?B' n) t * s t) \<le> u n t"
   4.742 +         using psfis_nonneg[OF ps_u] unfolding nonneg_def indicator_fn_def by auto
   4.743 +    qed }
   4.744 +  hence *: "\<exists>N. \<forall>n\<ge>N. z * ?sum n \<le> x n" by (auto intro!: exI[of _ 0])
   4.745 +
   4.746 +  show "z * r \<le> y" unfolding r pos_simple_integral_def
   4.747 +  proof (rule LIMSEQ_le[OF mult_right.LIMSEQ `x ----> y` *],
   4.748 +         simp, rule LIMSEQ_setsum, rule mult_right.LIMSEQ)
   4.749 +    fix i assume "i \<in> s'"
   4.750 +    from psfis_nonneg[OF `r \<in> psfis s`, unfolded nonneg_def]
   4.751 +    have "\<And>t. 0 \<le> s t" by simp
   4.752 +
   4.753 +    have *: "(\<Union>j. a i \<inter> ?B' j) = a i"
   4.754 +    proof (safe, simp, safe)
   4.755 +      fix t assume "t \<in> a i"
   4.756 +      thus "t \<in> space M" using t_in_space[OF `i \<in> s'`] by auto
   4.757 +      show "\<exists>j. z * s t \<le> u j t"
   4.758 +      proof (cases "s t = 0")
   4.759 +        case True thus ?thesis
   4.760 +          using psfis_nonneg[OF ps_u] unfolding nonneg_def by auto
   4.761 +      next
   4.762 +        case False with `0 \<le> s t`
   4.763 +        have "0 < s t" by auto
   4.764 +        hence "z * s t < 1 * s t" using `0 < z` `z < 1`
   4.765 +          by (auto intro!: mult_strict_right_mono simp del: mult_1_left)
   4.766 +        also have "... \<le> f t" using f_upper_bound `t \<in> space M` by auto
   4.767 +        finally obtain b where "\<And>j. b \<le> j \<Longrightarrow> z * s t < u j t" using `t \<in> space M`
   4.768 +          using mono_conv_outgrow[of "\<lambda>n. u n t" "f t" "z * s t"]
   4.769 +          using mono_convergentD[OF mono] by auto
   4.770 +        from this[of b] show ?thesis by (auto intro!: exI[of _ b])
   4.771 +      qed
   4.772 +    qed
   4.773 +
   4.774 +    show "(\<lambda>n. measure M (a i \<inter> ?B' n)) ----> measure M (a i)"
   4.775 +    proof (safe intro!:
   4.776 +        monotone_convergence[of "\<lambda>n. a i \<inter> ?B' n", unfolded comp_def *])
   4.777 +      fix n show "a i \<inter> ?B' n \<in> sets M"
   4.778 +        using B'_inter_a_in_M[of n] `i \<in> s'` by auto
   4.779 +    next
   4.780 +      fix j t assume "t \<in> space M" and "z * s t \<le> u j t"
   4.781 +      thus "z * s t \<le> u (Suc j) t"
   4.782 +        using mono_convergentD(1)[OF mono, unfolded incseq_def,
   4.783 +          rule_format, of t j "Suc j"]
   4.784 +        by auto
   4.785 +    qed
   4.786 +  qed
   4.787 +qed
   4.788 +
   4.789 +lemma psfis_nnfis:
   4.790 +  "a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"
   4.791 +  unfolding nnfis_def mono_convergent_def incseq_def
   4.792 +  by (auto intro!: exI[of _ "\<lambda>n. f"] exI[of _ "\<lambda>n. a"] LIMSEQ_const)
   4.793 +
   4.794 +lemma nnfis_times:
   4.795 +  assumes "a \<in> nnfis f" and "0 \<le> z"
   4.796 +  shows "z * a \<in> nnfis (\<lambda>t. z * f t)"
   4.797 +proof -
   4.798 +  obtain u x where "mono_convergent u f (space M)" and
   4.799 +    "\<And>n. x n \<in> psfis (u n)" "x ----> a"
   4.800 +    using `a \<in> nnfis f` unfolding nnfis_def by auto
   4.801 +  with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
   4.802 +    by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
   4.803 +      LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
   4.804 +qed
   4.805 +
   4.806 +lemma nnfis_add:
   4.807 +  assumes "a \<in> nnfis f" and "b \<in> nnfis g"
   4.808 +  shows "a + b \<in> nnfis (\<lambda>t. f t + g t)"
   4.809 +proof -
   4.810 +  obtain u x w y
   4.811 +    where "mono_convergent u f (space M)" and
   4.812 +    "\<And>n. x n \<in> psfis (u n)" "x ----> a" and
   4.813 +    "mono_convergent w g (space M)" and
   4.814 +    "\<And>n. y n \<in> psfis (w n)" "y ----> b"
   4.815 +    using `a \<in> nnfis f` `b \<in> nnfis g` unfolding nnfis_def by auto
   4.816 +  thus ?thesis unfolding nnfis_def mono_convergent_def incseq_def
   4.817 +    by (auto intro!: exI[of _ "\<lambda>n a. u n a + w n a"] exI[of _ "\<lambda>n. x n + y n"]
   4.818 +      LIMSEQ_add LIMSEQ_const psfis_add add_mono)
   4.819 +qed
   4.820 +
   4.821 +lemma nnfis_mono:
   4.822 +  assumes nnfis: "a \<in> nnfis f" "b \<in> nnfis g"
   4.823 +  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
   4.824 +  shows "a \<le> b"
   4.825 +proof -
   4.826 +  obtain u x w y where
   4.827 +    mc: "mono_convergent u f (space M)" "mono_convergent w g (space M)" and
   4.828 +    psfis: "\<And>n. x n \<in> psfis (u n)" "\<And>n. y n \<in> psfis (w n)" and
   4.829 +    limseq: "x ----> a" "y ----> b" using nnfis unfolding nnfis_def by auto
   4.830 +  show ?thesis
   4.831 +  proof (rule LIMSEQ_le_const2[OF limseq(1)], rule exI[of _ 0], safe)
   4.832 +    fix n
   4.833 +    show "x n \<le> b"
   4.834 +    proof (rule psfis_mono_conv_mono[OF mc(2) psfis(2) limseq(2) psfis(1)])
   4.835 +      fix t assume "t \<in> space M"
   4.836 +      from mono_convergent_le[OF mc(1) this] mono[OF this]
   4.837 +      show "u n t \<le> g t" by (rule order_trans)
   4.838 +    qed
   4.839 +  qed
   4.840 +qed
   4.841 +
   4.842 +lemma nnfis_unique:
   4.843 +  assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"
   4.844 +  shows "a = b"
   4.845 +  using nnfis_mono[OF a b] nnfis_mono[OF b a]
   4.846 +  by (auto intro!: real_le_antisym[of a b])
   4.847 +
   4.848 +lemma psfis_equiv:
   4.849 +  assumes "a \<in> psfis f" and "nonneg g"
   4.850 +  and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
   4.851 +  shows "a \<in> psfis g"
   4.852 +  using assms unfolding psfis_def pos_simple_def by auto
   4.853 +
   4.854 +lemma psfis_mon_upclose:
   4.855 +  assumes "\<And>m. a m \<in> psfis (u m)"
   4.856 +  shows "\<exists>c. c \<in> psfis (mon_upclose n u)"
   4.857 +proof (induct n)
   4.858 +  case 0 thus ?case unfolding mon_upclose.simps using assms ..
   4.859 +next
   4.860 +  case (Suc n)
   4.861 +  then obtain sn an xn where ps: "(sn, an, xn) \<in> pos_simple (mon_upclose n u)"
   4.862 +    unfolding psfis_def by auto
   4.863 +  obtain ss as xs where ps': "(ss, as, xs) \<in> pos_simple (u (Suc n))"
   4.864 +    using assms[of "Suc n"] unfolding psfis_def by auto
   4.865 +  from pos_simple_common_partition[OF ps ps'] guess x x' a s .
   4.866 +  hence "(s, a, upclose x x') \<in> pos_simple (mon_upclose (Suc n) u)"
   4.867 +    by (simp add: upclose_def pos_simple_def nonneg_def max_def)
   4.868 +  thus ?case unfolding psfis_def by auto
   4.869 +qed
   4.870 +
   4.871 +text {* Beppo-Levi monotone convergence theorem *}
   4.872 +lemma nnfis_mon_conv:
   4.873 +  assumes mc: "mono_convergent f h (space M)"
   4.874 +  and nnfis: "\<And>n. x n \<in> nnfis (f n)"
   4.875 +  and "x ----> z"
   4.876 +  shows "z \<in> nnfis h"
   4.877 +proof -
   4.878 +  have "\<forall>n. \<exists>u y. mono_convergent u (f n) (space M) \<and> (\<forall>m. y m \<in> psfis (u m)) \<and>
   4.879 +    y ----> x n"
   4.880 +    using nnfis unfolding nnfis_def by auto
   4.881 +  from choice[OF this] guess u ..
   4.882 +  from choice[OF this] guess y ..
   4.883 +  hence mc_u: "\<And>n. mono_convergent (u n) (f n) (space M)"
   4.884 +    and psfis: "\<And>n m. y n m \<in> psfis (u n m)" and "\<And>n. y n ----> x n"
   4.885 +    by auto
   4.886 +
   4.887 +  let "?upclose n" = "mon_upclose n (\<lambda>m. u m n)"
   4.888 +
   4.889 +  have "\<exists>c. \<forall>n. c n \<in> psfis (?upclose n)"
   4.890 +    by (safe intro!: choice psfis_mon_upclose) (rule psfis)
   4.891 +  then guess c .. note c = this[rule_format]
   4.892 +
   4.893 +  show ?thesis unfolding nnfis_def
   4.894 +  proof (safe intro!: exI)
   4.895 +    show mc_upclose: "mono_convergent ?upclose h (space M)"
   4.896 +      by (rule mon_upclose_mono_convergent[OF mc_u mc])
   4.897 +    show psfis_upclose: "\<And>n. c n \<in> psfis (?upclose n)"
   4.898 +      using c .
   4.899 +
   4.900 +    { fix n m :: nat assume "n \<le> m"
   4.901 +      hence "c n \<le> c m"
   4.902 +        using psfis_mono[OF c c]
   4.903 +        using mono_convergentD(1)[OF mc_upclose, unfolded incseq_def]
   4.904 +        by auto }
   4.905 +    hence "incseq c" unfolding incseq_def by auto
   4.906 +
   4.907 +    { fix n
   4.908 +      have c_nnfis: "c n \<in> nnfis (?upclose n)" using c by (rule psfis_nnfis)
   4.909 +      from nnfis_mono[OF c_nnfis nnfis]
   4.910 +        mon_upclose_le_mono_convergent[OF mc_u]
   4.911 +        mono_convergentD(1)[OF mc]
   4.912 +      have "c n \<le> x n" by fast }
   4.913 +    note c_less_x = this
   4.914 +
   4.915 +    { fix n
   4.916 +      note c_less_x[of n]
   4.917 +      also have "x n \<le> z"
   4.918 +      proof (rule incseq_le)
   4.919 +        show "x ----> z" by fact
   4.920 +        from mono_convergentD(1)[OF mc]
   4.921 +        show "incseq x" unfolding incseq_def
   4.922 +          by (auto intro!: nnfis_mono[OF nnfis nnfis])
   4.923 +      qed
   4.924 +      finally have "c n \<le> z" . }
   4.925 +    note c_less_z = this
   4.926 +
   4.927 +    have "convergent c"
   4.928 +    proof (rule Bseq_mono_convergent[unfolded incseq_def[symmetric]])
   4.929 +      show "Bseq c"
   4.930 +        using pos_psfis[OF c] c_less_z
   4.931 +        by (auto intro!: BseqI'[of _ z])
   4.932 +      show "incseq c" by fact
   4.933 +    qed
   4.934 +    then obtain l where l: "c ----> l" unfolding convergent_def by auto
   4.935 +
   4.936 +    have "l \<le> z" using c_less_x l
   4.937 +      by (auto intro!: LIMSEQ_le[OF _ `x ----> z`])
   4.938 +    moreover have "z \<le> l"
   4.939 +    proof (rule LIMSEQ_le_const2[OF `x ----> z`], safe intro!: exI[of _ 0])
   4.940 +      fix n
   4.941 +      have "l \<in> nnfis h"
   4.942 +        unfolding nnfis_def using l mc_upclose psfis_upclose by auto
   4.943 +      from nnfis this mono_convergent_le[OF mc]
   4.944 +      show "x n \<le> l" by (rule nnfis_mono)
   4.945 +    qed
   4.946 +    ultimately have "l = z" by (rule real_le_antisym)
   4.947 +    thus "c ----> z" using `c ----> l` by simp
   4.948 +  qed
   4.949 +qed
   4.950 +
   4.951 +lemma nnfis_pos_on_mspace:
   4.952 +  assumes "a \<in> nnfis f" and "x \<in>space M"
   4.953 +  shows "0 \<le> f x"
   4.954 +using assms
   4.955 +proof -
   4.956 +  from assms[unfolded nnfis_def] guess u y by auto note uy = this
   4.957 +  hence "\<And> n. 0 \<le> u n x" 
   4.958 +    unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
   4.959 +    by auto
   4.960 +  thus "0 \<le> f x" using uy[rule_format]
   4.961 +    unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
   4.962 +    using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans
   4.963 +    by fast
   4.964 +qed
   4.965 +
   4.966 +lemma nnfis_borel_measurable:
   4.967 +  assumes "a \<in> nnfis f"
   4.968 +  shows "f \<in> borel_measurable M"
   4.969 +using assms unfolding nnfis_def
   4.970 +apply auto
   4.971 +apply (rule mono_convergent_borel_measurable)
   4.972 +using psfis_borel_measurable
   4.973 +by auto
   4.974 +
   4.975 +lemma borel_measurable_mon_conv_psfis:
   4.976 +  assumes f_borel: "f \<in> borel_measurable M"
   4.977 +  and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
   4.978 +  shows"\<exists>u x. mono_convergent u f (space M) \<and> (\<forall>n. x n \<in> psfis (u n))"
   4.979 +proof (safe intro!: exI)
   4.980 +  let "?I n" = "{0<..<n * 2^n}"
   4.981 +  let "?A n i" = "{w \<in> space M. real (i :: nat) / 2^(n::nat) \<le> f w \<and> f w < real (i + 1) / 2^n}"
   4.982 +  let "?u n t" = "\<Sum>i\<in>?I n. real i / 2^n * indicator_fn (?A n i) t"
   4.983 +  let "?x n" = "\<Sum>i\<in>?I n. real i / 2^n * measure M (?A n i)"
   4.984 +
   4.985 +  let "?w n t" = "if f t < real n then real (natfloor (f t * 2^n)) / 2^n else 0"
   4.986 +
   4.987 +  { fix t n assume t: "t \<in> space M"
   4.988 +    have "?u n t = ?w n t" (is "_ = (if _ then real ?i / _ else _)")
   4.989 +    proof (cases "f t < real n")
   4.990 +      case True
   4.991 +      with nonneg t
   4.992 +      have i: "?i < n * 2^n"
   4.993 +        by (auto simp: real_of_nat_power[symmetric]
   4.994 +                 intro!: less_natfloor mult_nonneg_nonneg)
   4.995 +
   4.996 +      hence t_in_A: "t \<in> ?A n ?i"
   4.997 +        unfolding divide_le_eq less_divide_eq
   4.998 +        using nonneg t True
   4.999 +        by (auto intro!: real_natfloor_le
  4.1000 +          real_natfloor_gt_diff_one[unfolded diff_less_eq]
  4.1001 +          simp: real_of_nat_Suc zero_le_mult_iff)
  4.1002 +
  4.1003 +      hence *: "real ?i / 2^n \<le> f t"
  4.1004 +        "f t < real (?i + 1) / 2^n" by auto
  4.1005 +      { fix j assume "t \<in> ?A n j"
  4.1006 +        hence "real j / 2^n \<le> f t"
  4.1007 +          and "f t < real (j + 1) / 2^n" by auto
  4.1008 +        with * have "j \<in> {?i}" unfolding divide_le_eq less_divide_eq
  4.1009 +          by auto }
  4.1010 +      hence *: "\<And>j. t \<in> ?A n j \<longleftrightarrow> j \<in> {?i}" using t_in_A by auto
  4.1011 +
  4.1012 +      have "?u n t = real ?i / 2^n"
  4.1013 +        unfolding indicator_fn_def if_distrib *
  4.1014 +          setsum_cases[OF finite_greaterThanLessThan]
  4.1015 +        using i by (cases "?i = 0") simp_all
  4.1016 +      thus ?thesis using True by auto
  4.1017 +    next
  4.1018 +      case False
  4.1019 +      have "?u n t = (\<Sum>i \<in> {0 <..< n*2^n}. 0)"
  4.1020 +      proof (rule setsum_cong)
  4.1021 +        fix i assume "i \<in> {0 <..< n*2^n}"
  4.1022 +        hence "i + 1 \<le> n * 2^n" by simp
  4.1023 +        hence "real (i + 1) \<le> real n * 2^n"
  4.1024 +          unfolding real_of_nat_le_iff[symmetric]
  4.1025 +          by (auto simp: real_of_nat_power[symmetric])
  4.1026 +        also have "... \<le> f t * 2^n"
  4.1027 +          using False by (auto intro!: mult_nonneg_nonneg)
  4.1028 +        finally have "t \<notin> ?A n i"
  4.1029 +          by (auto simp: divide_le_eq less_divide_eq)
  4.1030 +        thus "real i / 2^n * indicator_fn (?A n i) t = 0"
  4.1031 +          unfolding indicator_fn_def by auto
  4.1032 +      qed simp
  4.1033 +      thus ?thesis using False by auto
  4.1034 +    qed }
  4.1035 +  note u_at_t = this
  4.1036 +
  4.1037 +  show "mono_convergent ?u f (space M)" unfolding mono_convergent_def
  4.1038 +  proof safe
  4.1039 +    fix t assume t: "t \<in> space M"
  4.1040 +    { fix m n :: nat assume "m \<le> n"
  4.1041 +      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
  4.1042 +      have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
  4.1043 +        apply (subst *)
  4.1044 +        apply (subst class_semiring.mul_a)
  4.1045 +        apply (subst real_of_nat_le_iff)
  4.1046 +        apply (rule le_mult_natfloor)
  4.1047 +        using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
  4.1048 +      hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
  4.1049 +        apply (subst *)
  4.1050 +        apply (subst (3) class_semiring.mul_c)
  4.1051 +        apply (subst class_semiring.mul_a)
  4.1052 +        by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
  4.1053 +    thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
  4.1054 +      by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)
  4.1055 +
  4.1056 +    show "(\<lambda>i. ?u i t) ----> f t" unfolding u_at_t[OF t]
  4.1057 +    proof (rule LIMSEQ_I, safe intro!: exI)
  4.1058 +      fix r :: real and n :: nat
  4.1059 +      let ?N = "natfloor (1/r) + 1"
  4.1060 +      assume "0 < r" and N: "max ?N (natfloor (f t) + 1) \<le> n"
  4.1061 +      hence "?N \<le> n" by auto
  4.1062 +
  4.1063 +      have "1 / r < real (natfloor (1/r) + 1)" using real_natfloor_add_one_gt
  4.1064 +        by (simp add: real_of_nat_Suc)
  4.1065 +      also have "... < 2^?N" by (rule two_realpow_gt)
  4.1066 +      finally have less_r: "1 / 2^?N < r" using `0 < r`
  4.1067 +        by (auto simp: less_divide_eq divide_less_eq algebra_simps)
  4.1068 +
  4.1069 +      have "f t < real (natfloor (f t) + 1)" using real_natfloor_add_one_gt[of "f t"] by auto
  4.1070 +      also have "... \<le> real n" unfolding real_of_nat_le_iff using N by auto
  4.1071 +      finally have "f t < real n" .
  4.1072 +
  4.1073 +      have "real (natfloor (f t * 2^n)) \<le> f t * 2^n"
  4.1074 +        using nonneg[OF t] by (auto intro!: real_natfloor_le mult_nonneg_nonneg)
  4.1075 +      hence less: "real (natfloor (f t * 2^n)) / 2^n \<le> f t" unfolding divide_le_eq by auto
  4.1076 +
  4.1077 +      have "f t * 2 ^ n - 1 < real (natfloor (f t * 2^n))" using real_natfloor_gt_diff_one .
  4.1078 +      hence "f t - real (natfloor (f t * 2^n)) / 2^n < 1 / 2^n"
  4.1079 +        by (auto simp: less_divide_eq divide_less_eq algebra_simps)
  4.1080 +      also have "... \<le> 1 / 2^?N" using `?N \<le> n`
  4.1081 +        by (auto intro!: divide_left_mono mult_pos_pos simp del: power_Suc)
  4.1082 +      also have "... < r" using less_r .
  4.1083 +      finally show "norm (?w n t - f t) < r" using `f t < real n` less by auto
  4.1084 +    qed
  4.1085 +  qed
  4.1086 +
  4.1087 +  fix n
  4.1088 +  show "?x n \<in> psfis (?u n)"
  4.1089 +  proof (rule psfis_intro)
  4.1090 +    show "?A n ` ?I n \<subseteq> sets M"
  4.1091 +    proof safe
  4.1092 +      fix i :: nat
  4.1093 +      from Int[OF
  4.1094 +        f_borel[unfolded borel_measurable_less_iff, rule_format, of "real (i+1) / 2^n"]
  4.1095 +        f_borel[unfolded borel_measurable_ge_iff, rule_format, of "real i / 2^n"]]
  4.1096 +      show "?A n i \<in> sets M"
  4.1097 +        by (metis Collect_conj_eq Int_commute Int_left_absorb Int_left_commute)
  4.1098 +    qed
  4.1099 +    show "nonneg (\<lambda>i :: nat. real i / 2 ^ n)"
  4.1100 +      unfolding nonneg_def by (auto intro!: divide_nonneg_pos)
  4.1101 +  qed auto
  4.1102 +qed
  4.1103 +
  4.1104 +lemma nnfis_dom_conv:
  4.1105 +  assumes borel: "f \<in> borel_measurable M"
  4.1106 +  and nnfis: "b \<in> nnfis g"
  4.1107 +  and ord: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
  4.1108 +  and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
  4.1109 +  shows "\<exists>a. a \<in> nnfis f \<and> a \<le> b"
  4.1110 +proof -
  4.1111 +  obtain u x where mc_f: "mono_convergent u f (space M)" and
  4.1112 +    psfis: "\<And>n. x n \<in> psfis (u n)"
  4.1113 +    using borel_measurable_mon_conv_psfis[OF borel nonneg] by auto
  4.1114 +
  4.1115 +  { fix n
  4.1116 +    { fix t assume t: "t \<in> space M"
  4.1117 +      note mono_convergent_le[OF mc_f this, of n]
  4.1118 +      also note ord[OF t]
  4.1119 +      finally have "u n t \<le> g t" . }
  4.1120 +    from nnfis_mono[OF psfis_nnfis[OF psfis] nnfis this]
  4.1121 +    have "x n \<le> b" by simp }
  4.1122 +  note x_less_b = this
  4.1123 +
  4.1124 +  have "convergent x"
  4.1125 +  proof (safe intro!: Bseq_mono_convergent)
  4.1126 +    from x_less_b pos_psfis[OF psfis]
  4.1127 +    show "Bseq x" by (auto intro!: BseqI'[of _ b])
  4.1128 +
  4.1129 +    fix n m :: nat assume *: "n \<le> m"
  4.1130 +    show "x n \<le> x m"
  4.1131 +    proof (rule psfis_mono[OF `x n \<in> psfis (u n)` `x m \<in> psfis (u m)`])
  4.1132 +      fix t assume "t \<in> space M"
  4.1133 +      from mc_f[THEN mono_convergentD(1), unfolded incseq_def, OF this]
  4.1134 +      show "u n t \<le> u m t" using * by auto
  4.1135 +    qed
  4.1136 +  qed
  4.1137 +  then obtain a where "x ----> a" unfolding convergent_def by auto
  4.1138 +  with LIMSEQ_le_const2[OF `x ----> a`] x_less_b mc_f psfis
  4.1139 +  show ?thesis unfolding nnfis_def by auto
  4.1140 +qed
  4.1141 +
  4.1142 +lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
  4.1143 +  unfolding psfis_def pos_simple_def pos_simple_integral_def
  4.1144 +  by (auto simp: nonneg_def
  4.1145 +      intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
  4.1146 +
  4.1147 +lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"
  4.1148 +  by (auto intro: the_equality nnfis_unique)
  4.1149 +
  4.1150 +lemma nnfis_cong:
  4.1151 +  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
  4.1152 +  shows "nnfis f = nnfis g"
  4.1153 +proof -
  4.1154 +  { fix f g :: "'a \<Rightarrow> real" assume cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
  4.1155 +    fix x assume "x \<in> nnfis f"
  4.1156 +    then guess u y unfolding nnfis_def by safe note x = this
  4.1157 +    hence "mono_convergent u g (space M)"
  4.1158 +      unfolding mono_convergent_def using cong by auto
  4.1159 +    with x(2,3) have "x \<in> nnfis g" unfolding nnfis_def by auto }
  4.1160 +  from this[OF cong] this[OF cong[symmetric]]
  4.1161 +  show ?thesis by safe
  4.1162 +qed
  4.1163 +
  4.1164 +lemma integral_cong:
  4.1165 +  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
  4.1166 +  shows "integral f = integral g"
  4.1167 +proof -
  4.1168 +  have "nnfis (pos_part f) = nnfis (pos_part g)"
  4.1169 +    using cong by (auto simp: pos_part_def intro!: nnfis_cong)
  4.1170 +  moreover
  4.1171 +  have "nnfis (neg_part f) = nnfis (neg_part g)"
  4.1172 +    using cong by (auto simp: neg_part_def intro!: nnfis_cong)
  4.1173 +  ultimately show ?thesis
  4.1174 +    unfolding integral_def by auto
  4.1175 +qed
  4.1176 +
  4.1177 +lemma nnfis_integral:
  4.1178 +  assumes "a \<in> nnfis f"
  4.1179 +  shows "integrable f" and "integral f = a"
  4.1180 +proof -
  4.1181 +  have a: "a \<in> nnfis (pos_part f)"
  4.1182 +    using assms nnfis_pos_on_mspace[OF assms]
  4.1183 +    by (auto intro!: nnfis_mon_conv[of "\<lambda>i. f" _ "\<lambda>i. a"]
  4.1184 +      LIMSEQ_const simp: mono_convergent_def pos_part_def incseq_def max_def)
  4.1185 +
  4.1186 +  have "\<And>t. t \<in> space M \<Longrightarrow> neg_part f t = 0"
  4.1187 +    unfolding neg_part_def min_def
  4.1188 +    using nnfis_pos_on_mspace[OF assms] by auto
  4.1189 +  hence 0: "0 \<in> nnfis (neg_part f)"
  4.1190 +    by (auto simp: nnfis_def mono_convergent_def psfis_0 incseq_def
  4.1191 +          intro!: LIMSEQ_const exI[of _ "\<lambda> x n. 0"] exI[of _ "\<lambda> n. 0"])
  4.1192 +
  4.1193 +  from 0 a show "integrable f" "integral f = a"
  4.1194 +    unfolding integrable_def integral_def by auto
  4.1195 +qed
  4.1196 +
  4.1197 +lemma nnfis_minus_nnfis_integral:
  4.1198 +  assumes "a \<in> nnfis f" and "b \<in> nnfis g"
  4.1199 +  shows "integrable (\<lambda>t. f t - g t)" and "integral (\<lambda>t. f t - g t) = a - b"
  4.1200 +proof -
  4.1201 +  have borel: "(\<lambda>t. f t - g t) \<in> borel_measurable M" using assms
  4.1202 +    by (blast intro:
  4.1203 +      borel_measurable_diff_borel_measurable nnfis_borel_measurable)
  4.1204 +
  4.1205 +  have "\<exists>x. x \<in> nnfis (pos_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
  4.1206 +    (is "\<exists>x. x \<in> nnfis ?pp \<and> _")
  4.1207 +  proof (rule nnfis_dom_conv)
  4.1208 +    show "?pp \<in> borel_measurable M"
  4.1209 +      using borel by (rule pos_part_neg_part_borel_measurable)
  4.1210 +    show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
  4.1211 +    fix t assume "t \<in> space M"
  4.1212 +    with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
  4.1213 +    show "?pp t \<le> f t + g t" unfolding pos_part_def by auto
  4.1214 +    show "0 \<le> ?pp t" using nonneg_pos_part[of "\<lambda>t. f t - g t"]
  4.1215 +      unfolding nonneg_def by auto
  4.1216 +  qed
  4.1217 +  then obtain x where x: "x \<in> nnfis ?pp" by auto
  4.1218 +  moreover
  4.1219 +  have "\<exists>x. x \<in> nnfis (neg_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
  4.1220 +    (is "\<exists>x. x \<in> nnfis ?np \<and> _")
  4.1221 +  proof (rule nnfis_dom_conv)
  4.1222 +    show "?np \<in> borel_measurable M"
  4.1223 +      using borel by (rule pos_part_neg_part_borel_measurable)
  4.1224 +    show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
  4.1225 +    fix t assume "t \<in> space M"
  4.1226 +    with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
  4.1227 +    show "?np t \<le> f t + g t" unfolding neg_part_def by auto
  4.1228 +    show "0 \<le> ?np t" using nonneg_neg_part[of "\<lambda>t. f t - g t"]
  4.1229 +      unfolding nonneg_def by auto
  4.1230 +  qed
  4.1231 +  then obtain y where y: "y \<in> nnfis ?np" by auto
  4.1232 +  ultimately show "integrable (\<lambda>t. f t - g t)"
  4.1233 +    unfolding integrable_def by auto
  4.1234 +
  4.1235 +  from x and y
  4.1236 +  have "a + y \<in> nnfis (\<lambda>t. f t + ?np t)"
  4.1237 +    and "b + x \<in> nnfis (\<lambda>t. g t + ?pp t)" using assms by (auto intro: nnfis_add)
  4.1238 +  moreover
  4.1239 +  have "\<And>t. f t + ?np t = g t + ?pp t"
  4.1240 +    unfolding pos_part_def neg_part_def by auto
  4.1241 +  ultimately have "a - b = x - y"
  4.1242 +    using nnfis_unique by (auto simp: algebra_simps)
  4.1243 +  thus "integral (\<lambda>t. f t - g t) = a - b"
  4.1244 +    unfolding integral_def
  4.1245 +    using the_nnfis[OF x] the_nnfis[OF y] by simp
  4.1246 +qed
  4.1247 +
  4.1248 +lemma integral_borel_measurable:
  4.1249 +  "integrable f \<Longrightarrow> f \<in> borel_measurable M"
  4.1250 +  unfolding integrable_def
  4.1251 +  by (subst pos_part_neg_part_borel_measurable_iff)
  4.1252 +   (auto intro: nnfis_borel_measurable)
  4.1253 +
  4.1254 +lemma integral_indicator_fn:
  4.1255 +  assumes "a \<in> sets M"
  4.1256 +  shows "integral (indicator_fn a) = measure M a"
  4.1257 +  and "integrable (indicator_fn a)"
  4.1258 +  using psfis_indicator[OF assms, THEN psfis_nnfis]
  4.1259 +  by (auto intro!: nnfis_integral)
  4.1260 +
  4.1261 +lemma integral_add:
  4.1262 +  assumes "integrable f" and "integrable g"
  4.1263 +  shows "integrable (\<lambda>t. f t + g t)"
  4.1264 +  and "integral (\<lambda>t. f t + g t) = integral f + integral g"
  4.1265 +proof -
  4.1266 +  { fix t
  4.1267 +    have "pos_part f t + pos_part g t - (neg_part f t + neg_part g t) =
  4.1268 +      f t + g t"
  4.1269 +      unfolding pos_part_def neg_part_def by auto }
  4.1270 +  note part_sum = this
  4.1271 +
  4.1272 +  from assms obtain a b c d where
  4.1273 +    a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
  4.1274 +    c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
  4.1275 +    unfolding integrable_def by auto
  4.1276 +  note sums = nnfis_add[OF a c] nnfis_add[OF b d]
  4.1277 +  note int = nnfis_minus_nnfis_integral[OF sums, unfolded part_sum]
  4.1278 +
  4.1279 +  show "integrable (\<lambda>t. f t + g t)" using int(1) .
  4.1280 +
  4.1281 +  show "integral (\<lambda>t. f t + g t) = integral f + integral g"
  4.1282 +    using int(2) sums a b c d by (simp add: the_nnfis integral_def)
  4.1283 +qed
  4.1284 +
  4.1285 +lemma integral_mono:
  4.1286 +  assumes "integrable f" and "integrable g"
  4.1287 +  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
  4.1288 +  shows "integral f \<le> integral g"
  4.1289 +proof -
  4.1290 +  from assms obtain a b c d where
  4.1291 +    a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
  4.1292 +    c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
  4.1293 +    unfolding integrable_def by auto
  4.1294 +
  4.1295 +  have "a \<le> c"
  4.1296 +  proof (rule nnfis_mono[OF a c])
  4.1297 +    fix t assume "t \<in> space M"
  4.1298 +    from mono[OF this] show "pos_part f t \<le> pos_part g t"
  4.1299 +      unfolding pos_part_def by auto
  4.1300 +  qed
  4.1301 +  moreover have "d \<le> b"
  4.1302 +  proof (rule nnfis_mono[OF d b])
  4.1303 +    fix t assume "t \<in> space M"
  4.1304 +    from mono[OF this] show "neg_part g t \<le> neg_part f t"
  4.1305 +      unfolding neg_part_def by auto
  4.1306 +  qed
  4.1307 +  ultimately have "a - b \<le> c - d" by auto
  4.1308 +  thus ?thesis unfolding integral_def
  4.1309 +    using a b c d by (simp add: the_nnfis)
  4.1310 +qed
  4.1311 +
  4.1312 +lemma integral_uminus:
  4.1313 +  assumes "integrable f"
  4.1314 +  shows "integrable (\<lambda>t. - f t)"
  4.1315 +  and "integral (\<lambda>t. - f t) = - integral f"
  4.1316 +proof -
  4.1317 +  have "pos_part f = neg_part (\<lambda>t.-f t)" and "neg_part f = pos_part (\<lambda>t.-f t)"
  4.1318 +    unfolding pos_part_def neg_part_def by (auto intro!: ext)
  4.1319 +  with assms show "integrable (\<lambda>t.-f t)" and "integral (\<lambda>t.-f t) = -integral f"
  4.1320 +    unfolding integrable_def integral_def by simp_all
  4.1321 +qed
  4.1322 +
  4.1323 +lemma integral_times_const:
  4.1324 +  assumes "integrable f"
  4.1325 +  shows "integrable (\<lambda>t. a * f t)" (is "?P a")
  4.1326 +  and "integral (\<lambda>t. a * f t) = a * integral f" (is "?I a")
  4.1327 +proof -
  4.1328 +  { fix a :: real assume "0 \<le> a"
  4.1329 +    hence "pos_part (\<lambda>t. a * f t) = (\<lambda>t. a * pos_part f t)"
  4.1330 +      and "neg_part (\<lambda>t. a * f t) = (\<lambda>t. a * neg_part f t)"
  4.1331 +      unfolding pos_part_def neg_part_def max_def min_def
  4.1332 +      by (auto intro!: ext simp: zero_le_mult_iff)
  4.1333 +    moreover
  4.1334 +    obtain x y where x: "x \<in> nnfis (pos_part f)" and y: "y \<in> nnfis (neg_part f)"
  4.1335 +      using assms unfolding integrable_def by auto
  4.1336 +    ultimately
  4.1337 +    have "a * x \<in> nnfis (pos_part (\<lambda>t. a * f t))" and
  4.1338 +      "a * y \<in> nnfis (neg_part (\<lambda>t. a * f t))"
  4.1339 +      using nnfis_times[OF _ `0 \<le> a`] by auto
  4.1340 +    with x y have "?P a \<and> ?I a"
  4.1341 +      unfolding integrable_def integral_def by (auto simp: algebra_simps) }
  4.1342 +  note int = this
  4.1343 +
  4.1344 +  have "?P a \<and> ?I a"
  4.1345 +  proof (cases "0 \<le> a")
  4.1346 +    case True from int[OF this] show ?thesis .
  4.1347 +  next
  4.1348 +    case False with int[of "- a"] integral_uminus[of "\<lambda>t. - a * f t"]
  4.1349 +    show ?thesis by auto
  4.1350 +  qed
  4.1351 +  thus "integrable (\<lambda>t. a * f t)"
  4.1352 +    and "integral (\<lambda>t. a * f t) = a * integral f" by simp_all
  4.1353 +qed
  4.1354 +
  4.1355 +lemma integral_cmul_indicator:
  4.1356 +  assumes "s \<in> sets M"
  4.1357 +  shows "integral (\<lambda>x. c * indicator_fn s x) = c * (measure M s)"
  4.1358 +  and "integrable (\<lambda>x. c * indicator_fn s x)"
  4.1359 +using assms integral_times_const integral_indicator_fn by auto
  4.1360 +
  4.1361 +lemma integral_zero:
  4.1362 +  shows "integral (\<lambda>x. 0) = 0"
  4.1363 +  and "integrable (\<lambda>x. 0)"
  4.1364 +  using integral_cmul_indicator[OF empty_sets, of 0]
  4.1365 +  unfolding indicator_fn_def by auto
  4.1366 +
  4.1367 +lemma integral_setsum:
  4.1368 +  assumes "finite S"
  4.1369 +  assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"
  4.1370 +  shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
  4.1371 +    and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I s")
  4.1372 +proof -
  4.1373 +  from assms have "?int S \<and> ?I S"
  4.1374 +  proof (induct S)
  4.1375 +    case empty thus ?case by (simp add: integral_zero)
  4.1376 +  next
  4.1377 +    case (insert i S)
  4.1378 +    thus ?case
  4.1379 +      apply simp
  4.1380 +      apply (subst integral_add)
  4.1381 +      using assms apply auto
  4.1382 +      apply (subst integral_add)
  4.1383 +      using assms by auto
  4.1384 +  qed
  4.1385 +  thus "?int S" and "?I S" by auto
  4.1386 +qed
  4.1387 +
  4.1388 +lemma markov_ineq:
  4.1389 +  assumes "integrable f" "0 < a" "integrable (\<lambda>x. \<bar>f x\<bar>^n)"
  4.1390 +  shows "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
  4.1391 +using assms
  4.1392 +proof -
  4.1393 +  from assms have "0 < a ^ n" using real_root_pow_pos by auto
  4.1394 +  from assms have "f \<in> borel_measurable M"
  4.1395 +    using integral_borel_measurable[OF `integrable f`] by auto
  4.1396 +  hence w: "{w . w \<in> space M \<and> a \<le> f w} \<in> sets M"
  4.1397 +    using borel_measurable_ge_iff by auto
  4.1398 +  have i: "integrable (indicator_fn {w . w \<in> space M \<and> a \<le> f w})"
  4.1399 +    using integral_indicator_fn[OF w] by simp
  4.1400 +  have v1: "\<And> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t 
  4.1401 +            \<le> (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t"
  4.1402 +    unfolding indicator_fn_def
  4.1403 +    using `0 < a` power_mono[of a] assms by auto
  4.1404 +  have v2: "\<And> t. (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t \<le> \<bar>f t\<bar> ^ n"
  4.1405 +    unfolding indicator_fn_def 
  4.1406 +    using power_mono[of a _ n] abs_ge_self `a > 0` 
  4.1407 +    by auto
  4.1408 +  have "{w \<in> space M. a \<le> f w} \<inter> space M = {w . a \<le> f w} \<inter> space M"
  4.1409 +    using Collect_eq by auto
  4.1410 +  from Int_absorb2[OF sets_into_space[OF w]] `0 < a ^ n` sets_into_space[OF w] w this
  4.1411 +  have "(a ^ n) * (measure M ((f -` {y . a \<le> y}) \<inter> space M)) =
  4.1412 +        (a ^ n) * measure M {w . w \<in> space M \<and> a \<le> f w}"
  4.1413 +    unfolding vimage_Collect_eq[of f] by simp
  4.1414 +  also have "\<dots> = integral (\<lambda> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t)"
  4.1415 +    using integral_cmul_indicator[OF w] i by auto
  4.1416 +  also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"
  4.1417 +    apply (rule integral_mono)
  4.1418 +    using integral_cmul_indicator[OF w]
  4.1419 +      `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto
  4.1420 +  finally show "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
  4.1421 +    unfolding atLeast_def
  4.1422 +    by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
  4.1423 +qed
  4.1424 +
  4.1425 +lemma integral_finite_on_sets:
  4.1426 +  assumes "f \<in> borel_measurable M" and "finite (space M)" and "a \<in> sets M"
  4.1427 +  shows "integral (\<lambda>x. f x * indicator_fn a x) =
  4.1428 +    (\<Sum> r \<in> f`a. r * measure M (f -` {r} \<inter> a))" (is "integral ?f = _")
  4.1429 +proof -
  4.1430 +  { fix x assume "x \<in> a"
  4.1431 +    with assms have "f -` {f x} \<inter> space M \<in> sets M"
  4.1432 +      by (subst Int_commute)
  4.1433 +         (auto simp: vimage_def Int_def
  4.1434 +               intro!: borel_measurable_const
  4.1435 +                      borel_measurable_eq_borel_measurable)
  4.1436 +    from Int[OF this assms(3)]
  4.1437 +         sets_into_space[OF assms(3), THEN Int_absorb1]
  4.1438 +    have "f -` {f x} \<inter> a \<in> sets M" by (simp add: Int_assoc) }
  4.1439 +  note vimage_f = this
  4.1440 +
  4.1441 +  have "finite a"
  4.1442 +    using assms(2,3) sets_into_space
  4.1443 +    by (auto intro: finite_subset)
  4.1444 +
  4.1445 +  have "integral (\<lambda>x. f x * indicator_fn a x) =
  4.1446 +    integral (\<lambda>x. \<Sum>i\<in>f ` a. i * indicator_fn (f -` {i} \<inter> a) x)"
  4.1447 +    (is "_ = integral (\<lambda>x. setsum (?f x) _)")
  4.1448 +    unfolding indicator_fn_def if_distrib
  4.1449 +    using `finite a` by (auto simp: setsum_cases intro!: integral_cong)
  4.1450 +  also have "\<dots> = (\<Sum>i\<in>f`a. integral (\<lambda>x. ?f x i))"
  4.1451 +  proof (rule integral_setsum, safe)
  4.1452 +    fix n x assume "x \<in> a"
  4.1453 +    thus "integrable (\<lambda>y. ?f y (f x))"
  4.1454 +      using integral_indicator_fn(2)[OF vimage_f]
  4.1455 +      by (auto intro!: integral_times_const)
  4.1456 +  qed (simp add: `finite a`)
  4.1457 +  also have "\<dots> = (\<Sum>i\<in>f`a. i * measure M (f -` {i} \<inter> a))"
  4.1458 +    using integral_cmul_indicator[OF vimage_f]
  4.1459 +    by (auto intro!: setsum_cong)
  4.1460 +  finally show ?thesis .
  4.1461 +qed
  4.1462 +
  4.1463 +lemma integral_finite:
  4.1464 +  assumes "f \<in> borel_measurable M" and "finite (space M)"
  4.1465 +  shows "integral f = (\<Sum> r \<in> f ` space M. r * measure M (f -` {r} \<inter> space M))"
  4.1466 +  using integral_finite_on_sets[OF assms top]
  4.1467 +    integral_cong[of "\<lambda>x. f x * indicator_fn (space M) x" f]
  4.1468 +  by (auto simp add: indicator_fn_def)
  4.1469 +
  4.1470 +lemma integral_finite_singleton:
  4.1471 +  assumes fin: "finite (space M)" and "Pow (space M) = sets M"
  4.1472 +  shows "integral f = (\<Sum>x \<in> space M. f x * measure M {x})"
  4.1473 +proof -
  4.1474 +  have "f \<in> borel_measurable M"
  4.1475 +    unfolding borel_measurable_le_iff
  4.1476 +    using assms by auto
  4.1477 +  { fix r let ?x = "f -` {r} \<inter> space M"
  4.1478 +    have "?x \<subseteq> space M" by auto
  4.1479 +    with assms have "measure M ?x = (\<Sum>i \<in> ?x. measure M {i})"
  4.1480 +      by (auto intro!: measure_real_sum_image) }
  4.1481 +  note measure_eq_setsum = this
  4.1482 +  show ?thesis
  4.1483 +    unfolding integral_finite[OF `f \<in> borel_measurable M` fin]
  4.1484 +      measure_eq_setsum setsum_right_distrib
  4.1485 +    apply (subst setsum_Sigma)
  4.1486 +    apply (simp add: assms)
  4.1487 +    apply (simp add: assms)
  4.1488 +  proof (rule setsum_reindex_cong[symmetric])
  4.1489 +    fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
  4.1490 +    thus "(\<lambda>(x, y). x * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}"
  4.1491 +      by auto
  4.1492 +  qed (auto intro!: image_eqI inj_onI)
  4.1493 +qed
  4.1494 +
  4.1495 +lemma borel_measurable_inverse:
  4.1496 +  assumes "f \<in> borel_measurable M"
  4.1497 +  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
  4.1498 +  unfolding borel_measurable_ge_iff
  4.1499 +proof (safe, rule linorder_cases)
  4.1500 +  fix a :: real assume "0 < a"
  4.1501 +  { fix w
  4.1502 +    from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
  4.1503 +      by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
  4.1504 +                linorder_not_le real_le_refl real_le_trans real_less_def
  4.1505 +                xt1(7) zero_less_divide_1_iff) }
  4.1506 +  hence "{w \<in> space M. a \<le> inverse (f w)} =
  4.1507 +    {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
  4.1508 +  with Int assms[unfolded borel_measurable_gr_iff]
  4.1509 +    assms[unfolded borel_measurable_le_iff]
  4.1510 +  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
  4.1511 +next
  4.1512 +  fix a :: real assume "0 = a"
  4.1513 +  { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
  4.1514 +      unfolding `0 = a`[symmetric] by auto }
  4.1515 +  thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
  4.1516 +    using assms[unfolded borel_measurable_ge_iff] by simp
  4.1517 +next
  4.1518 +  fix a :: real assume "a < 0"
  4.1519 +  { fix w
  4.1520 +    from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
  4.1521 +      apply (cases "0 \<le> f w")
  4.1522 +      apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
  4.1523 +                   zero_le_divide_1_iff)
  4.1524 +      apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
  4.1525 +                   linorder_not_le real_le_refl real_le_trans)
  4.1526 +      done }
  4.1527 +  hence "{w \<in> space M. a \<le> inverse (f w)} =
  4.1528 +    {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
  4.1529 +  with Un assms[unfolded borel_measurable_ge_iff]
  4.1530 +    assms[unfolded borel_measurable_le_iff]
  4.1531 +  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
  4.1532 +qed
  4.1533 +
  4.1534 +lemma borel_measurable_divide:
  4.1535 +  assumes "f \<in> borel_measurable M"
  4.1536 +  and "g \<in> borel_measurable M"
  4.1537 +  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
  4.1538 +  unfolding field_divide_inverse
  4.1539 +  by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
  4.1540 +
  4.1541 +lemma RN_deriv_finite_singleton:
  4.1542 +  fixes v :: "'a set \<Rightarrow> real"
  4.1543 +  assumes finite: "finite (space M)" and Pow: "Pow (space M) = sets M"
  4.1544 +  and ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
  4.1545 +  and eq_0: "\<And>x. measure M {x} = 0 \<Longrightarrow> v {x} = 0"
  4.1546 +  and "x \<in> space M" and "measure M {x} \<noteq> 0"
  4.1547 +  shows "RN_deriv v x = v {x} / (measure M {x})" (is "_ = ?v x")
  4.1548 +  unfolding RN_deriv_def
  4.1549 +proof (rule someI2_ex[where Q = "\<lambda>f. f x = ?v x"], rule exI[where x = ?v], safe)
  4.1550 +  show "(\<lambda>a. v {a} / measure_space.measure M {a}) \<in> borel_measurable M"
  4.1551 +    unfolding borel_measurable_le_iff using Pow by auto
  4.1552 +next
  4.1553 +  fix a assume "a \<in> sets M"
  4.1554 +  hence "a \<subseteq> space M" and "finite a"
  4.1555 +    using sets_into_space finite by (auto intro: finite_subset)
  4.1556 +  have *: "\<And>x a. (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) =
  4.1557 +    v {x} * indicator_fn a x" using eq_0 by auto
  4.1558 +
  4.1559 +  from measure_space.measure_real_sum_image[OF ms_v, of a]
  4.1560 +    Pow `a \<in> sets M` sets_into_space `finite a`
  4.1561 +  have "v a = (\<Sum>x\<in>a. v {x})" by auto
  4.1562 +  thus "integral (\<lambda>x. v {x} / measure_space.measure M {x} * indicator_fn a x) = v a"
  4.1563 +    apply (simp add: eq_0 integral_finite_singleton[OF finite Pow])
  4.1564 +    apply (unfold divide_1)
  4.1565 +    by (simp add: * indicator_fn_def if_distrib setsum_cases finite `a \<subseteq> space M` Int_absorb1)
  4.1566 +next
  4.1567 +  fix w assume "w \<in> borel_measurable M"
  4.1568 +  assume int_eq_v: "\<forall>a\<in>sets M. integral (\<lambda>x. w x * indicator_fn a x) = v a"
  4.1569 +  have "{x} \<in> sets M" using Pow `x \<in> space M` by auto
  4.1570 +
  4.1571 +  have "w x * measure M {x} =
  4.1572 +    (\<Sum>y\<in>space M. w y * indicator_fn {x} y * measure M {y})"
  4.1573 +    apply (subst (3) mult_commute)
  4.1574 +    unfolding indicator_fn_def if_distrib setsum_cases[OF finite]
  4.1575 +    using `x \<in> space M` by simp
  4.1576 +  also have "... = v {x}"
  4.1577 +    using int_eq_v[rule_format, OF `{x} \<in> sets M`]
  4.1578 +    by (simp add: integral_finite_singleton[OF finite Pow])
  4.1579 +  finally show "w x = v {x} / measure M {x}"
  4.1580 +    using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
  4.1581 +qed fact
  4.1582 +
  4.1583 +lemma countable_space_integral_reduce:
  4.1584 +  assumes "positive M (measure M)" and "f \<in> borel_measurable M"
  4.1585 +  and "countable (f ` space M)"
  4.1586 +  and "\<not> finite (pos_part f ` space M)"
  4.1587 +  and "\<not> finite (neg_part f ` space M)"
  4.1588 +  and "((\<lambda>r. r * measure m (neg_part f -` {r} \<inter> space m)) o enumerate (neg_part f ` space M)) sums n"
  4.1589 +  and "((\<lambda>r. r * measure m (pos_part f -` {r} \<inter> space m)) o enumerate (pos_part f ` space M)) sums p"
  4.1590 +  shows "integral f = p - n"
  4.1591 +oops
  4.1592 +
  4.1593 +(*
  4.1594 +val countable_space_integral_reduce = store_thm
  4.1595 +  ("countable_space_integral_reduce",
  4.1596 +   "\<forall>m f p n. measure_space m \<and>
  4.1597 +	     positive m \<and>
  4.1598 +	     f \<in> borel_measurable (space m, sets m) \<and>
  4.1599 +	     countable (IMAGE f (space m)) \<and>
  4.1600 +	     ~(FINITE (IMAGE (pos_part f) (space m))) \<and>
  4.1601 +	     ~(FINITE (IMAGE (neg_part f) (space m))) \<and>
  4.1602 +	     (\<lambda>r. r *
  4.1603 +		  measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
  4.1604 +		enumerate ((IMAGE (neg_part f) (space m))) sums n \<and>
  4.1605 +	     (\<lambda>r. r *
  4.1606 +		  measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
  4.1607 +		enumerate ((IMAGE (pos_part f) (space m))) sums p ==>
  4.1608 +	     (integral m f = p - n)",
  4.1609 +   RW_TAC std_ss [integral_def]
  4.1610 +   ++ Suff `((@i. i \<in> nnfis m (pos_part f)) = p) \<and> ((@i. i \<in> nnfis m (neg_part f)) = n)`
  4.1611 +   >> RW_TAC std_ss []
  4.1612 +   ++ (CONJ_TAC ++ MATCH_MP_TAC SELECT_UNIQUE ++ RW_TAC std_ss [])
  4.1613 +   >> (Suff `p \<in> nnfis m (pos_part f)` >> METIS_TAC [nnfis_unique]
  4.1614 +       ++ MATCH_MP_TAC nnfis_mon_conv
  4.1615 +       ++ `BIJ (enumerate(IMAGE (pos_part f) (space m))) UNIV (IMAGE (pos_part f) (space m))`
  4.1616 +		by (`countable (IMAGE (pos_part f) (space m))`
  4.1617 +			by (MATCH_MP_TAC COUNTABLE_SUBSET
  4.1618 +			    ++ Q.EXISTS_TAC `0 INSERT (IMAGE f (space m))`
  4.1619 +			    ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, pos_part_def, COUNTABLE_INSERT, IN_INSERT]
  4.1620 +			    ++ METIS_TAC [])
  4.1621 +		     ++ METIS_TAC [COUNTABLE_ALT])
  4.1622 +       ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
  4.1623 +       ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m)))
  4.1624 +			(pred_set$count n) then pos_part f t else 0)`
  4.1625 +       ++ Q.EXISTS_TAC `(\<lambda>n.
  4.1626 +         sum (0,n)
  4.1627 +           ((\<lambda>r.
  4.1628 +               r *
  4.1629 +               measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
  4.1630 +            enumerate (IMAGE (pos_part f) (space m))))`
  4.1631 +       ++ ASM_SIMP_TAC std_ss []
  4.1632 +       ++ CONJ_TAC
  4.1633 +       >> (RW_TAC std_ss [mono_convergent_def]
  4.1634 +	   >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, pos_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS])
  4.1635 +	   ++ RW_TAC std_ss [SEQ]
  4.1636 +	   ++ `\<exists>N. enumerate (IMAGE (pos_part f) (space m)) N = (pos_part f) t`
  4.1637 +		by METIS_TAC [IN_IMAGE]
  4.1638 +	   ++ Q.EXISTS_TAC `SUC N`
  4.1639 +	   ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
  4.1640 +	   ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
  4.1641 +	   ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, pos_part_def])
  4.1642 +       ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
  4.1643 +	   ++ `(\<lambda>t. (if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m))) (pred_set$count n')
  4.1644 +      			then pos_part f t else  0)) =
  4.1645 +		(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
  4.1646 +			indicator_fn ((\<lambda>i. PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i}
  4.1647 +					   \<inter> (space m)) i) t)
  4.1648 +		     (pred_set$count n'))`
  4.1649 +		by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
  4.1650 +		    >> (`pred_set$count n' = x INSERT (pred_set$count n')`
  4.1651 +				by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
  4.1652 +			++ POP_ORW
  4.1653 +			++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
  4.1654 +			++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
  4.1655 +				REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
  4.1656 +			++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
  4.1657 +			++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
  4.1658 +				enumerate (IMAGE (pos_part f) (space m)) x' *
  4.1659 +				(if enumerate (IMAGE (pos_part f) (space m)) x =
  4.1660 +				enumerate (IMAGE (pos_part f) (space m)) x'
  4.1661 +				then 1 else 0) else 0)) = (\<lambda>x. 0)`
  4.1662 +				by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
  4.1663 +			++ POP_ORW
  4.1664 +			++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
  4.1665 +		    ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
  4.1666 +		    >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
  4.1667 +		    ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
  4.1668 +			REAL_SUM_IMAGE_IN_IF]
  4.1669 +		    ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
  4.1670 +			(\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i *
  4.1671 +           		(if (pos_part f t = enumerate (IMAGE (pos_part f) (space m)) i) \<and>
  4.1672 +             		 t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
  4.1673 +			by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
  4.1674 +		    ++ POP_ORW
  4.1675 +		    ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
  4.1676 +	   ++ POP_ORW
  4.1677 +	   ++ `((\<lambda>r. r * measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
  4.1678 +		enumerate (IMAGE (pos_part f) (space m))) =
  4.1679 +		(\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
  4.1680 +			measure m ((\<lambda>i.
  4.1681 +                PREIMAGE (pos_part f)
  4.1682 +                  {enumerate (IMAGE (pos_part f) (space m)) i} \<inter>
  4.1683 +                space m) i))`
  4.1684 +		by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
  4.1685 +	   ++ POP_ORW
  4.1686 +	   ++ MATCH_MP_TAC psfis_intro
  4.1687 +	   ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
  4.1688 +	   ++ REVERSE CONJ_TAC
  4.1689 +	   >> (FULL_SIMP_TAC real_ss [IN_IMAGE, pos_part_def]
  4.1690 +	       ++ METIS_TAC [REAL_LE_REFL])
  4.1691 +	   ++ `(pos_part f) \<in> borel_measurable (space m, sets m)`
  4.1692 +		by METIS_TAC [pos_part_neg_part_borel_measurable]
  4.1693 +	   ++ REPEAT STRIP_TAC
  4.1694 +	   ++ `PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i} \<inter> space m =
  4.1695 +		{w | w \<in> space m \<and> ((pos_part f) w = (\<lambda>w. enumerate (IMAGE (pos_part f) (space m)) i) w)}`
  4.1696 +		by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
  4.1697 +		    ++ DECIDE_TAC)
  4.1698 +	   ++ POP_ORW
  4.1699 +	   ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
  4.1700 +	   ++ METIS_TAC [borel_measurable_const, measure_space_def])
  4.1701 +   ++ Suff `n \<in> nnfis m (neg_part f)` >> METIS_TAC [nnfis_unique]
  4.1702 +   ++ MATCH_MP_TAC nnfis_mon_conv
  4.1703 +   ++ `BIJ (enumerate(IMAGE (neg_part f) (space m))) UNIV (IMAGE (neg_part f) (space m))`
  4.1704 +		by (`countable (IMAGE (neg_part f) (space m))`
  4.1705 +			by (MATCH_MP_TAC COUNTABLE_SUBSET
  4.1706 +			    ++ Q.EXISTS_TAC `0 INSERT (IMAGE abs (IMAGE f (space m)))`
  4.1707 +			    ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, abs, neg_part_def, COUNTABLE_INSERT, IN_INSERT, COUNTABLE_IMAGE]
  4.1708 +			    ++ METIS_TAC [])
  4.1709 +		     ++ METIS_TAC [COUNTABLE_ALT])
  4.1710 +   ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
  4.1711 +   ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m)))
  4.1712 +			(pred_set$count n) then neg_part f t else 0)`
  4.1713 +   ++ Q.EXISTS_TAC `(\<lambda>n.
  4.1714 +         sum (0,n)
  4.1715 +           ((\<lambda>r.
  4.1716 +               r *
  4.1717 +               measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
  4.1718 +            enumerate (IMAGE (neg_part f) (space m))))`
  4.1719 +   ++ ASM_SIMP_TAC std_ss []
  4.1720 +   ++ CONJ_TAC
  4.1721 +   >> (RW_TAC std_ss [mono_convergent_def]
  4.1722 +	   >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, neg_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS, REAL_LE_NEGTOTAL])
  4.1723 +	   ++ RW_TAC std_ss [SEQ]
  4.1724 +	   ++ `\<exists>N. enumerate (IMAGE (neg_part f) (space m)) N = (neg_part f) t`
  4.1725 +		by METIS_TAC [IN_IMAGE]
  4.1726 +	   ++ Q.EXISTS_TAC `SUC N`
  4.1727 +	   ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
  4.1728 +	   ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
  4.1729 +	   ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, neg_part_def])
  4.1730 +   ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
  4.1731 +	   ++ `(\<lambda>t. (if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m))) (pred_set$count n')
  4.1732 +      			then neg_part f t else  0)) =
  4.1733 +		(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
  4.1734 +			indicator_fn ((\<lambda>i. PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i}
  4.1735 +					   \<inter> (space m)) i) t)
  4.1736 +		     (pred_set$count n'))`
  4.1737 +		by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
  4.1738 +		    >> (`pred_set$count n' = x INSERT (pred_set$count n')`
  4.1739 +				by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
  4.1740 +			++ POP_ORW
  4.1741 +			++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
  4.1742 +			++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
  4.1743 +				REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
  4.1744 +			++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
  4.1745 +			++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
  4.1746 +				enumerate (IMAGE (neg_part f) (space m)) x' *
  4.1747 +				(if enumerate (IMAGE (neg_part f) (space m)) x =
  4.1748 +				enumerate (IMAGE (neg_part f) (space m)) x'
  4.1749 +				then 1 else 0) else 0)) = (\<lambda>x. 0)`
  4.1750 +				by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
  4.1751 +			++ POP_ORW
  4.1752 +			++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
  4.1753 +		    ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
  4.1754 +		    >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
  4.1755 +		    ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
  4.1756 +			REAL_SUM_IMAGE_IN_IF]
  4.1757 +		    ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
  4.1758 +			(\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i *
  4.1759 +           		(if (neg_part f t = enumerate (IMAGE (neg_part f) (space m)) i) \<and>
  4.1760 +             		 t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
  4.1761 +			by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
  4.1762 +		    ++ POP_ORW
  4.1763 +		    ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
  4.1764 +	   ++ POP_ORW
  4.1765 +	   ++ `((\<lambda>r. r * measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
  4.1766 +		enumerate (IMAGE (neg_part f) (space m))) =
  4.1767 +		(\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
  4.1768 +			measure m ((\<lambda>i.
  4.1769 +                PREIMAGE (neg_part f)
  4.1770 +                  {enumerate (IMAGE (neg_part f) (space m)) i} \<inter>
  4.1771 +                space m) i))`
  4.1772 +		by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
  4.1773 +	   ++ POP_ORW
  4.1774 +	   ++ MATCH_MP_TAC psfis_intro
  4.1775 +	   ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
  4.1776 +	   ++ REVERSE CONJ_TAC
  4.1777 +	   >> (FULL_SIMP_TAC real_ss [IN_IMAGE, neg_part_def]
  4.1778 +	       ++ METIS_TAC [REAL_LE_REFL, REAL_LE_NEGTOTAL])
  4.1779 +	   ++ `(neg_part f) \<in> borel_measurable (space m, sets m)`
  4.1780 +		by METIS_TAC [pos_part_neg_part_borel_measurable]
  4.1781 +	   ++ REPEAT STRIP_TAC
  4.1782 +	   ++ `PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i} \<inter> space m =
  4.1783 +		{w | w \<in> space m \<and> ((neg_part f) w = (\<lambda>w. enumerate (IMAGE (neg_part f) (space m)) i) w)}`
  4.1784 +		by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
  4.1785 +		    ++ DECIDE_TAC)
  4.1786 +	   ++ POP_ORW
  4.1787 +	   ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
  4.1788 +	   ++ METIS_TAC [borel_measurable_const, measure_space_def]);
  4.1789 +*)
  4.1790 +
  4.1791 +end
  4.1792 +
  4.1793 +end
  4.1794 \ No newline at end of file
     5.1 --- a/src/HOL/Probability/Measure.thy	Thu Mar 04 19:50:45 2010 +0100
     5.2 +++ b/src/HOL/Probability/Measure.thy	Thu Mar 04 21:52:26 2010 +0100
     5.3 @@ -104,7 +104,7 @@
     5.4    have ra: "range (binaryset A B) \<subseteq> sets M"
     5.5     by (simp add: range_binaryset_eq empty A B) 
     5.6   have di:  "disjoint_family (binaryset A B)" using disj
     5.7 -   by (simp add: disjoint_family_def binaryset_def Int_commute) 
     5.8 +   by (simp add: disjoint_family_on_def binaryset_def Int_commute) 
     5.9   from closed_cdi_Disj [OF cdi ra di]
    5.10   show ?thesis
    5.11     by (simp add: UN_binaryset_eq) 
    5.12 @@ -118,7 +118,7 @@
    5.13    have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
    5.14      by (simp add: range_binaryset_eq  A B empty_sets smallest_ccdi_sets.Basic)
    5.15    have di:  "disjoint_family (binaryset A B)" using disj
    5.16 -    by (simp add: disjoint_family_def binaryset_def Int_commute) 
    5.17 +    by (simp add: disjoint_family_on_def binaryset_def Int_commute) 
    5.18    from Disj [OF ra di]
    5.19    show ?thesis
    5.20      by (simp add: UN_binaryset_eq) 
    5.21 @@ -164,7 +164,7 @@
    5.22    have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
    5.23      by blast
    5.24    moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
    5.25 -    by (auto simp add: disjoint_family_def) 
    5.26 +    by (auto simp add: disjoint_family_on_def) 
    5.27    ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
    5.28      by (rule smallest_ccdi_sets.Disj) 
    5.29    show ?case
    5.30 @@ -208,7 +208,7 @@
    5.31    have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
    5.32      by blast
    5.33    moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
    5.34 -    by (auto simp add: disjoint_family_def) 
    5.35 +    by (auto simp add: disjoint_family_on_def) 
    5.36    ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
    5.37      by (rule smallest_ccdi_sets.Disj) 
    5.38    show ?case
    5.39 @@ -355,7 +355,7 @@
    5.40    hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
    5.41      by (metis add_commute le_add_diff_inverse nat_less_le)
    5.42    thus ?thesis
    5.43 -    by (auto simp add: disjoint_family_def)
    5.44 +    by (auto simp add: disjoint_family_on_def)
    5.45        (metis insert_absorb insert_subset le_SucE le_antisym not_leE) 
    5.46  qed
    5.47  
    5.48 @@ -642,7 +642,7 @@
    5.49                    show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
    5.50                      using f12 rA2 by (auto simp add: measurable_def)
    5.51                    show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
    5.52 -                    by (auto simp add: disjoint_family_def) 
    5.53 +                    by (auto simp add: disjoint_family_on_def) 
    5.54                    show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
    5.55                      proof (rule sigma_algebra.countable_UN [OF sa1])
    5.56                        show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
    5.57 @@ -820,7 +820,98 @@
    5.58    thus ?thesis
    5.59      by (metis subset_refl s)
    5.60  qed
    5.61 -  
    5.62 +
    5.63 +lemma (in measure_space) measure_finitely_additive':
    5.64 +  assumes "f \<in> ({0 :: nat ..< n} \<rightarrow> sets M)"
    5.65 +  assumes "\<And> a b. \<lbrakk>a < n ; b < n ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
    5.66 +  assumes "s = \<Union> (f ` {0 ..< n})"
    5.67 +  shows "(\<Sum> i \<in> {0 ..< n}. (measure M \<circ> f) i) = measure M s"
    5.68 +proof -
    5.69 +  def f' == "\<lambda> i. (if i < n then f i else {})"
    5.70 +  have rf: "range f' \<subseteq> sets M" unfolding f'_def 
    5.71 +    using assms empty_sets by auto
    5.72 +  have df: "disjoint_family f'" unfolding f'_def disjoint_family_on_def 
    5.73 +    using assms by simp
    5.74 +  have "\<Union> range f' = (\<Union> i \<in> {0 ..< n}. f i)" 
    5.75 +    unfolding f'_def by auto
    5.76 +  then have "measure M s = measure M (\<Union> range f')" 
    5.77 +    using assms by simp
    5.78 +  then have part1: "(\<lambda> i. measure M (f' i)) sums measure M s" 
    5.79 +    using df rf ca[unfolded countably_additive_def, rule_format, of f']
    5.80 +    by auto
    5.81 +
    5.82 +  have "(\<lambda> i. measure M (f' i)) sums (\<Sum> i \<in> {0 ..< n}. measure M (f' i))" 
    5.83 +    using series_zero[of "n" "\<lambda> i. measure M (f' i)", rule_format] 
    5.84 +    unfolding f'_def by simp
    5.85 +  also have "\<dots> = (\<Sum> i \<in> {0 ..< n}. measure M (f i))" 
    5.86 +    unfolding f'_def by auto
    5.87 +  finally have part2: "(\<lambda> i. measure M (f' i)) sums (\<Sum> i \<in> {0 ..< n}. measure M (f i))" by simp
    5.88 +  show ?thesis 
    5.89 +    using sums_unique[OF part1] 
    5.90 +          sums_unique[OF part2] by auto
    5.91 +qed
    5.92 +
    5.93 +
    5.94 +lemma (in measure_space) measure_finitely_additive:
    5.95 +  assumes "finite r"
    5.96 +  assumes "r \<subseteq> sets M"
    5.97 +  assumes d: "\<And> a b. \<lbrakk>a \<in> r ; b \<in> r ; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
    5.98 +  shows "(\<Sum> i \<in> r. measure M i) = measure M (\<Union> r)"
    5.99 +using assms
   5.100 +proof -
   5.101 +  (* counting the elements in r is enough *)
   5.102 +  let ?R = "{0 ..< card r}"
   5.103 +  obtain f where f: "f ` ?R = r" "inj_on f ?R"
   5.104 +    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite r`]
   5.105 +    by auto
   5.106 +  hence f_into_sets: "f \<in> ?R \<rightarrow> sets M" using assms by auto
   5.107 +  have disj: "\<And> a b. \<lbrakk>a \<in> ?R ; b \<in> ?R ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
   5.108 +  proof -
   5.109 +    fix a b assume asm: "a \<in> ?R" "b \<in> ?R" "a \<noteq> b"
   5.110 +    hence neq: "f a \<noteq> f b" using f[unfolded inj_on_def, rule_format] by blast
   5.111 +    from asm have "f a \<in> r" "f b \<in> r" using f by auto
   5.112 +    thus "f a \<inter> f b = {}" using d[of "f a" "f b"] f using neq by auto
   5.113 +  qed
   5.114 +  have "(\<Union> r) = (\<Union> i \<in> ?R. f i)"
   5.115 +    using f by auto
   5.116 +  hence "measure M (\<Union> r)= measure M (\<Union> i \<in> ?R. f i)" by simp
   5.117 +  also have "\<dots> = (\<Sum> i \<in> ?R. measure M (f i))"
   5.118 +    using measure_finitely_additive'[OF f_into_sets disj] by simp
   5.119 +  also have "\<dots> = (\<Sum> a \<in> r. measure M a)" 
   5.120 +    using f[rule_format] setsum_reindex[of f ?R "\<lambda> a. measure M a"] by auto
   5.121 +  finally show ?thesis by simp
   5.122 +qed
   5.123 +
   5.124 +lemma (in measure_space) measure_finitely_additive'':
   5.125 +  assumes "finite s"
   5.126 +  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<in> sets M"
   5.127 +  assumes d: "disjoint_family_on a s"
   5.128 +  shows "(\<Sum> i \<in> s. measure M (a i)) = measure M (\<Union> i \<in> s. a i)"
   5.129 +using assms
   5.130 +proof -
   5.131 +  (* counting the elements in s is enough *)
   5.132 +  let ?R = "{0 ..< card s}"
   5.133 +  obtain f where f: "f ` ?R = s" "inj_on f ?R"
   5.134 +    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite s`]
   5.135 +    by auto
   5.136 +  hence f_into_sets: "a \<circ> f \<in> ?R \<rightarrow> sets M" using assms unfolding o_def by auto
   5.137 +  have disj: "\<And> i j. \<lbrakk>i \<in> ?R ; j \<in> ?R ; i \<noteq> j\<rbrakk> \<Longrightarrow> (a \<circ> f) i \<inter> (a \<circ> f) j = {}"
   5.138 +  proof -
   5.139 +    fix i j assume asm: "i \<in> ?R" "j \<in> ?R" "i \<noteq> j"
   5.140 +    hence neq: "f i \<noteq> f j" using f[unfolded inj_on_def, rule_format] by blast
   5.141 +    from asm have "f i \<in> s" "f j \<in> s" using f by auto
   5.142 +    thus "(a \<circ> f) i \<inter> (a \<circ> f) j = {}"
   5.143 +      using d f neq unfolding disjoint_family_on_def by auto
   5.144 +  qed
   5.145 +  have "(\<Union> i \<in> s. a i) = (\<Union> i \<in> f ` ?R. a i)" using f by auto
   5.146 +  hence "(\<Union> i \<in> s. a i) = (\<Union> i \<in> ?R. a (f i))" by auto
   5.147 +  hence "measure M (\<Union> i \<in> s. a i) = (\<Sum> i \<in> ?R. measure M (a (f i)))"
   5.148 +    using measure_finitely_additive'[OF f_into_sets disj] by simp
   5.149 +  also have "\<dots> = (\<Sum> i \<in> s. measure M (a i))"
   5.150 +    using f[rule_format] setsum_reindex[of f ?R "\<lambda> i. measure M (a i)"] by auto
   5.151 +  finally show ?thesis by simp
   5.152 +qed
   5.153 +
   5.154  lemma (in sigma_algebra) sigma_algebra_extend:
   5.155       "sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
   5.156     by unfold_locales (auto intro!: space_closed)
   5.157 @@ -845,7 +936,7 @@
   5.158        hence "finite (A ` I)"
   5.159          by (metis finite_UnionD finite_subset fin) 
   5.160        moreover have "inj_on A I" using disj
   5.161 -        by (auto simp add: I_def disjoint_family_def inj_on_def) 
   5.162 +        by (auto simp add: I_def disjoint_family_on_def inj_on_def) 
   5.163        ultimately have finI: "finite I"
   5.164          by (metis finite_imageD)
   5.165        hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
   5.166 @@ -873,7 +964,7 @@
   5.167            have "f (A n \<union> (\<Union> x<n. A x)) = f (A n) + f (\<Union> i<n. A i)"
   5.168              proof (rule Caratheodory.additiveD [OF addf])
   5.169                show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
   5.170 -                by (auto simp add: disjoint_family_def nat_less_le) blast
   5.171 +                by (auto simp add: disjoint_family_on_def nat_less_le) blast
   5.172                show "A n \<in> sets M" using A 
   5.173                  by (force simp add: Mf_def) 
   5.174                show "(\<Union>i<n. A i) \<in> sets M"
   5.175 @@ -906,5 +997,4 @@
   5.176        \<Longrightarrow> measure_space M"
   5.177    by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) 
   5.178  
   5.179 -end
   5.180 -
   5.181 +end
   5.182 \ No newline at end of file
     6.1 --- a/src/HOL/Probability/Probability.thy	Thu Mar 04 19:50:45 2010 +0100
     6.2 +++ b/src/HOL/Probability/Probability.thy	Thu Mar 04 21:52:26 2010 +0100
     6.3 @@ -1,5 +1,5 @@
     6.4  theory Probability
     6.5 -imports Measure Borel
     6.6 +imports Probability_Space
     6.7  begin
     6.8  
     6.9  end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Probability/Probability_Space.thy	Thu Mar 04 21:52:26 2010 +0100
     7.3 @@ -0,0 +1,458 @@
     7.4 +theory Probability_Space
     7.5 +imports Lebesgue
     7.6 +begin
     7.7 +
     7.8 +locale prob_space = measure_space +
     7.9 +  assumes prob_space: "measure M (space M) = 1"
    7.10 +begin
    7.11 +
    7.12 +abbreviation "events \<equiv> sets M"
    7.13 +abbreviation "prob \<equiv> measure M"
    7.14 +abbreviation "prob_preserving \<equiv> measure_preserving"
    7.15 +abbreviation "random_variable \<equiv> \<lambda> s X. X \<in> measurable M s"
    7.16 +abbreviation "expectation \<equiv> integral"
    7.17 +
    7.18 +definition
    7.19 +  "indep A B \<longleftrightarrow> A \<in> events \<and> B \<in> events \<and> prob (A \<inter> B) = prob A * prob B"
    7.20 +
    7.21 +definition
    7.22 +  "indep_families F G \<longleftrightarrow> (\<forall> A \<in> F. \<forall> B \<in> G. indep A B)"
    7.23 +
    7.24 +definition
    7.25 +  "distribution X = (\<lambda>s. prob ((X -` s) \<inter> (space M)))"
    7.26 +
    7.27 +definition
    7.28 +  "probably e \<longleftrightarrow> e \<in> events \<and> prob e = 1"
    7.29 +
    7.30 +definition
    7.31 +  "possibly e \<longleftrightarrow> e \<in> events \<and> prob e \<noteq> 0"
    7.32 +
    7.33 +definition
    7.34 +  "joint_distribution X Y \<equiv> (\<lambda>a. prob ((\<lambda>x. (X x, Y x)) -` a \<inter> space M))"
    7.35 +
    7.36 +definition
    7.37 +  "conditional_expectation X s \<equiv> THE f. random_variable borel_space f \<and>
    7.38 +    (\<forall> g \<in> s. integral (\<lambda>x. f x * indicator_fn g x) =
    7.39 +              integral (\<lambda>x. X x * indicator_fn g x))"
    7.40 +
    7.41 +definition
    7.42 +  "conditional_prob e1 e2 \<equiv> conditional_expectation (indicator_fn e1) e2"
    7.43 +
    7.44 +lemma positive: "positive M prob"
    7.45 +  unfolding positive_def using positive empty_measure by blast
    7.46 +
    7.47 +lemma prob_compl:
    7.48 +  assumes "s \<in> events"
    7.49 +  shows "prob (space M - s) = 1 - prob s"
    7.50 +using assms
    7.51 +proof -
    7.52 +  have "prob ((space M - s) \<union> s) = prob (space M - s) + prob s"
    7.53 +    using assms additive[unfolded additive_def] by blast
    7.54 +  thus ?thesis by (simp add:Un_absorb2[OF sets_into_space[OF assms]] prob_space)
    7.55 +qed
    7.56 +
    7.57 +lemma indep_space:
    7.58 +  assumes "s \<in> events"
    7.59 +  shows "indep (space M) s"
    7.60 +using assms prob_space
    7.61 +unfolding indep_def by auto
    7.62 +
    7.63 +
    7.64 +lemma prob_space_increasing:
    7.65 +  "increasing M prob"
    7.66 +by (rule additive_increasing[OF positive additive])
    7.67 +
    7.68 +lemma prob_subadditive:
    7.69 +  assumes "s \<in> events" "t \<in> events"
    7.70 +  shows "prob (s \<union> t) \<le> prob s + prob t"
    7.71 +using assms
    7.72 +proof -
    7.73 +  have "prob (s \<union> t) = prob ((s - t) \<union> t)" by simp
    7.74 +  also have "\<dots> = prob (s - t) + prob t"
    7.75 +    using additive[unfolded additive_def, rule_format, of "s-t" "t"] 
    7.76 +      assms by blast
    7.77 +  also have "\<dots> \<le> prob s + prob t"
    7.78 +    using prob_space_increasing[unfolded increasing_def, rule_format] assms
    7.79 +    by auto
    7.80 +  finally show ?thesis by simp
    7.81 +qed
    7.82 +
    7.83 +lemma prob_zero_union:
    7.84 +  assumes "s \<in> events" "t \<in> events" "prob t = 0"
    7.85 +  shows "prob (s \<union> t) = prob s"
    7.86 +using assms 
    7.87 +proof -
    7.88 +  have "prob (s \<union> t) \<le> prob s"
    7.89 +    using prob_subadditive[of s t] assms by auto
    7.90 +  moreover have "prob (s \<union> t) \<ge> prob s"
    7.91 +    using prob_space_increasing[unfolded increasing_def, rule_format] 
    7.92 +      assms by auto
    7.93 +  ultimately show ?thesis by simp
    7.94 +qed
    7.95 +
    7.96 +lemma prob_eq_compl:
    7.97 +  assumes "s \<in> events" "t \<in> events"
    7.98 +  assumes "prob (space M - s) = prob (space M - t)"
    7.99 +  shows "prob s = prob t"
   7.100 +using assms prob_compl by auto
   7.101 +
   7.102 +lemma prob_one_inter:
   7.103 +  assumes events:"s \<in> events" "t \<in> events"
   7.104 +  assumes "prob t = 1"
   7.105 +  shows "prob (s \<inter> t) = prob s"
   7.106 +using assms
   7.107 +proof -
   7.108 +  have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)" 
   7.109 +    using prob_compl[of "t"] prob_zero_union assms by auto
   7.110 +  then show "prob (s \<inter> t) = prob s" 
   7.111 +    using prob_eq_compl[of "s \<inter> t"] events by (simp only: Diff_Int) auto
   7.112 +qed
   7.113 +
   7.114 +lemma prob_eq_bigunion_image:
   7.115 +  assumes "range f \<subseteq> events" "range g \<subseteq> events"
   7.116 +  assumes "disjoint_family f" "disjoint_family g"
   7.117 +  assumes "\<And> n :: nat. prob (f n) = prob (g n)"
   7.118 +  shows "(prob (\<Union> i. f i) = prob (\<Union> i. g i))"
   7.119 +using assms 
   7.120 +proof -
   7.121 +  have a: "(\<lambda> i. prob (f i)) sums (prob (\<Union> i. f i))" 
   7.122 +    using ca[unfolded countably_additive_def] assms by blast
   7.123 +  have b: "(\<lambda> i. prob (g i)) sums (prob (\<Union> i. g i))"
   7.124 +    using ca[unfolded countably_additive_def] assms by blast
   7.125 +  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
   7.126 +qed
   7.127 +
   7.128 +lemma prob_countably_subadditive: 
   7.129 +  assumes "range f \<subseteq> events" 
   7.130 +  assumes "summable (prob \<circ> f)"
   7.131 +  shows "prob (\<Union>i. f i) \<le> (\<Sum> i. prob (f i))"
   7.132 +using assms
   7.133 +proof -
   7.134 +  def f' == "\<lambda> i. f i - (\<Union> j \<in> {0 ..< i}. f j)"
   7.135 +  have "(\<Union> i. f' i) \<subseteq> (\<Union> i. f i)" unfolding f'_def by auto
   7.136 +  moreover have "(\<Union> i. f' i) \<supseteq> (\<Union> i. f i)"
   7.137 +  proof (rule subsetI)
   7.138 +    fix x assume "x \<in> (\<Union> i. f i)"
   7.139 +    then obtain k where "x \<in> f k" by blast
   7.140 +    hence k: "k \<in> {m. x \<in> f m}" by simp
   7.141 +    have "\<exists> l. x \<in> f l \<and> (\<forall> l' < l. x \<notin> f l')"
   7.142 +      using wfE_min[of "{(x, y). x < y}" "k" "{m. x \<in> f m}", 
   7.143 +        OF wf_less k] by auto
   7.144 +    thus "x \<in> (\<Union> i. f' i)" unfolding f'_def by auto
   7.145 +  qed
   7.146 +  ultimately have uf'f: "(\<Union> i. f' i) = (\<Union> i. f i)" by (rule equalityI)
   7.147 +
   7.148 +  have df': "\<And> i j. i < j \<Longrightarrow> f' i \<inter> f' j = {}"
   7.149 +    unfolding f'_def by auto
   7.150 +  have "\<And> i j. i \<noteq> j \<Longrightarrow> f' i \<inter> f' j = {}"
   7.151 +    apply (drule iffD1[OF nat_neq_iff])
   7.152 +    using df' by auto
   7.153 +  hence df: "disjoint_family f'" unfolding disjoint_family_on_def by simp
   7.154 +
   7.155 +  have rf': "\<And> i. f' i \<in> events"
   7.156 +  proof -
   7.157 +    fix i :: nat
   7.158 +    have "(\<Union> {f j | j. j \<in> {0 ..< i}}) = (\<Union> j \<in> {0 ..< i}. f j)" by blast
   7.159 +    hence "(\<Union> {f j | j. j \<in> {0 ..< i}}) \<in> events 
   7.160 +      \<Longrightarrow> (\<Union> j \<in> {0 ..< i}. f j) \<in> events" by auto
   7.161 +    thus "f' i \<in> events" 
   7.162 +      unfolding f'_def 
   7.163 +      using assms finite_union[of "{f j | j. j \<in> {0 ..< i}}"]
   7.164 +        Diff[of "f i" "\<Union> j \<in> {0 ..< i}. f j"] by auto
   7.165 +  qed
   7.166 +  hence uf': "(\<Union> range f') \<in> events" by auto
   7.167 +  
   7.168 +  have "\<And> i. prob (f' i) \<le> prob (f i)"
   7.169 +    using prob_space_increasing[unfolded increasing_def, rule_format, OF rf']
   7.170 +      assms rf' unfolding f'_def by blast
   7.171 +
   7.172 +  hence absinc: "\<And> i. \<bar> prob (f' i) \<bar> \<le> prob (f i)"
   7.173 +    using abs_of_nonneg positive[unfolded positive_def]
   7.174 +      assms rf' by auto
   7.175 +
   7.176 +  have "prob (\<Union> i. f i) = prob (\<Union> i. f' i)" using uf'f by simp
   7.177 +
   7.178 +  also have "\<dots> = (\<Sum> i. prob (f' i))"
   7.179 +    using ca[unfolded countably_additive_def, rule_format]
   7.180 +    sums_unique rf' uf' df
   7.181 +    by auto
   7.182 +  
   7.183 +  also have "\<dots> \<le> (\<Sum> i. prob (f i))"
   7.184 +    using summable_le2[of "\<lambda> i. prob (f' i)" "\<lambda> i. prob (f i)", 
   7.185 +      rule_format, OF absinc]
   7.186 +      assms[unfolded o_def] by auto
   7.187 +
   7.188 +  finally show ?thesis by auto
   7.189 +qed
   7.190 +
   7.191 +lemma prob_countably_zero:
   7.192 +  assumes "range c \<subseteq> events"
   7.193 +  assumes "\<And> i. prob (c i) = 0"
   7.194 +  shows "(prob (\<Union> i :: nat. c i) = 0)"
   7.195 +  using assms
   7.196 +proof -
   7.197 +  have leq0: "0 \<le> prob (\<Union> i. c i)"
   7.198 +    using assms positive[unfolded positive_def, rule_format] 
   7.199 +    by auto
   7.200 +
   7.201 +  have "prob (\<Union> i. c i) \<le> (\<Sum> i. prob (c i))"
   7.202 +    using prob_countably_subadditive[of c, unfolded o_def]
   7.203 +      assms sums_zero sums_summable by auto
   7.204 +
   7.205 +  also have "\<dots> = 0"
   7.206 +    using assms sums_zero 
   7.207 +      sums_unique[of "\<lambda> i. prob (c i)" "0"] by auto
   7.208 +
   7.209 +  finally show "prob (\<Union> i. c i) = 0"
   7.210 +    using leq0 by auto
   7.211 +qed
   7.212 +
   7.213 +lemma indep_sym:
   7.214 +   "indep a b \<Longrightarrow> indep b a"
   7.215 +unfolding indep_def using Int_commute[of a b] by auto
   7.216 +
   7.217 +lemma indep_refl:
   7.218 +  assumes "a \<in> events"
   7.219 +  shows "indep a a = (prob a = 0) \<or> (prob a = 1)"
   7.220 +using assms unfolding indep_def by auto
   7.221 +
   7.222 +lemma prob_equiprobable_finite_unions:
   7.223 +  assumes "s \<in> events" 
   7.224 +  assumes "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
   7.225 +  assumes "finite s"
   7.226 +  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
   7.227 +  shows "prob s = of_nat (card s) * prob {SOME x. x \<in> s}"
   7.228 +using assms
   7.229 +proof (cases "s = {}")
   7.230 +  case True thus ?thesis by simp
   7.231 +next
   7.232 +  case False hence " \<exists> x. x \<in> s" by blast
   7.233 +  from someI_ex[OF this] assms
   7.234 +  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast
   7.235 +  have "prob s = (\<Sum> x \<in> s. prob {x})"
   7.236 +    using assms measure_real_sum_image by blast
   7.237 +  also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
   7.238 +  also have "\<dots> = of_nat (card s) * prob {(SOME x. x \<in> s)}"
   7.239 +    using setsum_constant assms by auto
   7.240 +  finally show ?thesis by simp
   7.241 +qed
   7.242 +
   7.243 +lemma prob_real_sum_image_fn:
   7.244 +  assumes "e \<in> events"
   7.245 +  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
   7.246 +  assumes "finite s"
   7.247 +  assumes "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
   7.248 +  assumes "space M \<subseteq> (\<Union> i \<in> s. f i)"
   7.249 +  shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
   7.250 +using assms
   7.251 +proof -
   7.252 +  let ?S = "{0 ..< card s}"
   7.253 +  obtain g where "g ` ?S = s \<and> inj_on g ?S"
   7.254 +    using ex_bij_betw_nat_finite[unfolded bij_betw_def, of s] assms by auto
   7.255 +  moreover hence gs: "g ` ?S = s" by simp
   7.256 +  ultimately have ginj: "inj_on g ?S" by simp
   7.257 +  let ?f' = "\<lambda> i. e \<inter> f (g i)"
   7.258 +  have f': "?f' \<in> ?S \<rightarrow> events"
   7.259 +    using gs assms by blast
   7.260 +  hence "\<And> i j. \<lbrakk>i \<in> ?S ; j \<in> ?S ; i \<noteq> j\<rbrakk> 
   7.261 +    \<Longrightarrow> ?f' i \<inter> ?f' j = {}" using assms ginj[unfolded inj_on_def] gs f' by blast
   7.262 +  hence df': "\<And> i j. \<lbrakk>i < card s ; j < card s ; i \<noteq> j\<rbrakk> 
   7.263 +    \<Longrightarrow> ?f' i \<inter> ?f' j = {}" by simp
   7.264 +
   7.265 +  have "e = e \<inter> space M" using assms sets_into_space by simp
   7.266 +  also hence "\<dots> = e \<inter> (\<Union> x \<in> s. f x)" using assms by blast
   7.267 +  also have "\<dots> = (\<Union> x \<in> g ` ?S. e \<inter> f x)" using gs by simp
   7.268 +  also have "\<dots> = (\<Union> i \<in> ?S. ?f' i)" by simp
   7.269 +  finally have "prob e = prob (\<Union> i \<in> ?S. ?f' i)" by simp
   7.270 +  also have "\<dots> = (\<Sum> i \<in> ?S. prob (?f' i))"
   7.271 +    apply (subst measure_finitely_additive'')
   7.272 +    using f' df' assms by (auto simp: disjoint_family_on_def)
   7.273 +  also have "\<dots> = (\<Sum> x \<in> g ` ?S. prob (e \<inter> f x))" 
   7.274 +    using setsum_reindex[of g "?S" "\<lambda> x. prob (e \<inter> f x)"]
   7.275 +      ginj by simp
   7.276 +  also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))" using gs by simp
   7.277 +  finally show ?thesis by simp
   7.278 +qed
   7.279 +
   7.280 +lemma distribution_prob_space:
   7.281 +  assumes "random_variable s X"
   7.282 +  shows "prob_space \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>"
   7.283 +using assms
   7.284 +proof -
   7.285 +  let ?N = "\<lparr>space = space s, sets = sets s, measure = distribution X\<rparr>"
   7.286 +  interpret s: sigma_algebra "s" using assms[unfolded measurable_def] by auto
   7.287 +  hence sigN: "sigma_algebra ?N" using s.sigma_algebra_extend by auto
   7.288 +
   7.289 +  have pos: "\<And> e. e \<in> sets s \<Longrightarrow> distribution X e \<ge> 0"
   7.290 +    unfolding distribution_def
   7.291 +    using positive[unfolded positive_def]
   7.292 +    assms[unfolded measurable_def] by auto
   7.293 +
   7.294 +  have cas: "countably_additive ?N (distribution X)"
   7.295 +  proof -
   7.296 +    {
   7.297 +      fix f :: "nat \<Rightarrow> 'c \<Rightarrow> bool"
   7.298 +      let ?g = "\<lambda> n. X -` f n \<inter> space M"
   7.299 +      assume asm: "range f \<subseteq> sets s" "UNION UNIV f \<in> sets s" "disjoint_family f"
   7.300 +      hence "range ?g \<subseteq> events" 
   7.301 +        using assms unfolding measurable_def by blast
   7.302 +      from ca[unfolded countably_additive_def, 
   7.303 +        rule_format, of ?g, OF this] countable_UN[OF this] asm
   7.304 +      have "(\<lambda> n. prob (?g n)) sums prob (UNION UNIV ?g)"
   7.305 +        unfolding disjoint_family_on_def by blast
   7.306 +      moreover have "(X -` (\<Union> n. f n)) = (\<Union> n. X -` f n)" by blast
   7.307 +      ultimately have "(\<lambda> n. distribution X (f n)) sums distribution X (UNION UNIV f)"
   7.308 +        unfolding distribution_def by simp
   7.309 +    } thus ?thesis unfolding countably_additive_def by simp
   7.310 +  qed
   7.311 +
   7.312 +  have ds0: "distribution X {} = 0"
   7.313 +    unfolding distribution_def by simp
   7.314 +
   7.315 +  have "X -` space s \<inter> space M = space M"
   7.316 +    using assms[unfolded measurable_def] by auto
   7.317 +  hence ds1: "distribution X (space s) = 1"
   7.318 +    unfolding measurable_def distribution_def using prob_space by simp
   7.319 +
   7.320 +  from ds0 ds1 cas pos sigN
   7.321 +  show "prob_space ?N"
   7.322 +    unfolding prob_space_def prob_space_axioms_def
   7.323 +    measure_space_def measure_space_axioms_def by simp
   7.324 +qed
   7.325 +
   7.326 +lemma distribution_lebesgue_thm1:
   7.327 +  assumes "random_variable s X"
   7.328 +  assumes "A \<in> sets s"
   7.329 +  shows "distribution X A = expectation (indicator_fn (X -` A \<inter> space M))"
   7.330 +unfolding distribution_def
   7.331 +using assms unfolding measurable_def
   7.332 +using integral_indicator_fn by auto
   7.333 +
   7.334 +lemma distribution_lebesgue_thm2:
   7.335 +  assumes "random_variable s X" "A \<in> sets s"
   7.336 +  shows "distribution X A = measure_space.integral \<lparr>space = space s, sets = sets s, measure = distribution X\<rparr> (indicator_fn A)"
   7.337 +  (is "_ = measure_space.integral ?M _")
   7.338 +proof -
   7.339 +  interpret S: prob_space ?M using assms(1) by (rule distribution_prob_space)
   7.340 +
   7.341 +  show ?thesis
   7.342 +    using S.integral_indicator_fn(1)
   7.343 +    using assms unfolding distribution_def by auto
   7.344 +qed
   7.345 +
   7.346 +lemma finite_expectation1:
   7.347 +  assumes "finite (space M)" "random_variable borel_space X"
   7.348 +  shows "expectation X = (\<Sum> r \<in> X ` space M. r * prob (X -` {r} \<inter> space M))"
   7.349 +  using assms integral_finite measurable_def
   7.350 +  unfolding borel_measurable_def by auto
   7.351 +
   7.352 +lemma finite_expectation:
   7.353 +  assumes "finite (space M) \<and> random_variable borel_space X"
   7.354 +  shows "expectation X = (\<Sum> r \<in> X ` (space M). r * distribution X {r})"
   7.355 +using assms unfolding distribution_def using finite_expectation1 by auto
   7.356 +
   7.357 +lemma finite_marginal_product_space_POW:
   7.358 +  assumes "Pow (space M) = events"
   7.359 +  assumes "random_variable \<lparr> space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
   7.360 +  assumes "random_variable \<lparr> space = Y ` (space M), sets = Pow (Y ` (space M))\<rparr> Y"
   7.361 +  assumes "finite (space M)"
   7.362 +  shows "measure_space \<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))),
   7.363 +  sets = Pow ((X ` (space M)) \<times> (Y ` (space M))),
   7.364 +  measure = (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))\<rparr>"
   7.365 +  using assms
   7.366 +proof -
   7.367 +  let "?S" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))), 
   7.368 +    sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"
   7.369 +  let "?M" = "\<lparr> space = ((X ` (space M)) \<times> (Y ` (space M))), 
   7.370 +    sets = Pow ((X ` (space M)) \<times> (Y ` (space M)))\<rparr>"
   7.371 +  have pos: "positive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))"
   7.372 +    unfolding positive_def using positive[unfolded positive_def] assms by auto
   7.373 +  { fix x y
   7.374 +    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms by auto
   7.375 +    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms by auto
   7.376 +    assume "x \<inter> y = {}"
   7.377 +    from additive[unfolded additive_def, rule_format, OF A B] this
   7.378 +    have "prob (((\<lambda>x. (X x, Y x)) -` x \<union>
   7.379 +      (\<lambda>x. (X x, Y x)) -` y) \<inter> space M) =
   7.380 +      prob ((\<lambda>x. (X x, Y x)) -` x \<inter> space M) +
   7.381 +      prob ((\<lambda>x. (X x, Y x)) -` y \<inter> space M)" 
   7.382 +      apply (subst Int_Un_distrib2)
   7.383 +      by auto }
   7.384 +  hence add: "additive ?S (\<lambda>a. prob ((\<lambda>x. (X x,Y x)) -` a \<inter> space M))"
   7.385 +    unfolding additive_def by auto
   7.386 +  interpret S: sigma_algebra "?S" 
   7.387 +    unfolding sigma_algebra_def algebra_def
   7.388 +      sigma_algebra_axioms_def by auto
   7.389 +  show ?thesis
   7.390 +     using add pos S.finite_additivity_sufficient assms by auto
   7.391 +qed
   7.392 +
   7.393 +lemma finite_marginal_product_space_POW2:
   7.394 +  assumes "Pow (space M) = events"
   7.395 +  assumes "random_variable \<lparr>space = s1, sets = Pow s1\<rparr> X"
   7.396 +  assumes "random_variable \<lparr>space = s2, sets = Pow s2\<rparr> Y"
   7.397 +  assumes "finite (space M)"
   7.398 +  assumes "finite s1" "finite s2"
   7.399 +  shows "measure_space \<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y\<rparr>"
   7.400 +proof -
   7.401 +  let "?S" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2) \<rparr>"
   7.402 +  let "?M" = "\<lparr> space = s1 \<times> s2, sets = Pow (s1 \<times> s2), measure = joint_distribution X Y \<rparr>"
   7.403 +  have pos: "positive ?S (joint_distribution X Y)" using positive
   7.404 +    unfolding positive_def joint_distribution_def using assms by auto
   7.405 +  { fix x y
   7.406 +    have A: "((\<lambda>x. (X x, Y x)) -` x) \<inter> space M \<in> sets M" using assms by auto
   7.407 +    have B: "((\<lambda>x. (X x, Y x)) -` y) \<inter> space M \<in> sets M" using assms by auto
   7.408 +    assume "x \<inter> y = {}"
   7.409 +    from additive[unfolded additive_def, rule_format, OF A B] this
   7.410 +    have "prob (((\<lambda>x. (X x, Y x)) -` x \<union>
   7.411 +      (\<lambda>x. (X x, Y x)) -` y) \<inter> space M) =
   7.412 +      prob ((\<lambda>x. (X x, Y x)) -` x \<inter> space M) +
   7.413 +      prob ((\<lambda>x. (X x, Y x)) -` y \<inter> space M)" 
   7.414 +      apply (subst Int_Un_distrib2)
   7.415 +      by auto }
   7.416 +  hence add: "additive ?S (joint_distribution X Y)"
   7.417 +    unfolding additive_def joint_distribution_def by auto
   7.418 +  interpret S: sigma_algebra "?S" 
   7.419 +    unfolding sigma_algebra_def algebra_def
   7.420 +      sigma_algebra_axioms_def by auto
   7.421 +  show ?thesis
   7.422 +     using add pos S.finite_additivity_sufficient assms by auto
   7.423 +qed
   7.424 +
   7.425 +lemma prob_x_eq_1_imp_prob_y_eq_0:
   7.426 +  assumes "{x} \<in> events"
   7.427 +  assumes "(prob {x} = 1)"
   7.428 +  assumes "{y} \<in> events"
   7.429 +  assumes "y \<noteq> x"
   7.430 +  shows "prob {y} = 0"
   7.431 +  using prob_one_inter[of "{y}" "{x}"] assms by auto
   7.432 +
   7.433 +lemma distribution_x_eq_1_imp_distribution_y_eq_0:
   7.434 +  assumes X: "random_variable \<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr> X"
   7.435 +  assumes "(distribution X {x} = 1)"
   7.436 +  assumes "y \<noteq> x"
   7.437 +  shows "distribution X {y} = 0"
   7.438 +proof -
   7.439 +  let ?S = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M))\<rparr>"
   7.440 +  let ?M = "\<lparr>space = X ` (space M), sets = Pow (X ` (space M)), measure = distribution X\<rparr>"
   7.441 +  interpret S: prob_space ?M
   7.442 +    using distribution_prob_space[OF X] by auto
   7.443 +  { assume "{x} \<notin> sets ?M"
   7.444 +    hence "x \<notin> X ` space M" by auto
   7.445 +    hence "X -` {x} \<inter> space M = {}" by auto
   7.446 +    hence "distribution X {x} = 0" unfolding distribution_def by auto
   7.447 +    hence "False" using assms by auto }
   7.448 +  hence x: "{x} \<in> sets ?M" by auto
   7.449 +  { assume "{y} \<notin> sets ?M"
   7.450 +    hence "y \<notin> X ` space M" by auto
   7.451 +    hence "X -` {y} \<inter> space M = {}" by auto
   7.452 +    hence "distribution X {y} = 0" unfolding distribution_def by auto }
   7.453 +  moreover
   7.454 +  { assume "{y} \<in> sets ?M"
   7.455 +    hence "distribution X {y} = 0" using assms S.prob_x_eq_1_imp_prob_y_eq_0[OF x] by auto }
   7.456 +  ultimately show ?thesis by auto
   7.457 +qed
   7.458 +
   7.459 +end
   7.460 +
   7.461 +end