add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
authorhoelzl
Fri Dec 05 12:06:18 2014 +0100 (2014-12-05)
changeset 59092d469103c0737
parent 59091 4c8205fe3644
child 59093 2b106e58a177
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
CONTRIBUTORS
src/HOL/Probability/Embed_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Interval_Integral.thy
src/HOL/Probability/Lebesgue_Integral_Substitution.thy
src/HOL/Probability/Probability.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Set_Integral.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/Stream_Space.thy
     1.1 --- a/CONTRIBUTORS	Thu Dec 04 21:28:35 2014 +0100
     1.2 +++ b/CONTRIBUTORS	Fri Dec 05 12:06:18 2014 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM and Jeremy Avigad, Luke Serafin, CMU
     1.8 +  Various integration theorems: mostly integration on intervals and substitution.
     1.9 +
    1.10  * September 2014: Florian Haftmann, TUM
    1.11    Lexicographic order on functions and
    1.12    sum/product over function bodies.
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Probability/Embed_Measure.thy	Fri Dec 05 12:06:18 2014 +0100
     2.3 @@ -0,0 +1,343 @@
     2.4 +(*  Title:      HOL/Probability/Embed_Measure.thy
     2.5 +    Author:     Manuel Eberl, TU München
     2.6 +
     2.7 +    Defines measure embeddings with injective functions, i.e. lifting a measure on some values 
     2.8 +    to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a 
     2.9 +    measure on the left part of the sum type 'a + 'b)
    2.10 +*)
    2.11 +
    2.12 +section {* Embed Measure Spaces with a Function *}
    2.13 +
    2.14 +theory Embed_Measure
    2.15 +imports Binary_Product_Measure
    2.16 +begin
    2.17 +
    2.18 +definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
    2.19 +  "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M} 
    2.20 +                           (\<lambda>A. emeasure M (f -` A \<inter> space M))"
    2.21 +
    2.22 +lemma space_embed_measure: "space (embed_measure M f) = f ` space M"
    2.23 +  unfolding embed_measure_def 
    2.24 +  by (subst space_measure_of) (auto dest: sets.sets_into_space)
    2.25 +
    2.26 +lemma sets_embed_measure':
    2.27 +  assumes inj: "inj_on f (space M)" 
    2.28 +  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
    2.29 +  unfolding embed_measure_def
    2.30 +proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI)
    2.31 +  fix s assume "s \<in> {f ` A |A. A \<in> sets M}"
    2.32 +  then obtain s' where s'_props: "s = f ` s'" "s' \<in> sets M" by auto
    2.33 +  hence "f ` space M - s = f ` (space M - s')" using inj
    2.34 +    by (auto dest: inj_onD sets.sets_into_space)
    2.35 +  also have "... \<in> {f ` A |A. A \<in> sets M}" using s'_props by auto
    2.36 +  finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" .
    2.37 +next
    2.38 +  fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}"
    2.39 +  then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
    2.40 +    by (auto simp: subset_eq choice_iff)
    2.41 +  moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
    2.42 +  ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" by blast
    2.43 +qed (auto dest: sets.sets_into_space)
    2.44 +
    2.45 +lemma the_inv_into_vimage:
    2.46 +  "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A"
    2.47 +  by (auto simp: the_inv_into_f_f)
    2.48 +
    2.49 +lemma sets_embed_eq_vimage_algebra:
    2.50 +  assumes "inj_on f (space M)"
    2.51 +  shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
    2.52 +  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image
    2.53 +           dest: sets.sets_into_space
    2.54 +           intro!: image_cong the_inv_into_vimage[symmetric])
    2.55 +
    2.56 +lemma sets_embed_measure:
    2.57 +  assumes inj: "inj f" 
    2.58 +  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
    2.59 +  using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD)
    2.60 +
    2.61 +lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)"
    2.62 +  unfolding embed_measure_def
    2.63 +  by (intro in_measure_of) (auto dest: sets.sets_into_space)
    2.64 +
    2.65 +lemma measurable_embed_measure1:
    2.66 +  assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N" 
    2.67 +  shows "g \<in> measurable (embed_measure M f) N"
    2.68 +  unfolding measurable_def
    2.69 +proof safe
    2.70 +  fix A assume "A \<in> sets N"
    2.71 +  with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M"
    2.72 +    by (rule measurable_sets)
    2.73 +  then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)"
    2.74 +    by (rule in_sets_embed_measure)
    2.75 +  also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)"
    2.76 +    by (auto simp: space_embed_measure)
    2.77 +  finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" .
    2.78 +qed (insert measurable_space[OF assms], auto simp: space_embed_measure)
    2.79 +
    2.80 +lemma measurable_embed_measure2':
    2.81 +  assumes "inj_on f (space M)" 
    2.82 +  shows "f \<in> measurable M (embed_measure M f)"
    2.83 +proof-
    2.84 +  {
    2.85 +    fix A assume A: "A \<in> sets M"
    2.86 +    also from this have "A = A \<inter> space M" by auto
    2.87 +    also have "... = f -` f ` A \<inter> space M" using A assms
    2.88 +      by (auto dest: inj_onD sets.sets_into_space)
    2.89 +    finally have "f -` f ` A \<inter> space M \<in> sets M" .
    2.90 +  }
    2.91 +  thus ?thesis using assms unfolding embed_measure_def
    2.92 +    by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
    2.93 +qed
    2.94 +
    2.95 +lemma measurable_embed_measure2:
    2.96 +  assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)"
    2.97 +  by (auto simp: inj_vimage_image_eq embed_measure_def
    2.98 +           intro!: measurable_measure_of dest: sets.sets_into_space)
    2.99 +
   2.100 +lemma embed_measure_eq_distr':
   2.101 +  assumes "inj_on f (space M)"
   2.102 +  shows "embed_measure M f = distr M (embed_measure M f) f"
   2.103 +proof-
   2.104 +  have "distr M (embed_measure M f) f = 
   2.105 +            measure_of (f ` space M) {f ` A |A. A \<in> sets M}
   2.106 +                       (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def
   2.107 +      by (simp add: space_embed_measure sets_embed_measure'[OF assms])
   2.108 +  also have "... = embed_measure M f" unfolding embed_measure_def ..
   2.109 +  finally show ?thesis ..
   2.110 +qed
   2.111 +
   2.112 +lemma embed_measure_eq_distr:
   2.113 +    "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
   2.114 +  by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
   2.115 +
   2.116 +lemma nn_integral_embed_measure:
   2.117 +  "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   2.118 +  nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
   2.119 +  apply (subst embed_measure_eq_distr, simp)
   2.120 +  apply (subst nn_integral_distr)
   2.121 +  apply (simp_all add: measurable_embed_measure2)
   2.122 +  done
   2.123 +
   2.124 +lemma emeasure_embed_measure':
   2.125 +    assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
   2.126 +    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
   2.127 +  by (subst embed_measure_eq_distr'[OF assms(1)])
   2.128 +     (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)])
   2.129 +
   2.130 +lemma emeasure_embed_measure:
   2.131 +    assumes "inj f" "A \<in> sets (embed_measure M f)"
   2.132 +    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
   2.133 + using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD)
   2.134 +
   2.135 +lemma embed_measure_comp: 
   2.136 +  assumes [simp]: "inj f" "inj g"
   2.137 +  shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
   2.138 +proof-
   2.139 +  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)
   2.140 +  note measurable_embed_measure2[measurable]
   2.141 +  have "embed_measure (embed_measure M f) g = 
   2.142 +            distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
   2.143 +      by (subst (1 2) embed_measure_eq_distr) 
   2.144 +         (simp_all add: distr_distr sets_embed_measure cong: distr_cong)
   2.145 +  also have "... = embed_measure M (g \<circ> f)"
   2.146 +      by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
   2.147 +         (auto simp: sets_embed_measure o_def image_image[symmetric] 
   2.148 +               intro: inj_comp cong: distr_cong)
   2.149 +  finally show ?thesis .
   2.150 +qed
   2.151 +
   2.152 +lemma sigma_finite_embed_measure:
   2.153 +  assumes "sigma_finite_measure M" and inj: "inj f"
   2.154 +  shows "sigma_finite_measure (embed_measure M f)"
   2.155 +proof
   2.156 +  case goal1
   2.157 +  from assms(1) interpret sigma_finite_measure M .
   2.158 +  from sigma_finite_countable obtain A where
   2.159 +      A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast
   2.160 +  show ?case
   2.161 +  proof (intro exI[of _ "op ` f`A"] conjI allI)
   2.162 +    from A_props show "countable (op ` f`A)" by auto
   2.163 +    from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)" 
   2.164 +      by (auto simp: sets_embed_measure)
   2.165 +    from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"
   2.166 +      by (auto simp: space_embed_measure intro!: imageI)
   2.167 +    from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
   2.168 +      by (intro ballI, subst emeasure_embed_measure)
   2.169 +         (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
   2.170 +  qed
   2.171 +qed
   2.172 +
   2.173 +lemma embed_measure_count_space: 
   2.174 +    "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
   2.175 +  apply (subst distr_bij_count_space[of f A "f`A", symmetric])
   2.176 +  apply (simp add: inj_on_def bij_betw_def)
   2.177 +  apply (subst embed_measure_eq_distr)
   2.178 +  apply simp
   2.179 +  apply (auto intro!: measure_eqI imageI simp: sets_embed_measure subset_image_iff)
   2.180 +  apply blast
   2.181 +  apply (subst (1 2) emeasure_distr)
   2.182 +  apply (auto simp: space_embed_measure sets_embed_measure)
   2.183 +  done
   2.184 +
   2.185 +lemma sets_embed_measure_alt:
   2.186 +    "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
   2.187 +  by (auto simp: sets_embed_measure)
   2.188 +
   2.189 +lemma emeasure_embed_measure_image':
   2.190 +  assumes "inj_on f (space M)" "X \<in> sets M"
   2.191 +  shows "emeasure (embed_measure M f) (f`X) = emeasure M X"
   2.192 +proof-
   2.193 +  from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)"
   2.194 +    by (subst emeasure_embed_measure') (auto simp: sets_embed_measure')
   2.195 +  also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space)
   2.196 +  finally show ?thesis .
   2.197 +qed
   2.198 +
   2.199 +lemma emeasure_embed_measure_image:
   2.200 +    "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X"
   2.201 +  by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq)
   2.202 +
   2.203 +lemma embed_measure_eq_iff:
   2.204 +  assumes "inj f"
   2.205 +  shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
   2.206 +proof
   2.207 +  from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)
   2.208 +  assume asm: "?M = ?N"
   2.209 +  hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
   2.210 +  with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
   2.211 +  moreover {
   2.212 +    fix X assume "X \<in> sets A"
   2.213 +    from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp
   2.214 +    with `X \<in> sets A` and `sets A = sets B` and assms 
   2.215 +        have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image)
   2.216 +  }
   2.217 +  ultimately show "A = B" by (rule measure_eqI)
   2.218 +qed simp
   2.219 +
   2.220 +lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A"
   2.221 +  by (auto simp: the_inv_into_f_f)
   2.222 +
   2.223 +lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)"
   2.224 +  using map_prod_surj_on[OF refl refl] .
   2.225 +
   2.226 +lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"
   2.227 +  by auto
   2.228 +
   2.229 +lemma embed_measure_prod:
   2.230 +  assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N"
   2.231 +  shows "embed_measure M f \<Otimes>\<^sub>M embed_measure N g = embed_measure (M \<Otimes>\<^sub>M N) (\<lambda>(x, y). (f x, g y))"
   2.232 +    (is "?L = _")
   2.233 +  unfolding map_prod_def[symmetric]
   2.234 +proof (rule pair_measure_eqI)
   2.235 +  have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
   2.236 +    using f g by (auto simp: inj_on_def)
   2.237 +  
   2.238 +  show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
   2.239 +    unfolding map_prod_def[symmetric]
   2.240 +    apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra
   2.241 +      cong: vimage_algebra_cong)
   2.242 +    apply (subst vimage_algebra_Sup_sigma)
   2.243 +    apply (simp_all add: space_pair_measure[symmetric])
   2.244 +    apply (auto simp add: the_inv_into_f_f
   2.245 +                simp del: map_prod_simp
   2.246 +                del: prod_fun_imageE) []
   2.247 +    apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
   2.248 +    apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
   2.249 +    apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
   2.250 +       space_pair_measure[symmetric] map_prod_image[symmetric])
   2.251 +    apply (intro arg_cong[where f=sets] arg_cong[where f=Sup_sigma] arg_cong2[where f=insert] vimage_algebra_cong)
   2.252 +    apply (auto simp: map_prod_image the_inv_into_f_f
   2.253 +                simp del: map_prod_simp del: prod_fun_imageE)
   2.254 +    apply (simp_all add: the_inv_into_f_f space_pair_measure)
   2.255 +    done
   2.256 +
   2.257 +  note measurable_embed_measure2[measurable]
   2.258 +  fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"
   2.259 +  moreover have "f -` A \<times> g -` B \<inter> space (M \<Otimes>\<^sub>M N) = (f -` A \<inter> space M) \<times> (g -` B \<inter> space N)"
   2.260 +    by (auto simp: space_pair_measure)
   2.261 +  ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =
   2.262 +                     emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"
   2.263 +    by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure
   2.264 +                  sigma_finite_measure.emeasure_pair_measure_Times)
   2.265 +qed (insert assms, simp_all add: sigma_finite_embed_measure)
   2.266 +
   2.267 +lemma density_embed_measure:
   2.268 +  assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"
   2.269 +  shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")
   2.270 +proof (rule measure_eqI)
   2.271 +  fix X assume X: "X \<in> sets ?M1"
   2.272 +  from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)" 
   2.273 +    by (rule measurable_embed_measure2)
   2.274 +  from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f" 
   2.275 +    by (subst emeasure_density) simp_all
   2.276 +  also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"
   2.277 +    by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr)
   2.278 +       (auto intro!: borel_measurable_ereal_times borel_measurable_indicator)
   2.279 +  also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"
   2.280 +    by (intro nn_integral_cong) (auto split: split_indicator)
   2.281 +  also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"
   2.282 +    by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])
   2.283 +  also from X and inj have "... = emeasure ?M2 X" 
   2.284 +    by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)
   2.285 +  finally show "emeasure ?M1 X = emeasure ?M2 X" .
   2.286 +qed (simp_all add: sets_embed_measure inj)
   2.287 +
   2.288 +lemma density_embed_measure':
   2.289 +  assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"
   2.290 +  shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"
   2.291 +proof-
   2.292 +  have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"
   2.293 +    by (rule density_embed_measure[OF inj])
   2.294 +       (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong, 
   2.295 +        rule inv, rule measurable_ident_sets, simp, rule Mg)
   2.296 +  also have "density M (g \<circ> f' \<circ> f) = density M g"
   2.297 +    by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)
   2.298 +  finally show ?thesis .
   2.299 +qed
   2.300 +
   2.301 +lemma inj_on_image_subset_iff:
   2.302 +  assumes "inj_on f C" "A \<subseteq> C"  "B \<subseteq> C"
   2.303 +  shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
   2.304 +proof (intro iffI subsetI)
   2.305 +  fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"
   2.306 +  from B have "f x \<in> f ` A" by blast
   2.307 +  with A have "f x \<in> f ` B" by blast
   2.308 +  then obtain y where "f x = f y" and "y \<in> B" by blast
   2.309 +  with assms and B have "x = y" by (auto dest: inj_onD)
   2.310 +  with `y \<in> B` show "x \<in> B" by simp
   2.311 +qed auto
   2.312 +  
   2.313 +
   2.314 +lemma AE_embed_measure':
   2.315 +  assumes inj: "inj_on f (space M)"
   2.316 +  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   2.317 +proof
   2.318 +  let ?M = "embed_measure M f"
   2.319 +  assume "AE x in ?M. P x"
   2.320 +  then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"
   2.321 +    by (force elim: AE_E)
   2.322 +  then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)
   2.323 +  moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}" 
   2.324 +    by (auto simp: inj space_embed_measure)
   2.325 +  from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"
   2.326 +    by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])
   2.327 +       (insert A'_props, auto dest: sets.sets_into_space)
   2.328 +  moreover from A_props A'_props have "emeasure M A' = 0"
   2.329 +    by (simp add: emeasure_embed_measure_image' inj)
   2.330 +  ultimately show "AE x in M. P (f x)" by (intro AE_I)
   2.331 +next
   2.332 +  let ?M = "embed_measure M f"
   2.333 +  assume "AE x in M. P (f x)"
   2.334 +  then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"
   2.335 +    by (force elim: AE_E)
   2.336 +  hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"
   2.337 +    by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)
   2.338 +  thus "AE x in ?M. P x" by (intro AE_I)
   2.339 +qed
   2.340 +
   2.341 +lemma AE_embed_measure:
   2.342 +  assumes inj: "inj f"
   2.343 +  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
   2.344 +  using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
   2.345 +
   2.346 +end
     3.1 --- a/src/HOL/Probability/Giry_Monad.thy	Thu Dec 04 21:28:35 2014 +0100
     3.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Dec 05 12:06:18 2014 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  *)
     3.5  
     3.6  theory Giry_Monad
     3.7 -  imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax"
     3.8 +  imports Probability_Measure Lebesgue_Integral_Substitution "~~/src/HOL/Library/Monad_Syntax" 
     3.9  begin
    3.10  
    3.11  section {* Sub-probability spaces *}
    3.12 @@ -50,6 +50,65 @@
    3.13  lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1"
    3.14    using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure)
    3.15  
    3.16 +lemma emeasure_density_distr_interval:
    3.17 +  fixes h :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real" and g' :: "real \<Rightarrow> real"
    3.18 +  assumes [simp]: "a \<le> b"
    3.19 +  assumes Mf[measurable]: "f \<in> borel_measurable borel"
    3.20 +  assumes Mg[measurable]: "g \<in> borel_measurable borel"
    3.21 +  assumes Mg'[measurable]: "g' \<in> borel_measurable borel"
    3.22 +  assumes Mh[measurable]: "h \<in> borel_measurable borel"
    3.23 +  assumes prob: "subprob_space (density lborel f)"
    3.24 +  assumes nonnegf: "\<And>x. f x \<ge> 0"
    3.25 +  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
    3.26 +  assumes contg': "continuous_on {a..b} g'"
    3.27 +  assumes mono: "strict_mono_on g {a..b}" and inv: "\<And>x. h x \<in> {a..b} \<Longrightarrow> g (h x) = x"
    3.28 +  assumes range: "{a..b} \<subseteq> range h"
    3.29 +  shows "emeasure (distr (density lborel f) lborel h) {a..b} = 
    3.30 +             emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}"
    3.31 +proof (cases "a < b")
    3.32 +  assume "a < b"
    3.33 +  from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
    3.34 +  from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on)
    3.35 +  from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0"
    3.36 +    by (rule mono_on_imp_deriv_nonneg) (auto simp: interior_atLeastAtMost_real)
    3.37 +  from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
    3.38 +    by (rule continuous_ge_on_Iii) (simp_all add: `a < b`)
    3.39 +
    3.40 +  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
    3.41 +  have A: "h -` {a..b} = {g a..g b}"
    3.42 +  proof (intro equalityI subsetI)
    3.43 +    fix x assume x: "x \<in> h -` {a..b}"
    3.44 +    hence "g (h x) \<in> {g a..g b}" by (auto intro: mono_onD[OF mono'])
    3.45 +    with inv and x show "x \<in> {g a..g b}" by simp
    3.46 +  next
    3.47 +    fix y assume y: "y \<in> {g a..g b}"
    3.48 +    with IVT'[OF _ _ _ contg, of y] obtain x where "x \<in> {a..b}" "y = g x" by auto
    3.49 +    with range and inv show "y \<in> h -` {a..b}" by auto
    3.50 +  qed
    3.51 +
    3.52 +  have prob': "subprob_space (distr (density lborel f) lborel h)"
    3.53 +    by (rule subprob_space.subprob_space_distr[OF prob]) (simp_all add: Mh)
    3.54 +  have B: "emeasure (distr (density lborel f) lborel h) {a..b} = 
    3.55 +            \<integral>\<^sup>+x. f x * indicator (h -` {a..b}) x \<partial>lborel"
    3.56 +    by (subst emeasure_distr) (simp_all add: emeasure_density Mf Mh measurable_sets_borel[OF Mh])
    3.57 +  also note A
    3.58 +  also have "emeasure (distr (density lborel f) lborel h) {a..b} \<le> 1"
    3.59 +    by (rule subprob_space.subprob_emeasure_le_1) (rule prob')
    3.60 +  hence "emeasure (distr (density lborel f) lborel h) {a..b} \<noteq> \<infinity>" by auto
    3.61 +  with assms have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
    3.62 +                      (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
    3.63 +    by (intro nn_integral_substitution_aux)
    3.64 +       (auto simp: derivg_nonneg A B emeasure_density mult.commute `a < b`)
    3.65 +  also have "... = emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}" 
    3.66 +    by (simp add: emeasure_density)
    3.67 +  finally show ?thesis .
    3.68 +next
    3.69 +  assume "\<not>a < b"
    3.70 +  with `a \<le> b` have [simp]: "b = a" by (simp add: not_less del: `a \<le> b`)
    3.71 +  from inv and range have "h -` {a} = {g a}" by auto
    3.72 +  thus ?thesis by (simp_all add: emeasure_distr emeasure_density measurable_sets_borel[OF Mh])
    3.73 +qed
    3.74 +
    3.75  locale pair_subprob_space = 
    3.76    pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
    3.77  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Probability/Interval_Integral.thy	Fri Dec 05 12:06:18 2014 +0100
     4.3 @@ -0,0 +1,1095 @@
     4.4 +(*  Title:      HOL/Probability/Interval_Integral.thy
     4.5 +    Author:     Jeremy Avigad, Johannes Hölzl, Luke Serafin
     4.6 +
     4.7 +Lebesgue integral over an interval (with endpoints possibly +-\<infinity>)
     4.8 +*)
     4.9 +
    4.10 +theory Interval_Integral
    4.11 +  imports Set_Integral
    4.12 +begin
    4.13 +
    4.14 +lemma continuous_on_vector_derivative:
    4.15 +  "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
    4.16 +  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
    4.17 +
    4.18 +lemma has_vector_derivative_weaken:
    4.19 +  fixes x D and f g s t
    4.20 +  assumes f: "(f has_vector_derivative D) (at x within t)"
    4.21 +    and "x \<in> s" "s \<subseteq> t" 
    4.22 +    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
    4.23 +  shows "(g has_vector_derivative D) (at x within s)"
    4.24 +proof -
    4.25 +  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
    4.26 +    unfolding has_vector_derivative_def has_derivative_iff_norm
    4.27 +    using assms by (intro conj_cong Lim_cong_within refl) auto
    4.28 +  then show ?thesis
    4.29 +    using has_vector_derivative_within_subset[OF f `s \<subseteq> t`] by simp
    4.30 +qed
    4.31 +
    4.32 +definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
    4.33 +
    4.34 +lemma einterval_eq[simp]:
    4.35 +  shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
    4.36 +    and einterval_eq_Ici: "einterval (ereal a) \<infinity> = {a <..}"
    4.37 +    and einterval_eq_Iic: "einterval (- \<infinity>) (ereal b) = {..< b}"
    4.38 +    and einterval_eq_UNIV: "einterval (- \<infinity>) \<infinity> = UNIV"
    4.39 +  by (auto simp: einterval_def)
    4.40 +
    4.41 +lemma einterval_same: "einterval a a = {}"
    4.42 +  by (auto simp add: einterval_def)
    4.43 +
    4.44 +lemma einterval_iff: "x \<in> einterval a b \<longleftrightarrow> a < ereal x \<and> ereal x < b"
    4.45 +  by (simp add: einterval_def)
    4.46 +
    4.47 +lemma einterval_nonempty: "a < b \<Longrightarrow> \<exists>c. c \<in> einterval a b"
    4.48 +  by (cases a b rule: ereal2_cases, auto simp: einterval_def intro!: dense gt_ex lt_ex)
    4.49 +
    4.50 +lemma open_einterval[simp]: "open (einterval a b)"
    4.51 +  by (cases a b rule: ereal2_cases)
    4.52 +     (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros)
    4.53 +
    4.54 +lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
    4.55 +  unfolding einterval_def by measurable
    4.56 +
    4.57 +(* 
    4.58 +    Approximating a (possibly infinite) interval
    4.59 +*)
    4.60 +
    4.61 +lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
    4.62 + unfolding filterlim_def by (auto intro: le_supI1)
    4.63 +
    4.64 +lemma ereal_incseq_approx:
    4.65 +  fixes a b :: ereal
    4.66 +  assumes "a < b"
    4.67 +  obtains X :: "nat \<Rightarrow> real" where 
    4.68 +    "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X ----> b"
    4.69 +proof (cases b)
    4.70 +  case PInf
    4.71 +  with `a < b` have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
    4.72 +    by (cases a) auto
    4.73 +  moreover have " (\<lambda>x. ereal (real (Suc x))) ----> \<infinity>"
    4.74 +    using natceiling_le_eq by (subst LIMSEQ_Suc_iff) (auto simp: Lim_PInfty)
    4.75 +  moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) ----> \<infinity>"
    4.76 +    apply (subst LIMSEQ_Suc_iff)
    4.77 +    apply (subst Lim_PInfty)
    4.78 +    apply (metis add.commute diff_le_eq natceiling_le_eq ereal_less_eq(3))
    4.79 +    done
    4.80 +  ultimately show thesis
    4.81 +    by (intro that[of "\<lambda>i. real a + Suc i"])
    4.82 +       (auto simp: incseq_def PInf)
    4.83 +next
    4.84 +  case (real b')
    4.85 +  def d \<equiv> "b' - (if a = -\<infinity> then b' - 1 else real a)"
    4.86 +  with `a < b` have a': "0 < d"
    4.87 +    by (cases a) (auto simp: real)
    4.88 +  moreover
    4.89 +  have "\<And>i r. r < b' \<Longrightarrow> (b' - r) * 1 < (b' - r) * real (Suc (Suc i))"
    4.90 +    by (intro mult_strict_left_mono) auto
    4.91 +  with `a < b` a' have "\<And>i. a < ereal (b' - d / real (Suc (Suc i)))"
    4.92 +    by (cases a) (auto simp: real d_def field_simps)
    4.93 +  moreover have "(\<lambda>i. b' - d / Suc (Suc i)) ----> b'"
    4.94 +    apply (subst filterlim_sequentially_Suc)
    4.95 +    apply (subst filterlim_sequentially_Suc)
    4.96 +    apply (rule tendsto_eq_intros)
    4.97 +    apply (auto intro!: tendsto_divide_0[OF tendsto_const] filterlim_sup1
    4.98 +                simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
    4.99 +    done
   4.100 +  ultimately show thesis
   4.101 +    by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"])
   4.102 +       (auto simp add: real incseq_def intro!: divide_left_mono)
   4.103 +qed (insert `a < b`, auto)
   4.104 +
   4.105 +lemma ereal_decseq_approx:
   4.106 +  fixes a b :: ereal
   4.107 +  assumes "a < b"
   4.108 +  obtains X :: "nat \<Rightarrow> real" where 
   4.109 +    "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X ----> a"
   4.110 +proof -
   4.111 +  have "-b < -a" using `a < b` by simp
   4.112 +  from ereal_incseq_approx[OF this] guess X .
   4.113 +  then show thesis
   4.114 +    apply (intro that[of "\<lambda>i. - X i"])
   4.115 +    apply (auto simp add: uminus_ereal.simps[symmetric] decseq_def incseq_def
   4.116 +                simp del: uminus_ereal.simps)
   4.117 +    apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
   4.118 +    done
   4.119 +qed
   4.120 +
   4.121 +lemma einterval_Icc_approximation:
   4.122 +  fixes a b :: ereal
   4.123 +  assumes "a < b"
   4.124 +  obtains u l :: "nat \<Rightarrow> real" where 
   4.125 +    "einterval a b = (\<Union>i. {l i .. u i})"
   4.126 +    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
   4.127 +    "l ----> a" "u ----> b"
   4.128 +proof -
   4.129 +  from dense[OF `a < b`] obtain c where "a < c" "c < b" by safe
   4.130 +  from ereal_incseq_approx[OF `c < b`] guess u . note u = this
   4.131 +  from ereal_decseq_approx[OF `a < c`] guess l . note l = this
   4.132 +  { fix i from less_trans[OF `l i < c` `c < u i`] have "l i < u i" by simp }
   4.133 +  have "einterval a b = (\<Union>i. {l i .. u i})"
   4.134 +  proof (auto simp: einterval_iff)
   4.135 +    fix x assume "a < ereal x" "ereal x < b"
   4.136 +    have "eventually (\<lambda>i. ereal (l i) < ereal x) sequentially"
   4.137 +      using l(4) `a < ereal x` by (rule order_tendstoD)
   4.138 +    moreover 
   4.139 +    have "eventually (\<lambda>i. ereal x < ereal (u i)) sequentially"
   4.140 +      using u(4) `ereal x< b` by (rule order_tendstoD)
   4.141 +    ultimately have "eventually (\<lambda>i. l i < x \<and> x < u i) sequentially"
   4.142 +      by eventually_elim auto
   4.143 +    then show "\<exists>i. l i \<le> x \<and> x \<le> u i"
   4.144 +      by (auto intro: less_imp_le simp: eventually_sequentially)
   4.145 +  next
   4.146 +    fix x i assume "l i \<le> x" "x \<le> u i" 
   4.147 +    with `a < ereal (l i)` `ereal (u i) < b`
   4.148 +    show "a < ereal x" "ereal x < b"
   4.149 +      by (auto simp del: ereal_less_eq(3) simp add: ereal_less_eq(3)[symmetric])
   4.150 +  qed
   4.151 +  show thesis
   4.152 +    by (intro that) fact+
   4.153 +qed
   4.154 +
   4.155 +(* TODO: in this definition, it would be more natural if einterval a b included a and b when 
   4.156 +   they are real. *)
   4.157 +definition interval_lebesgue_integral :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> 'a::{banach, second_countable_topology}" where
   4.158 +  "interval_lebesgue_integral M a b f =
   4.159 +    (if a \<le> b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))"
   4.160 +
   4.161 +syntax
   4.162 +  "_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
   4.163 +  ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)
   4.164 +
   4.165 +translations
   4.166 +  "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
   4.167 +
   4.168 +definition interval_lebesgue_integrable :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a::{banach, second_countable_topology}) \<Rightarrow> bool" where
   4.169 +  "interval_lebesgue_integrable M a b f =
   4.170 +    (if a \<le> b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)"
   4.171 +
   4.172 +syntax
   4.173 +  "_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
   4.174 +  ("(4LBINT _=_.._. _)" [0,60,60,61] 60)
   4.175 +
   4.176 +translations
   4.177 +  "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
   4.178 +
   4.179 +(*
   4.180 +    Basic properties of integration over an interval.
   4.181 +*)
   4.182 +
   4.183 +lemma interval_lebesgue_integral_cong:
   4.184 +  "a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
   4.185 +    interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
   4.186 +  by (auto intro: set_lebesgue_integral_cong simp: interval_lebesgue_integral_def)
   4.187 +
   4.188 +lemma interval_lebesgue_integral_cong_AE:
   4.189 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
   4.190 +    a \<le> b \<Longrightarrow> AE x \<in> einterval a b in M. f x = g x \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
   4.191 +    interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
   4.192 +  by (auto intro: set_lebesgue_integral_cong_AE simp: interval_lebesgue_integral_def)
   4.193 +
   4.194 +lemma interval_lebesgue_integral_add [intro, simp]: 
   4.195 +  fixes M a b f 
   4.196 +  assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
   4.197 +  shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and 
   4.198 +    "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) = 
   4.199 +   interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
   4.200 +using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def 
   4.201 +    field_simps)
   4.202 +
   4.203 +lemma interval_lebesgue_integral_diff [intro, simp]: 
   4.204 +  fixes M a b f 
   4.205 +  assumes "interval_lebesgue_integrable M a b f"
   4.206 +    "interval_lebesgue_integrable M a b g"
   4.207 +  shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and 
   4.208 +    "interval_lebesgue_integral M a b (\<lambda>x. f x - g x) = 
   4.209 +   interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g"
   4.210 +using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def 
   4.211 +    field_simps)
   4.212 +
   4.213 +lemma interval_lebesgue_integrable_mult_right [intro, simp]:
   4.214 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   4.215 +  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
   4.216 +    interval_lebesgue_integrable M a b (\<lambda>x. c * f x)"
   4.217 +  by (simp add: interval_lebesgue_integrable_def)
   4.218 +
   4.219 +lemma interval_lebesgue_integrable_mult_left [intro, simp]:
   4.220 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   4.221 +  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
   4.222 +    interval_lebesgue_integrable M a b (\<lambda>x. f x * c)"
   4.223 +  by (simp add: interval_lebesgue_integrable_def)
   4.224 +
   4.225 +lemma interval_lebesgue_integrable_divide [intro, simp]:
   4.226 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
   4.227 +  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
   4.228 +    interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
   4.229 +  by (simp add: interval_lebesgue_integrable_def)
   4.230 +
   4.231 +lemma interval_lebesgue_integral_mult_right [simp]:
   4.232 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   4.233 +  shows "interval_lebesgue_integral M a b (\<lambda>x. c * f x) =
   4.234 +    c * interval_lebesgue_integral M a b f"
   4.235 +  by (simp add: interval_lebesgue_integral_def)
   4.236 +
   4.237 +lemma interval_lebesgue_integral_mult_left [simp]:
   4.238 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   4.239 +  shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) =
   4.240 +    interval_lebesgue_integral M a b f * c"
   4.241 +  by (simp add: interval_lebesgue_integral_def)
   4.242 +
   4.243 +lemma interval_lebesgue_integral_divide [simp]:
   4.244 +  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
   4.245 +  shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) =
   4.246 +    interval_lebesgue_integral M a b f / c"
   4.247 +  by (simp add: interval_lebesgue_integral_def)
   4.248 +
   4.249 +lemma interval_lebesgue_integral_uminus:
   4.250 +  "interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f"
   4.251 +  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
   4.252 +
   4.253 +lemma interval_lebesgue_integral_of_real:
   4.254 +  "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) =
   4.255 +    of_real (interval_lebesgue_integral M a b f)"
   4.256 +  unfolding interval_lebesgue_integral_def
   4.257 +  by (auto simp add: interval_lebesgue_integral_def set_integral_complex_of_real)
   4.258 +
   4.259 +lemma interval_lebesgue_integral_le_eq: 
   4.260 +  fixes a b f
   4.261 +  assumes "a \<le> b"
   4.262 +  shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
   4.263 +using assms by (auto simp add: interval_lebesgue_integral_def)
   4.264 +
   4.265 +lemma interval_lebesgue_integral_gt_eq: 
   4.266 +  fixes a b f
   4.267 +  assumes "a > b"
   4.268 +  shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"
   4.269 +using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
   4.270 +
   4.271 +lemma interval_lebesgue_integral_gt_eq':
   4.272 +  fixes a b f
   4.273 +  assumes "a > b"
   4.274 +  shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f"
   4.275 +using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
   4.276 +
   4.277 +lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
   4.278 +  by (simp add: interval_lebesgue_integral_def einterval_same)
   4.279 +
   4.280 +lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)"
   4.281 +  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def einterval_same)
   4.282 +
   4.283 +lemma interval_integrable_endpoints_reverse:
   4.284 +  "interval_lebesgue_integrable lborel a b f \<longleftrightarrow>
   4.285 +    interval_lebesgue_integrable lborel b a f"
   4.286 +  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)
   4.287 +
   4.288 +lemma interval_integral_reflect:
   4.289 +  "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
   4.290 +proof (induct a b rule: linorder_wlog)
   4.291 +  case (sym a b) then show ?case
   4.292 +    by (auto simp add: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
   4.293 +             split: split_if_asm)
   4.294 +next
   4.295 +  case (le a b) then show ?case
   4.296 +    unfolding interval_lebesgue_integral_def
   4.297 +    by (subst set_integral_reflect)
   4.298 +       (auto simp: interval_lebesgue_integrable_def einterval_iff
   4.299 +                   ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
   4.300 +                   uminus_ereal.simps[symmetric]
   4.301 +             simp del: uminus_ereal.simps
   4.302 +             intro!: integral_cong
   4.303 +             split: split_indicator)
   4.304 +qed
   4.305 +
   4.306 +(*
   4.307 +    Basic properties of integration over an interval wrt lebesgue measure.
   4.308 +*)
   4.309 +
   4.310 +lemma interval_integral_zero [simp]:
   4.311 +  fixes a b :: ereal
   4.312 +  shows"LBINT x=a..b. 0 = 0" 
   4.313 +using assms unfolding interval_lebesgue_integral_def einterval_eq 
   4.314 +by simp
   4.315 +
   4.316 +lemma interval_integral_const [intro, simp]:
   4.317 +  fixes a b c :: real
   4.318 +  shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)" 
   4.319 +using assms unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq 
   4.320 +by (auto simp add:  less_imp_le field_simps measure_def)
   4.321 +
   4.322 +lemma interval_integral_cong_AE:
   4.323 +  assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
   4.324 +  assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
   4.325 +  shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
   4.326 +  using assms
   4.327 +proof (induct a b rule: linorder_wlog)
   4.328 +  case (sym a b) then show ?case
   4.329 +    by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
   4.330 +next
   4.331 +  case (le a b) then show ?case
   4.332 +    by (auto simp: interval_lebesgue_integral_def max_def min_def
   4.333 +             intro!: set_lebesgue_integral_cong_AE)
   4.334 +qed
   4.335 +
   4.336 +lemma interval_integral_cong:
   4.337 +  assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x" 
   4.338 +  shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
   4.339 +  using assms
   4.340 +proof (induct a b rule: linorder_wlog)
   4.341 +  case (sym a b) then show ?case
   4.342 +    by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
   4.343 +next
   4.344 +  case (le a b) then show ?case
   4.345 +    by (auto simp: interval_lebesgue_integral_def max_def min_def
   4.346 +             intro!: set_lebesgue_integral_cong)
   4.347 +qed
   4.348 +
   4.349 +lemma interval_lebesgue_integrable_cong_AE:
   4.350 +    "f \<in> borel_measurable lborel \<Longrightarrow> g \<in> borel_measurable lborel \<Longrightarrow>
   4.351 +    AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x \<Longrightarrow>
   4.352 +    interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g"
   4.353 +  apply (simp add: interval_lebesgue_integrable_def )
   4.354 +  apply (intro conjI impI set_integrable_cong_AE)
   4.355 +  apply (auto simp: min_def max_def)
   4.356 +  done
   4.357 +
   4.358 +lemma interval_integrable_abs_iff:
   4.359 +  fixes f :: "real \<Rightarrow> real"
   4.360 +  shows  "f \<in> borel_measurable lborel \<Longrightarrow>
   4.361 +    interval_lebesgue_integrable lborel a b (\<lambda>x. \<bar>f x\<bar>) = interval_lebesgue_integrable lborel a b f"
   4.362 +  unfolding interval_lebesgue_integrable_def
   4.363 +  by (subst (1 2) set_integrable_abs_iff') simp_all
   4.364 +
   4.365 +lemma interval_integral_Icc:
   4.366 +  fixes a b :: real
   4.367 +  shows "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a..b}. f x)"
   4.368 +  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
   4.369 +           simp add: interval_lebesgue_integral_def)
   4.370 +
   4.371 +lemma interval_integral_Icc':
   4.372 +  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {x. a \<le> ereal x \<and> ereal x \<le> b}. f x)"
   4.373 +  by (auto intro!: set_integral_discrete_difference[where X="{real a, real b}"]
   4.374 +           simp add: interval_lebesgue_integral_def einterval_iff)
   4.375 +
   4.376 +lemma interval_integral_Ioc:
   4.377 +  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a<..b}. f x)"
   4.378 +  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
   4.379 +           simp add: interval_lebesgue_integral_def einterval_iff)
   4.380 +
   4.381 +(* TODO: other versions as well? *) (* Yes: I need the Icc' version. *)
   4.382 +lemma interval_integral_Ioc':
   4.383 +  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {x. a < ereal x \<and> ereal x \<le> b}. f x)"
   4.384 +  by (auto intro!: set_integral_discrete_difference[where X="{real a, real b}"]
   4.385 +           simp add: interval_lebesgue_integral_def einterval_iff)
   4.386 +
   4.387 +lemma interval_integral_Ico:
   4.388 +  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a..<b}. f x)"
   4.389 +  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
   4.390 +           simp add: interval_lebesgue_integral_def einterval_iff)
   4.391 +
   4.392 +lemma interval_integral_Ioi:
   4.393 +  "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real a <..}. f x)"
   4.394 +  by (auto simp add: interval_lebesgue_integral_def einterval_iff)
   4.395 +
   4.396 +lemma interval_integral_Ioo:
   4.397 +  "a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real a <..< real b}. f x)"
   4.398 +  by (auto simp add: interval_lebesgue_integral_def einterval_iff)
   4.399 +
   4.400 +lemma interval_integral_discrete_difference:
   4.401 +  fixes f :: "real \<Rightarrow> 'b::{banach, second_countable_topology}" and a b :: ereal
   4.402 +  assumes "countable X"
   4.403 +  and eq: "\<And>x. a \<le> b \<Longrightarrow> a < x \<Longrightarrow> x < b \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   4.404 +  and anti_eq: "\<And>x. b \<le> a \<Longrightarrow> b < x \<Longrightarrow> x < a \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
   4.405 +  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   4.406 +  shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
   4.407 +  unfolding interval_lebesgue_integral_def
   4.408 +  apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms)
   4.409 +  apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
   4.410 +  done
   4.411 +
   4.412 +lemma interval_integral_sum: 
   4.413 +  fixes a b c :: ereal
   4.414 +  assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" 
   4.415 +  shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
   4.416 +proof -
   4.417 +  let ?I = "\<lambda>a b. LBINT x=a..b. f x"
   4.418 +  { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
   4.419 +    then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
   4.420 +      by (auto simp: interval_lebesgue_integrable_def)
   4.421 +    then have f: "set_borel_measurable borel (einterval a c) f"
   4.422 +      by (drule_tac borel_measurable_integrable) simp
   4.423 +    have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b \<union> einterval b c. f x)"
   4.424 +    proof (rule set_integral_cong_set)
   4.425 +      show "AE x in lborel. (x \<in> einterval a b \<union> einterval b c) = (x \<in> einterval a c)"
   4.426 +        using AE_lborel_singleton[of "real b"] ord
   4.427 +        by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff)
   4.428 +    qed (insert ord, auto intro!: set_borel_measurable_subset[OF f] simp: einterval_iff)
   4.429 +    also have "\<dots> = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)"
   4.430 +      using ord
   4.431 +      by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less)
   4.432 +    finally have "?I a b + ?I b c = ?I a c"
   4.433 +      using ord by (simp add: interval_lebesgue_integral_def)
   4.434 +  } note 1 = this
   4.435 +  { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
   4.436 +    from 1[OF this] have "?I b c + ?I a b = ?I a c"
   4.437 +      by (metis add.commute)
   4.438 +  } note 2 = this
   4.439 +  have 3: "\<And>a b. b \<le> a \<Longrightarrow> (LBINT x=a..b. f x) = - (LBINT x=b..a. f x)"
   4.440 +    by (rule interval_integral_endpoints_reverse)
   4.441 +  show ?thesis
   4.442 +    using integrable
   4.443 +    by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
   4.444 +       (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
   4.445 +qed
   4.446 +
   4.447 +lemma interval_integrable_isCont:
   4.448 +  fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   4.449 +  shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow>
   4.450 +    interval_lebesgue_integrable lborel a b f"
   4.451 +proof (induct a b rule: linorder_wlog)
   4.452 +  case (le a b) then show ?case
   4.453 +    by (auto simp: interval_lebesgue_integrable_def
   4.454 +             intro!: set_integrable_subset[OF borel_integrable_compact[of "{a .. b}"]]
   4.455 +                     continuous_at_imp_continuous_on)
   4.456 +qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1])
   4.457 +
   4.458 +lemma interval_integrable_continuous_on:
   4.459 +  fixes a b :: real and f
   4.460 +  assumes "a \<le> b" and "continuous_on {a..b} f"
   4.461 +  shows "interval_lebesgue_integrable lborel a b f"
   4.462 +using assms unfolding interval_lebesgue_integrable_def apply simp
   4.463 +  by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto)
   4.464 +
   4.465 +lemma interval_integral_eq_integral: 
   4.466 +  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   4.467 +  shows "a \<le> b \<Longrightarrow> set_integrable lborel {a..b} f \<Longrightarrow> LBINT x=a..b. f x = integral {a..b} f"
   4.468 +  by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral)
   4.469 +
   4.470 +lemma interval_integral_eq_integral': 
   4.471 +  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   4.472 +  shows "a \<le> b \<Longrightarrow> set_integrable lborel (einterval a b) f \<Longrightarrow> LBINT x=a..b. f x = integral (einterval a b) f"
   4.473 +  by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
   4.474 +  
   4.475 +(*
   4.476 +    General limit approximation arguments
   4.477 +*)
   4.478 +
   4.479 +lemma interval_integral_Icc_approx_nonneg:
   4.480 +  fixes a b :: ereal
   4.481 +  assumes "a < b"
   4.482 +  fixes u l :: "nat \<Rightarrow> real"
   4.483 +  assumes  approx: "einterval a b = (\<Union>i. {l i .. u i})"
   4.484 +    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
   4.485 +    "l ----> a" "u ----> b"
   4.486 +  fixes f :: "real \<Rightarrow> real"
   4.487 +  assumes f_integrable: "\<And>i. set_integrable lborel {l i..u i} f"
   4.488 +  assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
   4.489 +  assumes f_measurable: "set_borel_measurable lborel (einterval a b) f"
   4.490 +  assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) ----> C"
   4.491 +  shows 
   4.492 +    "set_integrable lborel (einterval a b) f"
   4.493 +    "(LBINT x=a..b. f x) = C"
   4.494 +proof -
   4.495 +  have 1: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
   4.496 +  have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
   4.497 +  proof -
   4.498 +     from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x"
   4.499 +      by eventually_elim
   4.500 +         (metis approx(5) approx(6) dual_order.strict_trans1 ereal_less_eq(3) le_less_trans)
   4.501 +    then show ?thesis
   4.502 +      apply eventually_elim
   4.503 +      apply (auto simp: mono_def split: split_indicator)
   4.504 +      apply (metis approx(3) decseqD order_trans)
   4.505 +      apply (metis approx(2) incseqD order_trans)
   4.506 +      done
   4.507 +  qed
   4.508 +  have 3: "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) ----> indicator (einterval a b) x *\<^sub>R f x"
   4.509 +  proof -
   4.510 +    { fix x i assume "l i \<le> x" "x \<le> u i"
   4.511 +      then have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
   4.512 +        apply (auto simp: eventually_sequentially intro!: exI[of _ i])
   4.513 +        apply (metis approx(3) decseqD order_trans)
   4.514 +        apply (metis approx(2) incseqD order_trans)
   4.515 +        done
   4.516 +      then have "eventually (\<lambda>i. f x * indicator {l i..u i} x = f x) sequentially"
   4.517 +        by eventually_elim auto }
   4.518 +    then show ?thesis
   4.519 +      unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator)
   4.520 +  qed
   4.521 +  have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) ----> C"
   4.522 +    using lbint_lim by (simp add: interval_integral_Icc approx less_imp_le)
   4.523 +  have 5: "set_borel_measurable lborel (einterval a b) f" by (rule assms)
   4.524 +  have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)"
   4.525 +    using assms by (simp add: interval_lebesgue_integral_def less_imp_le)
   4.526 +  also have "... = C" by (rule integral_monotone_convergence [OF 1 2 3 4 5])
   4.527 +  finally show "(LBINT x=a..b. f x) = C" .
   4.528 +
   4.529 +  show "set_integrable lborel (einterval a b) f" 
   4.530 +    by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
   4.531 +qed
   4.532 +
   4.533 +lemma interval_integral_Icc_approx_integrable:
   4.534 +  fixes u l :: "nat \<Rightarrow> real" and a b :: ereal
   4.535 +  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   4.536 +  assumes "a < b"
   4.537 +  assumes  approx: "einterval a b = (\<Union>i. {l i .. u i})"
   4.538 +    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
   4.539 +    "l ----> a" "u ----> b"
   4.540 +  assumes f_integrable: "set_integrable lborel (einterval a b) f"
   4.541 +  shows "(\<lambda>i. LBINT x=l i.. u i. f x) ----> (LBINT x=a..b. f x)"
   4.542 +proof -
   4.543 +  have "(\<lambda>i. LBINT x:{l i.. u i}. f x) ----> (LBINT x:einterval a b. f x)"
   4.544 +  proof (rule integral_dominated_convergence)
   4.545 +    show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))"
   4.546 +      by (rule integrable_norm) fact
   4.547 +    show "set_borel_measurable lborel (einterval a b) f"
   4.548 +      using f_integrable by (rule borel_measurable_integrable)
   4.549 +    then show "\<And>i. set_borel_measurable lborel {l i..u i} f"
   4.550 +      by (rule set_borel_measurable_subset) (auto simp: approx)
   4.551 +    show "\<And>i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \<le> norm (indicator (einterval a b) x *\<^sub>R f x)"
   4.552 +      by (intro AE_I2) (auto simp: approx split: split_indicator)
   4.553 +    show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) ----> indicator (einterval a b) x *\<^sub>R f x"
   4.554 +    proof (intro AE_I2 tendsto_intros Lim_eventually)
   4.555 +      fix x
   4.556 +      { fix i assume "l i \<le> x" "x \<le> u i" 
   4.557 +        with `incseq u`[THEN incseqD, of i] `decseq l`[THEN decseqD, of i]
   4.558 +        have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
   4.559 +          by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) }
   4.560 +      then show "eventually (\<lambda>xa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially"
   4.561 +        using approx order_tendstoD(2)[OF `l ----> a`, of x] order_tendstoD(1)[OF `u ----> b`, of x]
   4.562 +        by (auto split: split_indicator)
   4.563 +    qed
   4.564 +  qed
   4.565 +  with `a < b` `\<And>i. l i < u i` show ?thesis
   4.566 +    by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
   4.567 +qed
   4.568 +
   4.569 +(*
   4.570 +  A slightly stronger version of integral_FTC_atLeastAtMost and related facts, 
   4.571 +  with continuous_on instead of isCont
   4.572 +
   4.573 +  TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
   4.574 +*)
   4.575 +
   4.576 +(*
   4.577 +TODO: many proofs below require inferences like
   4.578 +
   4.579 +  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y
   4.580 +
   4.581 +where x and y are real. These should be better automated.
   4.582 +*)
   4.583 +
   4.584 +(*
   4.585 +    The first Fundamental Theorem of Calculus
   4.586 +
   4.587 +    First, for finite intervals, and then two versions for arbitrary intervals.
   4.588 +*)
   4.589 +
   4.590 +lemma interval_integral_FTC_finite:
   4.591 +  fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
   4.592 +  assumes f: "continuous_on {min a b..max a b} f"
   4.593 +  assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within 
   4.594 +    {min a b..max a b})" 
   4.595 +  shows "(LBINT x=a..b. f x) = F b - F a"
   4.596 +  apply (case_tac "a \<le> b")
   4.597 +  apply (subst interval_integral_Icc, simp)
   4.598 +  apply (rule integral_FTC_atLeastAtMost, assumption)
   4.599 +  apply (metis F max_def min_def)
   4.600 +  using f apply (simp add: min_absorb1 max_absorb2)
   4.601 +  apply (subst interval_integral_endpoints_reverse)
   4.602 +  apply (subst interval_integral_Icc, simp)
   4.603 +  apply (subst integral_FTC_atLeastAtMost, auto)
   4.604 +  apply (metis F max_def min_def)
   4.605 +using f by (simp add: min_absorb2 max_absorb1)
   4.606 +
   4.607 +lemma interval_integral_FTC_nonneg:
   4.608 +  fixes f F :: "real \<Rightarrow> real" and a b :: ereal
   4.609 +  assumes "a < b"
   4.610 +  assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x" 
   4.611 +  assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" 
   4.612 +  assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
   4.613 +  assumes A: "((F \<circ> real) ---> A) (at_right a)"
   4.614 +  assumes B: "((F \<circ> real) ---> B) (at_left b)"
   4.615 +  shows
   4.616 +    "set_integrable lborel (einterval a b) f" 
   4.617 +    "(LBINT x=a..b. f x) = B - A"
   4.618 +proof -
   4.619 +  from einterval_Icc_approximation[OF `a < b`] guess u l . note approx = this
   4.620 +  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   4.621 +    by (rule order_less_le_trans, rule approx, force)
   4.622 +  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   4.623 +    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
   4.624 +  have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
   4.625 +    using assms approx apply (intro interval_integral_FTC_finite)
   4.626 +    apply (auto simp add: less_imp_le min_def max_def
   4.627 +      has_field_derivative_iff_has_vector_derivative[symmetric])
   4.628 +    apply (rule continuous_at_imp_continuous_on, auto intro!: f)
   4.629 +    by (rule DERIV_subset [OF F], auto)
   4.630 +  have 1: "\<And>i. set_integrable lborel {l i..u i} f"
   4.631 +  proof -
   4.632 +    fix i show "set_integrable lborel {l i .. u i} f"
   4.633 +      using `a < l i` `u i < b`
   4.634 +      by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
   4.635 +         (auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric])
   4.636 +  qed
   4.637 +  have 2: "set_borel_measurable lborel (einterval a b) f"
   4.638 +    by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous 
   4.639 +             simp: continuous_on_eq_continuous_at einterval_iff f)
   4.640 +  have 3: "(\<lambda>i. LBINT x=l i..u i. f x) ----> B - A"
   4.641 +    apply (subst FTCi)
   4.642 +    apply (intro tendsto_intros)
   4.643 +    using B approx unfolding tendsto_at_iff_sequentially comp_def
   4.644 +    using tendsto_at_iff_sequentially[where 'a=real]
   4.645 +    apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
   4.646 +    using A approx unfolding tendsto_at_iff_sequentially comp_def
   4.647 +    by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
   4.648 +  show "(LBINT x=a..b. f x) = B - A"
   4.649 +    by (rule interval_integral_Icc_approx_nonneg [OF `a < b` approx 1 f_nonneg 2 3])
   4.650 +  show "set_integrable lborel (einterval a b) f" 
   4.651 +    by (rule interval_integral_Icc_approx_nonneg [OF `a < b` approx 1 f_nonneg 2 3])
   4.652 +qed
   4.653 +
   4.654 +lemma interval_integral_FTC_integrable:
   4.655 +  fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal
   4.656 +  assumes "a < b"
   4.657 +  assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)" 
   4.658 +  assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" 
   4.659 +  assumes f_integrable: "set_integrable lborel (einterval a b) f"
   4.660 +  assumes A: "((F \<circ> real) ---> A) (at_right a)"
   4.661 +  assumes B: "((F \<circ> real) ---> B) (at_left b)"
   4.662 +  shows "(LBINT x=a..b. f x) = B - A"
   4.663 +proof -
   4.664 +  from einterval_Icc_approximation[OF `a < b`] guess u l . note approx = this
   4.665 +  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   4.666 +    by (rule order_less_le_trans, rule approx, force)
   4.667 +  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   4.668 +    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
   4.669 +  have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
   4.670 +    using assms approx
   4.671 +    by (auto simp add: less_imp_le min_def max_def
   4.672 +             intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite
   4.673 +             intro: has_vector_derivative_at_within)
   4.674 +  have "(\<lambda>i. LBINT x=l i..u i. f x) ----> B - A"
   4.675 +    apply (subst FTCi)
   4.676 +    apply (intro tendsto_intros)
   4.677 +    using B approx unfolding tendsto_at_iff_sequentially comp_def
   4.678 +    apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
   4.679 +    using A approx unfolding tendsto_at_iff_sequentially comp_def
   4.680 +    by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
   4.681 +  moreover have "(\<lambda>i. LBINT x=l i..u i. f x) ----> (LBINT x=a..b. f x)"
   4.682 +    by (rule interval_integral_Icc_approx_integrable [OF `a < b` approx f_integrable])
   4.683 +  ultimately show ?thesis
   4.684 +    by (elim LIMSEQ_unique)
   4.685 +qed
   4.686 +
   4.687 +(* 
   4.688 +  The second Fundamental Theorem of Calculus and existence of antiderivatives on an
   4.689 +  einterval.
   4.690 +*)
   4.691 +
   4.692 +lemma interval_integral_FTC2:
   4.693 +  fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
   4.694 +  assumes "a \<le> c" "c \<le> b"
   4.695 +  and contf: "continuous_on {a..b} f"
   4.696 +  fixes x :: real
   4.697 +  assumes "a \<le> x" and "x \<le> b"
   4.698 +  shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
   4.699 +proof -
   4.700 +  let ?F = "(\<lambda>u. LBINT y=a..u. f y)"
   4.701 +  have intf: "set_integrable lborel {a..b} f"
   4.702 +    by (rule borel_integrable_atLeastAtMost', rule contf)
   4.703 +  have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
   4.704 +    apply (intro integral_has_vector_derivative)
   4.705 +    using `a \<le> x` `x \<le> b` by (intro continuous_on_subset [OF contf], auto)
   4.706 +  then have "((\<lambda>u. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})"
   4.707 +    by simp
   4.708 +  then have "(?F has_vector_derivative (f x)) (at x within {a..b})"
   4.709 +    by (rule has_vector_derivative_weaken)
   4.710 +       (auto intro!: assms interval_integral_eq_integral[symmetric] set_integrable_subset [OF intf])
   4.711 +  then have "((\<lambda>x. (LBINT y=c..a. f y) + ?F x) has_vector_derivative (f x)) (at x within {a..b})"
   4.712 +    by (auto intro!: derivative_eq_intros)
   4.713 +  then show ?thesis
   4.714 +  proof (rule has_vector_derivative_weaken)
   4.715 +    fix u assume "u \<in> {a .. b}"
   4.716 +    then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)"
   4.717 +      using assms
   4.718 +      apply (intro interval_integral_sum)
   4.719 +      apply (auto simp add: interval_lebesgue_integrable_def simp del: real_scaleR_def)
   4.720 +      by (rule set_integrable_subset [OF intf], auto simp add: min_def max_def)
   4.721 +  qed (insert assms, auto)
   4.722 +qed
   4.723 +
   4.724 +lemma einterval_antiderivative: 
   4.725 +  fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space"
   4.726 +  assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x"
   4.727 +  shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
   4.728 +proof -
   4.729 +  from einterval_nonempty [OF `a < b`] obtain c :: real where [simp]: "a < c" "c < b" 
   4.730 +    by (auto simp add: einterval_def)
   4.731 +  let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
   4.732 +  show ?thesis
   4.733 +  proof (rule exI, clarsimp)
   4.734 +    fix x :: real
   4.735 +    assume [simp]: "a < x" "x < b"
   4.736 +    have 1: "a < min c x" by simp
   4.737 +    from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x" 
   4.738 +      by (auto simp add: einterval_def)
   4.739 +    have 2: "max c x < b" by simp
   4.740 +    from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b" 
   4.741 +      by (auto simp add: einterval_def)
   4.742 +    show "(?F has_vector_derivative f x) (at x)"
   4.743 +      (* TODO: factor out the next three lines to has_field_derivative_within_open *)
   4.744 +      unfolding has_vector_derivative_def
   4.745 +      apply (subst has_derivative_within_open [of _ "{d<..<e}", symmetric], auto)
   4.746 +      apply (subst has_vector_derivative_def [symmetric])
   4.747 +      apply (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
   4.748 +      apply (rule interval_integral_FTC2, auto simp add: less_imp_le)
   4.749 +      apply (rule continuous_at_imp_continuous_on)
   4.750 +      apply (auto intro!: contf)
   4.751 +      apply (rule order_less_le_trans, rule `a < d`, auto)
   4.752 +      apply (rule order_le_less_trans) prefer 2
   4.753 +      by (rule `e < b`, auto)
   4.754 +  qed
   4.755 +qed
   4.756 +
   4.757 +(*
   4.758 +    The substitution theorem
   4.759 +
   4.760 +    Once again, three versions: first, for finite intervals, and then two versions for
   4.761 +    arbitrary intervals.
   4.762 +*)
   4.763 +  
   4.764 +lemma interval_integral_substitution_finite:
   4.765 +  fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
   4.766 +  assumes "a \<le> b"
   4.767 +  and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
   4.768 +  and contf : "continuous_on (g ` {a..b}) f"
   4.769 +  and contg': "continuous_on {a..b} g'"
   4.770 +  shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
   4.771 +proof-
   4.772 +  have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
   4.773 +    using derivg unfolding has_field_derivative_iff_has_vector_derivative .
   4.774 +  then have contg [simp]: "continuous_on {a..b} g"
   4.775 +    by (rule continuous_on_vector_derivative) auto
   4.776 +  have 1: "\<And>u. min (g a) (g b) \<le> u \<Longrightarrow> u \<le> max (g a) (g b) \<Longrightarrow> 
   4.777 +      \<exists>x\<in>{a..b}. u = g x"
   4.778 +    apply (case_tac "g a \<le> g b")
   4.779 +    apply (auto simp add: min_def max_def less_imp_le)
   4.780 +    apply (frule (1) IVT' [of g], auto simp add: assms)
   4.781 +    by (frule (1) IVT2' [of g], auto simp add: assms)
   4.782 +  from contg `a \<le> b` have "\<exists>c d. g ` {a..b} = {c..d} \<and> c \<le> d"
   4.783 +    by (elim continuous_image_closed_interval)
   4.784 +  then obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \<le> d" by auto
   4.785 +  have "\<exists>F. \<forall>x\<in>{a..b}. (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))"
   4.786 +    apply (rule exI, auto, subst g_im)
   4.787 +    apply (rule interval_integral_FTC2 [of c c d])
   4.788 +    using `c \<le> d` apply auto
   4.789 +    apply (rule continuous_on_subset [OF contf])
   4.790 +    using g_im by auto
   4.791 +  then guess F ..
   4.792 +  then have derivF: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> 
   4.793 +    (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" by auto
   4.794 +  have contf2: "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
   4.795 +    apply (rule continuous_on_subset [OF contf])
   4.796 +    apply (auto simp add: image_def)
   4.797 +    by (erule 1)
   4.798 +  have contfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
   4.799 +    by (blast intro: continuous_on_compose2 contf contg)
   4.800 +  have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
   4.801 +    apply (subst interval_integral_Icc, simp add: assms)
   4.802 +    apply (rule integral_FTC_atLeastAtMost[of a b "\<lambda>x. F (g x)", OF `a \<le> b`])
   4.803 +    apply (rule vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def])
   4.804 +    apply (auto intro!: continuous_on_scaleR contg' contfg)
   4.805 +    done
   4.806 +  moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
   4.807 +    apply (rule interval_integral_FTC_finite)
   4.808 +    apply (rule contf2)
   4.809 +    apply (frule (1) 1, auto)
   4.810 +    apply (rule has_vector_derivative_within_subset [OF derivF])
   4.811 +    apply (auto simp add: image_def)
   4.812 +    by (rule 1, auto)
   4.813 +  ultimately show ?thesis by simp
   4.814 +qed
   4.815 +
   4.816 +(* TODO: is it possible to lift the assumption here that g' is nonnegative? *)
   4.817 +
   4.818 +lemma interval_integral_substitution_integrable:
   4.819 +  fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal
   4.820 +  assumes "a < b" 
   4.821 +  and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
   4.822 +  and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
   4.823 +  and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
   4.824 +  and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x"
   4.825 +  and A: "((ereal \<circ> g \<circ> real) ---> A) (at_right a)"
   4.826 +  and B: "((ereal \<circ> g \<circ> real) ---> B) (at_left b)"
   4.827 +  and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
   4.828 +  and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
   4.829 +  shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
   4.830 +proof -
   4.831 +  from einterval_Icc_approximation[OF `a < b`] guess u l . note approx [simp] = this
   4.832 +  note less_imp_le [simp]
   4.833 +  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   4.834 +    by (rule order_less_le_trans, rule approx, force)
   4.835 +  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   4.836 +    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
   4.837 +  have [simp]: "\<And>i. l i < b" 
   4.838 +    apply (rule order_less_trans) prefer 2 
   4.839 +    by (rule approx, auto, rule approx)
   4.840 +  have [simp]: "\<And>i. a < u i" 
   4.841 +    by (rule order_less_trans, rule approx, auto, rule approx)
   4.842 +  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
   4.843 +  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
   4.844 +  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
   4.845 +    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
   4.846 +    apply (rule exI, rule conjI, rule deriv_g)
   4.847 +    apply (erule order_less_le_trans, auto)
   4.848 +    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
   4.849 +    apply (rule g'_nonneg)
   4.850 +    apply (rule less_imp_le, erule order_less_le_trans, auto)
   4.851 +    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
   4.852 +  have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   4.853 +  proof - 
   4.854 +    have A2: "(\<lambda>i. g (l i)) ----> A"
   4.855 +      using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
   4.856 +      by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
   4.857 +    hence A3: "\<And>i. g (l i) \<ge> A"
   4.858 +      by (intro decseq_le, auto simp add: decseq_def)
   4.859 +    have B2: "(\<lambda>i. g (u i)) ----> B"
   4.860 +      using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
   4.861 +      by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
   4.862 +    hence B3: "\<And>i. g (u i) \<le> B"
   4.863 +      by (intro incseq_le, auto simp add: incseq_def)
   4.864 +    show "A \<le> B"
   4.865 +      apply (rule order_trans [OF A3 [of 0]])
   4.866 +      apply (rule order_trans [OF _ B3 [of 0]])
   4.867 +      by auto
   4.868 +    { fix x :: real
   4.869 +      assume "A < x" and "x < B"   
   4.870 +      then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
   4.871 +        apply (intro eventually_conj order_tendstoD)
   4.872 +        by (rule A2, assumption, rule B2, assumption)
   4.873 +      hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
   4.874 +        by (simp add: eventually_sequentially, auto)
   4.875 +    } note AB = this
   4.876 +    show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   4.877 +      apply (auto simp add: einterval_def)
   4.878 +      apply (erule (1) AB)
   4.879 +      apply (rule order_le_less_trans, rule A3, simp)
   4.880 +      apply (rule order_less_le_trans) prefer 2
   4.881 +      by (rule B3, simp) 
   4.882 +  qed
   4.883 +  (* finally, the main argument *)
   4.884 +  {
   4.885 +     fix i
   4.886 +     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
   4.887 +        apply (rule interval_integral_substitution_finite, auto)
   4.888 +        apply (rule DERIV_subset)
   4.889 +        unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
   4.890 +        apply (rule deriv_g)
   4.891 +        apply (auto intro!: continuous_at_imp_continuous_on contf contg')
   4.892 +        done
   4.893 +  } note eq1 = this
   4.894 +  have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) ----> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
   4.895 +    apply (rule interval_integral_Icc_approx_integrable [OF `a < b` approx])
   4.896 +    by (rule assms)
   4.897 +  hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
   4.898 +    by (simp add: eq1)
   4.899 +  have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
   4.900 +    apply (auto simp add: incseq_def)
   4.901 +    apply (rule order_le_less_trans)
   4.902 +    prefer 2 apply (assumption, auto)
   4.903 +    by (erule order_less_le_trans, rule g_nondec, auto)
   4.904 +  have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x = A..B. f x)"
   4.905 +    apply (subst interval_lebesgue_integral_le_eq, auto simp del: real_scaleR_def)
   4.906 +    apply (subst interval_lebesgue_integral_le_eq, rule `A \<le> B`)
   4.907 +    apply (subst un, rule set_integral_cont_up, auto simp del: real_scaleR_def)
   4.908 +    apply (rule incseq)
   4.909 +    apply (subst un [symmetric])
   4.910 +    by (rule integrable2)
   4.911 +  thus ?thesis by (intro LIMSEQ_unique [OF _ 2])
   4.912 +qed
   4.913 +
   4.914 +(* TODO: the last two proofs are only slightly different. Factor out common part?
   4.915 +   An alternative: make the second one the main one, and then have another lemma
   4.916 +   that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *)
   4.917 +
   4.918 +lemma interval_integral_substitution_nonneg:
   4.919 +  fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal
   4.920 +  assumes "a < b" 
   4.921 +  and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
   4.922 +  and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
   4.923 +  and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
   4.924 +  and f_nonneg: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> 0 \<le> f (g x)" (* TODO: make this AE? *)
   4.925 +  and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x"
   4.926 +  and A: "((ereal \<circ> g \<circ> real) ---> A) (at_right a)"
   4.927 +  and B: "((ereal \<circ> g \<circ> real) ---> B) (at_left b)"
   4.928 +  and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)"
   4.929 +  shows 
   4.930 +    "set_integrable lborel (einterval A B) f"
   4.931 +    "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
   4.932 +proof -
   4.933 +  from einterval_Icc_approximation[OF `a < b`] guess u l . note approx [simp] = this
   4.934 +  note less_imp_le [simp]
   4.935 +  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
   4.936 +    by (rule order_less_le_trans, rule approx, force)
   4.937 +  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
   4.938 +    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
   4.939 +  have [simp]: "\<And>i. l i < b" 
   4.940 +    apply (rule order_less_trans) prefer 2 
   4.941 +    by (rule approx, auto, rule approx)
   4.942 +  have [simp]: "\<And>i. a < u i" 
   4.943 +    by (rule order_less_trans, rule approx, auto, rule approx)
   4.944 +  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
   4.945 +  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
   4.946 +  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
   4.947 +    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
   4.948 +    apply (rule exI, rule conjI, rule deriv_g)
   4.949 +    apply (erule order_less_le_trans, auto)
   4.950 +    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
   4.951 +    apply (rule g'_nonneg)
   4.952 +    apply (rule less_imp_le, erule order_less_le_trans, auto)
   4.953 +    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
   4.954 +  have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   4.955 +  proof - 
   4.956 +    have A2: "(\<lambda>i. g (l i)) ----> A"
   4.957 +      using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
   4.958 +      by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
   4.959 +    hence A3: "\<And>i. g (l i) \<ge> A"
   4.960 +      by (intro decseq_le, auto simp add: decseq_def)
   4.961 +    have B2: "(\<lambda>i. g (u i)) ----> B"
   4.962 +      using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
   4.963 +      by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
   4.964 +    hence B3: "\<And>i. g (u i) \<le> B"
   4.965 +      by (intro incseq_le, auto simp add: incseq_def)
   4.966 +    show "A \<le> B"
   4.967 +      apply (rule order_trans [OF A3 [of 0]])
   4.968 +      apply (rule order_trans [OF _ B3 [of 0]])
   4.969 +      by auto
   4.970 +    { fix x :: real
   4.971 +      assume "A < x" and "x < B"   
   4.972 +      then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
   4.973 +        apply (intro eventually_conj order_tendstoD)
   4.974 +        by (rule A2, assumption, rule B2, assumption)
   4.975 +      hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
   4.976 +        by (simp add: eventually_sequentially, auto)
   4.977 +    } note AB = this
   4.978 +    show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
   4.979 +      apply (auto simp add: einterval_def)
   4.980 +      apply (erule (1) AB)
   4.981 +      apply (rule order_le_less_trans, rule A3, simp)
   4.982 +      apply (rule order_less_le_trans) prefer 2
   4.983 +      by (rule B3, simp) 
   4.984 +  qed
   4.985 +  (* finally, the main argument *)
   4.986 +  {
   4.987 +     fix i
   4.988 +     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
   4.989 +        apply (rule interval_integral_substitution_finite, auto)
   4.990 +        apply (rule DERIV_subset, rule deriv_g, auto)
   4.991 +        apply (rule continuous_at_imp_continuous_on, auto, rule contf, auto)
   4.992 +        by (rule continuous_at_imp_continuous_on, auto, rule contg', auto)
   4.993 +     then have "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)"
   4.994 +       by (simp add: ac_simps)
   4.995 +  } note eq1 = this
   4.996 +  have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x)
   4.997 +      ----> (LBINT x=a..b. f (g x) * g' x)"
   4.998 +    apply (rule interval_integral_Icc_approx_integrable [OF `a < b` approx])
   4.999 +    by (rule assms)
  4.1000 +  hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. f (g x) * g' x)"
  4.1001 +    by (simp add: eq1)
  4.1002 +  have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
  4.1003 +    apply (auto simp add: incseq_def)
  4.1004 +    apply (rule order_le_less_trans)
  4.1005 +    prefer 2 apply assumption
  4.1006 +    apply (rule g_nondec, auto)
  4.1007 +    by (erule order_less_le_trans, rule g_nondec, auto)
  4.1008 +  have img: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> \<exists>c \<ge> l i. c \<le> u i \<and> x = g c"
  4.1009 +    apply (frule (1) IVT' [of g], auto)   
  4.1010 +    apply (rule continuous_at_imp_continuous_on, auto)
  4.1011 +    by (rule DERIV_isCont, rule deriv_g, auto)
  4.1012 +  have nonneg_f2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
  4.1013 +    by (frule (1) img, auto, rule f_nonneg, auto)
  4.1014 +  have contf_2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> isCont f x"
  4.1015 +    by (frule (1) img, auto, rule contf, auto)
  4.1016 +  have integrable: "set_integrable lborel (\<Union>i. {g (l i)<..<g (u i)}) f"
  4.1017 +    apply (rule pos_integrable_to_top, auto simp del: real_scaleR_def)
  4.1018 +    apply (rule incseq)
  4.1019 +    apply (rule nonneg_f2, erule less_imp_le, erule less_imp_le)
  4.1020 +    apply (rule set_integrable_subset)
  4.1021 +    apply (rule borel_integrable_atLeastAtMost')
  4.1022 +    apply (rule continuous_at_imp_continuous_on)
  4.1023 +    apply (clarsimp, erule (1) contf_2, auto)
  4.1024 +    apply (erule less_imp_le)+
  4.1025 +    using 2 unfolding interval_lebesgue_integral_def
  4.1026 +    by auto
  4.1027 +  thus "set_integrable lborel (einterval A B) f"
  4.1028 +    by (simp add: un)
  4.1029 +
  4.1030 +  have "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
  4.1031 +  proof (rule interval_integral_substitution_integrable)
  4.1032 +    show "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
  4.1033 +      using integrable_fg by (simp add: ac_simps)
  4.1034 +  qed fact+
  4.1035 +  then show "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
  4.1036 +    by (simp add: ac_simps)
  4.1037 +qed
  4.1038 +
  4.1039 +
  4.1040 +syntax
  4.1041 +"_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
  4.1042 +("(2CLBINT _. _)" [0,60] 60)
  4.1043 +
  4.1044 +translations
  4.1045 +"CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
  4.1046 +
  4.1047 +syntax
  4.1048 +"_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
  4.1049 +("(3CLBINT _:_. _)" [0,60,61] 60)
  4.1050 +
  4.1051 +translations
  4.1052 +"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
  4.1053 +
  4.1054 +abbreviation complex_interval_lebesgue_integral :: 
  4.1055 +    "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> complex" where
  4.1056 +  "complex_interval_lebesgue_integral M a b f \<equiv> interval_lebesgue_integral M a b f"
  4.1057 +
  4.1058 +abbreviation complex_interval_lebesgue_integrable :: 
  4.1059 +  "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" where
  4.1060 +  "complex_interval_lebesgue_integrable M a b f \<equiv> interval_lebesgue_integrable M a b f"
  4.1061 +
  4.1062 +syntax
  4.1063 +  "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
  4.1064 +  ("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
  4.1065 +
  4.1066 +translations
  4.1067 +  "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
  4.1068 +
  4.1069 +lemma interval_integral_norm:
  4.1070 +  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
  4.1071 +  shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
  4.1072 +    norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
  4.1073 +  using integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
  4.1074 +  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
  4.1075 +
  4.1076 +lemma interval_integral_norm2:
  4.1077 +  "interval_lebesgue_integrable lborel a b f \<Longrightarrow> 
  4.1078 +    norm (LBINT t=a..b. f t) \<le> abs (LBINT t=a..b. norm (f t))"
  4.1079 +proof (induct a b rule: linorder_wlog)
  4.1080 +  case (sym a b) then show ?case
  4.1081 +    by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
  4.1082 +next
  4.1083 +  case (le a b) 
  4.1084 +  then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"  
  4.1085 +    using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
  4.1086 +    by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
  4.1087 +             intro!: integral_nonneg_AE abs_of_nonneg)
  4.1088 +  then show ?case
  4.1089 +    using le by (simp add: interval_integral_norm)
  4.1090 +qed
  4.1091 +
  4.1092 +(* TODO: should we have a library of facts like these? *)
  4.1093 +lemma integral_cos: "t \<noteq> 0 \<Longrightarrow> LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t"
  4.1094 +  apply (intro interval_integral_FTC_finite continuous_intros)
  4.1095 +  by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric])
  4.1096 +
  4.1097 +
  4.1098 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Fri Dec 05 12:06:18 2014 +0100
     5.3 @@ -0,0 +1,707 @@
     5.4 +(*  Title:      HOL/Probability/Lebesgue_Integral_Substitution.thy
     5.5 +    Author:     Manuel Eberl
     5.6 +
     5.7 +    Provides lemmas for integration by substitution for the basic integral types.
     5.8 +    Note that the substitution function must have a nonnegative derivative.
     5.9 +    This could probably be weakened somehow.
    5.10 +*)
    5.11 +
    5.12 +section {* Integration by Substition *}
    5.13 +
    5.14 +theory Lebesgue_Integral_Substitution
    5.15 +imports Interval_Integral
    5.16 +begin
    5.17 +
    5.18 +lemma measurable_sets_borel:
    5.19 +    "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
    5.20 +  by (drule (1) measurable_sets) simp
    5.21 +
    5.22 +lemma closure_Iii: 
    5.23 +  assumes "a < b"
    5.24 +  shows "closure {a<..<b::real} = {a..b}"
    5.25 +proof-
    5.26 +  have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less)
    5.27 +  also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp
    5.28 +  also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less)
    5.29 +  finally show ?thesis .
    5.30 +qed
    5.31 +
    5.32 +lemma continuous_ge_on_Iii:
    5.33 +  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
    5.34 +  shows "g (x::real) \<ge> (a::real)"
    5.35 +proof-
    5.36 +  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric])
    5.37 +  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
    5.38 +  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
    5.39 +  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
    5.40 +    by (auto simp: continuous_on_closed_vimage)
    5.41 +  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
    5.42 +  finally show ?thesis using `x \<in> {c..d}` by auto 
    5.43 +qed 
    5.44 +
    5.45 +lemma interior_real_semiline':
    5.46 +  fixes a :: real
    5.47 +  shows "interior {..a} = {..<a}"
    5.48 +proof -
    5.49 +  {
    5.50 +    fix y
    5.51 +    assume "a > y"
    5.52 +    then have "y \<in> interior {..a}"
    5.53 +      apply (simp add: mem_interior)
    5.54 +      apply (rule_tac x="(a-y)" in exI)
    5.55 +      apply (auto simp add: dist_norm)
    5.56 +      done
    5.57 +  }
    5.58 +  moreover
    5.59 +  {
    5.60 +    fix y
    5.61 +    assume "y \<in> interior {..a}"
    5.62 +    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
    5.63 +      using mem_interior_cball[of y "{..a}"] by auto
    5.64 +    moreover from e have "y + e \<in> cball y e"
    5.65 +      by (auto simp add: cball_def dist_norm)
    5.66 +    ultimately have "a \<ge> y + e" by auto
    5.67 +    then have "a > y" using e by auto
    5.68 +  }
    5.69 +  ultimately show ?thesis by auto
    5.70 +qed
    5.71 +
    5.72 +lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
    5.73 +proof-
    5.74 +  have "{a..b} = {a..} \<inter> {..b}" by auto
    5.75 +  also have "interior ... = {a<..} \<inter> {..<b}" 
    5.76 +    by (simp add: interior_real_semiline interior_real_semiline')
    5.77 +  also have "... = {a<..<b}" by auto
    5.78 +  finally show ?thesis .
    5.79 +qed
    5.80 +
    5.81 +lemma nn_integral_indicator_singleton[simp]:
    5.82 +  assumes [measurable]: "{y} \<in> sets M"
    5.83 +  shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
    5.84 +proof-
    5.85 +  have "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f y) * indicator {y} x \<partial>M)"
    5.86 +    by (subst nn_integral_max_0[symmetric]) (auto intro!: nn_integral_cong split: split_indicator)
    5.87 +  then show ?thesis
    5.88 +    by (simp add: nn_integral_cmult)
    5.89 +qed
    5.90 +
    5.91 +lemma nn_integral_set_ereal:
    5.92 +  "(\<integral>\<^sup>+x. ereal (f x) * indicator A x \<partial>M) = (\<integral>\<^sup>+x. ereal (f x * indicator A x) \<partial>M)"
    5.93 +  by (rule nn_integral_cong) (simp split: split_indicator)
    5.94 +
    5.95 +lemma nn_integral_indicator_singleton'[simp]:
    5.96 +  assumes [measurable]: "{y} \<in> sets M"
    5.97 +  shows "(\<integral>\<^sup>+x. ereal (f x * indicator {y} x) \<partial>M) = max 0 (f y) * emeasure M {y}"
    5.98 +  by (subst nn_integral_set_ereal[symmetric]) simp
    5.99 +
   5.100 +lemma set_borel_measurable_sets:
   5.101 +  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   5.102 +  assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
   5.103 +  shows "f -` B \<inter> X \<in> sets M"
   5.104 +proof -
   5.105 +  have "f \<in> borel_measurable (restrict_space M X)"
   5.106 +    using assms by (subst borel_measurable_restrict_space_iff) auto
   5.107 +  then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
   5.108 +    by (rule measurable_sets) fact
   5.109 +  with `X \<in> sets M` show ?thesis
   5.110 +    by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
   5.111 +qed
   5.112 +
   5.113 +lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
   5.114 +  assumes "A \<in> sets borel" 
   5.115 +  assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
   5.116 +          un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
   5.117 +  shows "P (A::real set)"
   5.118 +proof-
   5.119 +  let ?G = "range (\<lambda>(a,b). {a..b::real})"
   5.120 +  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" 
   5.121 +      using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
   5.122 +  thus ?thesis
   5.123 +  proof (induction rule: sigma_sets_induct_disjoint) 
   5.124 +    case (union f)
   5.125 +      from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
   5.126 +      with union show ?case by (auto intro: un)
   5.127 +  next
   5.128 +    case (basic A)
   5.129 +    then obtain a b where "A = {a .. b}" by auto
   5.130 +    then show ?case
   5.131 +      by (cases "a \<le> b") (auto intro: int empty)
   5.132 +  qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
   5.133 +qed
   5.134 +
   5.135 +definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
   5.136 +
   5.137 +lemma mono_onI:
   5.138 +  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A"
   5.139 +  unfolding mono_on_def by simp
   5.140 +
   5.141 +lemma mono_onD:
   5.142 +  "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
   5.143 +  unfolding mono_on_def by simp
   5.144 +
   5.145 +lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
   5.146 +  unfolding mono_def mono_on_def by auto
   5.147 +
   5.148 +lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
   5.149 +  unfolding mono_on_def by auto
   5.150 +
   5.151 +definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s"
   5.152 +
   5.153 +lemma strict_mono_onI:
   5.154 +  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A"
   5.155 +  unfolding strict_mono_on_def by simp
   5.156 +
   5.157 +lemma strict_mono_onD:
   5.158 +  "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
   5.159 +  unfolding strict_mono_on_def by simp
   5.160 +
   5.161 +lemma mono_on_greaterD:
   5.162 +  assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
   5.163 +  shows "x > y"
   5.164 +proof (rule ccontr)
   5.165 +  assume "\<not>x > y"
   5.166 +  hence "x \<le> y" by (simp add: not_less)
   5.167 +  from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
   5.168 +  with assms(4) show False by simp
   5.169 +qed
   5.170 +
   5.171 +lemma strict_mono_inv:
   5.172 +  fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
   5.173 +  assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
   5.174 +  shows "strict_mono g"
   5.175 +proof
   5.176 +  fix x y :: 'b assume "x < y"
   5.177 +  from `surj f` obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
   5.178 +  with `x < y` and `strict_mono f` have "x' < y'" by (simp add: strict_mono_less)
   5.179 +  with inv show "g x < g y" by simp
   5.180 +qed
   5.181 +
   5.182 +lemma strict_mono_on_imp_inj_on:
   5.183 +  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
   5.184 +  shows "inj_on f A"
   5.185 +proof (rule inj_onI)
   5.186 +  fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
   5.187 +  thus "x = y"
   5.188 +    by (cases x y rule: linorder_cases)
   5.189 +       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 
   5.190 +qed
   5.191 +
   5.192 +lemma strict_mono_on_leD:
   5.193 +  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
   5.194 +  shows "f x \<le> f y"
   5.195 +proof (insert le_less_linear[of y x], elim disjE)
   5.196 +  assume "x < y"
   5.197 +  with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
   5.198 +  thus ?thesis by (rule less_imp_le)
   5.199 +qed (insert assms, simp)
   5.200 +
   5.201 +lemma strict_mono_on_eqD:
   5.202 +  fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
   5.203 +  assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
   5.204 +  shows "y = x"
   5.205 +  using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
   5.206 +
   5.207 +lemma mono_on_imp_deriv_nonneg:
   5.208 +  assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
   5.209 +  assumes "x \<in> interior A"
   5.210 +  shows "D \<ge> 0"
   5.211 +proof (rule tendsto_le_const)
   5.212 +  let ?A' = "(\<lambda>y. y - x) ` interior A"
   5.213 +  from deriv show "((\<lambda>h. (f (x + h) - f x) / h) ---> D) (at 0)"
   5.214 +      by (simp add: field_has_derivative_at has_field_derivative_def)
   5.215 +  from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset)
   5.216 +
   5.217 +  show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
   5.218 +  proof (subst eventually_at_topological, intro exI conjI ballI impI)
   5.219 +    have "open (interior A)" by simp
   5.220 +    hence "open (op + (-x) ` interior A)" by (rule open_translation)
   5.221 +    also have "(op + (-x) ` interior A) = ?A'" by auto
   5.222 +    finally show "open ?A'" .
   5.223 +  next
   5.224 +    from `x \<in> interior A` show "0 \<in> ?A'" by auto
   5.225 +  next
   5.226 +    fix h assume "h \<in> ?A'"
   5.227 +    hence "x + h \<in> interior A" by auto
   5.228 +    with mono' and `x \<in> interior A` show "(f (x + h) - f x) / h \<ge> 0"
   5.229 +      by (cases h rule: linorder_cases[of _ 0])
   5.230 +         (simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps)
   5.231 +  qed
   5.232 +qed simp
   5.233 +
   5.234 +lemma strict_mono_on_imp_mono_on: 
   5.235 +  "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
   5.236 +  by (rule mono_onI, rule strict_mono_on_leD)
   5.237 +
   5.238 +lemma has_real_derivative_imp_continuous_on:
   5.239 +  assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
   5.240 +  shows "continuous_on A f"
   5.241 +  apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
   5.242 +  apply (intro ballI Deriv.differentiableI)
   5.243 +  apply (rule has_field_derivative_subset[OF assms])
   5.244 +  apply simp_all
   5.245 +  done
   5.246 +
   5.247 +lemma closure_contains_Sup:
   5.248 +  fixes S :: "real set"
   5.249 +  assumes "S \<noteq> {}" "bdd_above S"
   5.250 +  shows "Sup S \<in> closure S"
   5.251 +proof-
   5.252 +  have "Inf (uminus ` S) \<in> closure (uminus ` S)" 
   5.253 +      using assms by (intro closure_contains_Inf) auto
   5.254 +  also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
   5.255 +  also have "closure (uminus ` S) = uminus ` closure S"
   5.256 +      by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
   5.257 +  finally show ?thesis by auto
   5.258 +qed
   5.259 +
   5.260 +lemma closed_contains_Sup:
   5.261 +  fixes S :: "real set"
   5.262 +  shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
   5.263 +  by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
   5.264 +
   5.265 +lemma deriv_nonneg_imp_mono:
   5.266 +  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   5.267 +  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   5.268 +  assumes ab: "a \<le> b"
   5.269 +  shows "g a \<le> g b"
   5.270 +proof (cases "a < b")
   5.271 +  assume "a < b"
   5.272 +  from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
   5.273 +  from MVT2[OF `a < b` this] and deriv 
   5.274 +    obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
   5.275 +  from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
   5.276 +  with g_ab show ?thesis by simp
   5.277 +qed (insert ab, simp)
   5.278 +
   5.279 +lemma continuous_interval_vimage_Int:
   5.280 +  assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   5.281 +  assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}"
   5.282 +  obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d"
   5.283 +proof-
   5.284 +    let ?A = "{a..b} \<inter> g -` {c..d}"
   5.285 +    from IVT'[of g a c b, OF _ _ `a \<le> b` assms(1)] assms(4,5) 
   5.286 +         obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto
   5.287 +    from IVT'[of g a d b, OF _ _ `a \<le> b` assms(1)] assms(4,5) 
   5.288 +         obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto
   5.289 +    hence [simp]: "?A \<noteq> {}" by blast
   5.290 +
   5.291 +    def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A"
   5.292 +    have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def
   5.293 +        by (intro subsetI) (auto intro: cInf_lower cSup_upper)
   5.294 +    moreover from assms have "closed ?A" 
   5.295 +        using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
   5.296 +    hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def
   5.297 +        by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
   5.298 +    hence "{c'..d'} \<subseteq> ?A" using assms 
   5.299 +        by (intro subsetI)
   5.300 +           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] 
   5.301 +                 intro!: mono)
   5.302 +    moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
   5.303 +    moreover have "g c' \<le> c" "g d' \<ge> d"
   5.304 +      apply (insert c'' d'' c'd'_in_set)
   5.305 +      apply (subst c''(2)[symmetric])
   5.306 +      apply (auto simp: c'_def intro!: mono cInf_lower c'') []
   5.307 +      apply (subst d''(2)[symmetric])
   5.308 +      apply (auto simp: d'_def intro!: mono cSup_upper d'') []
   5.309 +      done
   5.310 +    with c'd'_in_set have "g c' = c" "g d' = d" by auto
   5.311 +    ultimately show ?thesis using that by blast
   5.312 +qed
   5.313 +
   5.314 +lemma nn_integral_substitution_aux:
   5.315 +  fixes f :: "real \<Rightarrow> ereal"
   5.316 +  assumes Mf: "f \<in> borel_measurable borel"
   5.317 +  assumes nonnegf: "\<And>x. f x \<ge> 0"
   5.318 +  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   5.319 +  assumes contg': "continuous_on {a..b} g'" 
   5.320 +  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   5.321 +  assumes "a < b"
   5.322 +  shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
   5.323 +             (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
   5.324 +proof-
   5.325 +  from `a < b` have [simp]: "a \<le> b" by simp
   5.326 +  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   5.327 +  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and 
   5.328 +                             Mg': "set_borel_measurable borel {a..b} g'" 
   5.329 +      by (simp_all only: set_measurable_continuous_on_ivl)
   5.330 +  from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
   5.331 +    by (simp only: has_field_derivative_iff_has_vector_derivative)
   5.332 +
   5.333 +  have real_ind[simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x" 
   5.334 +      by (auto split: split_indicator)
   5.335 +  have ereal_ind[simp]: "\<And>A x. ereal (indicator A x) = indicator A x" 
   5.336 +      by (auto split: split_indicator)
   5.337 +  have [simp]: "\<And>x A. indicator A (g x) = indicator (g -` A) x" 
   5.338 +      by (auto split: split_indicator)
   5.339 +
   5.340 +  from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   5.341 +    by (rule deriv_nonneg_imp_mono) simp_all
   5.342 +  with monog have [simp]: "g a \<le> g b" by (auto intro: mono_onD)
   5.343 +
   5.344 +  show ?thesis
   5.345 +  proof (induction rule: borel_measurable_induct[OF Mf nonnegf, case_names cong set mult add sup])
   5.346 +    case (cong f1 f2)
   5.347 +    from cong.hyps(3) have "f1 = f2" by auto
   5.348 +    with cong show ?case by simp
   5.349 +  next
   5.350 +    case (set A)
   5.351 +    from set.hyps show ?case
   5.352 +    proof (induction rule: borel_set_induct)
   5.353 +      case empty
   5.354 +      thus ?case by simp
   5.355 +    next
   5.356 +      case (interval c d)
   5.357 +      {
   5.358 +        fix u v :: real assume asm: "{u..v} \<subseteq> {g a..g b}" "u \<le> v"
   5.359 +        
   5.360 +        obtain u' v' where u'v': "{a..b} \<inter> g-`{u..v} = {u'..v'}" "u' \<le> v'" "g u' = u" "g v' = v"
   5.361 +             using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all
   5.362 +        hence "{u'..v'} \<subseteq> {a..b}" "{u'..v'} \<subseteq> g -` {u..v}" by blast+
   5.363 +        with u'v'(2) have "u' \<in> g -` {u..v}" "v' \<in> g -` {u..v}" by auto
   5.364 +        from u'v'(1) have [simp]: "{a..b} \<inter> g -` {u..v} \<in> sets borel" by simp
   5.365 +        
   5.366 +        have A: "continuous_on {min u' v'..max u' v'} g'"
   5.367 +            by (simp only: u'v' max_absorb2 min_absorb1) 
   5.368 +               (intro continuous_on_subset[OF contg'], insert u'v', auto)
   5.369 +        have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})"
   5.370 +           using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF `{u'..v'} \<subseteq> {a..b}`]) auto
   5.371 +        hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow> 
   5.372 +                      (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" 
   5.373 +            by (simp only: u'v' max_absorb2 min_absorb1) 
   5.374 +               (auto simp: has_field_derivative_iff_has_vector_derivative)
   5.375 +        have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
   5.376 +          by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all
   5.377 +        hence "(\<integral>\<^sup>+x. ereal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) = 
   5.378 +                   LBINT x:{a..b} \<inter> g-`{u..v}. g' x" 
   5.379 +          by (subst ereal_ind[symmetric], subst times_ereal.simps, subst nn_integral_eq_integral)
   5.380 +             (auto intro: measurable_sets Mg simp: derivg_nonneg mult.commute split: split_indicator)
   5.381 +        also from interval_integral_FTC_finite[OF A B]
   5.382 +            have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u"
   5.383 +                by (simp add: u'v' interval_integral_Icc `u \<le> v`)
   5.384 +        finally have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) =
   5.385 +                           ereal (v - u)" .
   5.386 +      } note A = this
   5.387 +  
   5.388 +      have "(\<integral>\<^sup>+x. indicator {c..d} (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) =
   5.389 +               (\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {c..d}) x \<partial>lborel)" 
   5.390 +        by (intro nn_integral_cong) (simp split: split_indicator)
   5.391 +      also have "{a..b} \<inter> g-`{c..d} = {a..b} \<inter> g-`{max (g a) c..min (g b) d}" 
   5.392 +        using `a \<le> b` `c \<le> d`
   5.393 +        by (auto intro!: monog intro: order.trans)
   5.394 +      also have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ... x \<partial>lborel) =
   5.395 +        (if max (g a) c \<le> min (g b) d then min (g b) d - max (g a) c else 0)"
   5.396 +         using `c \<le> d` by (simp add: A)
   5.397 +      also have "... = (\<integral>\<^sup>+ x. indicator ({g a..g b} \<inter> {c..d}) x \<partial>lborel)"
   5.398 +        by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:)
   5.399 +      also have "... = (\<integral>\<^sup>+ x. indicator {c..d} x * indicator {g a..g b} x \<partial>lborel)"
   5.400 +        by (intro nn_integral_cong) (auto split: split_indicator)
   5.401 +      finally show ?case ..
   5.402 +
   5.403 +      next
   5.404 +
   5.405 +      case (compl A)
   5.406 +      note `A \<in> sets borel`[measurable]
   5.407 +      from emeasure_mono[of "A \<inter> {g a..g b}" "{g a..g b}" lborel]
   5.408 +          have [simp]: "emeasure lborel (A \<inter> {g a..g b}) \<noteq> \<infinity>" by auto
   5.409 +      have [simp]: "g -` A \<inter> {a..b} \<in> sets borel"
   5.410 +        by (rule set_borel_measurable_sets[OF Mg]) auto
   5.411 +      have [simp]: "g -` (-A) \<inter> {a..b} \<in> sets borel"
   5.412 +        by (rule set_borel_measurable_sets[OF Mg]) auto
   5.413 +
   5.414 +      have "(\<integral>\<^sup>+x. indicator (-A) x * indicator {g a..g b} x \<partial>lborel) = 
   5.415 +                (\<integral>\<^sup>+x. indicator (-A \<inter> {g a..g b}) x \<partial>lborel)" 
   5.416 +        by (rule nn_integral_cong) (simp split: split_indicator)
   5.417 +      also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg
   5.418 +        by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
   5.419 +      also have "{g a..g b} - A = {g a..g b} - A \<inter> {g a..g b}" by blast
   5.420 +      also have "emeasure lborel ... = g b - g a - emeasure lborel (A \<inter> {g a..g b})"
   5.421 +             using `A \<in> sets borel` by (subst emeasure_Diff) (auto simp: real_of_ereal_minus)
   5.422 +     also have "emeasure lborel (A \<inter> {g a..g b}) = 
   5.423 +                    \<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel" 
   5.424 +       using `A \<in> sets borel`
   5.425 +       by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong)
   5.426 +          (simp split: split_indicator)
   5.427 +      also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
   5.428 +        by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
   5.429 +      also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
   5.430 +        by (intro integral_FTC_atLeastAtMost[symmetric])
   5.431 +           (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
   5.432 +                 has_vector_derivative_at_within)
   5.433 +      also have "ereal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
   5.434 +        using borel_integrable_atLeastAtMost'[OF contg']
   5.435 +        by (subst nn_integral_eq_integral)
   5.436 +           (simp_all add: mult.commute derivg_nonneg split: split_indicator)
   5.437 +      also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x))
   5.438 +                            \<in> borel_measurable borel" using Mg'
   5.439 +        by (intro borel_measurable_ereal_times borel_measurable_indicator)
   5.440 +           (simp_all add: mult.commute)
   5.441 +      have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<le>
   5.442 +                        (\<integral>\<^sup>+x. ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   5.443 +         by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
   5.444 +      note integrable = borel_integrable_atLeastAtMost'[OF contg']
   5.445 +      with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> \<infinity>"
   5.446 +          by (auto simp: real_integrable_def nn_integral_set_ereal mult.commute)
   5.447 +      have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I = 
   5.448 +                  \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) - 
   5.449 +                        indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel"
   5.450 +        apply (intro nn_integral_diff[symmetric])
   5.451 +        apply (insert Mg', simp add: mult.commute) []
   5.452 +        apply (insert Mg'', simp) []
   5.453 +        apply (simp split: split_indicator add: derivg_nonneg)
   5.454 +        apply (rule notinf)
   5.455 +        apply (simp split: split_indicator add: derivg_nonneg)
   5.456 +        done
   5.457 +      also have "... = \<integral>\<^sup>+ x. indicator (-A) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   5.458 +        by (intro nn_integral_cong) (simp split: split_indicator)
   5.459 +      finally show ?case .
   5.460 +
   5.461 +    next
   5.462 +      case (union f)
   5.463 +      then have [simp]: "\<And>i. {a..b} \<inter> g -` f i \<in> sets borel"
   5.464 +        by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto
   5.465 +      have "g -` (\<Union>i. f i) \<inter> {a..b} = (\<Union>i. {a..b} \<inter> g -` f i)" by auto
   5.466 +      hence "g -` (\<Union>i. f i) \<inter> {a..b} \<in> sets borel" by (auto simp del: UN_simps)
   5.467 +
   5.468 +      have "(\<integral>\<^sup>+x. indicator (\<Union>i. f i) x * indicator {g a..g b} x \<partial>lborel) = 
   5.469 +                \<integral>\<^sup>+x. indicator (\<Union>i. {g a..g b} \<inter> f i) x \<partial>lborel"
   5.470 +          by (intro nn_integral_cong) (simp split: split_indicator)
   5.471 +      also from union have "... = emeasure lborel (\<Union>i. {g a..g b} \<inter> f i)" by simp
   5.472 +      also from union have "... = (\<Sum>i. emeasure lborel ({g a..g b} \<inter> f i))"
   5.473 +        by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def)
   5.474 +      also from union have "... = (\<Sum>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel)" by simp
   5.475 +      also have "(\<lambda>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel) = 
   5.476 +                           (\<lambda>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel)"
   5.477 +        by (intro ext nn_integral_cong) (simp split: split_indicator)
   5.478 +      also from union.IH have "(\<Sum>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel) = 
   5.479 +          (\<Sum>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" by simp
   5.480 +      also have "(\<lambda>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) =
   5.481 +                         (\<lambda>i. \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x \<partial>lborel)"
   5.482 +        by (intro ext nn_integral_cong) (simp split: split_indicator)
   5.483 +      also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel"
   5.484 +        using Mg'
   5.485 +        apply (intro nn_integral_suminf[symmetric])
   5.486 +        apply (rule borel_measurable_ereal_times, simp add: borel_measurable_ereal mult.commute)
   5.487 +        apply (rule borel_measurable_indicator, subst sets_lborel)
   5.488 +        apply (simp_all split: split_indicator add: derivg_nonneg)
   5.489 +        done
   5.490 +      also have "(\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) =
   5.491 +                      (\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x)"
   5.492 +        by (intro ext) (simp split: split_indicator)
   5.493 +      also have "(\<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x) \<partial>lborel) =
   5.494 +                     \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * (\<Sum>i. indicator (g -` f i) x) \<partial>lborel"
   5.495 +        by (intro nn_integral_cong suminf_cmult_ereal) (auto split: split_indicator simp: derivg_nonneg)
   5.496 +      also from union have "(\<lambda>x. \<Sum>i. indicator (g -` f i) x :: ereal) = (\<lambda>x. indicator (\<Union>i. g -` f i) x)"
   5.497 +        by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def)
   5.498 +      also have "(\<integral>\<^sup>+x. ereal (g' x * indicator {a..b} x) * ... x \<partial>lborel) =
   5.499 +                    (\<integral>\<^sup>+x. indicator (\<Union>i. f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   5.500 +       by (intro nn_integral_cong) (simp split: split_indicator)
   5.501 +      finally show ?case .
   5.502 +  qed
   5.503 +
   5.504 +next
   5.505 +  case (mult f c)
   5.506 +    note Mf[measurable] = `f \<in> borel_measurable borel`
   5.507 +    let ?I = "indicator {a..b}"
   5.508 +    have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   5.509 +      by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf])
   5.510 +         (simp_all add: borel_measurable_ereal mult.commute)
   5.511 +    also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)"
   5.512 +      by (intro ext) (simp split: split_indicator)
   5.513 +    finally have Mf': "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" .
   5.514 +    with mult show ?case
   5.515 +      by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac)
   5.516 + 
   5.517 +next
   5.518 +  case (add f2 f1)
   5.519 +    let ?I = "indicator {a..b}"
   5.520 +    {
   5.521 +      fix f :: "real \<Rightarrow> ereal" assume Mf: "f \<in> borel_measurable borel"
   5.522 +      have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   5.523 +        by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf])
   5.524 +           (simp_all add: borel_measurable_ereal mult.commute)
   5.525 +      also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)"
   5.526 +        by (intro ext) (simp split: split_indicator)
   5.527 +      finally have "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" .
   5.528 +    } note Mf' = this[OF `f1 \<in> borel_measurable borel`] this[OF `f2 \<in> borel_measurable borel`]
   5.529 +    from add have not_neginf: "\<And>x. f1 x \<noteq> -\<infinity>" "\<And>x. f2 x \<noteq> -\<infinity>" 
   5.530 +      by (metis Infty_neq_0(1) ereal_0_le_uminus_iff ereal_infty_less_eq(1))+
   5.531 +
   5.532 +    have "(\<integral>\<^sup>+ x. (f1 x + f2 x) * indicator {g a..g b} x \<partial>lborel) =
   5.533 +             (\<integral>\<^sup>+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x \<partial>lborel)"
   5.534 +      by (intro nn_integral_cong) (simp split: split_indicator)
   5.535 +    also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) +
   5.536 +                                (\<integral>\<^sup>+ x. f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   5.537 +      by (simp_all add: nn_integral_add)
   5.538 +    also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x + 
   5.539 +                                      f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   5.540 +      by (intro nn_integral_add[symmetric])
   5.541 +         (auto simp add: Mf' derivg_nonneg split: split_indicator)
   5.542 +    also from not_neginf have "... = \<integral>\<^sup>+ x. (f1 (g x) + f2 (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   5.543 +      by (intro nn_integral_cong) (simp split: split_indicator add: ereal_distrib)
   5.544 +    finally show ?case .
   5.545 +
   5.546 +next
   5.547 +  case (sup F)
   5.548 +  {
   5.549 +    fix i
   5.550 +    let ?I = "indicator {a..b}"
   5.551 +    have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
   5.552 +      by (rule_tac borel_measurable_ereal_times, rule_tac measurable_compose[OF _ sup.hyps(1)])
   5.553 +         (simp_all add: mult.commute)
   5.554 +    also have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ereal (g' x) * ?I x)"
   5.555 +      by (intro ext) (simp split: split_indicator)
   5.556 +     finally have "... \<in> borel_measurable borel" .
   5.557 +  } note Mf' = this
   5.558 +
   5.559 +    have "(\<integral>\<^sup>+x. (SUP i. F i x) * indicator {g a..g b} x \<partial>lborel) = 
   5.560 +               \<integral>\<^sup>+x. (SUP i. F i x* indicator {g a..g b} x) \<partial>lborel"
   5.561 +      by (intro nn_integral_cong) (simp split: split_indicator)
   5.562 +    also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i x* indicator {g a..g b} x \<partial>lborel)"
   5.563 +      by (intro nn_integral_monotone_convergence_SUP)
   5.564 +         (auto simp: incseq_def le_fun_def split: split_indicator)
   5.565 +    also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
   5.566 +      by simp
   5.567 +    also from sup have "... =  \<integral>\<^sup>+x. (SUP i. F i (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel"
   5.568 +      by (intro nn_integral_monotone_convergence_SUP[symmetric])
   5.569 +         (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
   5.570 +               intro!: ereal_mult_right_mono)
   5.571 +    also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   5.572 +      by (subst mult.assoc, subst mult.commute, subst SUP_ereal_cmult)
   5.573 +         (auto split: split_indicator simp: derivg_nonneg mult_ac)
   5.574 +    finally show ?case by simp
   5.575 +  qed
   5.576 +qed
   5.577 +
   5.578 +lemma nn_integral_substitution:
   5.579 +  fixes f :: "real \<Rightarrow> real"
   5.580 +  assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
   5.581 +  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   5.582 +  assumes contg': "continuous_on {a..b} g'" 
   5.583 +  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   5.584 +  assumes "a \<le> b"
   5.585 +  shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
   5.586 +             (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
   5.587 +proof (cases "a = b")
   5.588 +  assume "a \<noteq> b"
   5.589 +  with `a \<le> b` have "a < b" by auto
   5.590 +  let ?f' = "\<lambda>x. max 0 (f x * indicator {g a..g b} x)"
   5.591 +
   5.592 +  from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   5.593 +    by (rule deriv_nonneg_imp_mono) simp_all
   5.594 +  have bounds: "\<And>x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g x \<ge> g a" "\<And>x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g x \<le> g b"
   5.595 +    by (auto intro: monog)
   5.596 +
   5.597 +  from derivg_nonneg have nonneg: 
   5.598 +    "\<And>f x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g' x \<noteq> 0 \<Longrightarrow> f x * ereal (g' x) \<ge> 0 \<Longrightarrow> f x \<ge> 0"
   5.599 +    by (force simp: ereal_zero_le_0_iff field_simps)
   5.600 +  have nonneg': "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<not> 0 \<le> f (g x) \<Longrightarrow> 0 \<le> f (g x) * g' x \<Longrightarrow> g' x = 0"
   5.601 +    by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff)
   5.602 +
   5.603 +  have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
   5.604 +            (\<integral>\<^sup>+x. ereal (?f' x) * indicator {g a..g b} x \<partial>lborel)"
   5.605 +    by (subst nn_integral_max_0[symmetric], intro nn_integral_cong) 
   5.606 +       (auto split: split_indicator simp: zero_ereal_def)
   5.607 +  also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel" using Mf
   5.608 +    by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg `a < b`]) 
   5.609 +       (auto simp add: zero_ereal_def mult.commute)
   5.610 +  also have "... = \<integral>\<^sup>+ x. max 0 (f (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   5.611 +    by (intro nn_integral_cong) 
   5.612 +       (auto split: split_indicator simp: max_def dest: bounds)
   5.613 +  also have "... = \<integral>\<^sup>+ x. max 0 (f (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel"
   5.614 +    by (intro nn_integral_cong)
   5.615 +       (auto simp: max_def derivg_nonneg split: split_indicator intro!: nonneg')
   5.616 +  also have "... = \<integral>\<^sup>+ x. f (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
   5.617 +    by (rule nn_integral_max_0)
   5.618 +  also have "... = \<integral>\<^sup>+x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
   5.619 +    by (intro nn_integral_cong) (simp split: split_indicator)
   5.620 +  finally show ?thesis .
   5.621 +qed auto
   5.622 +
   5.623 +lemma integral_substitution:
   5.624 +  assumes integrable: "set_integrable lborel {g a..g b} f"
   5.625 +  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   5.626 +  assumes contg': "continuous_on {a..b} g'" 
   5.627 +  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   5.628 +  assumes "a \<le> b"
   5.629 +  shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   5.630 +    and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
   5.631 +proof-
   5.632 +  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   5.633 +  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and 
   5.634 +                             Mg': "set_borel_measurable borel {a..b} g'" 
   5.635 +      by (simp_all only: set_measurable_continuous_on_ivl)
   5.636 +  from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   5.637 +    by (rule deriv_nonneg_imp_mono) simp_all
   5.638 +
   5.639 +  have "(\<lambda>x. ereal (f x) * indicator {g a..g b} x) = 
   5.640 +           (\<lambda>x. ereal (f x * indicator {g a..g b} x))" 
   5.641 +    by (intro ext) (simp split: split_indicator)
   5.642 +  with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel"
   5.643 +    unfolding real_integrable_def by (force simp: mult.commute)
   5.644 +  have "(\<lambda>x. ereal (-f x) * indicator {g a..g b} x) = 
   5.645 +           (\<lambda>x. -ereal (f x * indicator {g a..g b} x))" 
   5.646 +    by (intro ext) (simp split: split_indicator)
   5.647 +  with integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
   5.648 +    unfolding real_integrable_def by (force simp: mult.commute)
   5.649 +
   5.650 +  have "LBINT x. (f x :: real) * indicator {g a..g b} x = 
   5.651 +          real (\<integral>\<^sup>+ x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) -
   5.652 +          real (\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
   5.653 +    by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ereal mult.commute)
   5.654 +  also have "(\<integral>\<^sup>+x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) =
   5.655 +               (\<integral>\<^sup>+x. ereal (f x * indicator {g a..g b} x) \<partial>lborel)"
   5.656 +    by (intro nn_integral_cong) (simp split: split_indicator)
   5.657 +  also with M1 have A: "(\<integral>\<^sup>+ x. ereal (f x * indicator {g a..g b} x) \<partial>lborel) =
   5.658 +                            (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
   5.659 +    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`]) 
   5.660 +       (auto simp: nn_integral_set_ereal mult.commute)
   5.661 +  also have "(\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
   5.662 +               (\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
   5.663 +    by (intro nn_integral_cong) (simp split: split_indicator)
   5.664 +  also with M2 have B: "(\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
   5.665 +                            (\<integral>\<^sup>+ x. ereal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
   5.666 +    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`])
   5.667 +       (auto simp: nn_integral_set_ereal mult.commute)
   5.668 +
   5.669 +  also {
   5.670 +    from integrable have Mf: "set_borel_measurable borel {g a..g b} f" 
   5.671 +      unfolding real_integrable_def by simp
   5.672 +    from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg']
   5.673 +      have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
   5.674 +                     (g' x * indicator {a..b} x)) \<in> borel_measurable borel"  (is "?f \<in> _") 
   5.675 +      by (simp add: mult.commute)
   5.676 +    also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)"
   5.677 +      using monog by (intro ext) (auto split: split_indicator)
   5.678 +    finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   5.679 +      using A B integrable unfolding real_integrable_def 
   5.680 +      by (simp_all add: nn_integral_set_ereal mult.commute)
   5.681 +  } note integrable' = this
   5.682 +
   5.683 +  have "real (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) -
   5.684 +                  real (\<integral>\<^sup>+ x. ereal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
   5.685 +                (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable'
   5.686 +    by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
   5.687 +  finally show "(LBINT x. f x * indicator {g a..g b} x) = 
   5.688 +                     (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
   5.689 +qed
   5.690 +
   5.691 +lemma interval_integral_substitution:
   5.692 +  assumes integrable: "set_integrable lborel {g a..g b} f"
   5.693 +  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   5.694 +  assumes contg': "continuous_on {a..b} g'" 
   5.695 +  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   5.696 +  assumes "a \<le> b"
   5.697 +  shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
   5.698 +    and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)"
   5.699 +  apply (rule integral_substitution[OF assms], simp, simp)
   5.700 +  apply (subst (1 2) interval_integral_Icc, fact)
   5.701 +  apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
   5.702 +  using integral_substitution(2)[OF assms]
   5.703 +  apply (simp add: mult.commute)
   5.704 +  done
   5.705 +
   5.706 +lemma set_borel_integrable_singleton[simp]:
   5.707 +  "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
   5.708 +  by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto
   5.709 +
   5.710 +end
     6.1 --- a/src/HOL/Probability/Probability.thy	Thu Dec 04 21:28:35 2014 +0100
     6.2 +++ b/src/HOL/Probability/Probability.thy	Fri Dec 05 12:06:18 2014 +0100
     6.3 @@ -1,3 +1,7 @@
     6.4 +(*  Title:      HOL/Probability/Probability.thy
     6.5 +    Author:     Johannes Hölzl, TU München
     6.6 +*)
     6.7 +
     6.8  theory Probability
     6.9  imports
    6.10    Discrete_Topology
    6.11 @@ -7,6 +11,9 @@
    6.12    Distributions
    6.13    Probability_Mass_Function
    6.14    Stream_Space
    6.15 +  Embed_Measure
    6.16 +  Interval_Integral
    6.17 +  Set_Integral
    6.18    Giry_Monad
    6.19  begin
    6.20  
     7.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Dec 04 21:28:35 2014 +0100
     7.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Dec 05 12:06:18 2014 +0100
     7.3 @@ -385,7 +385,7 @@
     7.4      by (simp split: split_indicator)
     7.5    show "AE x in density (count_space UNIV) (ereal \<circ> f).
     7.6      measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
     7.7 -    by (simp add: AE_density nonneg emeasure_density measure_def nn_integral_cmult_indicator)
     7.8 +    by (simp add: AE_density nonneg measure_def emeasure_density max_def)
     7.9    show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
    7.10      by default (simp add: emeasure_density prob)
    7.11  qed simp
    7.12 @@ -395,7 +395,7 @@
    7.13    have *[simp]: "\<And>x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y"
    7.14      by (simp split: split_indicator)
    7.15    fix x show "measure (density (count_space UNIV) (ereal \<circ> f)) {x} = f x"
    7.16 -    by transfer (simp add: measure_def emeasure_density nn_integral_cmult_indicator nonneg)
    7.17 +    by transfer (simp add: measure_def emeasure_density nonneg max_def)
    7.18  qed
    7.19  
    7.20  end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Probability/Set_Integral.thy	Fri Dec 05 12:06:18 2014 +0100
     8.3 @@ -0,0 +1,597 @@
     8.4 +(*  Title:      HOL/Probability/Set_Integral.thy
     8.5 +    Author:     Jeremy Avigad, Johannes Hölzl, Luke Serafin
     8.6 +
     8.7 +Notation and useful facts for working with integrals over a set.
     8.8 +
     8.9 +TODO: keep all these? Need unicode translations as well.
    8.10 +*)
    8.11 +
    8.12 +theory Set_Integral
    8.13 +  imports Bochner_Integration Lebesgue_Measure
    8.14 +begin
    8.15 +
    8.16 +(* 
    8.17 +    Notation
    8.18 +*)
    8.19 +
    8.20 +syntax
    8.21 +"_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
    8.22 +("(3LINT _|_. _)" [0,110,60] 60)
    8.23 +
    8.24 +translations
    8.25 +"LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
    8.26 +
    8.27 +abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
    8.28 +
    8.29 +abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
    8.30 +
    8.31 +abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
    8.32 +
    8.33 +syntax
    8.34 +"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
    8.35 +("(4LINT _:_|_. _)" [0,60,110,61] 60)
    8.36 +
    8.37 +translations
    8.38 +"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
    8.39 +
    8.40 +abbreviation
    8.41 +  "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x"
    8.42 +
    8.43 +syntax
    8.44 +  "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
    8.45 +("AE _\<in>_ in _. _" [0,0,0,10] 10)
    8.46 +
    8.47 +translations
    8.48 +  "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)"
    8.49 +
    8.50 +(*
    8.51 +    Notation for integration wrt lebesgue measure on the reals:
    8.52 +
    8.53 +      LBINT x. f
    8.54 +      LBINT x : A. f
    8.55 +
    8.56 +    TODO: keep all these? Need unicode.
    8.57 +*)
    8.58 +
    8.59 +syntax
    8.60 +"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
    8.61 +("(2LBINT _. _)" [0,60] 60)
    8.62 +
    8.63 +translations
    8.64 +"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
    8.65 +
    8.66 +syntax
    8.67 +"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
    8.68 +("(3LBINT _:_. _)" [0,60,61] 60)
    8.69 +
    8.70 +translations
    8.71 +"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
    8.72 +
    8.73 +(* 
    8.74 +    Basic properties 
    8.75 +*)
    8.76 +
    8.77 +(*
    8.78 +lemma indicator_abs_eq: "\<And>A x. abs (indicator A x) = ((indicator A x) :: real)"
    8.79 +  by (auto simp add: indicator_def)
    8.80 +*)
    8.81 +
    8.82 +lemma set_lebesgue_integral_cong:
    8.83 +  assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
    8.84 +  shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
    8.85 +  using assms by (auto intro!: integral_cong split: split_indicator simp add: sets.sets_into_space)
    8.86 +
    8.87 +lemma set_lebesgue_integral_cong_AE:
    8.88 +  assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
    8.89 +  assumes "AE x \<in> A in M. f x = g x"
    8.90 +  shows "LINT x:A|M. f x = LINT x:A|M. g x"
    8.91 +proof-
    8.92 +  have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
    8.93 +    using assms by auto
    8.94 +  thus ?thesis by (intro integral_cong_AE) auto
    8.95 +qed
    8.96 +
    8.97 +lemma set_integrable_cong_AE:
    8.98 +    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
    8.99 +    AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow> 
   8.100 +    set_integrable M A f = set_integrable M A g"
   8.101 +  by (rule integrable_cong_AE) auto
   8.102 +
   8.103 +lemma set_integrable_subset: 
   8.104 +  fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.105 +  assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"  
   8.106 +  shows "set_integrable M B f"
   8.107 +proof -
   8.108 +  have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
   8.109 +    by (rule integrable_mult_indicator) fact+
   8.110 +  with `B \<subseteq> A` show ?thesis
   8.111 +    by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
   8.112 +qed
   8.113 +
   8.114 +(* TODO: integral_cmul_indicator should be named set_integral_const *)
   8.115 +(* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
   8.116 +
   8.117 +lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
   8.118 +  by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)
   8.119 +
   8.120 +lemma set_integral_mult_right [simp]: 
   8.121 +  fixes a :: "'a::{real_normed_field, second_countable_topology}"
   8.122 +  shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
   8.123 +  by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)
   8.124 +
   8.125 +lemma set_integral_mult_left [simp]: 
   8.126 +  fixes a :: "'a::{real_normed_field, second_countable_topology}"
   8.127 +  shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
   8.128 +  by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
   8.129 +
   8.130 +lemma set_integral_divide_zero [simp]: 
   8.131 +  fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}"
   8.132 +  shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
   8.133 +  by (subst integral_divide_zero[symmetric], intro integral_cong)
   8.134 +     (auto split: split_indicator)
   8.135 +
   8.136 +lemma set_integrable_scaleR_right [simp, intro]:
   8.137 +  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
   8.138 +  unfolding scaleR_left_commute by (rule integrable_scaleR_right)
   8.139 +
   8.140 +lemma set_integrable_scaleR_left [simp, intro]:
   8.141 +  fixes a :: "_ :: {banach, second_countable_topology}"
   8.142 +  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
   8.143 +  using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   8.144 +
   8.145 +lemma set_integrable_mult_right [simp, intro]:
   8.146 +  fixes a :: "'a::{real_normed_field, second_countable_topology}"
   8.147 +  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
   8.148 +  using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   8.149 +
   8.150 +lemma set_integrable_mult_left [simp, intro]:
   8.151 +  fixes a :: "'a::{real_normed_field, second_countable_topology}"
   8.152 +  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
   8.153 +  using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
   8.154 +
   8.155 +lemma set_integrable_divide [simp, intro]:
   8.156 +  fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}"
   8.157 +  assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
   8.158 +  shows "set_integrable M A (\<lambda>t. f t / a)"
   8.159 +proof -
   8.160 +  have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
   8.161 +    using assms by (rule integrable_divide_zero)
   8.162 +  also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
   8.163 +    by (auto split: split_indicator)
   8.164 +  finally show ?thesis .
   8.165 +qed
   8.166 +
   8.167 +lemma set_integral_add [simp, intro]:
   8.168 +  fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.169 +  assumes "set_integrable M A f" "set_integrable M A g"
   8.170 +  shows "set_integrable M A (\<lambda>x. f x + g x)"
   8.171 +    and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
   8.172 +  using assms by (simp_all add: scaleR_add_right)
   8.173 +
   8.174 +lemma set_integral_diff [simp, intro]:
   8.175 +  assumes "set_integrable M A f" "set_integrable M A g"
   8.176 +  shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
   8.177 +    (LINT x:A|M. f x) - (LINT x:A|M. g x)"
   8.178 +  using assms by (simp_all add: scaleR_diff_right)
   8.179 +
   8.180 +lemma set_integral_reflect:
   8.181 +  fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   8.182 +  shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
   8.183 +  using assms
   8.184 +  by (subst lborel_integral_real_affine[where c="-1" and t=0])
   8.185 +     (auto intro!: integral_cong split: split_indicator)
   8.186 +
   8.187 +(* question: why do we have this for negation, but multiplication by a constant
   8.188 +   requires an integrability assumption? *)
   8.189 +lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
   8.190 +  by (subst integral_minus[symmetric]) simp_all
   8.191 +
   8.192 +lemma set_integral_complex_of_real:
   8.193 +  "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
   8.194 +  by (subst integral_complex_of_real[symmetric])
   8.195 +     (auto intro!: integral_cong split: split_indicator)
   8.196 +
   8.197 +lemma set_integral_mono:
   8.198 +  fixes f g :: "_ \<Rightarrow> real"
   8.199 +  assumes "set_integrable M A f" "set_integrable M A g"
   8.200 +    "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   8.201 +  shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
   8.202 +using assms by (auto intro: integral_mono split: split_indicator)
   8.203 +
   8.204 +lemma set_integral_mono_AE: 
   8.205 +  fixes f g :: "_ \<Rightarrow> real"
   8.206 +  assumes "set_integrable M A f" "set_integrable M A g"
   8.207 +    "AE x \<in> A in M. f x \<le> g x"
   8.208 +  shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
   8.209 +using assms by (auto intro: integral_mono_AE split: split_indicator)
   8.210 +
   8.211 +lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
   8.212 +  using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
   8.213 +
   8.214 +lemma set_integrable_abs_iff:
   8.215 +  fixes f :: "_ \<Rightarrow> real"
   8.216 +  shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f" 
   8.217 +  by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
   8.218 +
   8.219 +lemma set_integrable_abs_iff':
   8.220 +  fixes f :: "_ \<Rightarrow> real"
   8.221 +  shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow> 
   8.222 +    set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
   8.223 +by (intro set_integrable_abs_iff) auto
   8.224 +
   8.225 +lemma set_integrable_discrete_difference:
   8.226 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   8.227 +  assumes "countable X"
   8.228 +  assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   8.229 +  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   8.230 +  shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
   8.231 +proof (rule integrable_discrete_difference[where X=X])
   8.232 +  show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
   8.233 +    using diff by (auto split: split_indicator)
   8.234 +qed fact+
   8.235 +
   8.236 +lemma set_integral_discrete_difference:
   8.237 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   8.238 +  assumes "countable X"
   8.239 +  assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   8.240 +  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   8.241 +  shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
   8.242 +proof (rule integral_discrete_difference[where X=X])
   8.243 +  show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
   8.244 +    using diff by (auto split: split_indicator)
   8.245 +qed fact+
   8.246 +
   8.247 +lemma set_integrable_Un:
   8.248 +  fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.249 +  assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
   8.250 +    and [measurable]: "A \<in> sets M" "B \<in> sets M"
   8.251 +  shows "set_integrable M (A \<union> B) f"
   8.252 +proof -
   8.253 +  have "set_integrable M (A - B) f"
   8.254 +    using f_A by (rule set_integrable_subset) auto
   8.255 +  from integrable_add[OF this f_B] show ?thesis
   8.256 +    by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
   8.257 +qed
   8.258 +
   8.259 +lemma set_integrable_UN:
   8.260 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.261 +  assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
   8.262 +    "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
   8.263 +  shows "set_integrable M (\<Union>i\<in>I. A i) f"
   8.264 +using assms by (induct I) (auto intro!: set_integrable_Un)
   8.265 +
   8.266 +lemma set_integral_Un:
   8.267 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.268 +  assumes "A \<inter> B = {}"
   8.269 +  and "set_integrable M A f"
   8.270 +  and "set_integrable M B f"
   8.271 +  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   8.272 +by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
   8.273 +      scaleR_add_left assms)
   8.274 +
   8.275 +lemma set_integral_cong_set:
   8.276 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.277 +  assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
   8.278 +    and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
   8.279 +  shows "LINT x:B|M. f x = LINT x:A|M. f x"
   8.280 +proof (rule integral_cong_AE)
   8.281 +  show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
   8.282 +    using ae by (auto simp: subset_eq split: split_indicator)
   8.283 +qed fact+
   8.284 +
   8.285 +lemma set_borel_measurable_subset:
   8.286 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.287 +  assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
   8.288 +  shows "set_borel_measurable M B f"
   8.289 +proof -
   8.290 +  have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
   8.291 +    by measurable
   8.292 +  also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
   8.293 +    using `B \<subseteq> A` by (auto simp: fun_eq_iff split: split_indicator)
   8.294 +  finally show ?thesis .
   8.295 +qed
   8.296 +
   8.297 +lemma set_integral_Un_AE:
   8.298 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.299 +  assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
   8.300 +  and "set_integrable M A f"
   8.301 +  and "set_integrable M B f"
   8.302 +  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   8.303 +proof -
   8.304 +  have f: "set_integrable M (A \<union> B) f"
   8.305 +    by (intro set_integrable_Un assms)
   8.306 +  then have f': "set_borel_measurable M (A \<union> B) f"
   8.307 +    by (rule borel_measurable_integrable)
   8.308 +  have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
   8.309 +  proof (rule set_integral_cong_set)  
   8.310 +    show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
   8.311 +      using ae by auto
   8.312 +    show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
   8.313 +      using f' by (rule set_borel_measurable_subset) auto
   8.314 +  qed fact
   8.315 +  also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)"
   8.316 +    by (auto intro!: set_integral_Un set_integrable_subset[OF f])
   8.317 +  also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
   8.318 +    using ae
   8.319 +    by (intro arg_cong2[where f="op+"] set_integral_cong_set)
   8.320 +       (auto intro!: set_borel_measurable_subset[OF f'])
   8.321 +  finally show ?thesis .
   8.322 +qed
   8.323 +
   8.324 +lemma set_integral_finite_Union:
   8.325 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   8.326 +  assumes "finite I" "disjoint_family_on A I"
   8.327 +    and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
   8.328 +  shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
   8.329 +  using assms
   8.330 +  apply induct
   8.331 +  apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
   8.332 +by (subst set_integral_Un, auto intro: set_integrable_UN)
   8.333 +
   8.334 +(* TODO: find a better name? *)
   8.335 +lemma pos_integrable_to_top:
   8.336 +  fixes l::real
   8.337 +  assumes "\<And>i. A i \<in> sets M" "mono A"
   8.338 +  assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
   8.339 +  and intgbl: "\<And>i::nat. set_integrable M (A i) f"
   8.340 +  and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) ----> l"
   8.341 +  shows "set_integrable M (\<Union>i. A i) f"
   8.342 +  apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
   8.343 +  apply (rule intgbl)
   8.344 +  prefer 3 apply (rule lim)
   8.345 +  apply (rule AE_I2)
   8.346 +  using `mono A` apply (auto simp: mono_def nneg split: split_indicator) []
   8.347 +proof (rule AE_I2)
   8.348 +  { fix x assume "x \<in> space M"
   8.349 +    show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Union>i. A i) x *\<^sub>R f x"
   8.350 +    proof cases
   8.351 +      assume "\<exists>i. x \<in> A i"
   8.352 +      then guess i ..
   8.353 +      then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
   8.354 +        using `x \<in> A i` `mono A` by (auto simp: eventually_sequentially mono_def)
   8.355 +      show ?thesis
   8.356 +        apply (intro Lim_eventually)
   8.357 +        using *
   8.358 +        apply eventually_elim
   8.359 +        apply (auto split: split_indicator)
   8.360 +        done
   8.361 +    qed auto }
   8.362 +  then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
   8.363 +    apply (rule borel_measurable_LIMSEQ)
   8.364 +    apply assumption
   8.365 +    apply (intro borel_measurable_integrable intgbl)
   8.366 +    done
   8.367 +qed
   8.368 +
   8.369 +(* Proof from Royden Real Analysis, p. 91. *)
   8.370 +lemma lebesgue_integral_countable_add:
   8.371 +  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   8.372 +  assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
   8.373 +    and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
   8.374 +    and intgbl: "set_integrable M (\<Union>i. A i) f"
   8.375 +  shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
   8.376 +proof (subst integral_suminf[symmetric])
   8.377 +  show int_A: "\<And>i. set_integrable M (A i) f"
   8.378 +    using intgbl by (rule set_integrable_subset) auto
   8.379 +  { fix x assume "x \<in> space M"
   8.380 +    have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
   8.381 +      by (intro sums_scaleR_left indicator_sums) fact }
   8.382 +  note sums = this
   8.383 +
   8.384 +  have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
   8.385 +    using int_A[THEN integrable_norm] by auto
   8.386 +
   8.387 +  show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
   8.388 +    using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
   8.389 +
   8.390 +  show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
   8.391 +  proof (rule summableI_nonneg_bounded)
   8.392 +    fix n
   8.393 +    show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
   8.394 +      using norm_f by (auto intro!: integral_nonneg_AE)
   8.395 +    
   8.396 +    have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
   8.397 +      (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
   8.398 +      by (simp add: abs_mult)
   8.399 +    also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
   8.400 +      using norm_f
   8.401 +      by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
   8.402 +    also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   8.403 +      using intgbl[THEN integrable_norm]
   8.404 +      by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
   8.405 +         (auto split: split_indicator)
   8.406 +    finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
   8.407 +      set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   8.408 +      by simp
   8.409 +  qed
   8.410 +  show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
   8.411 +    apply (rule integral_cong[OF refl])
   8.412 +    apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
   8.413 +    using sums_unique[OF indicator_sums[OF disj]]
   8.414 +    apply auto
   8.415 +    done
   8.416 +qed
   8.417 +
   8.418 +lemma set_integral_cont_up:
   8.419 +  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   8.420 +  assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
   8.421 +  and intgbl: "set_integrable M (\<Union>i. A i) f"
   8.422 +  shows "(\<lambda>i. LINT x:(A i)|M. f x) ----> LINT x:(\<Union>i. A i)|M. f x"
   8.423 +proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
   8.424 +  have int_A: "\<And>i. set_integrable M (A i) f"
   8.425 +    using intgbl by (rule set_integrable_subset) auto
   8.426 +  then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
   8.427 +    "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   8.428 +    using intgbl integrable_norm[OF intgbl] by auto
   8.429 +  
   8.430 +  { fix x i assume "x \<in> A i"
   8.431 +    with A have "(\<lambda>xa. indicator (A xa) x::real) ----> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) ----> 1"
   8.432 +      by (intro filterlim_cong refl)
   8.433 +         (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
   8.434 +  then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Union>i. A i) x *\<^sub>R f x"
   8.435 +    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
   8.436 +qed (auto split: split_indicator)
   8.437 +        
   8.438 +(* Can the int0 hypothesis be dropped? *)
   8.439 +lemma set_integral_cont_down:
   8.440 +  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   8.441 +  assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
   8.442 +  and int0: "set_integrable M (A 0) f"
   8.443 +  shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) ----> LINT x:(\<Inter>i. A i)|M. f x"
   8.444 +proof (rule integral_dominated_convergence)
   8.445 +  have int_A: "\<And>i. set_integrable M (A i) f"
   8.446 +    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
   8.447 +  show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
   8.448 +    using int0[THEN integrable_norm] by simp
   8.449 +  have "set_integrable M (\<Inter>i. A i) f"
   8.450 +    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
   8.451 +  with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
   8.452 +    by auto
   8.453 +  show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
   8.454 +    using A by (auto split: split_indicator simp: decseq_def)
   8.455 +  { fix x i assume "x \<in> space M" "x \<notin> A i"
   8.456 +    with A have "(\<lambda>i. indicator (A i) x::real) ----> 0 \<longleftrightarrow> (\<lambda>i. 0::real) ----> 0"
   8.457 +      by (intro filterlim_cong refl)
   8.458 +         (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
   8.459 +  then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Inter>i. A i) x *\<^sub>R f x"
   8.460 +    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
   8.461 +qed
   8.462 +
   8.463 +lemma set_integral_at_point:
   8.464 +  fixes a :: real
   8.465 +  assumes "set_integrable M {a} f"
   8.466 +  and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
   8.467 +  shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
   8.468 +proof-
   8.469 +  have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
   8.470 +    by (intro set_lebesgue_integral_cong) simp_all
   8.471 +  then show ?thesis using assms by simp
   8.472 +qed
   8.473 +
   8.474 +
   8.475 +abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
   8.476 +  "complex_integrable M f \<equiv> integrable M f"
   8.477 +
   8.478 +abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
   8.479 +  "integral\<^sup>C M f == integral\<^sup>L M f"
   8.480 +
   8.481 +syntax
   8.482 +  "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
   8.483 + ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
   8.484 +
   8.485 +translations
   8.486 +  "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
   8.487 +
   8.488 +syntax
   8.489 +  "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   8.490 +  ("(3CLINT _|_. _)" [0,110,60] 60)
   8.491 +
   8.492 +translations
   8.493 +  "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
   8.494 +
   8.495 +lemma complex_integrable_cnj [simp]:
   8.496 +  "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f"
   8.497 +proof
   8.498 +  assume "complex_integrable M (\<lambda>x. cnj (f x))"
   8.499 +  then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))"
   8.500 +    by (rule integrable_cnj)
   8.501 +  then show "complex_integrable M f"
   8.502 +    by simp
   8.503 +qed simp
   8.504 +
   8.505 +lemma complex_of_real_integrable_eq:
   8.506 +  "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f"
   8.507 +proof
   8.508 +  assume "complex_integrable M (\<lambda>x. complex_of_real (f x))"
   8.509 +  then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))"
   8.510 +    by (rule integrable_Re)
   8.511 +  then show "integrable M f"
   8.512 +    by simp
   8.513 +qed simp
   8.514 +
   8.515 +
   8.516 +abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
   8.517 +  "complex_set_integrable M A f \<equiv> set_integrable M A f"
   8.518 +
   8.519 +abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
   8.520 +  "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
   8.521 +
   8.522 +syntax
   8.523 +"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
   8.524 +("(4CLINT _:_|_. _)" [0,60,110,61] 60)
   8.525 +
   8.526 +translations
   8.527 +"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
   8.528 +
   8.529 +(*
   8.530 +lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = abs a * cmod x"
   8.531 +  apply (simp add: norm_mult)
   8.532 +  by (subst norm_mult, auto)
   8.533 +*)
   8.534 +
   8.535 +lemma borel_integrable_atLeastAtMost':
   8.536 +  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   8.537 +  assumes f: "continuous_on {a..b} f"
   8.538 +  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
   8.539 +  by (intro borel_integrable_compact compact_Icc f)
   8.540 +
   8.541 +lemma integral_FTC_atLeastAtMost:
   8.542 +  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
   8.543 +  assumes "a \<le> b"
   8.544 +    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
   8.545 +    and f: "continuous_on {a .. b} f"
   8.546 +  shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
   8.547 +proof -
   8.548 +  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
   8.549 +  have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
   8.550 +    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
   8.551 +  moreover
   8.552 +  have "(f has_integral F b - F a) {a .. b}"
   8.553 +    by (intro fundamental_theorem_of_calculus ballI assms) auto
   8.554 +  then have "(?f has_integral F b - F a) {a .. b}"
   8.555 +    by (subst has_integral_eq_eq[where g=f]) auto
   8.556 +  then have "(?f has_integral F b - F a) UNIV"
   8.557 +    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
   8.558 +  ultimately show "integral\<^sup>L lborel ?f = F b - F a"
   8.559 +    by (rule has_integral_unique)
   8.560 +qed
   8.561 +
   8.562 +lemma set_borel_integral_eq_integral:
   8.563 +  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
   8.564 +  assumes "set_integrable lborel S f"
   8.565 +  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
   8.566 +proof -
   8.567 +  let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
   8.568 +  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
   8.569 +    by (rule has_integral_integral_lborel) fact
   8.570 +  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
   8.571 +    apply (subst has_integral_restrict_univ [symmetric])
   8.572 +    apply (rule has_integral_eq)
   8.573 +    by auto
   8.574 +  thus "f integrable_on S"
   8.575 +    by (auto simp add: integrable_on_def)
   8.576 +  with 1 have "(f has_integral (integral S f)) S"
   8.577 +    by (intro integrable_integral, auto simp add: integrable_on_def)
   8.578 +  thus "LINT x : S | lborel. f x = integral S f"
   8.579 +    by (intro has_integral_unique [OF 1])
   8.580 +qed
   8.581 +
   8.582 +lemma set_borel_measurable_continuous:
   8.583 +  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   8.584 +  assumes "S \<in> sets borel" "continuous_on S f"
   8.585 +  shows "set_borel_measurable borel S f"
   8.586 +proof -
   8.587 +  have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel"
   8.588 +    by (intro assms borel_measurable_continuous_on_if continuous_on_const)
   8.589 +  also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)"
   8.590 +    by auto
   8.591 +  finally show ?thesis .
   8.592 +qed
   8.593 +
   8.594 +lemma set_measurable_continuous_on_ivl:
   8.595 +  assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
   8.596 +  shows "set_borel_measurable borel {a..b} f"
   8.597 +  by (rule set_borel_measurable_continuous[OF _ assms]) simp
   8.598 +
   8.599 +end
   8.600 +
     9.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 04 21:28:35 2014 +0100
     9.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Dec 05 12:06:18 2014 +0100
     9.3 @@ -2328,9 +2328,16 @@
     9.4    using sigma_sets_vimage_commute[of f X "space M" "sets M"]
     9.5    unfolding sets_vimage_algebra sets.sigma_sets_eq by simp
     9.6  
     9.7 -lemma vimage_algebra_cong: "sets M = sets N \<Longrightarrow> sets (vimage_algebra X f M) = sets (vimage_algebra X f N)"
     9.8 +lemma sets_vimage_algebra_cong: "sets M = sets N \<Longrightarrow> sets (vimage_algebra X f M) = sets (vimage_algebra X f N)"
     9.9    by (simp add: sets_vimage_algebra)
    9.10  
    9.11 +lemma vimage_algebra_cong:
    9.12 +  assumes "X = Y"
    9.13 +  assumes "\<And>x. x \<in> Y \<Longrightarrow> f x = g x"
    9.14 +  assumes "sets M = sets N"
    9.15 +  shows "vimage_algebra X f M = vimage_algebra Y g N"
    9.16 +  by (auto simp: vimage_algebra_def assms intro!: arg_cong2[where f=sigma])
    9.17 +
    9.18  lemma in_vimage_algebra: "A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets (vimage_algebra X f M)"
    9.19    by (auto simp: vimage_algebra_def)
    9.20  
    9.21 @@ -2397,6 +2404,14 @@
    9.22      by (auto intro!: sets_image_in_sets sets_Sup_in_sets del: subsetI simp: *)
    9.23  qed
    9.24  
    9.25 +lemma vimage_algebra_Sup_sigma:
    9.26 +  assumes [simp]: "MM \<noteq> {}" and "\<And>M. M \<in> MM \<Longrightarrow> f \<in> X \<rightarrow> space M"
    9.27 +  shows "vimage_algebra X f (Sup_sigma MM) = Sup_sigma (vimage_algebra X f ` MM)"
    9.28 +proof (rule measure_eqI)
    9.29 +  show "sets (vimage_algebra X f (Sup_sigma MM)) = sets (Sup_sigma (vimage_algebra X f ` MM))"
    9.30 +    using assms by (rule sets_vimage_Sup_eq)
    9.31 +qed (simp add: vimage_algebra_def Sup_sigma_def emeasure_sigma)
    9.32 +
    9.33  subsubsection {* Restricted Space Sigma Algebra *}
    9.34  
    9.35  definition restrict_space where
    10.1 --- a/src/HOL/Probability/Stream_Space.thy	Thu Dec 04 21:28:35 2014 +0100
    10.2 +++ b/src/HOL/Probability/Stream_Space.thy	Fri Dec 05 12:06:18 2014 +0100
    10.3 @@ -288,14 +288,14 @@
    10.4    using  S[THEN sets.sets_into_space]
    10.5    apply (subst restrict_space_eq_vimage_algebra)
    10.6    apply (simp add: space_stream_space streams_mono2)
    10.7 -  apply (subst vimage_algebra_cong[OF sets_stream_space_eq])
    10.8 +  apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq])
    10.9    apply (subst sets_stream_space_eq)
   10.10    apply (subst sets_vimage_Sup_eq)
   10.11    apply simp
   10.12    apply (auto intro: streams_mono) []
   10.13    apply (simp add: image_image space_restrict_space)
   10.14    apply (intro SUP_sigma_cong)
   10.15 -  apply (simp add: vimage_algebra_cong[OF restrict_space_eq_vimage_algebra])
   10.16 +  apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra])
   10.17    apply (subst (1 2) vimage_algebra_vimage_algebra_eq)
   10.18    apply (auto simp: streams_mono snth_in)
   10.19    done
   10.20 @@ -326,6 +326,23 @@
   10.21    finally show ?case .
   10.22  qed (simp add: streams_sets)
   10.23  
   10.24 +lemma sigma_sets_singletons:
   10.25 +  assumes "countable S"
   10.26 +  shows "sigma_sets S ((\<lambda>s. {s})`S) = Pow S"
   10.27 +proof safe
   10.28 +  interpret sigma_algebra S "sigma_sets S ((\<lambda>s. {s})`S)"
   10.29 +    by (rule sigma_algebra_sigma_sets) auto
   10.30 +  fix A assume "A \<subseteq> S"
   10.31 +  with assms have "(\<Union>a\<in>A. {a}) \<in> sigma_sets S ((\<lambda>s. {s})`S)"
   10.32 +    by (intro countable_UN') (auto dest: countable_subset)
   10.33 +  then show "A \<in> sigma_sets S ((\<lambda>s. {s})`S)"
   10.34 +    by simp
   10.35 +qed (auto dest: sigma_sets_into_sp[rotated])
   10.36 +
   10.37 +lemma sets_count_space_eq_sigma:
   10.38 +  "countable S \<Longrightarrow> sets (count_space S) = sets (sigma S ((\<lambda>s. {s})`S))"
   10.39 +  by (subst sets_measure_of) (auto simp: sigma_sets_singletons)
   10.40 +
   10.41  lemma sets_stream_space_sstart:
   10.42    assumes S[simp]: "countable S"
   10.43    shows "sets (stream_space (count_space S)) = sets (sigma (streams S) (sstart S`lists S \<union> {{}}))"
   10.44 @@ -402,11 +419,8 @@
   10.45  
   10.46    { fix M :: "'a stream measure" assume M: "sets M = sets (stream_space (count_space UNIV))"
   10.47      have "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
   10.48 -      apply (simp add: sets_eq_imp_space_eq[OF M] space_stream_space restrict_space_eq_vimage_algebra
   10.49 -        vimage_algebra_cong[OF M])
   10.50 -      apply (simp add: sets_eq_imp_space_eq[OF M] space_stream_space restrict_space_eq_vimage_algebra[symmetric])
   10.51 -      apply (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart)
   10.52 -      done }
   10.53 +      by (subst sets_restrict_space_cong[OF M])
   10.54 +         (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart) }
   10.55    from this[OF sets_M] this[OF sets_N]
   10.56    show "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
   10.57         "sets (restrict_space N (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"