author hoelzl Fri Dec 05 12:06:18 2014 +0100 (2014-12-05) changeset 59092 d469103c0737 parent 59091 4c8205fe3644 child 59093 2b106e58a177
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
 CONTRIBUTORS file | annotate | diff | revisions src/HOL/Probability/Embed_Measure.thy file | annotate | diff | revisions src/HOL/Probability/Giry_Monad.thy file | annotate | diff | revisions src/HOL/Probability/Interval_Integral.thy file | annotate | diff | revisions src/HOL/Probability/Lebesgue_Integral_Substitution.thy file | annotate | diff | revisions src/HOL/Probability/Probability.thy file | annotate | diff | revisions src/HOL/Probability/Probability_Mass_Function.thy file | annotate | diff | revisions src/HOL/Probability/Set_Integral.thy file | annotate | diff | revisions src/HOL/Probability/Sigma_Algebra.thy file | annotate | diff | revisions src/HOL/Probability/Stream_Space.thy file | annotate | diff | revisions
```     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.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.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.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.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> {{}})"
```