# HG changeset patch
# User hoelzl
# Date 1417777578 -3600
# Node ID d469103c07371b9df860b67d6d0a0f1b8417e616
# Parent  4c8205fe3644bf1205e62f88dd1c4038dca41205
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav

diff -r 4c8205fe3644 -r d469103c0737 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Dec 04 21:28:35 2014 +0100
+++ b/CONTRIBUTORS	Fri Dec 05 12:06:18 2014 +0100
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM and Jeremy Avigad, Luke Serafin, CMU
+  Various integration theorems: mostly integration on intervals and substitution.
+
 * September 2014: Florian Haftmann, TUM
   Lexicographic order on functions and
   sum/product over function bodies.
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Embed_Measure.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Embed_Measure.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -0,0 +1,343 @@
+(*  Title:      HOL/Probability/Embed_Measure.thy
+    Author:     Manuel Eberl, TU München
+
+    Defines measure embeddings with injective functions, i.e. lifting a measure on some values 
+    to a measure on "tagged" values (e.g. embed_measure M Inl lifts a measure on values 'a to a 
+    measure on the left part of the sum type 'a + 'b)
+*)
+
+section {* Embed Measure Spaces with a Function *}
+
+theory Embed_Measure
+imports Binary_Product_Measure
+begin
+
+definition embed_measure :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
+  "embed_measure M f = measure_of (f ` space M) {f ` A |A. A \<in> sets M} 
+                           (\<lambda>A. emeasure M (f -` A \<inter> space M))"
+
+lemma space_embed_measure: "space (embed_measure M f) = f ` space M"
+  unfolding embed_measure_def 
+  by (subst space_measure_of) (auto dest: sets.sets_into_space)
+
+lemma sets_embed_measure':
+  assumes inj: "inj_on f (space M)" 
+  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
+  unfolding embed_measure_def
+proof (intro sigma_algebra.sets_measure_of_eq sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI)
+  fix s assume "s \<in> {f ` A |A. A \<in> sets M}"
+  then obtain s' where s'_props: "s = f ` s'" "s' \<in> sets M" by auto
+  hence "f ` space M - s = f ` (space M - s')" using inj
+    by (auto dest: inj_onD sets.sets_into_space)
+  also have "... \<in> {f ` A |A. A \<in> sets M}" using s'_props by auto
+  finally show "f ` space M - s \<in> {f ` A |A. A \<in> sets M}" .
+next
+  fix A :: "nat \<Rightarrow> _" assume "range A \<subseteq> {f ` A |A. A \<in> sets M}"
+  then obtain A' where "\<And>i. A i = f ` A' i" "\<And>i. A' i \<in> sets M"
+    by (auto simp: subset_eq choice_iff)
+  moreover from this have "(\<Union>x. f ` A' x) = f ` (\<Union>x. A' x)" by blast
+  ultimately show "(\<Union>i. A i) \<in> {f ` A |A. A \<in> sets M}" by blast
+qed (auto dest: sets.sets_into_space)
+
+lemma the_inv_into_vimage:
+  "inj_on f X \<Longrightarrow> A \<subseteq> X \<Longrightarrow> the_inv_into X f -` A \<inter> (f`X) = f ` A"
+  by (auto simp: the_inv_into_f_f)
+
+lemma sets_embed_eq_vimage_algebra:
+  assumes "inj_on f (space M)"
+  shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
+  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image
+           dest: sets.sets_into_space
+           intro!: image_cong the_inv_into_vimage[symmetric])
+
+lemma sets_embed_measure:
+  assumes inj: "inj f" 
+  shows "sets (embed_measure M f) = {f ` A |A. A \<in> sets M}"
+  using assms by (subst sets_embed_measure') (auto intro!: inj_onI dest: injD)
+
+lemma in_sets_embed_measure: "A \<in> sets M \<Longrightarrow> f ` A \<in> sets (embed_measure M f)"
+  unfolding embed_measure_def
+  by (intro in_measure_of) (auto dest: sets.sets_into_space)
+
+lemma measurable_embed_measure1:
+  assumes g: "(\<lambda>x. g (f x)) \<in> measurable M N" 
+  shows "g \<in> measurable (embed_measure M f) N"
+  unfolding measurable_def
+proof safe
+  fix A assume "A \<in> sets N"
+  with g have "(\<lambda>x. g (f x)) -` A \<inter> space M \<in> sets M"
+    by (rule measurable_sets)
+  then have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) \<in> sets (embed_measure M f)"
+    by (rule in_sets_embed_measure)
+  also have "f ` ((\<lambda>x. g (f x)) -` A \<inter> space M) = g -` A \<inter> space (embed_measure M f)"
+    by (auto simp: space_embed_measure)
+  finally show "g -` A \<inter> space (embed_measure M f) \<in> sets (embed_measure M f)" .
+qed (insert measurable_space[OF assms], auto simp: space_embed_measure)
+
+lemma measurable_embed_measure2':
+  assumes "inj_on f (space M)" 
+  shows "f \<in> measurable M (embed_measure M f)"
+proof-
+  {
+    fix A assume A: "A \<in> sets M"
+    also from this have "A = A \<inter> space M" by auto
+    also have "... = f -` f ` A \<inter> space M" using A assms
+      by (auto dest: inj_onD sets.sets_into_space)
+    finally have "f -` f ` A \<inter> space M \<in> sets M" .
+  }
+  thus ?thesis using assms unfolding embed_measure_def
+    by (intro measurable_measure_of) (auto dest: sets.sets_into_space)
+qed
+
+lemma measurable_embed_measure2:
+  assumes [simp]: "inj f" shows "f \<in> measurable M (embed_measure M f)"
+  by (auto simp: inj_vimage_image_eq embed_measure_def
+           intro!: measurable_measure_of dest: sets.sets_into_space)
+
+lemma embed_measure_eq_distr':
+  assumes "inj_on f (space M)"
+  shows "embed_measure M f = distr M (embed_measure M f) f"
+proof-
+  have "distr M (embed_measure M f) f = 
+            measure_of (f ` space M) {f ` A |A. A \<in> sets M}
+                       (\<lambda>A. emeasure M (f -` A \<inter> space M))" unfolding distr_def
+      by (simp add: space_embed_measure sets_embed_measure'[OF assms])
+  also have "... = embed_measure M f" unfolding embed_measure_def ..
+  finally show ?thesis ..
+qed
+
+lemma embed_measure_eq_distr:
+    "inj f \<Longrightarrow> embed_measure M f = distr M (embed_measure M f) f"
+  by (rule embed_measure_eq_distr') (auto intro!: inj_onI dest: injD)
+
+lemma nn_integral_embed_measure:
+  "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
+  nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
+  apply (subst embed_measure_eq_distr, simp)
+  apply (subst nn_integral_distr)
+  apply (simp_all add: measurable_embed_measure2)
+  done
+
+lemma emeasure_embed_measure':
+    assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
+    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
+  by (subst embed_measure_eq_distr'[OF assms(1)])
+     (simp add: emeasure_distr[OF measurable_embed_measure2'[OF assms(1)] assms(2)])
+
+lemma emeasure_embed_measure:
+    assumes "inj f" "A \<in> sets (embed_measure M f)"
+    shows "emeasure (embed_measure M f) A = emeasure M (f -` A \<inter> space M)"
+ using assms by (intro emeasure_embed_measure') (auto intro!: inj_onI dest: injD)
+
+lemma embed_measure_comp: 
+  assumes [simp]: "inj f" "inj g"
+  shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
+proof-
+  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)
+  note measurable_embed_measure2[measurable]
+  have "embed_measure (embed_measure M f) g = 
+            distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
+      by (subst (1 2) embed_measure_eq_distr) 
+         (simp_all add: distr_distr sets_embed_measure cong: distr_cong)
+  also have "... = embed_measure M (g \<circ> f)"
+      by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
+         (auto simp: sets_embed_measure o_def image_image[symmetric] 
+               intro: inj_comp cong: distr_cong)
+  finally show ?thesis .
+qed
+
+lemma sigma_finite_embed_measure:
+  assumes "sigma_finite_measure M" and inj: "inj f"
+  shows "sigma_finite_measure (embed_measure M f)"
+proof
+  case goal1
+  from assms(1) interpret sigma_finite_measure M .
+  from sigma_finite_countable obtain A where
+      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
+  show ?case
+  proof (intro exI[of _ "op ` f`A"] conjI allI)
+    from A_props show "countable (op ` f`A)" by auto
+    from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)" 
+      by (auto simp: sets_embed_measure)
+    from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"
+      by (auto simp: space_embed_measure intro!: imageI)
+    from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
+      by (intro ballI, subst emeasure_embed_measure)
+         (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
+  qed
+qed
+
+lemma embed_measure_count_space: 
+    "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
+  apply (subst distr_bij_count_space[of f A "f`A", symmetric])
+  apply (simp add: inj_on_def bij_betw_def)
+  apply (subst embed_measure_eq_distr)
+  apply simp
+  apply (auto intro!: measure_eqI imageI simp: sets_embed_measure subset_image_iff)
+  apply blast
+  apply (subst (1 2) emeasure_distr)
+  apply (auto simp: space_embed_measure sets_embed_measure)
+  done
+
+lemma sets_embed_measure_alt:
+    "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M"
+  by (auto simp: sets_embed_measure)
+
+lemma emeasure_embed_measure_image':
+  assumes "inj_on f (space M)" "X \<in> sets M"
+  shows "emeasure (embed_measure M f) (f`X) = emeasure M X"
+proof-
+  from assms have "emeasure (embed_measure M f) (f`X) = emeasure M (f -` f ` X \<inter> space M)"
+    by (subst emeasure_embed_measure') (auto simp: sets_embed_measure')
+  also from assms have "f -` f ` X \<inter> space M = X" by (auto dest: inj_onD sets.sets_into_space)
+  finally show ?thesis .
+qed
+
+lemma emeasure_embed_measure_image:
+    "inj f \<Longrightarrow> X \<in> sets M \<Longrightarrow> emeasure (embed_measure M f) (f`X) = emeasure M X"
+  by (simp_all add: emeasure_embed_measure in_sets_embed_measure inj_vimage_image_eq)
+
+lemma embed_measure_eq_iff:
+  assumes "inj f"
+  shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
+proof
+  from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)
+  assume asm: "?M = ?N"
+  hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
+  with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
+  moreover {
+    fix X assume "X \<in> sets A"
+    from asm have "emeasure ?M (f`X) = emeasure ?N (f`X)" by simp
+    with `X \<in> sets A` and `sets A = sets B` and assms 
+        have "emeasure A X = emeasure B X" by (simp add: emeasure_embed_measure_image)
+  }
+  ultimately show "A = B" by (rule measure_eqI)
+qed simp
+
+lemma the_inv_into_in_Pi: "inj_on f A \<Longrightarrow> the_inv_into A f \<in> f ` A \<rightarrow> A"
+  by (auto simp: the_inv_into_f_f)
+
+lemma map_prod_image: "map_prod f g ` (A \<times> B) = (f`A) \<times> (g`B)"
+  using map_prod_surj_on[OF refl refl] .
+
+lemma map_prod_vimage: "map_prod f g -` (A \<times> B) = (f-`A) \<times> (g-`B)"
+  by auto
+
+lemma embed_measure_prod:
+  assumes f: "inj f" and g: "inj g" and [simp]: "sigma_finite_measure M" "sigma_finite_measure N"
+  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))"
+    (is "?L = _")
+  unfolding map_prod_def[symmetric]
+proof (rule pair_measure_eqI)
+  have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
+    using f g by (auto simp: inj_on_def)
+  
+  show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
+    unfolding map_prod_def[symmetric]
+    apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra
+      cong: vimage_algebra_cong)
+    apply (subst vimage_algebra_Sup_sigma)
+    apply (simp_all add: space_pair_measure[symmetric])
+    apply (auto simp add: the_inv_into_f_f
+                simp del: map_prod_simp
+                del: prod_fun_imageE) []
+    apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
+    apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
+    apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
+       space_pair_measure[symmetric] map_prod_image[symmetric])
+    apply (intro arg_cong[where f=sets] arg_cong[where f=Sup_sigma] arg_cong2[where f=insert] vimage_algebra_cong)
+    apply (auto simp: map_prod_image the_inv_into_f_f
+                simp del: map_prod_simp del: prod_fun_imageE)
+    apply (simp_all add: the_inv_into_f_f space_pair_measure)
+    done
+
+  note measurable_embed_measure2[measurable]
+  fix A B assume AB: "A \<in> sets (embed_measure M f)" "B \<in> sets (embed_measure N g)"
+  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)"
+    by (auto simp: space_pair_measure)
+  ultimately show "emeasure (embed_measure M f) A * emeasure (embed_measure N g) B =
+                     emeasure (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g)) (A \<times> B)"
+    by (simp add: map_prod_vimage sets[symmetric] emeasure_embed_measure
+                  sigma_finite_measure.emeasure_pair_measure_Times)
+qed (insert assms, simp_all add: sigma_finite_embed_measure)
+
+lemma density_embed_measure:
+  assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"
+  shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")
+proof (rule measure_eqI)
+  fix X assume X: "X \<in> sets ?M1"
+  from inj have Mf[measurable]: "f \<in> measurable M (embed_measure M f)" 
+    by (rule measurable_embed_measure2)
+  from Mg and X have "emeasure ?M1 X = \<integral>\<^sup>+ x. g x * indicator X x \<partial>embed_measure M f" 
+    by (subst emeasure_density) simp_all
+  also from X have "... = \<integral>\<^sup>+ x. g (f x) * indicator X (f x) \<partial>M"
+    by (subst embed_measure_eq_distr[OF inj], subst nn_integral_distr)
+       (auto intro!: borel_measurable_ereal_times borel_measurable_indicator)
+  also have "... = \<integral>\<^sup>+ x. g (f x) * indicator (f -` X \<inter> space M) x \<partial>M"
+    by (intro nn_integral_cong) (auto split: split_indicator)
+  also from X have "... = emeasure (density M (g \<circ> f)) (f -` X \<inter> space M)"
+    by (subst emeasure_density) (simp_all add: measurable_comp[OF Mf Mg] measurable_sets[OF Mf])
+  also from X and inj have "... = emeasure ?M2 X" 
+    by (subst emeasure_embed_measure) (simp_all add: sets_embed_measure)
+  finally show "emeasure ?M1 X = emeasure ?M2 X" .
+qed (simp_all add: sets_embed_measure inj)
+
+lemma density_embed_measure':
+  assumes inj: "inj f" and inv: "\<And>x. f' (f x) = x" and Mg[measurable]: "g \<in> borel_measurable M"
+  shows "density (embed_measure M f) (g \<circ> f') = embed_measure (density M g) f"
+proof-
+  have "density (embed_measure M f) (g \<circ> f') = embed_measure (density M (g \<circ> f' \<circ> f)) f"
+    by (rule density_embed_measure[OF inj])
+       (rule measurable_comp, rule measurable_embed_measure1, subst measurable_cong, 
+        rule inv, rule measurable_ident_sets, simp, rule Mg)
+  also have "density M (g \<circ> f' \<circ> f) = density M g"
+    by (intro density_cong) (subst measurable_cong, simp add: o_def inv, simp_all add: Mg inv)
+  finally show ?thesis .
+qed
+
+lemma inj_on_image_subset_iff:
+  assumes "inj_on f C" "A \<subseteq> C"  "B \<subseteq> C"
+  shows "f ` A \<subseteq> f ` B \<longleftrightarrow> A \<subseteq> B"
+proof (intro iffI subsetI)
+  fix x assume A: "f ` A \<subseteq> f ` B" and B: "x \<in> A"
+  from B have "f x \<in> f ` A" by blast
+  with A have "f x \<in> f ` B" by blast
+  then obtain y where "f x = f y" and "y \<in> B" by blast
+  with assms and B have "x = y" by (auto dest: inj_onD)
+  with `y \<in> B` show "x \<in> B" by simp
+qed auto
+  
+
+lemma AE_embed_measure':
+  assumes inj: "inj_on f (space M)"
+  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
+proof
+  let ?M = "embed_measure M f"
+  assume "AE x in ?M. P x"
+  then obtain A where A_props: "A \<in> sets ?M" "emeasure ?M A = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> A"
+    by (force elim: AE_E)
+  then obtain A' where A'_props: "A = f ` A'" "A' \<in> sets M" by (auto simp: sets_embed_measure' inj)
+  moreover have B: "{x\<in>space ?M. \<not>P x} = f ` {x\<in>space M. \<not>P (f x)}" 
+    by (auto simp: inj space_embed_measure)
+  from A_props(3) have "{x\<in>space M. \<not>P (f x)} \<subseteq> A'"
+    by (subst (asm) B, subst (asm) A'_props, subst (asm) inj_on_image_subset_iff[OF inj])
+       (insert A'_props, auto dest: sets.sets_into_space)
+  moreover from A_props A'_props have "emeasure M A' = 0"
+    by (simp add: emeasure_embed_measure_image' inj)
+  ultimately show "AE x in M. P (f x)" by (intro AE_I)
+next
+  let ?M = "embed_measure M f"
+  assume "AE x in M. P (f x)"
+  then obtain A where A_props: "A \<in> sets M" "emeasure M A = 0" "{x\<in>space M. \<not>P (f x)} \<subseteq> A"
+    by (force elim: AE_E)
+  hence "f`A \<in> sets ?M" "emeasure ?M (f`A) = 0" "{x\<in>space ?M. \<not>P x} \<subseteq> f`A"
+    by (auto simp: space_embed_measure emeasure_embed_measure_image' sets_embed_measure' inj)
+  thus "AE x in ?M. P x" by (intro AE_I)
+qed
+
+lemma AE_embed_measure:
+  assumes inj: "inj f"
+  shows "(AE x in embed_measure M f. P x) \<longleftrightarrow> (AE x in M. P (f x))"
+  using assms by (intro AE_embed_measure') (auto intro!: inj_onI dest: injD)
+
+end
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Thu Dec 04 21:28:35 2014 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -7,7 +7,7 @@
 *)
 
 theory Giry_Monad
-  imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax"
+  imports Probability_Measure Lebesgue_Integral_Substitution "~~/src/HOL/Library/Monad_Syntax" 
 begin
 
 section {* Sub-probability spaces *}
@@ -50,6 +50,65 @@
 lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1"
   using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure)
 
+lemma emeasure_density_distr_interval:
+  fixes h :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real" and g' :: "real \<Rightarrow> real"
+  assumes [simp]: "a \<le> b"
+  assumes Mf[measurable]: "f \<in> borel_measurable borel"
+  assumes Mg[measurable]: "g \<in> borel_measurable borel"
+  assumes Mg'[measurable]: "g' \<in> borel_measurable borel"
+  assumes Mh[measurable]: "h \<in> borel_measurable borel"
+  assumes prob: "subprob_space (density lborel f)"
+  assumes nonnegf: "\<And>x. f x \<ge> 0"
+  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes contg': "continuous_on {a..b} g'"
+  assumes mono: "strict_mono_on g {a..b}" and inv: "\<And>x. h x \<in> {a..b} \<Longrightarrow> g (h x) = x"
+  assumes range: "{a..b} \<subseteq> range h"
+  shows "emeasure (distr (density lborel f) lborel h) {a..b} = 
+             emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}"
+proof (cases "a < b")
+  assume "a < b"
+  from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
+  from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on)
+  from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0"
+    by (rule mono_on_imp_deriv_nonneg) (auto simp: interior_atLeastAtMost_real)
+  from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+    by (rule continuous_ge_on_Iii) (simp_all add: `a < b`)
+
+  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
+  have A: "h -` {a..b} = {g a..g b}"
+  proof (intro equalityI subsetI)
+    fix x assume x: "x \<in> h -` {a..b}"
+    hence "g (h x) \<in> {g a..g b}" by (auto intro: mono_onD[OF mono'])
+    with inv and x show "x \<in> {g a..g b}" by simp
+  next
+    fix y assume y: "y \<in> {g a..g b}"
+    with IVT'[OF _ _ _ contg, of y] obtain x where "x \<in> {a..b}" "y = g x" by auto
+    with range and inv show "y \<in> h -` {a..b}" by auto
+  qed
+
+  have prob': "subprob_space (distr (density lborel f) lborel h)"
+    by (rule subprob_space.subprob_space_distr[OF prob]) (simp_all add: Mh)
+  have B: "emeasure (distr (density lborel f) lborel h) {a..b} = 
+            \<integral>\<^sup>+x. f x * indicator (h -` {a..b}) x \<partial>lborel"
+    by (subst emeasure_distr) (simp_all add: emeasure_density Mf Mh measurable_sets_borel[OF Mh])
+  also note A
+  also have "emeasure (distr (density lborel f) lborel h) {a..b} \<le> 1"
+    by (rule subprob_space.subprob_emeasure_le_1) (rule prob')
+  hence "emeasure (distr (density lborel f) lborel h) {a..b} \<noteq> \<infinity>" by auto
+  with assms have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
+                      (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
+    by (intro nn_integral_substitution_aux)
+       (auto simp: derivg_nonneg A B emeasure_density mult.commute `a < b`)
+  also have "... = emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}" 
+    by (simp add: emeasure_density)
+  finally show ?thesis .
+next
+  assume "\<not>a < b"
+  with `a \<le> b` have [simp]: "b = a" by (simp add: not_less del: `a \<le> b`)
+  from inv and range have "h -` {a} = {g a}" by auto
+  thus ?thesis by (simp_all add: emeasure_distr emeasure_density measurable_sets_borel[OF Mh])
+qed
+
 locale pair_subprob_space = 
   pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
 
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Interval_Integral.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Interval_Integral.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -0,0 +1,1095 @@
+(*  Title:      HOL/Probability/Interval_Integral.thy
+    Author:     Jeremy Avigad, Johannes Hölzl, Luke Serafin
+
+Lebesgue integral over an interval (with endpoints possibly +-\<infinity>)
+*)
+
+theory Interval_Integral
+  imports Set_Integral
+begin
+
+lemma continuous_on_vector_derivative:
+  "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
+  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
+
+lemma has_vector_derivative_weaken:
+  fixes x D and f g s t
+  assumes f: "(f has_vector_derivative D) (at x within t)"
+    and "x \<in> s" "s \<subseteq> t" 
+    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
+  shows "(g has_vector_derivative D) (at x within s)"
+proof -
+  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
+    unfolding has_vector_derivative_def has_derivative_iff_norm
+    using assms by (intro conj_cong Lim_cong_within refl) auto
+  then show ?thesis
+    using has_vector_derivative_within_subset[OF f `s \<subseteq> t`] by simp
+qed
+
+definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
+
+lemma einterval_eq[simp]:
+  shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
+    and einterval_eq_Ici: "einterval (ereal a) \<infinity> = {a <..}"
+    and einterval_eq_Iic: "einterval (- \<infinity>) (ereal b) = {..< b}"
+    and einterval_eq_UNIV: "einterval (- \<infinity>) \<infinity> = UNIV"
+  by (auto simp: einterval_def)
+
+lemma einterval_same: "einterval a a = {}"
+  by (auto simp add: einterval_def)
+
+lemma einterval_iff: "x \<in> einterval a b \<longleftrightarrow> a < ereal x \<and> ereal x < b"
+  by (simp add: einterval_def)
+
+lemma einterval_nonempty: "a < b \<Longrightarrow> \<exists>c. c \<in> einterval a b"
+  by (cases a b rule: ereal2_cases, auto simp: einterval_def intro!: dense gt_ex lt_ex)
+
+lemma open_einterval[simp]: "open (einterval a b)"
+  by (cases a b rule: ereal2_cases)
+     (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros)
+
+lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
+  unfolding einterval_def by measurable
+
+(* 
+    Approximating a (possibly infinite) interval
+*)
+
+lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
+ unfolding filterlim_def by (auto intro: le_supI1)
+
+lemma ereal_incseq_approx:
+  fixes a b :: ereal
+  assumes "a < b"
+  obtains X :: "nat \<Rightarrow> real" where 
+    "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X ----> b"
+proof (cases b)
+  case PInf
+  with `a < b` have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
+    by (cases a) auto
+  moreover have " (\<lambda>x. ereal (real (Suc x))) ----> \<infinity>"
+    using natceiling_le_eq by (subst LIMSEQ_Suc_iff) (auto simp: Lim_PInfty)
+  moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) ----> \<infinity>"
+    apply (subst LIMSEQ_Suc_iff)
+    apply (subst Lim_PInfty)
+    apply (metis add.commute diff_le_eq natceiling_le_eq ereal_less_eq(3))
+    done
+  ultimately show thesis
+    by (intro that[of "\<lambda>i. real a + Suc i"])
+       (auto simp: incseq_def PInf)
+next
+  case (real b')
+  def d \<equiv> "b' - (if a = -\<infinity> then b' - 1 else real a)"
+  with `a < b` have a': "0 < d"
+    by (cases a) (auto simp: real)
+  moreover
+  have "\<And>i r. r < b' \<Longrightarrow> (b' - r) * 1 < (b' - r) * real (Suc (Suc i))"
+    by (intro mult_strict_left_mono) auto
+  with `a < b` a' have "\<And>i. a < ereal (b' - d / real (Suc (Suc i)))"
+    by (cases a) (auto simp: real d_def field_simps)
+  moreover have "(\<lambda>i. b' - d / Suc (Suc i)) ----> b'"
+    apply (subst filterlim_sequentially_Suc)
+    apply (subst filterlim_sequentially_Suc)
+    apply (rule tendsto_eq_intros)
+    apply (auto intro!: tendsto_divide_0[OF tendsto_const] filterlim_sup1
+                simp: at_infinity_eq_at_top_bot filterlim_real_sequentially)
+    done
+  ultimately show thesis
+    by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"])
+       (auto simp add: real incseq_def intro!: divide_left_mono)
+qed (insert `a < b`, auto)
+
+lemma ereal_decseq_approx:
+  fixes a b :: ereal
+  assumes "a < b"
+  obtains X :: "nat \<Rightarrow> real" where 
+    "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X ----> a"
+proof -
+  have "-b < -a" using `a < b` by simp
+  from ereal_incseq_approx[OF this] guess X .
+  then show thesis
+    apply (intro that[of "\<lambda>i. - X i"])
+    apply (auto simp add: uminus_ereal.simps[symmetric] decseq_def incseq_def
+                simp del: uminus_ereal.simps)
+    apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
+    done
+qed
+
+lemma einterval_Icc_approximation:
+  fixes a b :: ereal
+  assumes "a < b"
+  obtains u l :: "nat \<Rightarrow> real" where 
+    "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l ----> a" "u ----> b"
+proof -
+  from dense[OF `a < b`] obtain c where "a < c" "c < b" by safe
+  from ereal_incseq_approx[OF `c < b`] guess u . note u = this
+  from ereal_decseq_approx[OF `a < c`] guess l . note l = this
+  { fix i from less_trans[OF `l i < c` `c < u i`] have "l i < u i" by simp }
+  have "einterval a b = (\<Union>i. {l i .. u i})"
+  proof (auto simp: einterval_iff)
+    fix x assume "a < ereal x" "ereal x < b"
+    have "eventually (\<lambda>i. ereal (l i) < ereal x) sequentially"
+      using l(4) `a < ereal x` by (rule order_tendstoD)
+    moreover 
+    have "eventually (\<lambda>i. ereal x < ereal (u i)) sequentially"
+      using u(4) `ereal x< b` by (rule order_tendstoD)
+    ultimately have "eventually (\<lambda>i. l i < x \<and> x < u i) sequentially"
+      by eventually_elim auto
+    then show "\<exists>i. l i \<le> x \<and> x \<le> u i"
+      by (auto intro: less_imp_le simp: eventually_sequentially)
+  next
+    fix x i assume "l i \<le> x" "x \<le> u i" 
+    with `a < ereal (l i)` `ereal (u i) < b`
+    show "a < ereal x" "ereal x < b"
+      by (auto simp del: ereal_less_eq(3) simp add: ereal_less_eq(3)[symmetric])
+  qed
+  show thesis
+    by (intro that) fact+
+qed
+
+(* TODO: in this definition, it would be more natural if einterval a b included a and b when 
+   they are real. *)
+definition interval_lebesgue_integral :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> 'a::{banach, second_countable_topology}" where
+  "interval_lebesgue_integral M a b f =
+    (if a \<le> b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))"
+
+syntax
+  "_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
+  ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)
+
+translations
+  "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
+
+definition interval_lebesgue_integrable :: "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> 'a::{banach, second_countable_topology}) \<Rightarrow> bool" where
+  "interval_lebesgue_integrable M a b f =
+    (if a \<le> b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)"
+
+syntax
+  "_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
+  ("(4LBINT _=_.._. _)" [0,60,60,61] 60)
+
+translations
+  "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
+
+(*
+    Basic properties of integration over an interval.
+*)
+
+lemma interval_lebesgue_integral_cong:
+  "a \<le> b \<Longrightarrow> (\<And>x. x \<in> einterval a b \<Longrightarrow> f x = g x) \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
+    interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
+  by (auto intro: set_lebesgue_integral_cong simp: interval_lebesgue_integral_def)
+
+lemma interval_lebesgue_integral_cong_AE:
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
+    a \<le> b \<Longrightarrow> AE x \<in> einterval a b in M. f x = g x \<Longrightarrow> einterval a b \<in> sets M \<Longrightarrow>
+    interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
+  by (auto intro: set_lebesgue_integral_cong_AE simp: interval_lebesgue_integral_def)
+
+lemma interval_lebesgue_integral_add [intro, simp]: 
+  fixes M a b f 
+  assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
+  shows "interval_lebesgue_integrable M a b (\<lambda>x. f x + g x)" and 
+    "interval_lebesgue_integral M a b (\<lambda>x. f x + g x) = 
+   interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g"
+using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def 
+    field_simps)
+
+lemma interval_lebesgue_integral_diff [intro, simp]: 
+  fixes M a b f 
+  assumes "interval_lebesgue_integrable M a b f"
+    "interval_lebesgue_integrable M a b g"
+  shows "interval_lebesgue_integrable M a b (\<lambda>x. f x - g x)" and 
+    "interval_lebesgue_integral M a b (\<lambda>x. f x - g x) = 
+   interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g"
+using assms by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def 
+    field_simps)
+
+lemma interval_lebesgue_integrable_mult_right [intro, simp]:
+  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
+  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
+    interval_lebesgue_integrable M a b (\<lambda>x. c * f x)"
+  by (simp add: interval_lebesgue_integrable_def)
+
+lemma interval_lebesgue_integrable_mult_left [intro, simp]:
+  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
+  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
+    interval_lebesgue_integrable M a b (\<lambda>x. f x * c)"
+  by (simp add: interval_lebesgue_integrable_def)
+
+lemma interval_lebesgue_integrable_divide [intro, simp]:
+  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
+  shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
+    interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
+  by (simp add: interval_lebesgue_integrable_def)
+
+lemma interval_lebesgue_integral_mult_right [simp]:
+  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
+  shows "interval_lebesgue_integral M a b (\<lambda>x. c * f x) =
+    c * interval_lebesgue_integral M a b f"
+  by (simp add: interval_lebesgue_integral_def)
+
+lemma interval_lebesgue_integral_mult_left [simp]:
+  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
+  shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) =
+    interval_lebesgue_integral M a b f * c"
+  by (simp add: interval_lebesgue_integral_def)
+
+lemma interval_lebesgue_integral_divide [simp]:
+  fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field_inverse_zero, second_countable_topology}"
+  shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) =
+    interval_lebesgue_integral M a b f / c"
+  by (simp add: interval_lebesgue_integral_def)
+
+lemma interval_lebesgue_integral_uminus:
+  "interval_lebesgue_integral M a b (\<lambda>x. - f x) = - interval_lebesgue_integral M a b f"
+  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
+
+lemma interval_lebesgue_integral_of_real:
+  "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) =
+    of_real (interval_lebesgue_integral M a b f)"
+  unfolding interval_lebesgue_integral_def
+  by (auto simp add: interval_lebesgue_integral_def set_integral_complex_of_real)
+
+lemma interval_lebesgue_integral_le_eq: 
+  fixes a b f
+  assumes "a \<le> b"
+  shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
+using assms by (auto simp add: interval_lebesgue_integral_def)
+
+lemma interval_lebesgue_integral_gt_eq: 
+  fixes a b f
+  assumes "a > b"
+  shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"
+using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
+
+lemma interval_lebesgue_integral_gt_eq':
+  fixes a b f
+  assumes "a > b"
+  shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f"
+using assms by (auto simp add: interval_lebesgue_integral_def less_imp_le einterval_def)
+
+lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0"
+  by (simp add: interval_lebesgue_integral_def einterval_same)
+
+lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)"
+  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def einterval_same)
+
+lemma interval_integrable_endpoints_reverse:
+  "interval_lebesgue_integrable lborel a b f \<longleftrightarrow>
+    interval_lebesgue_integrable lborel b a f"
+  by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)
+
+lemma interval_integral_reflect:
+  "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
+proof (induct a b rule: linorder_wlog)
+  case (sym a b) then show ?case
+    by (auto simp add: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
+             split: split_if_asm)
+next
+  case (le a b) then show ?case
+    unfolding interval_lebesgue_integral_def
+    by (subst set_integral_reflect)
+       (auto simp: interval_lebesgue_integrable_def einterval_iff
+                   ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
+                   uminus_ereal.simps[symmetric]
+             simp del: uminus_ereal.simps
+             intro!: integral_cong
+             split: split_indicator)
+qed
+
+(*
+    Basic properties of integration over an interval wrt lebesgue measure.
+*)
+
+lemma interval_integral_zero [simp]:
+  fixes a b :: ereal
+  shows"LBINT x=a..b. 0 = 0" 
+using assms unfolding interval_lebesgue_integral_def einterval_eq 
+by simp
+
+lemma interval_integral_const [intro, simp]:
+  fixes a b c :: real
+  shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)" 
+using assms unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq 
+by (auto simp add:  less_imp_le field_simps measure_def)
+
+lemma interval_integral_cong_AE:
+  assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
+  assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
+  shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
+  using assms
+proof (induct a b rule: linorder_wlog)
+  case (sym a b) then show ?case
+    by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
+next
+  case (le a b) then show ?case
+    by (auto simp: interval_lebesgue_integral_def max_def min_def
+             intro!: set_lebesgue_integral_cong_AE)
+qed
+
+lemma interval_integral_cong:
+  assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x" 
+  shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
+  using assms
+proof (induct a b rule: linorder_wlog)
+  case (sym a b) then show ?case
+    by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
+next
+  case (le a b) then show ?case
+    by (auto simp: interval_lebesgue_integral_def max_def min_def
+             intro!: set_lebesgue_integral_cong)
+qed
+
+lemma interval_lebesgue_integrable_cong_AE:
+    "f \<in> borel_measurable lborel \<Longrightarrow> g \<in> borel_measurable lborel \<Longrightarrow>
+    AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x \<Longrightarrow>
+    interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g"
+  apply (simp add: interval_lebesgue_integrable_def )
+  apply (intro conjI impI set_integrable_cong_AE)
+  apply (auto simp: min_def max_def)
+  done
+
+lemma interval_integrable_abs_iff:
+  fixes f :: "real \<Rightarrow> real"
+  shows  "f \<in> borel_measurable lborel \<Longrightarrow>
+    interval_lebesgue_integrable lborel a b (\<lambda>x. \<bar>f x\<bar>) = interval_lebesgue_integrable lborel a b f"
+  unfolding interval_lebesgue_integrable_def
+  by (subst (1 2) set_integrable_abs_iff') simp_all
+
+lemma interval_integral_Icc:
+  fixes a b :: real
+  shows "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a..b}. f x)"
+  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
+           simp add: interval_lebesgue_integral_def)
+
+lemma interval_integral_Icc':
+  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {x. a \<le> ereal x \<and> ereal x \<le> b}. f x)"
+  by (auto intro!: set_integral_discrete_difference[where X="{real a, real b}"]
+           simp add: interval_lebesgue_integral_def einterval_iff)
+
+lemma interval_integral_Ioc:
+  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a<..b}. f x)"
+  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
+           simp add: interval_lebesgue_integral_def einterval_iff)
+
+(* TODO: other versions as well? *) (* Yes: I need the Icc' version. *)
+lemma interval_integral_Ioc':
+  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {x. a < ereal x \<and> ereal x \<le> b}. f x)"
+  by (auto intro!: set_integral_discrete_difference[where X="{real a, real b}"]
+           simp add: interval_lebesgue_integral_def einterval_iff)
+
+lemma interval_integral_Ico:
+  "a \<le> b \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {a..<b}. f x)"
+  by (auto intro!: set_integral_discrete_difference[where X="{a, b}"]
+           simp add: interval_lebesgue_integral_def einterval_iff)
+
+lemma interval_integral_Ioi:
+  "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real a <..}. f x)"
+  by (auto simp add: interval_lebesgue_integral_def einterval_iff)
+
+lemma interval_integral_Ioo:
+  "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)"
+  by (auto simp add: interval_lebesgue_integral_def einterval_iff)
+
+lemma interval_integral_discrete_difference:
+  fixes f :: "real \<Rightarrow> 'b::{banach, second_countable_topology}" and a b :: ereal
+  assumes "countable X"
+  and eq: "\<And>x. a \<le> b \<Longrightarrow> a < x \<Longrightarrow> x < b \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
+  and anti_eq: "\<And>x. b \<le> a \<Longrightarrow> b < x \<Longrightarrow> x < a \<Longrightarrow> x \<notin> X \<Longrightarrow> f x = g x"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
+  shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
+  unfolding interval_lebesgue_integral_def
+  apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms)
+  apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
+  done
+
+lemma interval_integral_sum: 
+  fixes a b c :: ereal
+  assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" 
+  shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
+proof -
+  let ?I = "\<lambda>a b. LBINT x=a..b. f x"
+  { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
+    then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
+      by (auto simp: interval_lebesgue_integrable_def)
+    then have f: "set_borel_measurable borel (einterval a c) f"
+      by (drule_tac borel_measurable_integrable) simp
+    have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b \<union> einterval b c. f x)"
+    proof (rule set_integral_cong_set)
+      show "AE x in lborel. (x \<in> einterval a b \<union> einterval b c) = (x \<in> einterval a c)"
+        using AE_lborel_singleton[of "real b"] ord
+        by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff)
+    qed (insert ord, auto intro!: set_borel_measurable_subset[OF f] simp: einterval_iff)
+    also have "\<dots> = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)"
+      using ord
+      by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less)
+    finally have "?I a b + ?I b c = ?I a c"
+      using ord by (simp add: interval_lebesgue_integral_def)
+  } note 1 = this
+  { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
+    from 1[OF this] have "?I b c + ?I a b = ?I a c"
+      by (metis add.commute)
+  } note 2 = this
+  have 3: "\<And>a b. b \<le> a \<Longrightarrow> (LBINT x=a..b. f x) = - (LBINT x=b..a. f x)"
+    by (rule interval_integral_endpoints_reverse)
+  show ?thesis
+    using integrable
+    by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
+       (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
+qed
+
+lemma interval_integrable_isCont:
+  fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow>
+    interval_lebesgue_integrable lborel a b f"
+proof (induct a b rule: linorder_wlog)
+  case (le a b) then show ?case
+    by (auto simp: interval_lebesgue_integrable_def
+             intro!: set_integrable_subset[OF borel_integrable_compact[of "{a .. b}"]]
+                     continuous_at_imp_continuous_on)
+qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1])
+
+lemma interval_integrable_continuous_on:
+  fixes a b :: real and f
+  assumes "a \<le> b" and "continuous_on {a..b} f"
+  shows "interval_lebesgue_integrable lborel a b f"
+using assms unfolding interval_lebesgue_integrable_def apply simp
+  by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto)
+
+lemma interval_integral_eq_integral: 
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  shows "a \<le> b \<Longrightarrow> set_integrable lborel {a..b} f \<Longrightarrow> LBINT x=a..b. f x = integral {a..b} f"
+  by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral)
+
+lemma interval_integral_eq_integral': 
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  shows "a \<le> b \<Longrightarrow> set_integrable lborel (einterval a b) f \<Longrightarrow> LBINT x=a..b. f x = integral (einterval a b) f"
+  by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
+  
+(*
+    General limit approximation arguments
+*)
+
+lemma interval_integral_Icc_approx_nonneg:
+  fixes a b :: ereal
+  assumes "a < b"
+  fixes u l :: "nat \<Rightarrow> real"
+  assumes  approx: "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l ----> a" "u ----> b"
+  fixes f :: "real \<Rightarrow> real"
+  assumes f_integrable: "\<And>i. set_integrable lborel {l i..u i} f"
+  assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
+  assumes f_measurable: "set_borel_measurable lborel (einterval a b) f"
+  assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) ----> C"
+  shows 
+    "set_integrable lborel (einterval a b) f"
+    "(LBINT x=a..b. f x) = C"
+proof -
+  have 1: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
+  have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
+  proof -
+     from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x"
+      by eventually_elim
+         (metis approx(5) approx(6) dual_order.strict_trans1 ereal_less_eq(3) le_less_trans)
+    then show ?thesis
+      apply eventually_elim
+      apply (auto simp: mono_def split: split_indicator)
+      apply (metis approx(3) decseqD order_trans)
+      apply (metis approx(2) incseqD order_trans)
+      done
+  qed
+  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"
+  proof -
+    { fix x i assume "l i \<le> x" "x \<le> u i"
+      then have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
+        apply (auto simp: eventually_sequentially intro!: exI[of _ i])
+        apply (metis approx(3) decseqD order_trans)
+        apply (metis approx(2) incseqD order_trans)
+        done
+      then have "eventually (\<lambda>i. f x * indicator {l i..u i} x = f x) sequentially"
+        by eventually_elim auto }
+    then show ?thesis
+      unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator)
+  qed
+  have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) ----> C"
+    using lbint_lim by (simp add: interval_integral_Icc approx less_imp_le)
+  have 5: "set_borel_measurable lborel (einterval a b) f" by (rule assms)
+  have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\<lambda>x. indicator (einterval a b) x *\<^sub>R f x)"
+    using assms by (simp add: interval_lebesgue_integral_def less_imp_le)
+  also have "... = C" by (rule integral_monotone_convergence [OF 1 2 3 4 5])
+  finally show "(LBINT x=a..b. f x) = C" .
+
+  show "set_integrable lborel (einterval a b) f" 
+    by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
+qed
+
+lemma interval_integral_Icc_approx_integrable:
+  fixes u l :: "nat \<Rightarrow> real" and a b :: ereal
+  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  assumes "a < b"
+  assumes  approx: "einterval a b = (\<Union>i. {l i .. u i})"
+    "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
+    "l ----> a" "u ----> b"
+  assumes f_integrable: "set_integrable lborel (einterval a b) f"
+  shows "(\<lambda>i. LBINT x=l i.. u i. f x) ----> (LBINT x=a..b. f x)"
+proof -
+  have "(\<lambda>i. LBINT x:{l i.. u i}. f x) ----> (LBINT x:einterval a b. f x)"
+  proof (rule integral_dominated_convergence)
+    show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))"
+      by (rule integrable_norm) fact
+    show "set_borel_measurable lborel (einterval a b) f"
+      using f_integrable by (rule borel_measurable_integrable)
+    then show "\<And>i. set_borel_measurable lborel {l i..u i} f"
+      by (rule set_borel_measurable_subset) (auto simp: approx)
+    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)"
+      by (intro AE_I2) (auto simp: approx split: split_indicator)
+    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"
+    proof (intro AE_I2 tendsto_intros Lim_eventually)
+      fix x
+      { fix i assume "l i \<le> x" "x \<le> u i" 
+        with `incseq u`[THEN incseqD, of i] `decseq l`[THEN decseqD, of i]
+        have "eventually (\<lambda>i. l i \<le> x \<and> x \<le> u i) sequentially"
+          by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) }
+      then show "eventually (\<lambda>xa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially"
+        using approx order_tendstoD(2)[OF `l ----> a`, of x] order_tendstoD(1)[OF `u ----> b`, of x]
+        by (auto split: split_indicator)
+    qed
+  qed
+  with `a < b` `\<And>i. l i < u i` show ?thesis
+    by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le)
+qed
+
+(*
+  A slightly stronger version of integral_FTC_atLeastAtMost and related facts, 
+  with continuous_on instead of isCont
+
+  TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
+*)
+
+(*
+TODO: many proofs below require inferences like
+
+  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y
+
+where x and y are real. These should be better automated.
+*)
+
+(*
+    The first Fundamental Theorem of Calculus
+
+    First, for finite intervals, and then two versions for arbitrary intervals.
+*)
+
+lemma interval_integral_FTC_finite:
+  fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
+  assumes f: "continuous_on {min a b..max a b} f"
+  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 
+    {min a b..max a b})" 
+  shows "(LBINT x=a..b. f x) = F b - F a"
+  apply (case_tac "a \<le> b")
+  apply (subst interval_integral_Icc, simp)
+  apply (rule integral_FTC_atLeastAtMost, assumption)
+  apply (metis F max_def min_def)
+  using f apply (simp add: min_absorb1 max_absorb2)
+  apply (subst interval_integral_endpoints_reverse)
+  apply (subst interval_integral_Icc, simp)
+  apply (subst integral_FTC_atLeastAtMost, auto)
+  apply (metis F max_def min_def)
+using f by (simp add: min_absorb2 max_absorb1)
+
+lemma interval_integral_FTC_nonneg:
+  fixes f F :: "real \<Rightarrow> real" and a b :: ereal
+  assumes "a < b"
+  assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x" 
+  assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" 
+  assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
+  assumes A: "((F \<circ> real) ---> A) (at_right a)"
+  assumes B: "((F \<circ> real) ---> B) (at_left b)"
+  shows
+    "set_integrable lborel (einterval a b) f" 
+    "(LBINT x=a..b. f x) = B - A"
+proof -
+  from einterval_Icc_approximation[OF `a < b`] guess u l . note approx = this
+  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
+    by (rule order_less_le_trans, rule approx, force)
+  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
+    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
+  have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
+    using assms approx apply (intro interval_integral_FTC_finite)
+    apply (auto simp add: less_imp_le min_def max_def
+      has_field_derivative_iff_has_vector_derivative[symmetric])
+    apply (rule continuous_at_imp_continuous_on, auto intro!: f)
+    by (rule DERIV_subset [OF F], auto)
+  have 1: "\<And>i. set_integrable lborel {l i..u i} f"
+  proof -
+    fix i show "set_integrable lborel {l i .. u i} f"
+      using `a < l i` `u i < b`
+      by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
+         (auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric])
+  qed
+  have 2: "set_borel_measurable lborel (einterval a b) f"
+    by (auto simp del: real_scaleR_def intro!: set_borel_measurable_continuous 
+             simp: continuous_on_eq_continuous_at einterval_iff f)
+  have 3: "(\<lambda>i. LBINT x=l i..u i. f x) ----> B - A"
+    apply (subst FTCi)
+    apply (intro tendsto_intros)
+    using B approx unfolding tendsto_at_iff_sequentially comp_def
+    using tendsto_at_iff_sequentially[where 'a=real]
+    apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
+    using A approx unfolding tendsto_at_iff_sequentially comp_def
+    by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
+  show "(LBINT x=a..b. f x) = B - A"
+    by (rule interval_integral_Icc_approx_nonneg [OF `a < b` approx 1 f_nonneg 2 3])
+  show "set_integrable lborel (einterval a b) f" 
+    by (rule interval_integral_Icc_approx_nonneg [OF `a < b` approx 1 f_nonneg 2 3])
+qed
+
+lemma interval_integral_FTC_integrable:
+  fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal
+  assumes "a < b"
+  assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)" 
+  assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x" 
+  assumes f_integrable: "set_integrable lborel (einterval a b) f"
+  assumes A: "((F \<circ> real) ---> A) (at_right a)"
+  assumes B: "((F \<circ> real) ---> B) (at_left b)"
+  shows "(LBINT x=a..b. f x) = B - A"
+proof -
+  from einterval_Icc_approximation[OF `a < b`] guess u l . note approx = this
+  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
+    by (rule order_less_le_trans, rule approx, force)
+  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
+    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
+  have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
+    using assms approx
+    by (auto simp add: less_imp_le min_def max_def
+             intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite
+             intro: has_vector_derivative_at_within)
+  have "(\<lambda>i. LBINT x=l i..u i. f x) ----> B - A"
+    apply (subst FTCi)
+    apply (intro tendsto_intros)
+    using B approx unfolding tendsto_at_iff_sequentially comp_def
+    apply (elim allE[of _ "\<lambda>i. ereal (u i)"], auto)
+    using A approx unfolding tendsto_at_iff_sequentially comp_def
+    by (elim allE[of _ "\<lambda>i. ereal (l i)"], auto)
+  moreover have "(\<lambda>i. LBINT x=l i..u i. f x) ----> (LBINT x=a..b. f x)"
+    by (rule interval_integral_Icc_approx_integrable [OF `a < b` approx f_integrable])
+  ultimately show ?thesis
+    by (elim LIMSEQ_unique)
+qed
+
+(* 
+  The second Fundamental Theorem of Calculus and existence of antiderivatives on an
+  einterval.
+*)
+
+lemma interval_integral_FTC2:
+  fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "a \<le> c" "c \<le> b"
+  and contf: "continuous_on {a..b} f"
+  fixes x :: real
+  assumes "a \<le> x" and "x \<le> b"
+  shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
+proof -
+  let ?F = "(\<lambda>u. LBINT y=a..u. f y)"
+  have intf: "set_integrable lborel {a..b} f"
+    by (rule borel_integrable_atLeastAtMost', rule contf)
+  have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
+    apply (intro integral_has_vector_derivative)
+    using `a \<le> x` `x \<le> b` by (intro continuous_on_subset [OF contf], auto)
+  then have "((\<lambda>u. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})"
+    by simp
+  then have "(?F has_vector_derivative (f x)) (at x within {a..b})"
+    by (rule has_vector_derivative_weaken)
+       (auto intro!: assms interval_integral_eq_integral[symmetric] set_integrable_subset [OF intf])
+  then have "((\<lambda>x. (LBINT y=c..a. f y) + ?F x) has_vector_derivative (f x)) (at x within {a..b})"
+    by (auto intro!: derivative_eq_intros)
+  then show ?thesis
+  proof (rule has_vector_derivative_weaken)
+    fix u assume "u \<in> {a .. b}"
+    then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)"
+      using assms
+      apply (intro interval_integral_sum)
+      apply (auto simp add: interval_lebesgue_integrable_def simp del: real_scaleR_def)
+      by (rule set_integrable_subset [OF intf], auto simp add: min_def max_def)
+  qed (insert assms, auto)
+qed
+
+lemma einterval_antiderivative: 
+  fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x"
+  shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
+proof -
+  from einterval_nonempty [OF `a < b`] obtain c :: real where [simp]: "a < c" "c < b" 
+    by (auto simp add: einterval_def)
+  let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
+  show ?thesis
+  proof (rule exI, clarsimp)
+    fix x :: real
+    assume [simp]: "a < x" "x < b"
+    have 1: "a < min c x" by simp
+    from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x" 
+      by (auto simp add: einterval_def)
+    have 2: "max c x < b" by simp
+    from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b" 
+      by (auto simp add: einterval_def)
+    show "(?F has_vector_derivative f x) (at x)"
+      (* TODO: factor out the next three lines to has_field_derivative_within_open *)
+      unfolding has_vector_derivative_def
+      apply (subst has_derivative_within_open [of _ "{d<..<e}", symmetric], auto)
+      apply (subst has_vector_derivative_def [symmetric])
+      apply (rule has_vector_derivative_within_subset [of _ _ _ "{d..e}"])
+      apply (rule interval_integral_FTC2, auto simp add: less_imp_le)
+      apply (rule continuous_at_imp_continuous_on)
+      apply (auto intro!: contf)
+      apply (rule order_less_le_trans, rule `a < d`, auto)
+      apply (rule order_le_less_trans) prefer 2
+      by (rule `e < b`, auto)
+  qed
+qed
+
+(*
+    The substitution theorem
+
+    Once again, three versions: first, for finite intervals, and then two versions for
+    arbitrary intervals.
+*)
+  
+lemma interval_integral_substitution_finite:
+  fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "a \<le> b"
+  and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
+  and contf : "continuous_on (g ` {a..b}) f"
+  and contg': "continuous_on {a..b} g'"
+  shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
+proof-
+  have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
+    using derivg unfolding has_field_derivative_iff_has_vector_derivative .
+  then have contg [simp]: "continuous_on {a..b} g"
+    by (rule continuous_on_vector_derivative) auto
+  have 1: "\<And>u. min (g a) (g b) \<le> u \<Longrightarrow> u \<le> max (g a) (g b) \<Longrightarrow> 
+      \<exists>x\<in>{a..b}. u = g x"
+    apply (case_tac "g a \<le> g b")
+    apply (auto simp add: min_def max_def less_imp_le)
+    apply (frule (1) IVT' [of g], auto simp add: assms)
+    by (frule (1) IVT2' [of g], auto simp add: assms)
+  from contg `a \<le> b` have "\<exists>c d. g ` {a..b} = {c..d} \<and> c \<le> d"
+    by (elim continuous_image_closed_interval)
+  then obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \<le> d" by auto
+  have "\<exists>F. \<forall>x\<in>{a..b}. (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))"
+    apply (rule exI, auto, subst g_im)
+    apply (rule interval_integral_FTC2 [of c c d])
+    using `c \<le> d` apply auto
+    apply (rule continuous_on_subset [OF contf])
+    using g_im by auto
+  then guess F ..
+  then have derivF: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> 
+    (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" by auto
+  have contf2: "continuous_on {min (g a) (g b)..max (g a) (g b)} f"
+    apply (rule continuous_on_subset [OF contf])
+    apply (auto simp add: image_def)
+    by (erule 1)
+  have contfg: "continuous_on {a..b} (\<lambda>x. f (g x))"
+    by (blast intro: continuous_on_compose2 contf contg)
+  have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)"
+    apply (subst interval_integral_Icc, simp add: assms)
+    apply (rule integral_FTC_atLeastAtMost[of a b "\<lambda>x. F (g x)", OF `a \<le> b`])
+    apply (rule vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def])
+    apply (auto intro!: continuous_on_scaleR contg' contfg)
+    done
+  moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)"
+    apply (rule interval_integral_FTC_finite)
+    apply (rule contf2)
+    apply (frule (1) 1, auto)
+    apply (rule has_vector_derivative_within_subset [OF derivF])
+    apply (auto simp add: image_def)
+    by (rule 1, auto)
+  ultimately show ?thesis by simp
+qed
+
+(* TODO: is it possible to lift the assumption here that g' is nonnegative? *)
+
+lemma interval_integral_substitution_integrable:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal
+  assumes "a < b" 
+  and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
+  and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
+  and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
+  and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x"
+  and A: "((ereal \<circ> g \<circ> real) ---> A) (at_right a)"
+  and B: "((ereal \<circ> g \<circ> real) ---> B) (at_left b)"
+  and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
+  and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
+  shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
+proof -
+  from einterval_Icc_approximation[OF `a < b`] guess u l . note approx [simp] = this
+  note less_imp_le [simp]
+  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
+    by (rule order_less_le_trans, rule approx, force)
+  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
+    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
+  have [simp]: "\<And>i. l i < b" 
+    apply (rule order_less_trans) prefer 2 
+    by (rule approx, auto, rule approx)
+  have [simp]: "\<And>i. a < u i" 
+    by (rule order_less_trans, rule approx, auto, rule approx)
+  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
+  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
+  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
+    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
+    apply (rule exI, rule conjI, rule deriv_g)
+    apply (erule order_less_le_trans, auto)
+    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
+    apply (rule g'_nonneg)
+    apply (rule less_imp_le, erule order_less_le_trans, auto)
+    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
+  have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
+  proof - 
+    have A2: "(\<lambda>i. g (l i)) ----> A"
+      using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
+      by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
+    hence A3: "\<And>i. g (l i) \<ge> A"
+      by (intro decseq_le, auto simp add: decseq_def)
+    have B2: "(\<lambda>i. g (u i)) ----> B"
+      using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
+      by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
+    hence B3: "\<And>i. g (u i) \<le> B"
+      by (intro incseq_le, auto simp add: incseq_def)
+    show "A \<le> B"
+      apply (rule order_trans [OF A3 [of 0]])
+      apply (rule order_trans [OF _ B3 [of 0]])
+      by auto
+    { fix x :: real
+      assume "A < x" and "x < B"   
+      then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
+        apply (intro eventually_conj order_tendstoD)
+        by (rule A2, assumption, rule B2, assumption)
+      hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
+        by (simp add: eventually_sequentially, auto)
+    } note AB = this
+    show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
+      apply (auto simp add: einterval_def)
+      apply (erule (1) AB)
+      apply (rule order_le_less_trans, rule A3, simp)
+      apply (rule order_less_le_trans) prefer 2
+      by (rule B3, simp) 
+  qed
+  (* finally, the main argument *)
+  {
+     fix i
+     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
+        apply (rule interval_integral_substitution_finite, auto)
+        apply (rule DERIV_subset)
+        unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+        apply (rule deriv_g)
+        apply (auto intro!: continuous_at_imp_continuous_on contf contg')
+        done
+  } note eq1 = this
+  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))"
+    apply (rule interval_integral_Icc_approx_integrable [OF `a < b` approx])
+    by (rule assms)
+  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))"
+    by (simp add: eq1)
+  have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
+    apply (auto simp add: incseq_def)
+    apply (rule order_le_less_trans)
+    prefer 2 apply (assumption, auto)
+    by (erule order_less_le_trans, rule g_nondec, auto)
+  have "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x = A..B. f x)"
+    apply (subst interval_lebesgue_integral_le_eq, auto simp del: real_scaleR_def)
+    apply (subst interval_lebesgue_integral_le_eq, rule `A \<le> B`)
+    apply (subst un, rule set_integral_cont_up, auto simp del: real_scaleR_def)
+    apply (rule incseq)
+    apply (subst un [symmetric])
+    by (rule integrable2)
+  thus ?thesis by (intro LIMSEQ_unique [OF _ 2])
+qed
+
+(* TODO: the last two proofs are only slightly different. Factor out common part?
+   An alternative: make the second one the main one, and then have another lemma
+   that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *)
+
+lemma interval_integral_substitution_nonneg:
+  fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal
+  assumes "a < b" 
+  and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
+  and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
+  and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"
+  and f_nonneg: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> 0 \<le> f (g x)" (* TODO: make this AE? *)
+  and g'_nonneg: "\<And>x. a \<le> ereal x \<Longrightarrow> ereal x \<le> b \<Longrightarrow> 0 \<le> g' x"
+  and A: "((ereal \<circ> g \<circ> real) ---> A) (at_right a)"
+  and B: "((ereal \<circ> g \<circ> real) ---> B) (at_left b)"
+  and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)"
+  shows 
+    "set_integrable lborel (einterval A B) f"
+    "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
+proof -
+  from einterval_Icc_approximation[OF `a < b`] guess u l . note approx [simp] = this
+  note less_imp_le [simp]
+  have [simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
+    by (rule order_less_le_trans, rule approx, force)
+  have [simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
+    by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx)
+  have [simp]: "\<And>i. l i < b" 
+    apply (rule order_less_trans) prefer 2 
+    by (rule approx, auto, rule approx)
+  have [simp]: "\<And>i. a < u i" 
+    by (rule order_less_trans, rule approx, auto, rule approx)
+  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> l j \<le> l i" by (rule decseqD, rule approx)
+  have [simp]: "\<And>i j. i \<le> j \<Longrightarrow> u i \<le> u j" by (rule incseqD, rule approx)
+  have g_nondec [simp]: "\<And>x y. a < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < b \<Longrightarrow> g x \<le> g y"
+    apply (erule DERIV_nonneg_imp_nondecreasing, auto)
+    apply (rule exI, rule conjI, rule deriv_g)
+    apply (erule order_less_le_trans, auto)
+    apply (rule order_le_less_trans, subst ereal_less_eq(3), assumption, auto)
+    apply (rule g'_nonneg)
+    apply (rule less_imp_le, erule order_less_le_trans, auto)
+    by (rule less_imp_le, rule le_less_trans, subst ereal_less_eq(3), assumption, auto)
+  have "A \<le> B" and un: "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
+  proof - 
+    have A2: "(\<lambda>i. g (l i)) ----> A"
+      using A apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
+      by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
+    hence A3: "\<And>i. g (l i) \<ge> A"
+      by (intro decseq_le, auto simp add: decseq_def)
+    have B2: "(\<lambda>i. g (u i)) ----> B"
+      using B apply (auto simp add: einterval_def tendsto_at_iff_sequentially comp_def)
+      by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
+    hence B3: "\<And>i. g (u i) \<le> B"
+      by (intro incseq_le, auto simp add: incseq_def)
+    show "A \<le> B"
+      apply (rule order_trans [OF A3 [of 0]])
+      apply (rule order_trans [OF _ B3 [of 0]])
+      by auto
+    { fix x :: real
+      assume "A < x" and "x < B"   
+      then have "eventually (\<lambda>i. ereal (g (l i)) < x \<and> x < ereal (g (u i))) sequentially"
+        apply (intro eventually_conj order_tendstoD)
+        by (rule A2, assumption, rule B2, assumption)
+      hence "\<exists>i. g (l i) < x \<and> x < g (u i)"
+        by (simp add: eventually_sequentially, auto)
+    } note AB = this
+    show "einterval A B = (\<Union>i. {g(l i)<..<g(u i)})"
+      apply (auto simp add: einterval_def)
+      apply (erule (1) AB)
+      apply (rule order_le_less_trans, rule A3, simp)
+      apply (rule order_less_le_trans) prefer 2
+      by (rule B3, simp) 
+  qed
+  (* finally, the main argument *)
+  {
+     fix i
+     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
+        apply (rule interval_integral_substitution_finite, auto)
+        apply (rule DERIV_subset, rule deriv_g, auto)
+        apply (rule continuous_at_imp_continuous_on, auto, rule contf, auto)
+        by (rule continuous_at_imp_continuous_on, auto, rule contg', auto)
+     then have "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)"
+       by (simp add: ac_simps)
+  } note eq1 = this
+  have "(\<lambda>i. LBINT x=l i..u i. f (g x) * g' x)
+      ----> (LBINT x=a..b. f (g x) * g' x)"
+    apply (rule interval_integral_Icc_approx_integrable [OF `a < b` approx])
+    by (rule assms)
+  hence 2: "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) ----> (LBINT x=a..b. f (g x) * g' x)"
+    by (simp add: eq1)
+  have incseq: "incseq (\<lambda>i. {g (l i)<..<g (u i)})"
+    apply (auto simp add: incseq_def)
+    apply (rule order_le_less_trans)
+    prefer 2 apply assumption
+    apply (rule g_nondec, auto)
+    by (erule order_less_le_trans, rule g_nondec, auto)
+  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"
+    apply (frule (1) IVT' [of g], auto)   
+    apply (rule continuous_at_imp_continuous_on, auto)
+    by (rule DERIV_isCont, rule deriv_g, auto)
+  have nonneg_f2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
+    by (frule (1) img, auto, rule f_nonneg, auto)
+  have contf_2: "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> isCont f x"
+    by (frule (1) img, auto, rule contf, auto)
+  have integrable: "set_integrable lborel (\<Union>i. {g (l i)<..<g (u i)}) f"
+    apply (rule pos_integrable_to_top, auto simp del: real_scaleR_def)
+    apply (rule incseq)
+    apply (rule nonneg_f2, erule less_imp_le, erule less_imp_le)
+    apply (rule set_integrable_subset)
+    apply (rule borel_integrable_atLeastAtMost')
+    apply (rule continuous_at_imp_continuous_on)
+    apply (clarsimp, erule (1) contf_2, auto)
+    apply (erule less_imp_le)+
+    using 2 unfolding interval_lebesgue_integral_def
+    by auto
+  thus "set_integrable lborel (einterval A B) f"
+    by (simp add: un)
+
+  have "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
+  proof (rule interval_integral_substitution_integrable)
+    show "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
+      using integrable_fg by (simp add: ac_simps)
+  qed fact+
+  then show "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
+    by (simp add: ac_simps)
+qed
+
+
+syntax
+"_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
+("(2CLBINT _. _)" [0,60] 60)
+
+translations
+"CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
+
+syntax
+"_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
+("(3CLBINT _:_. _)" [0,60,61] 60)
+
+translations
+"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
+
+abbreviation complex_interval_lebesgue_integral :: 
+    "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> complex" where
+  "complex_interval_lebesgue_integral M a b f \<equiv> interval_lebesgue_integral M a b f"
+
+abbreviation complex_interval_lebesgue_integrable :: 
+  "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> bool" where
+  "complex_interval_lebesgue_integrable M a b f \<equiv> interval_lebesgue_integrable M a b f"
+
+syntax
+  "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
+  ("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
+
+translations
+  "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
+
+lemma interval_integral_norm:
+  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
+    norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
+  using integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
+  by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def)
+
+lemma interval_integral_norm2:
+  "interval_lebesgue_integrable lborel a b f \<Longrightarrow> 
+    norm (LBINT t=a..b. f t) \<le> abs (LBINT t=a..b. norm (f t))"
+proof (induct a b rule: linorder_wlog)
+  case (sym a b) then show ?case
+    by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
+next
+  case (le a b) 
+  then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"  
+    using integrable_norm[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
+    by (auto simp add: interval_lebesgue_integral_def interval_lebesgue_integrable_def
+             intro!: integral_nonneg_AE abs_of_nonneg)
+  then show ?case
+    using le by (simp add: interval_integral_norm)
+qed
+
+(* TODO: should we have a library of facts like these? *)
+lemma integral_cos: "t \<noteq> 0 \<Longrightarrow> LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t"
+  apply (intro interval_integral_FTC_finite continuous_intros)
+  by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric])
+
+
+end
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Lebesgue_Integral_Substitution.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -0,0 +1,707 @@
+(*  Title:      HOL/Probability/Lebesgue_Integral_Substitution.thy
+    Author:     Manuel Eberl
+
+    Provides lemmas for integration by substitution for the basic integral types.
+    Note that the substitution function must have a nonnegative derivative.
+    This could probably be weakened somehow.
+*)
+
+section {* Integration by Substition *}
+
+theory Lebesgue_Integral_Substitution
+imports Interval_Integral
+begin
+
+lemma measurable_sets_borel:
+    "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
+  by (drule (1) measurable_sets) simp
+
+lemma closure_Iii: 
+  assumes "a < b"
+  shows "closure {a<..<b::real} = {a..b}"
+proof-
+  have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less)
+  also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp
+  also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less)
+  finally show ?thesis .
+qed
+
+lemma continuous_ge_on_Iii:
+  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
+  shows "g (x::real) \<ge> (a::real)"
+proof-
+  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric])
+  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
+  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
+  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
+    by (auto simp: continuous_on_closed_vimage)
+  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
+  finally show ?thesis using `x \<in> {c..d}` by auto 
+qed 
+
+lemma interior_real_semiline':
+  fixes a :: real
+  shows "interior {..a} = {..<a}"
+proof -
+  {
+    fix y
+    assume "a > y"
+    then have "y \<in> interior {..a}"
+      apply (simp add: mem_interior)
+      apply (rule_tac x="(a-y)" in exI)
+      apply (auto simp add: dist_norm)
+      done
+  }
+  moreover
+  {
+    fix y
+    assume "y \<in> interior {..a}"
+    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
+      using mem_interior_cball[of y "{..a}"] by auto
+    moreover from e have "y + e \<in> cball y e"
+      by (auto simp add: cball_def dist_norm)
+    ultimately have "a \<ge> y + e" by auto
+    then have "a > y" using e by auto
+  }
+  ultimately show ?thesis by auto
+qed
+
+lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
+proof-
+  have "{a..b} = {a..} \<inter> {..b}" by auto
+  also have "interior ... = {a<..} \<inter> {..<b}" 
+    by (simp add: interior_real_semiline interior_real_semiline')
+  also have "... = {a<..<b}" by auto
+  finally show ?thesis .
+qed
+
+lemma nn_integral_indicator_singleton[simp]:
+  assumes [measurable]: "{y} \<in> sets M"
+  shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
+proof-
+  have "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f y) * indicator {y} x \<partial>M)"
+    by (subst nn_integral_max_0[symmetric]) (auto intro!: nn_integral_cong split: split_indicator)
+  then show ?thesis
+    by (simp add: nn_integral_cmult)
+qed
+
+lemma nn_integral_set_ereal:
+  "(\<integral>\<^sup>+x. ereal (f x) * indicator A x \<partial>M) = (\<integral>\<^sup>+x. ereal (f x * indicator A x) \<partial>M)"
+  by (rule nn_integral_cong) (simp split: split_indicator)
+
+lemma nn_integral_indicator_singleton'[simp]:
+  assumes [measurable]: "{y} \<in> sets M"
+  shows "(\<integral>\<^sup>+x. ereal (f x * indicator {y} x) \<partial>M) = max 0 (f y) * emeasure M {y}"
+  by (subst nn_integral_set_ereal[symmetric]) simp
+
+lemma set_borel_measurable_sets:
+  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
+  assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
+  shows "f -` B \<inter> X \<in> sets M"
+proof -
+  have "f \<in> borel_measurable (restrict_space M X)"
+    using assms by (subst borel_measurable_restrict_space_iff) auto
+  then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
+    by (rule measurable_sets) fact
+  with `X \<in> sets M` show ?thesis
+    by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
+qed
+
+lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
+  assumes "A \<in> sets borel" 
+  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
+          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)"
+  shows "P (A::real set)"
+proof-
+  let ?G = "range (\<lambda>(a,b). {a..b::real})"
+  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" 
+      using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
+  thus ?thesis
+  proof (induction rule: sigma_sets_induct_disjoint) 
+    case (union f)
+      from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
+      with union show ?case by (auto intro: un)
+  next
+    case (basic A)
+    then obtain a b where "A = {a .. b}" by auto
+    then show ?case
+      by (cases "a \<le> b") (auto intro: int empty)
+  qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
+qed
+
+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"
+
+lemma mono_onI:
+  "(\<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"
+  unfolding mono_on_def by simp
+
+lemma mono_onD:
+  "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
+  unfolding mono_on_def by simp
+
+lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
+  unfolding mono_def mono_on_def by auto
+
+lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
+  unfolding mono_on_def by auto
+
+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"
+
+lemma strict_mono_onI:
+  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A"
+  unfolding strict_mono_on_def by simp
+
+lemma strict_mono_onD:
+  "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
+  unfolding strict_mono_on_def by simp
+
+lemma mono_on_greaterD:
+  assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
+  shows "x > y"
+proof (rule ccontr)
+  assume "\<not>x > y"
+  hence "x \<le> y" by (simp add: not_less)
+  from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
+  with assms(4) show False by simp
+qed
+
+lemma strict_mono_inv:
+  fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
+  assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
+  shows "strict_mono g"
+proof
+  fix x y :: 'b assume "x < y"
+  from `surj f` obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
+  with `x < y` and `strict_mono f` have "x' < y'" by (simp add: strict_mono_less)
+  with inv show "g x < g y" by simp
+qed
+
+lemma strict_mono_on_imp_inj_on:
+  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
+  shows "inj_on f A"
+proof (rule inj_onI)
+  fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
+  thus "x = y"
+    by (cases x y rule: linorder_cases)
+       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 
+qed
+
+lemma strict_mono_on_leD:
+  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
+  shows "f x \<le> f y"
+proof (insert le_less_linear[of y x], elim disjE)
+  assume "x < y"
+  with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
+  thus ?thesis by (rule less_imp_le)
+qed (insert assms, simp)
+
+lemma strict_mono_on_eqD:
+  fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
+  assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
+  shows "y = x"
+  using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
+
+lemma mono_on_imp_deriv_nonneg:
+  assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
+  assumes "x \<in> interior A"
+  shows "D \<ge> 0"
+proof (rule tendsto_le_const)
+  let ?A' = "(\<lambda>y. y - x) ` interior A"
+  from deriv show "((\<lambda>h. (f (x + h) - f x) / h) ---> D) (at 0)"
+      by (simp add: field_has_derivative_at has_field_derivative_def)
+  from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset)
+
+  show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
+  proof (subst eventually_at_topological, intro exI conjI ballI impI)
+    have "open (interior A)" by simp
+    hence "open (op + (-x) ` interior A)" by (rule open_translation)
+    also have "(op + (-x) ` interior A) = ?A'" by auto
+    finally show "open ?A'" .
+  next
+    from `x \<in> interior A` show "0 \<in> ?A'" by auto
+  next
+    fix h assume "h \<in> ?A'"
+    hence "x + h \<in> interior A" by auto
+    with mono' and `x \<in> interior A` show "(f (x + h) - f x) / h \<ge> 0"
+      by (cases h rule: linorder_cases[of _ 0])
+         (simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps)
+  qed
+qed simp
+
+lemma strict_mono_on_imp_mono_on: 
+  "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
+  by (rule mono_onI, rule strict_mono_on_leD)
+
+lemma has_real_derivative_imp_continuous_on:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
+  shows "continuous_on A f"
+  apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
+  apply (intro ballI Deriv.differentiableI)
+  apply (rule has_field_derivative_subset[OF assms])
+  apply simp_all
+  done
+
+lemma closure_contains_Sup:
+  fixes S :: "real set"
+  assumes "S \<noteq> {}" "bdd_above S"
+  shows "Sup S \<in> closure S"
+proof-
+  have "Inf (uminus ` S) \<in> closure (uminus ` S)" 
+      using assms by (intro closure_contains_Inf) auto
+  also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
+  also have "closure (uminus ` S) = uminus ` closure S"
+      by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
+  finally show ?thesis by auto
+qed
+
+lemma closed_contains_Sup:
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
+  by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
+
+lemma deriv_nonneg_imp_mono:
+  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes ab: "a \<le> b"
+  shows "g a \<le> g b"
+proof (cases "a < b")
+  assume "a < b"
+  from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
+  from MVT2[OF `a < b` this] and deriv 
+    obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
+  from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
+  with g_ab show ?thesis by simp
+qed (insert ab, simp)
+
+lemma continuous_interval_vimage_Int:
+  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"
+  assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}"
+  obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d"
+proof-
+    let ?A = "{a..b} \<inter> g -` {c..d}"
+    from IVT'[of g a c b, OF _ _ `a \<le> b` assms(1)] assms(4,5) 
+         obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto
+    from IVT'[of g a d b, OF _ _ `a \<le> b` assms(1)] assms(4,5) 
+         obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto
+    hence [simp]: "?A \<noteq> {}" by blast
+
+    def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A"
+    have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def
+        by (intro subsetI) (auto intro: cInf_lower cSup_upper)
+    moreover from assms have "closed ?A" 
+        using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
+    hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def
+        by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
+    hence "{c'..d'} \<subseteq> ?A" using assms 
+        by (intro subsetI)
+           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] 
+                 intro!: mono)
+    moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
+    moreover have "g c' \<le> c" "g d' \<ge> d"
+      apply (insert c'' d'' c'd'_in_set)
+      apply (subst c''(2)[symmetric])
+      apply (auto simp: c'_def intro!: mono cInf_lower c'') []
+      apply (subst d''(2)[symmetric])
+      apply (auto simp: d'_def intro!: mono cSup_upper d'') []
+      done
+    with c'd'_in_set have "g c' = c" "g d' = d" by auto
+    ultimately show ?thesis using that by blast
+qed
+
+lemma nn_integral_substitution_aux:
+  fixes f :: "real \<Rightarrow> ereal"
+  assumes Mf: "f \<in> borel_measurable borel"
+  assumes nonnegf: "\<And>x. f x \<ge> 0"
+  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes contg': "continuous_on {a..b} g'" 
+  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes "a < b"
+  shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
+             (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
+proof-
+  from `a < b` have [simp]: "a \<le> b" by simp
+  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
+  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and 
+                             Mg': "set_borel_measurable borel {a..b} g'" 
+      by (simp_all only: set_measurable_continuous_on_ivl)
+  from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
+    by (simp only: has_field_derivative_iff_has_vector_derivative)
+
+  have real_ind[simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x" 
+      by (auto split: split_indicator)
+  have ereal_ind[simp]: "\<And>A x. ereal (indicator A x) = indicator A x" 
+      by (auto split: split_indicator)
+  have [simp]: "\<And>x A. indicator A (g x) = indicator (g -` A) x" 
+      by (auto split: split_indicator)
+
+  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"
+    by (rule deriv_nonneg_imp_mono) simp_all
+  with monog have [simp]: "g a \<le> g b" by (auto intro: mono_onD)
+
+  show ?thesis
+  proof (induction rule: borel_measurable_induct[OF Mf nonnegf, case_names cong set mult add sup])
+    case (cong f1 f2)
+    from cong.hyps(3) have "f1 = f2" by auto
+    with cong show ?case by simp
+  next
+    case (set A)
+    from set.hyps show ?case
+    proof (induction rule: borel_set_induct)
+      case empty
+      thus ?case by simp
+    next
+      case (interval c d)
+      {
+        fix u v :: real assume asm: "{u..v} \<subseteq> {g a..g b}" "u \<le> v"
+        
+        obtain u' v' where u'v': "{a..b} \<inter> g-`{u..v} = {u'..v'}" "u' \<le> v'" "g u' = u" "g v' = v"
+             using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all
+        hence "{u'..v'} \<subseteq> {a..b}" "{u'..v'} \<subseteq> g -` {u..v}" by blast+
+        with u'v'(2) have "u' \<in> g -` {u..v}" "v' \<in> g -` {u..v}" by auto
+        from u'v'(1) have [simp]: "{a..b} \<inter> g -` {u..v} \<in> sets borel" by simp
+        
+        have A: "continuous_on {min u' v'..max u' v'} g'"
+            by (simp only: u'v' max_absorb2 min_absorb1) 
+               (intro continuous_on_subset[OF contg'], insert u'v', auto)
+        have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})"
+           using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF `{u'..v'} \<subseteq> {a..b}`]) auto
+        hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow> 
+                      (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" 
+            by (simp only: u'v' max_absorb2 min_absorb1) 
+               (auto simp: has_field_derivative_iff_has_vector_derivative)
+        have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
+          by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all
+        hence "(\<integral>\<^sup>+x. ereal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) = 
+                   LBINT x:{a..b} \<inter> g-`{u..v}. g' x" 
+          by (subst ereal_ind[symmetric], subst times_ereal.simps, subst nn_integral_eq_integral)
+             (auto intro: measurable_sets Mg simp: derivg_nonneg mult.commute split: split_indicator)
+        also from interval_integral_FTC_finite[OF A B]
+            have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u"
+                by (simp add: u'v' interval_integral_Icc `u \<le> v`)
+        finally have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) =
+                           ereal (v - u)" .
+      } note A = this
+  
+      have "(\<integral>\<^sup>+x. indicator {c..d} (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) =
+               (\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {c..d}) x \<partial>lborel)" 
+        by (intro nn_integral_cong) (simp split: split_indicator)
+      also have "{a..b} \<inter> g-`{c..d} = {a..b} \<inter> g-`{max (g a) c..min (g b) d}" 
+        using `a \<le> b` `c \<le> d`
+        by (auto intro!: monog intro: order.trans)
+      also have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ... x \<partial>lborel) =
+        (if max (g a) c \<le> min (g b) d then min (g b) d - max (g a) c else 0)"
+         using `c \<le> d` by (simp add: A)
+      also have "... = (\<integral>\<^sup>+ x. indicator ({g a..g b} \<inter> {c..d}) x \<partial>lborel)"
+        by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:)
+      also have "... = (\<integral>\<^sup>+ x. indicator {c..d} x * indicator {g a..g b} x \<partial>lborel)"
+        by (intro nn_integral_cong) (auto split: split_indicator)
+      finally show ?case ..
+
+      next
+
+      case (compl A)
+      note `A \<in> sets borel`[measurable]
+      from emeasure_mono[of "A \<inter> {g a..g b}" "{g a..g b}" lborel]
+          have [simp]: "emeasure lborel (A \<inter> {g a..g b}) \<noteq> \<infinity>" by auto
+      have [simp]: "g -` A \<inter> {a..b} \<in> sets borel"
+        by (rule set_borel_measurable_sets[OF Mg]) auto
+      have [simp]: "g -` (-A) \<inter> {a..b} \<in> sets borel"
+        by (rule set_borel_measurable_sets[OF Mg]) auto
+
+      have "(\<integral>\<^sup>+x. indicator (-A) x * indicator {g a..g b} x \<partial>lborel) = 
+                (\<integral>\<^sup>+x. indicator (-A \<inter> {g a..g b}) x \<partial>lborel)" 
+        by (rule nn_integral_cong) (simp split: split_indicator)
+      also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg
+        by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
+      also have "{g a..g b} - A = {g a..g b} - A \<inter> {g a..g b}" by blast
+      also have "emeasure lborel ... = g b - g a - emeasure lborel (A \<inter> {g a..g b})"
+             using `A \<in> sets borel` by (subst emeasure_Diff) (auto simp: real_of_ereal_minus)
+     also have "emeasure lborel (A \<inter> {g a..g b}) = 
+                    \<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel" 
+       using `A \<in> sets borel`
+       by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong)
+          (simp split: split_indicator)
+      also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
+        by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
+      also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
+        by (intro integral_FTC_atLeastAtMost[symmetric])
+           (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
+                 has_vector_derivative_at_within)
+      also have "ereal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
+        using borel_integrable_atLeastAtMost'[OF contg']
+        by (subst nn_integral_eq_integral)
+           (simp_all add: mult.commute derivg_nonneg split: split_indicator)
+      also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x))
+                            \<in> borel_measurable borel" using Mg'
+        by (intro borel_measurable_ereal_times borel_measurable_indicator)
+           (simp_all add: mult.commute)
+      have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<le>
+                        (\<integral>\<^sup>+x. ereal (g' x) * indicator {a..b} x \<partial>lborel)"
+         by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
+      note integrable = borel_integrable_atLeastAtMost'[OF contg']
+      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>"
+          by (auto simp: real_integrable_def nn_integral_set_ereal mult.commute)
+      have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I = 
+                  \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) - 
+                        indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel"
+        apply (intro nn_integral_diff[symmetric])
+        apply (insert Mg', simp add: mult.commute) []
+        apply (insert Mg'', simp) []
+        apply (simp split: split_indicator add: derivg_nonneg)
+        apply (rule notinf)
+        apply (simp split: split_indicator add: derivg_nonneg)
+        done
+      also have "... = \<integral>\<^sup>+ x. indicator (-A) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
+        by (intro nn_integral_cong) (simp split: split_indicator)
+      finally show ?case .
+
+    next
+      case (union f)
+      then have [simp]: "\<And>i. {a..b} \<inter> g -` f i \<in> sets borel"
+        by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto
+      have "g -` (\<Union>i. f i) \<inter> {a..b} = (\<Union>i. {a..b} \<inter> g -` f i)" by auto
+      hence "g -` (\<Union>i. f i) \<inter> {a..b} \<in> sets borel" by (auto simp del: UN_simps)
+
+      have "(\<integral>\<^sup>+x. indicator (\<Union>i. f i) x * indicator {g a..g b} x \<partial>lborel) = 
+                \<integral>\<^sup>+x. indicator (\<Union>i. {g a..g b} \<inter> f i) x \<partial>lborel"
+          by (intro nn_integral_cong) (simp split: split_indicator)
+      also from union have "... = emeasure lborel (\<Union>i. {g a..g b} \<inter> f i)" by simp
+      also from union have "... = (\<Sum>i. emeasure lborel ({g a..g b} \<inter> f i))"
+        by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def)
+      also from union have "... = (\<Sum>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel)" by simp
+      also have "(\<lambda>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel) = 
+                           (\<lambda>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel)"
+        by (intro ext nn_integral_cong) (simp split: split_indicator)
+      also from union.IH have "(\<Sum>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel) = 
+          (\<Sum>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" by simp
+      also have "(\<lambda>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) =
+                         (\<lambda>i. \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x \<partial>lborel)"
+        by (intro ext nn_integral_cong) (simp split: split_indicator)
+      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"
+        using Mg'
+        apply (intro nn_integral_suminf[symmetric])
+        apply (rule borel_measurable_ereal_times, simp add: borel_measurable_ereal mult.commute)
+        apply (rule borel_measurable_indicator, subst sets_lborel)
+        apply (simp_all split: split_indicator add: derivg_nonneg)
+        done
+      also have "(\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) =
+                      (\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x)"
+        by (intro ext) (simp split: split_indicator)
+      also have "(\<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x) \<partial>lborel) =
+                     \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * (\<Sum>i. indicator (g -` f i) x) \<partial>lborel"
+        by (intro nn_integral_cong suminf_cmult_ereal) (auto split: split_indicator simp: derivg_nonneg)
+      also from union have "(\<lambda>x. \<Sum>i. indicator (g -` f i) x :: ereal) = (\<lambda>x. indicator (\<Union>i. g -` f i) x)"
+        by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def)
+      also have "(\<integral>\<^sup>+x. ereal (g' x * indicator {a..b} x) * ... x \<partial>lborel) =
+                    (\<integral>\<^sup>+x. indicator (\<Union>i. f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
+       by (intro nn_integral_cong) (simp split: split_indicator)
+      finally show ?case .
+  qed
+
+next
+  case (mult f c)
+    note Mf[measurable] = `f \<in> borel_measurable borel`
+    let ?I = "indicator {a..b}"
+    have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
+      by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf])
+         (simp_all add: borel_measurable_ereal mult.commute)
+    also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)"
+      by (intro ext) (simp split: split_indicator)
+    finally have Mf': "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" .
+    with mult show ?case
+      by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac)
+ 
+next
+  case (add f2 f1)
+    let ?I = "indicator {a..b}"
+    {
+      fix f :: "real \<Rightarrow> ereal" assume Mf: "f \<in> borel_measurable borel"
+      have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
+        by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf])
+           (simp_all add: borel_measurable_ereal mult.commute)
+      also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)"
+        by (intro ext) (simp split: split_indicator)
+      finally have "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" .
+    } note Mf' = this[OF `f1 \<in> borel_measurable borel`] this[OF `f2 \<in> borel_measurable borel`]
+    from add have not_neginf: "\<And>x. f1 x \<noteq> -\<infinity>" "\<And>x. f2 x \<noteq> -\<infinity>" 
+      by (metis Infty_neq_0(1) ereal_0_le_uminus_iff ereal_infty_less_eq(1))+
+
+    have "(\<integral>\<^sup>+ x. (f1 x + f2 x) * indicator {g a..g b} x \<partial>lborel) =
+             (\<integral>\<^sup>+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x \<partial>lborel)"
+      by (intro nn_integral_cong) (simp split: split_indicator)
+    also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) +
+                                (\<integral>\<^sup>+ x. f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
+      by (simp_all add: nn_integral_add)
+    also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x + 
+                                      f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
+      by (intro nn_integral_add[symmetric])
+         (auto simp add: Mf' derivg_nonneg split: split_indicator)
+    also from not_neginf have "... = \<integral>\<^sup>+ x. (f1 (g x) + f2 (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
+      by (intro nn_integral_cong) (simp split: split_indicator add: ereal_distrib)
+    finally show ?case .
+
+next
+  case (sup F)
+  {
+    fix i
+    let ?I = "indicator {a..b}"
+    have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
+      by (rule_tac borel_measurable_ereal_times, rule_tac measurable_compose[OF _ sup.hyps(1)])
+         (simp_all add: mult.commute)
+    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)"
+      by (intro ext) (simp split: split_indicator)
+     finally have "... \<in> borel_measurable borel" .
+  } note Mf' = this
+
+    have "(\<integral>\<^sup>+x. (SUP i. F i x) * indicator {g a..g b} x \<partial>lborel) = 
+               \<integral>\<^sup>+x. (SUP i. F i x* indicator {g a..g b} x) \<partial>lborel"
+      by (intro nn_integral_cong) (simp split: split_indicator)
+    also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i x* indicator {g a..g b} x \<partial>lborel)"
+      by (intro nn_integral_monotone_convergence_SUP)
+         (auto simp: incseq_def le_fun_def split: split_indicator)
+    also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
+      by simp
+    also from sup have "... =  \<integral>\<^sup>+x. (SUP i. F i (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel"
+      by (intro nn_integral_monotone_convergence_SUP[symmetric])
+         (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
+               intro!: ereal_mult_right_mono)
+    also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
+      by (subst mult.assoc, subst mult.commute, subst SUP_ereal_cmult)
+         (auto split: split_indicator simp: derivg_nonneg mult_ac)
+    finally show ?case by simp
+  qed
+qed
+
+lemma nn_integral_substitution:
+  fixes f :: "real \<Rightarrow> real"
+  assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
+  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes contg': "continuous_on {a..b} g'" 
+  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes "a \<le> b"
+  shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
+             (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
+proof (cases "a = b")
+  assume "a \<noteq> b"
+  with `a \<le> b` have "a < b" by auto
+  let ?f' = "\<lambda>x. max 0 (f x * indicator {g a..g b} x)"
+
+  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"
+    by (rule deriv_nonneg_imp_mono) simp_all
+  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"
+    by (auto intro: monog)
+
+  from derivg_nonneg have nonneg: 
+    "\<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"
+    by (force simp: ereal_zero_le_0_iff field_simps)
+  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"
+    by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff)
+
+  have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
+            (\<integral>\<^sup>+x. ereal (?f' x) * indicator {g a..g b} x \<partial>lborel)"
+    by (subst nn_integral_max_0[symmetric], intro nn_integral_cong) 
+       (auto split: split_indicator simp: zero_ereal_def)
+  also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel" using Mf
+    by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg `a < b`]) 
+       (auto simp add: zero_ereal_def mult.commute)
+  also have "... = \<integral>\<^sup>+ x. max 0 (f (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
+    by (intro nn_integral_cong) 
+       (auto split: split_indicator simp: max_def dest: bounds)
+  also have "... = \<integral>\<^sup>+ x. max 0 (f (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel"
+    by (intro nn_integral_cong)
+       (auto simp: max_def derivg_nonneg split: split_indicator intro!: nonneg')
+  also have "... = \<integral>\<^sup>+ x. f (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
+    by (rule nn_integral_max_0)
+  also have "... = \<integral>\<^sup>+x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
+    by (intro nn_integral_cong) (simp split: split_indicator)
+  finally show ?thesis .
+qed auto
+
+lemma integral_substitution:
+  assumes integrable: "set_integrable lborel {g a..g b} f"
+  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes contg': "continuous_on {a..b} g'" 
+  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes "a \<le> b"
+  shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
+    and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
+proof-
+  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
+  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and 
+                             Mg': "set_borel_measurable borel {a..b} g'" 
+      by (simp_all only: set_measurable_continuous_on_ivl)
+  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"
+    by (rule deriv_nonneg_imp_mono) simp_all
+
+  have "(\<lambda>x. ereal (f x) * indicator {g a..g b} x) = 
+           (\<lambda>x. ereal (f x * indicator {g a..g b} x))" 
+    by (intro ext) (simp split: split_indicator)
+  with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel"
+    unfolding real_integrable_def by (force simp: mult.commute)
+  have "(\<lambda>x. ereal (-f x) * indicator {g a..g b} x) = 
+           (\<lambda>x. -ereal (f x * indicator {g a..g b} x))" 
+    by (intro ext) (simp split: split_indicator)
+  with integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
+    unfolding real_integrable_def by (force simp: mult.commute)
+
+  have "LBINT x. (f x :: real) * indicator {g a..g b} x = 
+          real (\<integral>\<^sup>+ x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) -
+          real (\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
+    by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ereal mult.commute)
+  also have "(\<integral>\<^sup>+x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) =
+               (\<integral>\<^sup>+x. ereal (f x * indicator {g a..g b} x) \<partial>lborel)"
+    by (intro nn_integral_cong) (simp split: split_indicator)
+  also with M1 have A: "(\<integral>\<^sup>+ x. ereal (f x * indicator {g a..g b} x) \<partial>lborel) =
+                            (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
+    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`]) 
+       (auto simp: nn_integral_set_ereal mult.commute)
+  also have "(\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
+               (\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
+    by (intro nn_integral_cong) (simp split: split_indicator)
+  also with M2 have B: "(\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
+                            (\<integral>\<^sup>+ x. ereal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
+    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`])
+       (auto simp: nn_integral_set_ereal mult.commute)
+
+  also {
+    from integrable have Mf: "set_borel_measurable borel {g a..g b} f" 
+      unfolding real_integrable_def by simp
+    from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg']
+      have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
+                     (g' x * indicator {a..b} x)) \<in> borel_measurable borel"  (is "?f \<in> _") 
+      by (simp add: mult.commute)
+    also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)"
+      using monog by (intro ext) (auto split: split_indicator)
+    finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
+      using A B integrable unfolding real_integrable_def 
+      by (simp_all add: nn_integral_set_ereal mult.commute)
+  } note integrable' = this
+
+  have "real (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) -
+                  real (\<integral>\<^sup>+ x. ereal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
+                (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable'
+    by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
+  finally show "(LBINT x. f x * indicator {g a..g b} x) = 
+                     (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
+qed
+
+lemma interval_integral_substitution:
+  assumes integrable: "set_integrable lborel {g a..g b} f"
+  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes contg': "continuous_on {a..b} g'" 
+  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes "a \<le> b"
+  shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
+    and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)"
+  apply (rule integral_substitution[OF assms], simp, simp)
+  apply (subst (1 2) interval_integral_Icc, fact)
+  apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
+  using integral_substitution(2)[OF assms]
+  apply (simp add: mult.commute)
+  done
+
+lemma set_borel_integrable_singleton[simp]:
+  "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
+  by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto
+
+end
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Thu Dec 04 21:28:35 2014 +0100
+++ b/src/HOL/Probability/Probability.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -1,3 +1,7 @@
+(*  Title:      HOL/Probability/Probability.thy
+    Author:     Johannes Hölzl, TU München
+*)
+
 theory Probability
 imports
   Discrete_Topology
@@ -7,6 +11,9 @@
   Distributions
   Probability_Mass_Function
   Stream_Space
+  Embed_Measure
+  Interval_Integral
+  Set_Integral
   Giry_Monad
 begin
 
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Dec 04 21:28:35 2014 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -385,7 +385,7 @@
     by (simp split: split_indicator)
   show "AE x in density (count_space UNIV) (ereal \<circ> f).
     measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
-    by (simp add: AE_density nonneg emeasure_density measure_def nn_integral_cmult_indicator)
+    by (simp add: AE_density nonneg measure_def emeasure_density max_def)
   show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
     by default (simp add: emeasure_density prob)
 qed simp
@@ -395,7 +395,7 @@
   have *[simp]: "\<And>x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y"
     by (simp split: split_indicator)
   fix x show "measure (density (count_space UNIV) (ereal \<circ> f)) {x} = f x"
-    by transfer (simp add: measure_def emeasure_density nn_integral_cmult_indicator nonneg)
+    by transfer (simp add: measure_def emeasure_density nonneg max_def)
 qed
 
 end
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Set_Integral.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Set_Integral.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -0,0 +1,597 @@
+(*  Title:      HOL/Probability/Set_Integral.thy
+    Author:     Jeremy Avigad, Johannes Hölzl, Luke Serafin
+
+Notation and useful facts for working with integrals over a set.
+
+TODO: keep all these? Need unicode translations as well.
+*)
+
+theory Set_Integral
+  imports Bochner_Integration Lebesgue_Measure
+begin
+
+(* 
+    Notation
+*)
+
+syntax
+"_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+("(3LINT _|_. _)" [0,110,60] 60)
+
+translations
+"LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
+
+abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
+
+abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
+
+abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
+
+syntax
+"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+("(4LINT _:_|_. _)" [0,60,110,61] 60)
+
+translations
+"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
+
+abbreviation
+  "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x"
+
+syntax
+  "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
+("AE _\<in>_ in _. _" [0,0,0,10] 10)
+
+translations
+  "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)"
+
+(*
+    Notation for integration wrt lebesgue measure on the reals:
+
+      LBINT x. f
+      LBINT x : A. f
+
+    TODO: keep all these? Need unicode.
+*)
+
+syntax
+"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
+("(2LBINT _. _)" [0,60] 60)
+
+translations
+"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
+
+syntax
+"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
+("(3LBINT _:_. _)" [0,60,61] 60)
+
+translations
+"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
+
+(* 
+    Basic properties 
+*)
+
+(*
+lemma indicator_abs_eq: "\<And>A x. abs (indicator A x) = ((indicator A x) :: real)"
+  by (auto simp add: indicator_def)
+*)
+
+lemma set_lebesgue_integral_cong:
+  assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
+  shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
+  using assms by (auto intro!: integral_cong split: split_indicator simp add: sets.sets_into_space)
+
+lemma set_lebesgue_integral_cong_AE:
+  assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  assumes "AE x \<in> A in M. f x = g x"
+  shows "LINT x:A|M. f x = LINT x:A|M. g x"
+proof-
+  have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
+    using assms by auto
+  thus ?thesis by (intro integral_cong_AE) auto
+qed
+
+lemma set_integrable_cong_AE:
+    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
+    AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow> 
+    set_integrable M A f = set_integrable M A g"
+  by (rule integrable_cong_AE) auto
+
+lemma set_integrable_subset: 
+  fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"  
+  shows "set_integrable M B f"
+proof -
+  have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
+    by (rule integrable_mult_indicator) fact+
+  with `B \<subseteq> A` show ?thesis
+    by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
+qed
+
+(* TODO: integral_cmul_indicator should be named set_integral_const *)
+(* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
+
+lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
+  by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)
+
+lemma set_integral_mult_right [simp]: 
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
+  by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)
+
+lemma set_integral_mult_left [simp]: 
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
+  by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
+
+lemma set_integral_divide_zero [simp]: 
+  fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}"
+  shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
+  by (subst integral_divide_zero[symmetric], intro integral_cong)
+     (auto split: split_indicator)
+
+lemma set_integrable_scaleR_right [simp, intro]:
+  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
+  unfolding scaleR_left_commute by (rule integrable_scaleR_right)
+
+lemma set_integrable_scaleR_left [simp, intro]:
+  fixes a :: "_ :: {banach, second_countable_topology}"
+  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
+  using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
+
+lemma set_integrable_mult_right [simp, intro]:
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
+  using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
+
+lemma set_integrable_mult_left [simp, intro]:
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
+  using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
+
+lemma set_integrable_divide [simp, intro]:
+  fixes a :: "'a::{real_normed_field, field_inverse_zero, second_countable_topology}"
+  assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
+  shows "set_integrable M A (\<lambda>t. f t / a)"
+proof -
+  have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
+    using assms by (rule integrable_divide_zero)
+  also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
+    by (auto split: split_indicator)
+  finally show ?thesis .
+qed
+
+lemma set_integral_add [simp, intro]:
+  fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes "set_integrable M A f" "set_integrable M A g"
+  shows "set_integrable M A (\<lambda>x. f x + g x)"
+    and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
+  using assms by (simp_all add: scaleR_add_right)
+
+lemma set_integral_diff [simp, intro]:
+  assumes "set_integrable M A f" "set_integrable M A g"
+  shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
+    (LINT x:A|M. f x) - (LINT x:A|M. g x)"
+  using assms by (simp_all add: scaleR_diff_right)
+
+lemma set_integral_reflect:
+  fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
+  using assms
+  by (subst lborel_integral_real_affine[where c="-1" and t=0])
+     (auto intro!: integral_cong split: split_indicator)
+
+(* question: why do we have this for negation, but multiplication by a constant
+   requires an integrability assumption? *)
+lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
+  by (subst integral_minus[symmetric]) simp_all
+
+lemma set_integral_complex_of_real:
+  "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
+  by (subst integral_complex_of_real[symmetric])
+     (auto intro!: integral_cong split: split_indicator)
+
+lemma set_integral_mono:
+  fixes f g :: "_ \<Rightarrow> real"
+  assumes "set_integrable M A f" "set_integrable M A g"
+    "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
+  shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
+using assms by (auto intro: integral_mono split: split_indicator)
+
+lemma set_integral_mono_AE: 
+  fixes f g :: "_ \<Rightarrow> real"
+  assumes "set_integrable M A f" "set_integrable M A g"
+    "AE x \<in> A in M. f x \<le> g x"
+  shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
+using assms by (auto intro: integral_mono_AE split: split_indicator)
+
+lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
+  using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
+
+lemma set_integrable_abs_iff:
+  fixes f :: "_ \<Rightarrow> real"
+  shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f" 
+  by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
+
+lemma set_integrable_abs_iff':
+  fixes f :: "_ \<Rightarrow> real"
+  shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow> 
+    set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
+by (intro set_integrable_abs_iff) auto
+
+lemma set_integrable_discrete_difference:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes "countable X"
+  assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
+  shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
+proof (rule integrable_discrete_difference[where X=X])
+  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"
+    using diff by (auto split: split_indicator)
+qed fact+
+
+lemma set_integral_discrete_difference:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes "countable X"
+  assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
+  shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
+proof (rule integral_discrete_difference[where X=X])
+  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"
+    using diff by (auto split: split_indicator)
+qed fact+
+
+lemma set_integrable_Un:
+  fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes f_A: "set_integrable M A f" and f_B:  "set_integrable M B f"
+    and [measurable]: "A \<in> sets M" "B \<in> sets M"
+  shows "set_integrable M (A \<union> B) f"
+proof -
+  have "set_integrable M (A - B) f"
+    using f_A by (rule set_integrable_subset) auto
+  from integrable_add[OF this f_B] show ?thesis
+    by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
+qed
+
+lemma set_integrable_UN:
+  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
+    "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
+  shows "set_integrable M (\<Union>i\<in>I. A i) f"
+using assms by (induct I) (auto intro!: set_integrable_Un)
+
+lemma set_integral_Un:
+  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes "A \<inter> B = {}"
+  and "set_integrable M A f"
+  and "set_integrable M B f"
+  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
+      scaleR_add_left assms)
+
+lemma set_integral_cong_set:
+  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
+    and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
+  shows "LINT x:B|M. f x = LINT x:A|M. f x"
+proof (rule integral_cong_AE)
+  show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
+    using ae by (auto simp: subset_eq split: split_indicator)
+qed fact+
+
+lemma set_borel_measurable_subset:
+  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
+  shows "set_borel_measurable M B f"
+proof -
+  have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
+    by measurable
+  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)"
+    using `B \<subseteq> A` by (auto simp: fun_eq_iff split: split_indicator)
+  finally show ?thesis .
+qed
+
+lemma set_integral_Un_AE:
+  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"
+  and "set_integrable M A f"
+  and "set_integrable M B f"
+  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+proof -
+  have f: "set_integrable M (A \<union> B) f"
+    by (intro set_integrable_Un assms)
+  then have f': "set_borel_measurable M (A \<union> B) f"
+    by (rule borel_measurable_integrable)
+  have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
+  proof (rule set_integral_cong_set)  
+    show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
+      using ae by auto
+    show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
+      using f' by (rule set_borel_measurable_subset) auto
+  qed fact
+  also have "\<dots> = (LINT x:(A - A \<inter> B)|M. f x) + (LINT x:(B - A \<inter> B)|M. f x)"
+    by (auto intro!: set_integral_Un set_integrable_subset[OF f])
+  also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+    using ae
+    by (intro arg_cong2[where f="op+"] set_integral_cong_set)
+       (auto intro!: set_borel_measurable_subset[OF f'])
+  finally show ?thesis .
+qed
+
+lemma set_integral_finite_Union:
+  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes "finite I" "disjoint_family_on A I"
+    and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
+  shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
+  using assms
+  apply induct
+  apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
+by (subst set_integral_Un, auto intro: set_integrable_UN)
+
+(* TODO: find a better name? *)
+lemma pos_integrable_to_top:
+  fixes l::real
+  assumes "\<And>i. A i \<in> sets M" "mono A"
+  assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
+  and intgbl: "\<And>i::nat. set_integrable M (A i) f"
+  and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) ----> l"
+  shows "set_integrable M (\<Union>i. A i) f"
+  apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
+  apply (rule intgbl)
+  prefer 3 apply (rule lim)
+  apply (rule AE_I2)
+  using `mono A` apply (auto simp: mono_def nneg split: split_indicator) []
+proof (rule AE_I2)
+  { fix x assume "x \<in> space M"
+    show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Union>i. A i) x *\<^sub>R f x"
+    proof cases
+      assume "\<exists>i. x \<in> A i"
+      then guess i ..
+      then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
+        using `x \<in> A i` `mono A` by (auto simp: eventually_sequentially mono_def)
+      show ?thesis
+        apply (intro Lim_eventually)
+        using *
+        apply eventually_elim
+        apply (auto split: split_indicator)
+        done
+    qed auto }
+  then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
+    apply (rule borel_measurable_LIMSEQ)
+    apply assumption
+    apply (intro borel_measurable_integrable intgbl)
+    done
+qed
+
+(* Proof from Royden Real Analysis, p. 91. *)
+lemma lebesgue_integral_countable_add:
+  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
+    and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
+    and intgbl: "set_integrable M (\<Union>i. A i) f"
+  shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
+proof (subst integral_suminf[symmetric])
+  show int_A: "\<And>i. set_integrable M (A i) f"
+    using intgbl by (rule set_integrable_subset) auto
+  { fix x assume "x \<in> space M"
+    have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
+      by (intro sums_scaleR_left indicator_sums) fact }
+  note sums = this
+
+  have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
+    using int_A[THEN integrable_norm] by auto
+
+  show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
+    using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
+
+  show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
+  proof (rule summableI_nonneg_bounded)
+    fix n
+    show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
+      using norm_f by (auto intro!: integral_nonneg_AE)
+    
+    have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
+      (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
+      by (simp add: abs_mult)
+    also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
+      using norm_f
+      by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
+    also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
+      using intgbl[THEN integrable_norm]
+      by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
+         (auto split: split_indicator)
+    finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
+      set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
+      by simp
+  qed
+  show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
+    apply (rule integral_cong[OF refl])
+    apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
+    using sums_unique[OF indicator_sums[OF disj]]
+    apply auto
+    done
+qed
+
+lemma set_integral_cont_up:
+  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
+  and intgbl: "set_integrable M (\<Union>i. A i) f"
+  shows "(\<lambda>i. LINT x:(A i)|M. f x) ----> LINT x:(\<Union>i. A i)|M. f x"
+proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
+  have int_A: "\<And>i. set_integrable M (A i) f"
+    using intgbl by (rule set_integrable_subset) auto
+  then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
+    "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
+    using intgbl integrable_norm[OF intgbl] by auto
+  
+  { fix x i assume "x \<in> A i"
+    with A have "(\<lambda>xa. indicator (A xa) x::real) ----> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) ----> 1"
+      by (intro filterlim_cong refl)
+         (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
+  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"
+    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
+qed (auto split: split_indicator)
+        
+(* Can the int0 hypothesis be dropped? *)
+lemma set_integral_cont_down:
+  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
+  and int0: "set_integrable M (A 0) f"
+  shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) ----> LINT x:(\<Inter>i. A i)|M. f x"
+proof (rule integral_dominated_convergence)
+  have int_A: "\<And>i. set_integrable M (A i) f"
+    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
+  show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
+    using int0[THEN integrable_norm] by simp
+  have "set_integrable M (\<Inter>i. A i) f"
+    using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
+  with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
+    by auto
+  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)"
+    using A by (auto split: split_indicator simp: decseq_def)
+  { fix x i assume "x \<in> space M" "x \<notin> A i"
+    with A have "(\<lambda>i. indicator (A i) x::real) ----> 0 \<longleftrightarrow> (\<lambda>i. 0::real) ----> 0"
+      by (intro filterlim_cong refl)
+         (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) }
+  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"
+    by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
+qed
+
+lemma set_integral_at_point:
+  fixes a :: real
+  assumes "set_integrable M {a} f"
+  and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
+  shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
+proof-
+  have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
+    by (intro set_lebesgue_integral_cong) simp_all
+  then show ?thesis using assms by simp
+qed
+
+
+abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
+  "complex_integrable M f \<equiv> integrable M f"
+
+abbreviation complex_lebesgue_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" ("integral\<^sup>C") where
+  "integral\<^sup>C M f == integral\<^sup>L M f"
+
+syntax
+  "_complex_lebesgue_integral" :: "pttrn \<Rightarrow> complex \<Rightarrow> 'a measure \<Rightarrow> complex"
+ ("\<integral>\<^sup>C _. _ \<partial>_" [60,61] 110)
+
+translations
+  "\<integral>\<^sup>Cx. f \<partial>M" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
+
+syntax
+  "_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+  ("(3CLINT _|_. _)" [0,110,60] 60)
+
+translations
+  "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\<lambda>x. f)"
+
+lemma complex_integrable_cnj [simp]:
+  "complex_integrable M (\<lambda>x. cnj (f x)) \<longleftrightarrow> complex_integrable M f"
+proof
+  assume "complex_integrable M (\<lambda>x. cnj (f x))"
+  then have "complex_integrable M (\<lambda>x. cnj (cnj (f x)))"
+    by (rule integrable_cnj)
+  then show "complex_integrable M f"
+    by simp
+qed simp
+
+lemma complex_of_real_integrable_eq:
+  "complex_integrable M (\<lambda>x. complex_of_real (f x)) \<longleftrightarrow> integrable M f"
+proof
+  assume "complex_integrable M (\<lambda>x. complex_of_real (f x))"
+  then have "integrable M (\<lambda>x. Re (complex_of_real (f x)))"
+    by (rule integrable_Re)
+  then show "integrable M f"
+    by simp
+qed simp
+
+
+abbreviation complex_set_integrable :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
+  "complex_set_integrable M A f \<equiv> set_integrable M A f"
+
+abbreviation complex_set_lebesgue_integral :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> complex" where
+  "complex_set_lebesgue_integral M A f \<equiv> set_lebesgue_integral M A f"
+
+syntax
+"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+("(4CLINT _:_|_. _)" [0,60,110,61] 60)
+
+translations
+"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
+
+(*
+lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = abs a * cmod x"
+  apply (simp add: norm_mult)
+  by (subst norm_mult, auto)
+*)
+
+lemma borel_integrable_atLeastAtMost':
+  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  assumes f: "continuous_on {a..b} f"
+  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
+  by (intro borel_integrable_compact compact_Icc f)
+
+lemma integral_FTC_atLeastAtMost:
+  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
+  assumes "a \<le> b"
+    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+    and f: "continuous_on {a .. b} f"
+  shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
+proof -
+  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
+  have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
+    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
+  moreover
+  have "(f has_integral F b - F a) {a .. b}"
+    by (intro fundamental_theorem_of_calculus ballI assms) auto
+  then have "(?f has_integral F b - F a) {a .. b}"
+    by (subst has_integral_eq_eq[where g=f]) auto
+  then have "(?f has_integral F b - F a) UNIV"
+    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
+  ultimately show "integral\<^sup>L lborel ?f = F b - F a"
+    by (rule has_integral_unique)
+qed
+
+lemma set_borel_integral_eq_integral:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "set_integrable lborel S f"
+  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
+proof -
+  let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
+  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
+    by (rule has_integral_integral_lborel) fact
+  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
+    apply (subst has_integral_restrict_univ [symmetric])
+    apply (rule has_integral_eq)
+    by auto
+  thus "f integrable_on S"
+    by (auto simp add: integrable_on_def)
+  with 1 have "(f has_integral (integral S f)) S"
+    by (intro integrable_integral, auto simp add: integrable_on_def)
+  thus "LINT x : S | lborel. f x = integral S f"
+    by (intro has_integral_unique [OF 1])
+qed
+
+lemma set_borel_measurable_continuous:
+  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
+  assumes "S \<in> sets borel" "continuous_on S f"
+  shows "set_borel_measurable borel S f"
+proof -
+  have "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable borel"
+    by (intro assms borel_measurable_continuous_on_if continuous_on_const)
+  also have "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. indicator S x *\<^sub>R f x)"
+    by auto
+  finally show ?thesis .
+qed
+
+lemma set_measurable_continuous_on_ivl:
+  assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
+  shows "set_borel_measurable borel {a..b} f"
+  by (rule set_borel_measurable_continuous[OF _ assms]) simp
+
+end
+
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Dec 04 21:28:35 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -2328,9 +2328,16 @@
   using sigma_sets_vimage_commute[of f X "space M" "sets M"]
   unfolding sets_vimage_algebra sets.sigma_sets_eq by simp
 
-lemma vimage_algebra_cong: "sets M = sets N \<Longrightarrow> sets (vimage_algebra X f M) = sets (vimage_algebra X f N)"
+lemma sets_vimage_algebra_cong: "sets M = sets N \<Longrightarrow> sets (vimage_algebra X f M) = sets (vimage_algebra X f N)"
   by (simp add: sets_vimage_algebra)
 
+lemma vimage_algebra_cong:
+  assumes "X = Y"
+  assumes "\<And>x. x \<in> Y \<Longrightarrow> f x = g x"
+  assumes "sets M = sets N"
+  shows "vimage_algebra X f M = vimage_algebra Y g N"
+  by (auto simp: vimage_algebra_def assms intro!: arg_cong2[where f=sigma])
+
 lemma in_vimage_algebra: "A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets (vimage_algebra X f M)"
   by (auto simp: vimage_algebra_def)
 
@@ -2397,6 +2404,14 @@
     by (auto intro!: sets_image_in_sets sets_Sup_in_sets del: subsetI simp: *)
 qed
 
+lemma vimage_algebra_Sup_sigma:
+  assumes [simp]: "MM \<noteq> {}" and "\<And>M. M \<in> MM \<Longrightarrow> f \<in> X \<rightarrow> space M"
+  shows "vimage_algebra X f (Sup_sigma MM) = Sup_sigma (vimage_algebra X f ` MM)"
+proof (rule measure_eqI)
+  show "sets (vimage_algebra X f (Sup_sigma MM)) = sets (Sup_sigma (vimage_algebra X f ` MM))"
+    using assms by (rule sets_vimage_Sup_eq)
+qed (simp add: vimage_algebra_def Sup_sigma_def emeasure_sigma)
+
 subsubsection {* Restricted Space Sigma Algebra *}
 
 definition restrict_space where
diff -r 4c8205fe3644 -r d469103c0737 src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Thu Dec 04 21:28:35 2014 +0100
+++ b/src/HOL/Probability/Stream_Space.thy	Fri Dec 05 12:06:18 2014 +0100
@@ -288,14 +288,14 @@
   using  S[THEN sets.sets_into_space]
   apply (subst restrict_space_eq_vimage_algebra)
   apply (simp add: space_stream_space streams_mono2)
-  apply (subst vimage_algebra_cong[OF sets_stream_space_eq])
+  apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq])
   apply (subst sets_stream_space_eq)
   apply (subst sets_vimage_Sup_eq)
   apply simp
   apply (auto intro: streams_mono) []
   apply (simp add: image_image space_restrict_space)
   apply (intro SUP_sigma_cong)
-  apply (simp add: vimage_algebra_cong[OF restrict_space_eq_vimage_algebra])
+  apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra])
   apply (subst (1 2) vimage_algebra_vimage_algebra_eq)
   apply (auto simp: streams_mono snth_in)
   done
@@ -326,6 +326,23 @@
   finally show ?case .
 qed (simp add: streams_sets)
 
+lemma sigma_sets_singletons:
+  assumes "countable S"
+  shows "sigma_sets S ((\<lambda>s. {s})`S) = Pow S"
+proof safe
+  interpret sigma_algebra S "sigma_sets S ((\<lambda>s. {s})`S)"
+    by (rule sigma_algebra_sigma_sets) auto
+  fix A assume "A \<subseteq> S"
+  with assms have "(\<Union>a\<in>A. {a}) \<in> sigma_sets S ((\<lambda>s. {s})`S)"
+    by (intro countable_UN') (auto dest: countable_subset)
+  then show "A \<in> sigma_sets S ((\<lambda>s. {s})`S)"
+    by simp
+qed (auto dest: sigma_sets_into_sp[rotated])
+
+lemma sets_count_space_eq_sigma:
+  "countable S \<Longrightarrow> sets (count_space S) = sets (sigma S ((\<lambda>s. {s})`S))"
+  by (subst sets_measure_of) (auto simp: sigma_sets_singletons)
+
 lemma sets_stream_space_sstart:
   assumes S[simp]: "countable S"
   shows "sets (stream_space (count_space S)) = sets (sigma (streams S) (sstart S`lists S \<union> {{}}))"
@@ -402,11 +419,8 @@
 
   { fix M :: "'a stream measure" assume M: "sets M = sets (stream_space (count_space UNIV))"
     have "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
-      apply (simp add: sets_eq_imp_space_eq[OF M] space_stream_space restrict_space_eq_vimage_algebra
-        vimage_algebra_cong[OF M])
-      apply (simp add: sets_eq_imp_space_eq[OF M] space_stream_space restrict_space_eq_vimage_algebra[symmetric])
-      apply (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart)
-      done }
+      by (subst sets_restrict_space_cong[OF M])
+         (simp add: sets_restrict_stream_space restrict_count_space sets_stream_space_sstart) }
   from this[OF sets_M] this[OF sets_N]
   show "sets (restrict_space M (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"
        "sets (restrict_space N (streams S)) = sigma_sets (streams S) (sstart S ` lists S \<union> {{}})"