add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
--- 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.
--- /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
--- 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
--- /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
--- /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
--- 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
--- 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
--- /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
+
--- 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
--- 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> {{}})"