move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
--- a/src/HOL/Analysis/Bochner_Integration.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Fri Sep 16 13:56:51 2016 +0200
@@ -187,7 +187,7 @@
using U by (auto
intro: borel_measurable_simple_function
intro!: borel_measurable_enn2real borel_measurable_times
- simp: U'_def zero_le_mult_iff enn2real_nonneg)
+ simp: U'_def zero_le_mult_iff)
show "incseq U'"
using U(2,3)
by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def enn2real_mono)
@@ -212,7 +212,7 @@
ultimately have U': "(\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z) = U' i"
by (simp add: U'_def fun_eq_iff)
have "\<And>x. x \<in> U' i ` space M \<Longrightarrow> 0 \<le> x"
- by (auto simp: U'_def enn2real_nonneg)
+ by (auto simp: U'_def)
with fin have "P (\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z)"
proof induct
case empty from set[of "{}"] show ?case
@@ -866,7 +866,7 @@
simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
by (simp add: simple_bochner_integrable.simps space_restrict_space
simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
- indicator_eq_0_iff conj_ac)
+ indicator_eq_0_iff conj_left_commute)
lemma simple_bochner_integral_restrict_space:
fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
@@ -1624,7 +1624,7 @@
with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
by auto
qed
- qed (auto simp: measure_nonneg integrable_mult_left_iff)
+ qed (auto simp: integrable_mult_left_iff)
also have "\<dots> = integral\<^sup>L M f"
using nonneg by (auto intro!: integral_cong_AE)
finally show ?thesis .
@@ -2466,10 +2466,10 @@
shows "ennreal (\<integral>x. enn2real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
proof (subst nn_integral_eq_integral[symmetric])
show "integrable M (\<lambda>x. enn2real (f x))"
- using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI enn2real_nonneg)
+ using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI)
show "(\<integral>\<^sup>+ x. ennreal (enn2real (f x)) \<partial>M) = integral\<^sup>N M f"
using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top])
-qed (auto simp: enn2real_nonneg)
+qed auto
lemma (in finite_measure) integral_less_AE:
fixes X Y :: "'a \<Rightarrow> real"
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Fri Sep 16 13:56:51 2016 +0200
@@ -1,7 +1,7 @@
section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
theory Cartesian_Euclidean_Space
-imports Finite_Cartesian_Product Henstock_Kurzweil_Integration
+imports Finite_Cartesian_Product Derivative (* Henstock_Kurzweil_Integration *)
begin
lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
@@ -927,7 +927,6 @@
unfolding dot_matrix_product transpose_columnvector[symmetric]
dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
-
lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\<bar>x$i\<bar> |i. i\<in>UNIV}"
by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right)
@@ -1409,12 +1408,6 @@
apply (rule bounded_linearI[where K=1])
using component_le_norm_cart[of _ k] unfolding real_norm_def by auto
-lemma integral_component_eq_cart[simp]:
- fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
- assumes "f integrable_on s"
- shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
- using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
-
lemma interval_split_cart:
"{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
"cbox a b \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Fri Sep 16 13:56:51 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Complex Analysis Basics\<close>
theory Complex_Analysis_Basics
-imports Cartesian_Euclidean_Space "~~/src/HOL/Library/Nonpos_Ints"
+imports Henstock_Kurzweil_Integration "~~/src/HOL/Library/Nonpos_Ints"
begin
--- a/src/HOL/Analysis/Derivative.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy Fri Sep 16 13:56:51 2016 +0200
@@ -9,6 +9,9 @@
imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
begin
+lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
+ by (rule bounded_linear_inner_left)
+
lemma onorm_inner_left:
assumes "bounded_linear r"
shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
@@ -2906,5 +2909,4 @@
by eventually_elim (auto simp: dist_norm field_simps)
qed (auto intro!: bounded_linear_intros simp: split_beta')
-
end
--- a/src/HOL/Analysis/Embed_Measure.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Embed_Measure.thy Fri Sep 16 13:56:51 2016 +0200
@@ -47,7 +47,7 @@
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
+ by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 Setcompr_eq_image
dest: sets.sets_into_space
intro!: image_cong the_inv_into_vimage[symmetric])
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 16 13:56:51 2016 +0200
@@ -0,0 +1,606 @@
+theory Equivalence_Lebesgue_Henstock_Integration
+ imports Lebesgue_Measure Henstock_Kurzweil_Integration
+begin
+
+subsection \<open>Equivalence Lebesgue integral on @{const lborel} and HK-integral\<close>
+
+lemma has_integral_measure_lborel:
+ fixes A :: "'a::euclidean_space set"
+ assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>"
+ shows "((\<lambda>x. 1) has_integral measure lborel A) A"
+proof -
+ { fix l u :: 'a
+ have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box l u)"
+ proof cases
+ assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
+ then show ?thesis
+ apply simp
+ apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
+ apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
+ using has_integral_const[of "1::real" l u]
+ apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
+ done
+ next
+ assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
+ then have "box l u = {}"
+ unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le)
+ then show ?thesis
+ by simp
+ qed }
+ note has_integral_box = this
+
+ { fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box a b)"
+ have "Int_stable (range (\<lambda>(a, b). box a b))"
+ by (auto simp: Int_stable_def box_Int_box)
+ moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV"
+ by auto
+ moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box a b))"
+ using A unfolding borel_eq_box by simp
+ ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box a b)"
+ proof (induction rule: sigma_sets_induct_disjoint)
+ case (basic A) then show ?case
+ by (auto simp: box_Int_box has_integral_box)
+ next
+ case empty then show ?case
+ by simp
+ next
+ case (compl A)
+ then have [measurable]: "A \<in> sets borel"
+ by (simp add: borel_eq_box)
+
+ have "((\<lambda>x. 1) has_integral ?M (box a b)) (box a b)"
+ by (simp add: has_integral_box)
+ moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
+ by (subst has_integral_restrict) (auto intro: compl)
+ ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
+ by (rule has_integral_sub)
+ then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
+ by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
+ then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
+ by (subst (asm) has_integral_restrict) auto
+ also have "?M (box a b) - ?M A = ?M (UNIV - A)"
+ by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2)
+ finally show ?case .
+ next
+ case (union F)
+ then have [measurable]: "\<And>i. F i \<in> sets borel"
+ by (simp add: borel_eq_box subset_eq)
+ have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
+ proof (rule has_integral_monotone_convergence_increasing)
+ let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
+ show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
+ using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff)
+ show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
+ by (intro setsum_mono2) auto
+ from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
+ by (auto simp add: disjoint_family_on_def)
+ show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
+ apply (auto simp: * setsum.If_cases Iio_Int_singleton)
+ apply (rule_tac k="Suc xa" in LIMSEQ_offset)
+ apply simp
+ done
+ have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
+ by (intro emeasure_mono) auto
+
+ with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
+ unfolding sums_def[symmetric] UN_extend_simps
+ by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique)
+ qed
+ then show ?case
+ by (subst (asm) has_integral_restrict) auto
+ qed }
+ note * = this
+
+ show ?thesis
+ proof (rule has_integral_monotone_convergence_increasing)
+ let ?B = "\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set"
+ let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real"
+ let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)"
+
+ show "\<And>n::nat. (?f n has_integral ?M n) A"
+ using * by (subst has_integral_restrict) simp_all
+ show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
+ by (auto simp: box_def)
+ { fix x assume "x \<in> A"
+ moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x"
+ by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
+ ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1"
+ by (simp add: indicator_def UN_box_eq_UNIV) }
+
+ have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
+ by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
+ also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))"
+ proof (intro ext emeasure_eq_ennreal_measure)
+ fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)"
+ by (intro emeasure_mono) auto
+ then show "emeasure lborel (A \<inter> ?B n) \<noteq> top"
+ by (auto simp: top_unique)
+ qed
+ finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A"
+ using emeasure_eq_ennreal_measure[of lborel A] finite
+ by (simp add: UN_box_eq_UNIV less_top)
+ qed
+qed
+
+lemma nn_integral_has_integral:
+ fixes f::"'a::euclidean_space \<Rightarrow> real"
+ assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
+ shows "(f has_integral r) UNIV"
+using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
+ case (set A)
+ then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+ by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
+ with set show ?case
+ by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
+next
+ case (mult g c)
+ then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r"
+ by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult)
+ with \<open>0 \<le> r\<close> \<open>0 \<le> c\<close>
+ obtain r' where "(c = 0 \<and> r = 0) \<or> (0 \<le> r' \<and> (\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel) = ennreal r' \<and> r = c * r')"
+ by (cases "\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel" rule: ennreal_cases)
+ (auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric])
+ with mult show ?case
+ by (auto intro!: has_integral_cmult_real)
+next
+ case (add g h)
+ then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
+ by (simp add: nn_integral_add)
+ with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
+ by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
+ (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
+ with add show ?case
+ by (auto intro!: has_integral_add)
+next
+ case (seq U)
+ note seq(1)[measurable] and f[measurable]
+
+ { fix i x
+ have "U i x \<le> f x"
+ using seq(5)
+ apply (rule LIMSEQ_le_const)
+ using seq(4)
+ apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
+ done }
+ note U_le_f = this
+
+ { fix i
+ have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
+ using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp
+ then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p" "p \<le> r" "0 \<le> p"
+ using seq(6) \<open>0\<le>r\<close> by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel" rule: ennreal_cases) (auto simp: top_unique)
+ moreover note seq
+ ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
+ by auto }
+ then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ennreal (U i x) \<partial>lborel) = ennreal (p i)"
+ and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i"
+ and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis
+
+ have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique)
+
+ have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
+ proof (rule monotone_convergence_increasing)
+ show "\<forall>k. U k integrable_on UNIV" using U_int by auto
+ show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
+ then show "bounded {integral UNIV (U k) |k. True}"
+ using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
+ show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
+ using seq by auto
+ qed
+ moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"
+ using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
+ ultimately have "integral UNIV f = r"
+ by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique)
+ with * show ?case
+ by (simp add: has_integral_integral)
+qed
+
+lemma nn_integral_lborel_eq_integral:
+ fixes f::"'a::euclidean_space \<Rightarrow> real"
+ assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
+ shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f"
+proof -
+ from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
+ by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
+ then show ?thesis
+ using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique)
+qed
+
+lemma nn_integral_integrable_on:
+ fixes f::"'a::euclidean_space \<Rightarrow> real"
+ assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
+ shows "f integrable_on UNIV"
+proof -
+ from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
+ by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
+ then show ?thesis
+ by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
+qed
+
+lemma nn_integral_has_integral_lborel:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
+ assumes I: "(f has_integral I) UNIV"
+ shows "integral\<^sup>N lborel f = I"
+proof -
+ from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
+ from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
+ let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"
+
+ note F(1)[THEN borel_measurable_simple_function, measurable]
+
+ have "0 \<le> I"
+ using I by (rule has_integral_nonneg) (simp add: nonneg)
+
+ have F_le_f: "enn2real (F i x) \<le> f x" for i x
+ using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "\<lambda>i. F i x"]
+ by (cases "F i x" rule: ennreal_cases) auto
+ let ?F = "\<lambda>i x. F i x * indicator (?B i) x"
+ have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))"
+ proof (subst nn_integral_monotone_convergence_SUP[symmetric])
+ { fix x
+ obtain j where j: "x \<in> ?B j"
+ using UN_box_eq_UNIV by auto
+
+ have "ennreal (f x) = (SUP i. F i x)"
+ using F(4)[of x] nonneg[of x] by (simp add: max_def)
+ also have "\<dots> = (SUP i. ?F i x)"
+ proof (rule SUP_eq)
+ fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x"
+ using j F(2)
+ by (intro bexI[of _ "max i j"])
+ (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def)
+ qed (auto intro!: F split: split_indicator)
+ finally have "ennreal (f x) = (SUP i. ?F i x)" . }
+ then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>lborel)"
+ by simp
+ qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator)
+ also have "\<dots> \<le> ennreal I"
+ proof (rule SUP_least)
+ fix i :: nat
+ have finite_F: "(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>"
+ proof (rule nn_integral_bound_simple_function)
+ have "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} \<le>
+ emeasure lborel (?B i)"
+ by (intro emeasure_mono) (auto split: split_indicator)
+ then show "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"
+ by (auto simp: less_top[symmetric] top_unique)
+ qed (auto split: split_indicator
+ intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal)
+
+ have int_F: "(\<lambda>x. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV"
+ using F(4) finite_F
+ by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg)
+
+ have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) =
+ (\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel)"
+ using F(3,4)
+ by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator)
+ also have "\<dots> = ennreal (integral UNIV (\<lambda>x. enn2real (F i x) * indicator (?B i) x))"
+ using F
+ by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F])
+ (auto split: split_indicator intro: enn2real_nonneg)
+ also have "\<dots> \<le> ennreal I"
+ by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f
+ simp: \<open>0 \<le> I\<close> split: split_indicator )
+ finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ennreal I" .
+ qed
+ finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) < \<infinity>"
+ by (auto simp: less_top[symmetric] top_unique)
+ from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis
+ by (simp add: integral_unique)
+qed
+
+lemma has_integral_iff_emeasure_lborel:
+ fixes A :: "'a::euclidean_space set"
+ assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
+ shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
+proof (cases "emeasure lborel A = \<infinity>")
+ case emeasure_A: True
+ have "\<not> (\<lambda>x. 1::real) integrable_on A"
+ proof
+ assume int: "(\<lambda>x. 1::real) integrable_on A"
+ then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
+ unfolding indicator_def[abs_def] integrable_restrict_univ .
+ then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
+ by auto
+ from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
+ by (simp add: ennreal_indicator)
+ qed
+ with emeasure_A show ?thesis
+ by auto
+next
+ case False
+ then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+ by (simp add: has_integral_measure_lborel less_top)
+ with False show ?thesis
+ by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
+qed
+
+lemma has_integral_integral_real:
+ fixes f::"'a::euclidean_space \<Rightarrow> real"
+ assumes f: "integrable lborel f"
+ shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
+using f proof induct
+ case (base A c) then show ?case
+ by (auto intro!: has_integral_mult_left simp: )
+ (simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel)
+next
+ case (add f g) then show ?case
+ by (auto intro!: has_integral_add)
+next
+ case (lim f s)
+ show ?case
+ proof (rule has_integral_dominated_convergence)
+ show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact
+ show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV"
+ using \<open>integrable lborel f\<close>
+ by (intro nn_integral_integrable_on)
+ (auto simp: integrable_iff_bounded abs_mult nn_integral_cmult ennreal_mult ennreal_mult_less_top)
+ show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
+ using lim by (auto simp add: abs_mult)
+ show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x"
+ using lim by auto
+ show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f"
+ using lim lim(1)[THEN borel_measurable_integrable]
+ by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
+ qed
+qed
+
+context
+ fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+begin
+
+lemma has_integral_integral_lborel:
+ assumes f: "integrable lborel f"
+ shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
+proof -
+ have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV"
+ using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto
+ also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f"
+ by (simp add: fun_eq_iff euclidean_representation)
+ also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f"
+ using f by (subst (2) eq_f[symmetric]) simp
+ finally show ?thesis .
+qed
+
+lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV"
+ using has_integral_integral_lborel by auto
+
+lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)"
+ using has_integral_integral_lborel by auto
+
+end
+
+subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
+
+text \<open>
+
+For the positive integral we replace continuity with Borel-measurability.
+
+\<close>
+
+lemma
+ fixes f :: "real \<Rightarrow> real"
+ assumes [measurable]: "f \<in> borel_measurable borel"
+ assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"
+ shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn)
+ and has_bochner_integral_FTC_Icc_nonneg:
+ "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
+ and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
+ and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int)
+proof -
+ have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x"
+ using f(2) by (auto split: split_indicator)
+
+ have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b\<Longrightarrow> F x \<le> F y" for x y
+ using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
+
+ have "(f has_integral F b - F a) {a..b}"
+ by (intro fundamental_theorem_of_calculus)
+ (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
+ intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
+ then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
+ unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a]
+ by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
+ then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
+ by (rule nn_integral_has_integral_lborel[OF *])
+ then show ?has
+ by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono \<open>a \<le> b\<close>)
+ then show ?eq ?int
+ unfolding has_bochner_integral_iff by auto
+ show ?nn
+ by (subst nn[symmetric])
+ (auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator)
+qed
+
+lemma
+ fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
+ assumes "a \<le> b"
+ assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+ assumes cont: "continuous_on {a .. b} f"
+ shows has_bochner_integral_FTC_Icc:
+ "has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has)
+ and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq)
+proof -
+ let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
+ have int: "integrable lborel ?f"
+ using borel_integrable_compact[OF _ cont] by auto
+ have "(f has_integral F b - F a) {a..b}"
+ using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
+ moreover
+ have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
+ using has_integral_integral_lborel[OF int]
+ unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
+ by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
+ ultimately show ?eq
+ by (auto dest: has_integral_unique)
+ then show ?has
+ using int by (auto simp: has_bochner_integral_iff)
+qed
+
+lemma
+ fixes f :: "real \<Rightarrow> real"
+ assumes "a \<le> b"
+ assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
+ assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+ shows has_bochner_integral_FTC_Icc_real:
+ "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
+ and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
+proof -
+ have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+ unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+ using deriv by (auto intro: DERIV_subset)
+ have 2: "continuous_on {a .. b} f"
+ using cont by (intro continuous_at_imp_continuous_on) auto
+ show ?has ?eq
+ using has_bochner_integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2]
+ by (auto simp: mult.commute)
+qed
+
+lemma nn_integral_FTC_atLeast:
+ fixes f :: "real \<Rightarrow> real"
+ assumes f_borel: "f \<in> borel_measurable borel"
+ assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
+ assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
+ assumes lim: "(F \<longlongrightarrow> T) at_top"
+ shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
+proof -
+ let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x"
+ let ?fR = "\<lambda>x. ennreal (f x) * indicator {a ..} x"
+
+ have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
+ using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
+ then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
+ by (intro tendsto_le_const[OF _ lim])
+ (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
+
+ have "(SUP i::nat. ?f i x) = ?fR x" for x
+ proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
+ from reals_Archimedean2[of "x - a"] guess n ..
+ then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
+ by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
+ then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
+ by (rule Lim_eventually)
+ qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
+ then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
+ by simp
+ also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
+ proof (rule nn_integral_monotone_convergence_SUP)
+ show "incseq ?f"
+ using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
+ show "\<And>i. (?f i) \<in> borel_measurable lborel"
+ using f_borel by auto
+ qed
+ also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))"
+ by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
+ also have "\<dots> = T - F a"
+ proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
+ have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
+ apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
+ apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
+ apply (rule filterlim_real_sequentially)
+ done
+ then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
+ by (simp add: F_mono F_le_T tendsto_diff)
+ qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
+ finally show ?thesis .
+qed
+
+lemma integral_power:
+ "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
+proof (subst integral_FTC_Icc_real)
+ fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
+ by (intro derivative_eq_intros) auto
+qed (auto simp: field_simps simp del: of_nat_Suc)
+
+subsection \<open>Integration by parts\<close>
+
+lemma integral_by_parts_integrable:
+ fixes f g F G::"real \<Rightarrow> real"
+ assumes "a \<le> b"
+ assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+ assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+ assumes [intro]: "!!x. DERIV F x :> f x"
+ assumes [intro]: "!!x. DERIV G x :> g x"
+ shows "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
+ by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)
+
+lemma integral_by_parts:
+ fixes f g F G::"real \<Rightarrow> real"
+ assumes [arith]: "a \<le> b"
+ assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+ assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+ assumes [intro]: "!!x. DERIV F x :> f x"
+ assumes [intro]: "!!x. DERIV G x :> g x"
+ shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
+ = F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
+proof-
+ have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
+ by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
+ (auto intro!: DERIV_isCont)
+
+ have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
+ (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
+ apply (subst Bochner_Integration.integral_add[symmetric])
+ apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
+ by (auto intro!: DERIV_isCont Bochner_Integration.integral_cong split: split_indicator)
+
+ thus ?thesis using 0 by auto
+qed
+
+lemma integral_by_parts':
+ fixes f g F G::"real \<Rightarrow> real"
+ assumes "a \<le> b"
+ assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+ assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+ assumes "!!x. DERIV F x :> f x"
+ assumes "!!x. DERIV G x :> g x"
+ shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
+ = F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
+ using integral_by_parts[OF assms] by (simp add: ac_simps)
+
+lemma has_bochner_integral_even_function:
+ fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+ assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
+ assumes even: "\<And>x. f (- x) = f x"
+ shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
+proof -
+ have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
+ by (auto split: split_indicator)
+ have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
+ by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
+ (auto simp: indicator even f)
+ with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)"
+ by (rule has_bochner_integral_add)
+ then have "has_bochner_integral lborel f (x + x)"
+ by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
+ (auto split: split_indicator)
+ then show ?thesis
+ by (simp add: scaleR_2)
+qed
+
+lemma has_bochner_integral_odd_function:
+ fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+ assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
+ assumes odd: "\<And>x. f (- x) = - f x"
+ shows "has_bochner_integral lborel f 0"
+proof -
+ have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
+ by (auto split: split_indicator)
+ have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
+ by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
+ (auto simp: indicator odd f)
+ from has_bochner_integral_minus[OF this]
+ have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
+ by simp
+ with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
+ by (rule has_bochner_integral_add)
+ then have "has_bochner_integral lborel f (x + - x)"
+ by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
+ (auto split: split_indicator)
+ then show ?thesis
+ by simp
+qed
+
+end
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Sep 16 13:56:51 2016 +0200
@@ -6,9 +6,7 @@
theory Henstock_Kurzweil_Integration
imports
- Derivative
- Uniform_Limit
- "~~/src/HOL/Library/Indicator_Function"
+ Lebesgue_Measure
begin
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
@@ -22,122 +20,19 @@
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
+lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
+ by auto
+
declare norm_triangle_ineq4[intro]
-lemma simple_image: "{f x |x . x \<in> s} = f ` s"
- by blast
-
-lemma linear_simps:
- assumes "bounded_linear f"
- shows
- "f (a + b) = f a + f b"
- "f (a - b) = f a - f b"
- "f 0 = 0"
- "f (- a) = - f a"
- "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
-proof -
- interpret f: bounded_linear f by fact
- show "f (a + b) = f a + f b" by (rule f.add)
- show "f (a - b) = f a - f b" by (rule f.diff)
- show "f 0 = 0" by (rule f.zero)
- show "f (- a) = - f a" by (rule f.minus)
- show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
-qed
-
-lemma bounded_linearI:
- assumes "\<And>x y. f (x + y) = f x + f y"
- and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
- and "\<And>x. norm (f x) \<le> norm x * K"
- shows "bounded_linear f"
- using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
-
-lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
- by (rule bounded_linear_inner_left)
-
-lemma transitive_stepwise_lt_eq:
- assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
- shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))"
- (is "?l = ?r")
-proof safe
- assume ?r
- fix n m :: nat
- assume "m < n"
- then show "R m n"
- proof (induct n arbitrary: m)
- case 0
- then show ?case by auto
- next
- case (Suc n)
- show ?case
- proof (cases "m < n")
- case True
- show ?thesis
- apply (rule assms[OF Suc(1)[OF True]])
- using \<open>?r\<close>
- apply auto
- done
- next
- case False
- then have "m = n"
- using Suc(2) by auto
- then show ?thesis
- using \<open>?r\<close> by auto
- qed
- qed
-qed auto
-
-lemma transitive_stepwise_gt:
- assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)"
- shows "\<forall>n>m. R m n"
-proof -
- have "\<forall>m. \<forall>n>m. R m n"
- apply (subst transitive_stepwise_lt_eq)
- apply (blast intro: assms)+
- done
- then show ?thesis by auto
-qed
-
-lemma transitive_stepwise_le_eq:
- assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
- shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))"
- (is "?l = ?r")
-proof safe
- assume ?r
- fix m n :: nat
- assume "m \<le> n"
- then show "R m n"
- proof (induct n arbitrary: m)
- case 0
- with assms show ?case by auto
- next
- case (Suc n)
- show ?case
- proof (cases "m \<le> n")
- case True
- with Suc.hyps \<open>\<forall>n. R n (Suc n)\<close> assms show ?thesis
- by blast
- next
- case False
- then have "m = Suc n"
- using Suc(2) by auto
- then show ?thesis
- using assms(1) by auto
- qed
- qed
-qed auto
-
lemma transitive_stepwise_le:
- assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
- and "\<And>n. R n (Suc n)"
+ assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
shows "\<forall>n\<ge>m. R m n"
-proof -
- have "\<forall>m. \<forall>n\<ge>m. R m n"
- apply (subst transitive_stepwise_le_eq)
- apply (blast intro: assms)+
- done
- then show ?thesis by auto
-qed
-
+proof (intro allI impI)
+ show "m \<le> n \<Longrightarrow> R m n" for n
+ by (induction rule: dec_induct)
+ (use assms in blast)+
+qed
subsection \<open>Some useful lemmas about intervals.\<close>
@@ -208,13 +103,28 @@
"finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}"
using interior_Union_subset_cbox[of f "UNIV - s"] by auto
+lemma interval_split:
+ fixes a :: "'a::euclidean_space"
+ assumes "k \<in> Basis"
+ shows
+ "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
+ "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
+ apply (rule_tac[!] set_eqI)
+ unfolding Int_iff mem_box mem_Collect_eq
+ using assms
+ apply auto
+ done
+
+lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
+ by (simp add: box_ne_empty)
+
subsection \<open>Bounds on intervals where they exist.\<close>
definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
- where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
+ where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
lemma interval_upperbound[simp]:
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
@@ -242,7 +152,6 @@
and "interval_lowerbound (cbox a b) = a"
using assms unfolding box_ne_empty by auto
-
lemma interval_upperbound_Times:
assumes "A \<noteq> {}" and "B \<noteq> {}"
shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
@@ -273,219 +182,83 @@
subsection \<open>Content (length, area, volume...) of an interval.\<close>
-definition "content (s::('a::euclidean_space) set) =
- (if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i - (interval_lowerbound s)\<bullet>i))"
-
-lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
- unfolding box_eq_empty unfolding not_ex not_less by auto
-
-lemma content_cbox:
- fixes a :: "'a::euclidean_space"
- assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
- shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
- using interval_not_empty[OF assms]
- unfolding content_def
- by auto
-
-lemma content_cbox':
- fixes a :: "'a::euclidean_space"
- assumes "cbox a b \<noteq> {}"
- shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
- using assms box_ne_empty(1) content_cbox by blast
+abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
+ where "content s \<equiv> measure lborel s"
+
+lemma content_cbox_cases:
+ "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
+ by (simp add: measure_lborel_cbox_eq inner_diff)
+
+lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+ unfolding content_cbox_cases by simp
+
+lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+ by (simp add: box_ne_empty inner_diff)
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
- by (auto simp: interval_upperbound_def interval_lowerbound_def content_def)
+ by simp
lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
by (auto simp: content_real)
-lemma content_singleton[simp]: "content {a} = 0"
-proof -
- have "content (cbox a a) = 0"
- by (subst content_cbox) (auto simp: ex_in_conv)
- then show ?thesis by (simp add: cbox_sing)
-qed
-
-lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
- proof -
- have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
- by auto
- have "0 \<in> cbox 0 (One::'a)"
- unfolding mem_box by auto
- then show ?thesis
- unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto
- qed
-
-lemma content_pos_le[intro]:
- fixes a::"'a::euclidean_space"
- shows "0 \<le> content (cbox a b)"
-proof (cases "cbox a b = {}")
- case False
- then have *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
- unfolding box_ne_empty .
- have "0 \<le> (\<Prod>i\<in>Basis. interval_upperbound (cbox a b) \<bullet> i - interval_lowerbound (cbox a b) \<bullet> i)"
- apply (rule setprod_nonneg)
- unfolding interval_bounds[OF *]
- using *
- apply auto
- done
- also have "\<dots> = content (cbox a b)" using False by (simp add: content_def)
- finally show ?thesis .
-qed (simp add: content_def)
-
-corollary content_nonneg [simp]:
- fixes a::"'a::euclidean_space"
- shows "~ content (cbox a b) < 0"
-using not_le by blast
-
-lemma content_pos_lt:
- fixes a :: "'a::euclidean_space"
- assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
- shows "0 < content (cbox a b)"
- using assms
- by (auto simp: content_def box_eq_empty intro!: setprod_pos)
-
-lemma content_eq_0:
- "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
- by (auto simp: content_def box_eq_empty intro!: setprod_pos bexI)
-
-lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
- by auto
-
-lemma content_cbox_cases:
- "content (cbox a (b::'a::euclidean_space)) =
- (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
- by (auto simp: not_le content_eq_0 intro: less_imp_le content_cbox)
+lemma content_singleton: "content {a} = 0"
+ by simp
+
+lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
+ by simp
+
+lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
+ by simp
+
+corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
+ using not_le by blast
+
+lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
+ by (auto simp: less_imp_le inner_diff box_eq_empty intro!: setprod_pos)
+
+lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
+ by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
- unfolding content_eq_0 interior_cbox box_eq_empty
- by auto
-
-lemma content_pos_lt_eq:
- "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
-proof (rule iffI)
- assume "0 < content (cbox a b)"
- then have "content (cbox a b) \<noteq> 0" by auto
- then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
- unfolding content_eq_0 not_ex not_le by fastforce
-next
- assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
- then show "0 < content (cbox a b)"
- by (metis content_pos_lt)
-qed
+ unfolding content_eq_0 interior_cbox box_eq_empty by auto
+
+lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
+ by (auto simp add: content_cbox_cases less_le setprod_nonneg)
lemma content_empty [simp]: "content {} = 0"
- unfolding content_def by auto
+ by simp
lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
by (simp add: content_real)
-lemma content_subset:
- assumes "cbox a b \<subseteq> cbox c d"
- shows "content (cbox a b) \<le> content (cbox c d)"
-proof (cases "cbox a b = {}")
- case True
- then show ?thesis
- using content_pos_le[of c d] by auto
-next
- case False
- then have ab_ne: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
- unfolding box_ne_empty by auto
- then have ab_ab: "a\<in>cbox a b" "b\<in>cbox a b"
- unfolding mem_box by auto
- have "cbox c d \<noteq> {}" using assms False by auto
- then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
- using assms unfolding box_ne_empty by auto
- have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
- using ab_ne by auto
- moreover
- have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
- using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
- assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)]
- by (metis diff_mono)
- ultimately show ?thesis
- unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
- by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF \<open>cbox c d \<noteq> {}\<close>])
-qed
+lemma content_subset: "cbox a b \<subseteq> cbox c d \<Longrightarrow> content (cbox a b) \<le> content (cbox c d)"
+ unfolding measure_def
+ by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq)
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
-lemma content_times[simp]: "content (A \<times> B) = content A * content B"
-proof (cases "A \<times> B = {}")
- let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
- let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
- assume nonempty: "A \<times> B \<noteq> {}"
- hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
- unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
- also have "... = content A * content B" unfolding content_def using nonempty
- apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
- apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
- done
- finally show ?thesis .
-qed (auto simp: content_def)
-
lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
- by (simp add: cbox_Pair_eq)
+ unfolding measure_lborel_cbox_eq Basis_prod_def
+ apply (subst setprod.union_disjoint)
+ apply (auto simp: bex_Un ball_Un)
+ apply (subst (1 2) setprod.reindex_nontrivial)
+ apply auto
+ done
lemma content_cbox_pair_eq0_D:
"content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
by (simp add: content_Pair)
-lemma content_eq_0_gen:
- fixes s :: "'a::euclidean_space set"
- assumes "bounded s"
- shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)" (is "_ = ?rhs")
-proof safe
- assume "content s = 0" then show ?rhs
- apply (clarsimp simp: ex_in_conv content_def split: if_split_asm)
- apply (rule_tac x=a in bexI)
- apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
- apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
- apply (drule cSUP_eq_cINF_D)
- apply (auto simp: bounded_inner_imp_bdd_above [OF assms] bounded_inner_imp_bdd_below [OF assms])
- done
-next
- fix i a
- assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a"
- then show "content s = 0"
- apply (clarsimp simp: content_def)
- apply (rule_tac x=i in bexI)
- apply (auto simp: interval_upperbound_def interval_lowerbound_def)
- done
-qed
-
-lemma content_0_subset_gen:
- fixes a :: "'a::euclidean_space"
- assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0"
-proof -
- have "bounded s"
- using assms by (metis bounded_subset)
- then show ?thesis
- using assms
- by (auto simp: content_eq_0_gen)
-qed
-
-lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0"
- by (simp add: content_0_subset_gen bounded_cbox)
-
-
-lemma interval_split:
- fixes a :: "'a::euclidean_space"
- assumes "k \<in> Basis"
- shows
- "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
- "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
- apply (rule_tac[!] set_eqI)
- unfolding Int_iff mem_box mem_Collect_eq
- using assms
- apply auto
- done
+lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0"
+ using emeasure_mono[of s "cbox a b" lborel]
+ by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)
lemma content_split:
fixes a :: "'a::euclidean_space"
assumes "k \<in> Basis"
shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+ -- \<open>Prove using measure theory\<close>
proof cases
note simps = interval_split[OF assms] content_cbox_cases
have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
@@ -2040,11 +1813,6 @@
"d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
unfolding setsum.operative_tagged_division[OF operative_content, symmetric] by blast
-lemma
- shows real_inner_1_left: "inner 1 x = x"
- and real_inner_1_right: "inner x 1 = x"
- by simp_all
-
lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
@@ -3988,8 +3756,7 @@
have "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
using norm_setsum by blast
also have "... \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)"
- apply (simp add: setsum_right_distrib[symmetric] mult.commute)
- using assms(2) mult_right_mono by blast
+ by (simp add: setsum_right_distrib[symmetric] mult.commute assms(2) mult_right_mono setsum_nonneg)
also have "... \<le> e * content (cbox a b)"
apply (rule mult_left_mono [OF _ e])
apply (simp add: sumeq)
@@ -4458,65 +4225,70 @@
assumes "0 < e"
and k: "k \<in> Basis"
obtains d where "0 < d" and "content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) < e"
-proof (cases "content (cbox a b) = 0")
- case True
- then have ce: "content (cbox a b) < e"
- by (metis \<open>0 < e\<close>)
+proof cases
+ assume *: "a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j)"
+ define a' where "a' d = (\<Sum>j\<in>Basis. (if j = k then max (a\<bullet>j) (c - d) else a\<bullet>j) *\<^sub>R j)" for d
+ define b' where "b' d = (\<Sum>j\<in>Basis. (if j = k then min (b\<bullet>j) (c + d) else b\<bullet>j) *\<^sub>R j)" for d
+
+ have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> (\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j)) (at_right 0)"
+ by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
+ also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
+ using k *
+ by (intro setprod_zero bexI[OF _ k])
+ (auto simp: b'_def a'_def inner_diff inner_setsum_left inner_not_same_Basis intro!: setsum.cong)
+ also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
+ ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
+ proof (intro tendsto_cong eventually_at_rightI)
+ fix d :: real assume d: "d \<in> {0<..<1}"
+ have "cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d} = cbox (a' d) (b' d)" for d
+ using * d k by (auto simp add: cbox_def set_eq_iff Int_def ball_conj_distrib abs_diff_le_iff a'_def b'_def)
+ moreover have "j \<in> Basis \<Longrightarrow> a' d \<bullet> j \<le> b' d \<bullet> j" for j
+ using * d k by (auto simp: a'_def b'_def)
+ ultimately show "(\<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) = content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})"
+ by simp
+ qed simp
+ finally have "((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)" .
+ from order_tendstoD(2)[OF this \<open>0<e\<close>]
+ obtain d' where "0 < d'" and d': "\<And>y. y > 0 \<Longrightarrow> y < d' \<Longrightarrow> content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> y}) < e"
+ by (subst (asm) eventually_at_right[of _ 1]) auto
show ?thesis
- apply (rule that[of 1])
- apply simp
- unfolding interval_doublesplit[OF k]
- apply (rule le_less_trans[OF content_subset ce])
- apply (auto simp: interval_doublesplit[symmetric] k)
- done
+ by (rule that[of "d'/2"], insert \<open>0<d'\<close> d'[of "d'/2"], auto)
next
- case False
- define d where "d = e / 3 / setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
- note False[unfolded content_eq_0 not_ex not_le, rule_format]
- then have "\<And>x. x \<in> Basis \<Longrightarrow> b\<bullet>x > a\<bullet>x"
- by (auto simp add:not_le)
- then have prod0: "0 < setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
- by (force simp add: setprod_pos field_simps)
- then have "d > 0"
- using assms
- by (auto simp add: d_def field_simps)
- then show ?thesis
- proof (rule that[of d])
- have *: "Basis = insert k (Basis - {k})"
- using k by auto
- have less_e: "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
- proof -
- have "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) \<le> 2 * d"
+ assume *: "\<not> (a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j))"
+ then have "(\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j) \<or> (c < a \<bullet> k \<or> b \<bullet> k < c)"
+ by (auto simp: not_le)
+ show thesis
+ proof cases
+ assume "\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j"
+ then have [simp]: "cbox a b = {}"
+ using box_ne_empty(1)[of a b] by auto
+ show ?thesis
+ by (rule that[of 1]) (simp_all add: \<open>0<e\<close>)
+ next
+ assume "\<not> (\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j)"
+ with * have "c < a \<bullet> k \<or> b \<bullet> k < c"
+ by auto
+ then show thesis
+ proof
+ assume c: "c < a \<bullet> k"
+ moreover have "x \<in> cbox a b \<Longrightarrow> c \<le> x \<bullet> k" for x
+ using k c by (auto simp: cbox_def)
+ ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c) / 2} = {}"
+ using k by (auto simp: cbox_def)
+ with \<open>0<e\<close> c that[of "(a \<bullet> k - c) / 2"] show ?thesis
by auto
- also have "\<dots> < e / (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i)"
- unfolding d_def
- using assms prod0
- by (auto simp add: field_simps)
- finally show "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
- unfolding pos_less_divide_eq[OF prod0] .
- qed
- show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
- proof (cases "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = {}")
- case True
- then show ?thesis
- using assms by simp
next
- case False
- then have
- "(\<Prod>i\<in>Basis - {k}. interval_upperbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i -
- interval_lowerbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i)
- = (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)"
- by (simp add: box_eq_empty interval_doublesplit[OF k])
- then show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
- unfolding content_def
- using assms False
- apply (subst *)
- apply (subst setprod.insert)
- apply (simp_all add: interval_doublesplit[OF k] box_eq_empty not_less less_e)
- done
- qed
- qed
-qed
+ assume c: "b \<bullet> k < c"
+ moreover have "x \<in> cbox a b \<Longrightarrow> x \<bullet> k \<le> c" for x
+ using k c by (auto simp: cbox_def)
+ ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k) / 2} = {}"
+ using k by (auto simp: cbox_def)
+ with \<open>0<e\<close> c that[of "(c - b \<bullet> k) / 2"] show ?thesis
+ by auto
+ qed
+ qed
+qed
+
lemma negligible_standard_hyperplane[intro]:
fixes k :: "'a::euclidean_space"
@@ -5695,6 +5467,7 @@
by auto
from fundamental_theorem_of_calculus[rule_format, OF \<open>a \<le> b\<close> deriv]
have "(i has_integral ?sum b - ?sum a) {a .. b}"
+ using atLeastatMost_empty'[simp del]
by (simp add: i_def g_def Dg_def)
also
have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)"
@@ -6036,7 +5809,7 @@
done
show ?thesis
using False
- apply (simp add: abs_eq_content del: content_real_if)
+ apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
done
@@ -6054,7 +5827,7 @@
done
have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
using True
- apply (simp add: abs_eq_content del: content_real_if)
+ apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
done
@@ -6274,6 +6047,62 @@
subsection \<open>Special case of a basic affine transformation.\<close>
+lemma AE_lborel_inner_neq:
+ assumes k: "k \<in> Basis"
+ shows "AE x in lborel. x \<bullet> k \<noteq> c"
+proof -
+ interpret finite_product_sigma_finite "\<lambda>_. lborel" Basis
+ proof qed simp
+
+ have "emeasure lborel {x\<in>space lborel. x \<bullet> k = c} = emeasure (\<Pi>\<^sub>M j::'a\<in>Basis. lborel) (\<Pi>\<^sub>E j\<in>Basis. if j = k then {c} else UNIV)"
+ using k
+ by (auto simp add: lborel_eq[where 'a='a] emeasure_distr intro!: arg_cong2[where f=emeasure])
+ (auto simp: space_PiM PiE_iff extensional_def split: if_split_asm)
+ also have "\<dots> = (\<Prod>j\<in>Basis. emeasure lborel (if j = k then {c} else UNIV))"
+ by (intro measure_times) auto
+ also have "\<dots> = 0"
+ by (intro setprod_zero bexI[OF _ k]) auto
+ finally show ?thesis
+ by (subst AE_iff_measurable[OF _ refl]) auto
+qed
+
+lemma content_image_stretch_interval:
+ fixes m :: "'a::euclidean_space \<Rightarrow> real"
+ defines "s f x \<equiv> (\<Sum>k::'a\<in>Basis. (f k * (x\<bullet>k)) *\<^sub>R k)"
+ shows "content (s m ` cbox a b) = \<bar>\<Prod>k\<in>Basis. m k\<bar> * content (cbox a b)"
+proof cases
+ have s[measurable]: "s f \<in> borel \<rightarrow>\<^sub>M borel" for f
+ by (auto simp: s_def[abs_def])
+ assume m: "\<forall>k\<in>Basis. m k \<noteq> 0"
+ then have s_comp_s: "s (\<lambda>k. 1 / m k) \<circ> s m = id" "s m \<circ> s (\<lambda>k. 1 / m k) = id"
+ by (auto simp: s_def[abs_def] fun_eq_iff euclidean_representation)
+ then have "inv (s (\<lambda>k. 1 / m k)) = s m" "bij (s (\<lambda>k. 1 / m k))"
+ by (auto intro: inv_unique_comp o_bij)
+ then have eq: "s m ` cbox a b = s (\<lambda>k. 1 / m k) -` cbox a b"
+ using bij_vimage_eq_inv_image[OF \<open>bij (s (\<lambda>k. 1 / m k))\<close>, of "cbox a b"] by auto
+ show ?thesis
+ using m unfolding eq measure_def
+ by (subst lborel_affine_euclidean[where c=m and t=0])
+ (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_setprod nn_integral_cmult
+ s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult setprod_nonneg)
+next
+ assume "\<not> (\<forall>k\<in>Basis. m k \<noteq> 0)"
+ then obtain k where k: "k \<in> Basis" "m k = 0" by auto
+ then have [simp]: "(\<Prod>k\<in>Basis. m k) = 0"
+ by (intro setprod_zero) auto
+ have "emeasure lborel {x\<in>space lborel. x \<in> s m ` cbox a b} = 0"
+ proof (rule emeasure_eq_0_AE)
+ show "AE x in lborel. x \<notin> s m ` cbox a b"
+ using AE_lborel_inner_neq[OF \<open>k\<in>Basis\<close>]
+ proof eventually_elim
+ show "x \<bullet> k \<noteq> 0 \<Longrightarrow> x \<notin> s m ` cbox a b " for x
+ using k by (auto simp: s_def[abs_def] cbox_def)
+ qed
+ qed
+ then show ?thesis
+ by (simp add: measure_def)
+qed
+
lemma interval_image_affinity_interval:
"\<exists>u v. (\<lambda>x. m *\<^sub>R (x::'a::euclidean_space) + c) ` cbox a b = cbox u v"
unfolding image_affinity_cbox
@@ -6344,43 +6173,6 @@
subsection \<open>Special case of stretching coordinate axes separately.\<close>
-lemma content_image_stretch_interval:
- "content ((\<lambda>x::'a::euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` cbox a b) =
- \<bar>setprod m Basis\<bar> * content (cbox a b)"
-proof (cases "cbox a b = {}")
- case True
- then show ?thesis
- unfolding content_def image_is_empty image_stretch_interval if_P[OF True] by auto
-next
- case False
- then have "(\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b \<noteq> {}"
- by auto
- then show ?thesis
- using False
- unfolding content_def image_stretch_interval
- apply -
- unfolding interval_bounds' if_not_P
- unfolding abs_setprod setprod.distrib[symmetric]
- apply (rule setprod.cong)
- apply (rule refl)
- unfolding lessThan_iff
- apply (simp only: inner_setsum_left_Basis)
- proof -
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "(m i < 0 \<or> m i > 0) \<or> m i = 0"
- by auto
- then show "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) - min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) =
- \<bar>m i\<bar> * (b \<bullet> i - a \<bullet> i)"
- apply -
- apply (erule disjE)+
- unfolding min_def max_def
- using False[unfolded box_ne_empty,rule_format,of i] i
- apply (auto simp add:field_simps not_le mult_le_cancel_left_neg mult_le_cancel_left_pos)
- done
- qed
-qed
-
lemma has_integral_stretch:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "(f has_integral i) (cbox a b)"
@@ -9324,7 +9116,7 @@
proof (rule, goal_cases)
case prems: (1 x)
have "e / (4 * content (cbox a b)) > 0"
- using \<open>e>0\<close> False content_pos_le[of a b] by auto
+ using \<open>e>0\<close> False content_pos_le[of a b] by (simp add: less_le)
from assms(3)[rule_format, OF prems, THEN LIMSEQ_D, OF this]
guess n .. note n=this
then show ?case
@@ -10314,7 +10106,7 @@
done
also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
apply (rule setsum.mono_neutral_left)
- apply (subst simple_image)
+ apply (subst Setcompr_eq_image)
apply (rule finite_imageI)+
apply fact
unfolding d'_def uv
@@ -10330,7 +10122,7 @@
using l by auto
qed
also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
- unfolding simple_image
+ unfolding Setcompr_eq_image
apply (rule setsum.reindex_nontrivial [unfolded o_def])
apply (rule finite_imageI)
apply (rule p')
@@ -10518,7 +10310,7 @@
apply auto
done
also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
- unfolding simple_image
+ unfolding Setcompr_eq_image
apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
apply (rule d')
proof goal_cases
@@ -10539,7 +10331,7 @@
qed
also have "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
apply (rule setsum.mono_neutral_right)
- unfolding simple_image
+ unfolding Setcompr_eq_image
apply (rule finite_imageI)
apply (rule d')
apply blast
@@ -11394,7 +11186,7 @@
also have "\<dots> < e' * norm (x - x0)"
using \<open>e' > 0\<close> content_pos_le[of a b]
by (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
- (auto simp: divide_simps e_def)
+ (auto simp: divide_simps e_def simp del: measure_nonneg)
finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
then show ?case
by (auto simp: divide_simps)
@@ -11509,7 +11301,7 @@
with \<open>e > 0\<close> have "e' > 0" by simp
then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)"
using u content_nonzero content_pos_le[of a b]
- by (auto simp: uniform_limit_iff dist_norm)
+ by (auto simp: uniform_limit_iff dist_norm simp del: measure_nonneg)
then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
proof eventually_elim
case (elim n)
@@ -11568,7 +11360,7 @@
fix k :: nat
show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
apply (rule integral_norm_bound_integral)
- unfolding simple_image
+ unfolding Setcompr_eq_image
apply (rule absolutely_integrable_onD)
apply (rule absolutely_integrable_inf_real)
prefer 5
@@ -11585,7 +11377,7 @@
qed
fix k :: nat
show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
- unfolding simple_image
+ unfolding Setcompr_eq_image
apply (rule absolutely_integrable_onD)
apply (rule absolutely_integrable_inf_real)
prefer 3
@@ -11638,7 +11430,7 @@
proof safe
fix k :: nat
show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
- apply (rule integral_norm_bound_integral) unfolding simple_image
+ apply (rule integral_norm_bound_integral) unfolding Setcompr_eq_image
apply (rule absolutely_integrable_onD)
apply(rule absolutely_integrable_sup_real)
prefer 5 unfolding real_norm_def
@@ -11656,7 +11448,7 @@
qed
fix k :: nat
show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
- unfolding simple_image
+ unfolding Setcompr_eq_image
apply (rule absolutely_integrable_onD)
apply (rule absolutely_integrable_sup_real)
prefer 3
@@ -12541,11 +12333,11 @@
define f :: "nat \<Rightarrow> real \<Rightarrow> real" where "f = (\<lambda>n x. if x \<in> {a..n} then x powr e else 0)"
define F where "F = (\<lambda>x. x powr (e + 1) / (e + 1))"
- have has_integral_f: "(f n has_integral (F n - F a)) {a..}"
+ have has_integral_f: "(f n has_integral (F n - F a)) {a..}"
if n: "n \<ge> a" for n :: nat
proof -
from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
- by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
+ by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
hence "(f n has_integral (F n - F a)) {a..n}"
by (rule has_integral_eq [rotated]) (simp add: f_def)
@@ -12559,12 +12351,12 @@
next
case False
have "(f n has_integral 0) {a}" by (rule has_integral_refl)
- hence "(f n has_integral 0) {a..}"
+ hence "(f n has_integral 0) {a..}"
by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
with False show ?thesis by (simp add: integral_unique)
qed
-
- have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and>
+
+ have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and>
(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> integral {a..} (\<lambda>x. x powr e)"
proof (intro monotone_convergence_increasing allI ballI)
fix n :: nat
@@ -12582,7 +12374,7 @@
from filterlim_real_sequentially
have "eventually (\<lambda>n. real n \<ge> x) at_top"
by (simp add: filterlim_at_top)
- with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
+ with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
by (auto elim!: eventually_mono simp: f_def)
thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
next
@@ -12603,11 +12395,11 @@
hence "eventually (\<lambda>n. F n - F a = integral {a..} (f n)) at_top"
by eventually_elim (simp add: integral_f)
moreover have "(\<lambda>n. F n - F a) \<longlonglongrightarrow> 0 / (e + 1) - F a" unfolding F_def
- by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
+ by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
filterlim_ident filterlim_real_sequentially | simp)+)
hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
- from conjunct2[OF *] and this
+ from conjunct2[OF *] and this
have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
with conjunct1[OF *] show ?thesis
by (simp add: has_integral_integral F_def)
@@ -12620,7 +12412,7 @@
proof -
from assms have "real_of_int (-int n) < -1" by simp
note has_integral_powr_to_inf[OF this \<open>a > 0\<close>]
- also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) =
+ also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) =
1 / (real (n - 1) * a powr (real (n - 1)))" using assms
by (simp add: divide_simps powr_add [symmetric] of_nat_diff)
also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
@@ -12630,4 +12422,33 @@
(insert assms, simp_all add: powr_minus powr_realpow divide_simps)
qed
+subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
+
+lemma integral_component_eq_cart[simp]:
+ fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
+ assumes "f integrable_on s"
+ shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
+ using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
+
+lemma content_closed_interval:
+ fixes a :: "'a::ordered_euclidean_space"
+ assumes "a \<le> b"
+ shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+ using content_cbox[of a b] assms
+ by (simp add: cbox_interval eucl_le[where 'a='a])
+
+lemma integrable_const_ivl[intro]:
+ fixes a::"'a::ordered_euclidean_space"
+ shows "(\<lambda>x. c) integrable_on {a .. b}"
+ unfolding cbox_interval[symmetric]
+ by (rule integrable_const)
+
+lemma integrable_on_subinterval:
+ fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+ assumes "f integrable_on s"
+ and "{a .. b} \<subseteq> s"
+ shows "f integrable_on {a .. b}"
+ using integrable_on_subcbox[of f s a b] assms
+ by (simp add: cbox_interval)
+
end
--- a/src/HOL/Analysis/Interval_Integral.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Fri Sep 16 13:56:51 2016 +0200
@@ -311,7 +311,7 @@
ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
uminus_ereal.simps[symmetric]
simp del: uminus_ereal.simps
- intro!: integral_cong
+ intro!: Bochner_Integration.integral_cong
split: split_indicator)
qed
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Fri Sep 16 13:56:51 2016 +0200
@@ -469,6 +469,10 @@
"emeasure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force
+lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
+ using emeasure_lborel_cbox[of x x] nonempty_Basis
+ by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant)
+
lemma
fixes l u :: real
assumes [simp]: "l \<le> u"
@@ -484,6 +488,17 @@
and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
by (simp_all add: measure_def inner_diff_left setprod_nonneg)
+lemma measure_lborel_cbox_eq:
+ "measure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
+ using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le)
+
+lemma measure_lborel_box_eq:
+ "measure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
+ using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force
+
+lemma measure_lborel_singleton[simp]: "measure lborel {x} = 0"
+ by (simp add: measure_def)
+
lemma sigma_finite_lborel: "sigma_finite_measure lborel"
proof
show "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets lborel \<and> \<Union>A = space lborel \<and> (\<forall>a\<in>A. emeasure lborel a \<noteq> \<infinity>)"
@@ -516,10 +531,6 @@
done
qed
-lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
- using emeasure_lborel_cbox[of x x] nonempty_Basis
- by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant)
-
lemma emeasure_lborel_countable:
fixes A :: "'a::euclidean_space set"
assumes "countable A"
@@ -572,46 +583,38 @@
{ fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto }
{ fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X"
- apply (auto simp: emeasure_eq emeasure_lborel_box_eq )
+ apply (auto simp: emeasure_eq emeasure_lborel_box_eq)
apply (subst box_eq_empty(1)[THEN iffD2])
apply (auto intro: less_imp_le simp: not_le)
done }
qed
-lemma lborel_affine:
- fixes t :: "'a::euclidean_space" assumes "c \<noteq> 0"
- shows "lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))" (is "_ = ?D")
+lemma lborel_affine_euclidean:
+ fixes c :: "'a::euclidean_space \<Rightarrow> real" and t
+ defines "T x \<equiv> t + (\<Sum>j\<in>Basis. (c j * (x \<bullet> j)) *\<^sub>R j)"
+ assumes c: "\<And>j. j \<in> Basis \<Longrightarrow> c j \<noteq> 0"
+ shows "lborel = density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" (is "_ = ?D")
proof (rule lborel_eqI)
let ?B = "Basis :: 'a set"
fix l u assume le: "\<And>b. b \<in> ?B \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
- show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
- proof cases
- assume "0 < c"
- then have "(\<lambda>x. t + c *\<^sub>R x) -` box l u = box ((l - t) /\<^sub>R c) ((u - t) /\<^sub>R c)"
- by (auto simp: field_simps box_def inner_simps)
- with \<open>0 < c\<close> show ?thesis
- using le
- by (auto simp: field_simps inner_simps setprod_dividef setprod_constant setprod_nonneg
- ennreal_mult[symmetric] emeasure_density nn_integral_distr emeasure_distr
- nn_integral_cmult emeasure_lborel_box_eq borel_measurable_indicator')
- next
- assume "\<not> 0 < c" with \<open>c \<noteq> 0\<close> have "c < 0" by auto
- then have "box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c) = (\<lambda>x. t + c *\<^sub>R x) -` box l u"
- by (auto simp: field_simps box_def inner_simps)
- then have *: "\<And>x. indicator (box l u) (t + c *\<^sub>R x) = (indicator (box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c)) x :: ennreal)"
- by (auto split: split_indicator)
- have **: "(\<Prod>x\<in>Basis. (l \<bullet> x - u \<bullet> x) / c) = (\<Prod>x\<in>Basis. u \<bullet> x - l \<bullet> x) / (-c) ^ card (Basis::'a set)"
- using \<open>c < 0\<close>
- by (auto simp add: field_simps setprod_dividef[symmetric] setprod_constant[symmetric]
- intro!: setprod.cong)
- show ?thesis
- using \<open>c < 0\<close> le
- by (auto simp: * ** field_simps emeasure_density nn_integral_distr nn_integral_cmult
- emeasure_lborel_box_eq inner_simps setprod_nonneg ennreal_mult[symmetric]
- borel_measurable_indicator')
- qed
+ have [measurable]: "T \<in> borel \<rightarrow>\<^sub>M borel"
+ by (simp add: T_def[abs_def])
+ have eq: "T -` box l u = box
+ (\<Sum>j\<in>Basis. (((if 0 < c j then l - t else u - t) \<bullet> j) / c j) *\<^sub>R j)
+ (\<Sum>j\<in>Basis. (((if 0 < c j then u - t else l - t) \<bullet> j) / c j) *\<^sub>R j)"
+ using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq)
+ with le c show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
+ by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps
+ field_simps divide_simps ennreal_mult'[symmetric] setprod_nonneg setprod.distrib[symmetric]
+ intro!: setprod.cong)
qed simp
+lemma lborel_affine:
+ fixes t :: "'a::euclidean_space"
+ shows "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))"
+ using lborel_affine_euclidean[where c="\<lambda>_::'a. c" and t=t]
+ unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric] euclidean_representation setprod_constant by simp
+
lemma lborel_real_affine:
"c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))"
using lborel_affine[of c t] by simp
@@ -726,378 +729,6 @@
lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
-subsection \<open>Equivalence Lebesgue integral on @{const lborel} and HK-integral\<close>
-
-lemma has_integral_measure_lborel:
- fixes A :: "'a::euclidean_space set"
- assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>"
- shows "((\<lambda>x. 1) has_integral measure lborel A) A"
-proof -
- { fix l u :: 'a
- have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box l u)"
- proof cases
- assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
- then show ?thesis
- apply simp
- apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
- apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
- using has_integral_const[of "1::real" l u]
- apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
- done
- next
- assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
- then have "box l u = {}"
- unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le)
- then show ?thesis
- by simp
- qed }
- note has_integral_box = this
-
- { fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box a b)"
- have "Int_stable (range (\<lambda>(a, b). box a b))"
- by (auto simp: Int_stable_def box_Int_box)
- moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV"
- by auto
- moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box a b))"
- using A unfolding borel_eq_box by simp
- ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box a b)"
- proof (induction rule: sigma_sets_induct_disjoint)
- case (basic A) then show ?case
- by (auto simp: box_Int_box has_integral_box)
- next
- case empty then show ?case
- by simp
- next
- case (compl A)
- then have [measurable]: "A \<in> sets borel"
- by (simp add: borel_eq_box)
-
- have "((\<lambda>x. 1) has_integral ?M (box a b)) (box a b)"
- by (simp add: has_integral_box)
- moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
- by (subst has_integral_restrict) (auto intro: compl)
- ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
- by (rule has_integral_sub)
- then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
- by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
- then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
- by (subst (asm) has_integral_restrict) auto
- also have "?M (box a b) - ?M A = ?M (UNIV - A)"
- by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2)
- finally show ?case .
- next
- case (union F)
- then have [measurable]: "\<And>i. F i \<in> sets borel"
- by (simp add: borel_eq_box subset_eq)
- have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
- proof (rule has_integral_monotone_convergence_increasing)
- let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
- show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
- using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff)
- show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
- by (intro setsum_mono2) auto
- from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
- by (auto simp add: disjoint_family_on_def)
- show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
- apply (auto simp: * setsum.If_cases Iio_Int_singleton)
- apply (rule_tac k="Suc xa" in LIMSEQ_offset)
- apply simp
- done
- have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
- by (intro emeasure_mono) auto
-
- with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
- unfolding sums_def[symmetric] UN_extend_simps
- by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique)
- qed
- then show ?case
- by (subst (asm) has_integral_restrict) auto
- qed }
- note * = this
-
- show ?thesis
- proof (rule has_integral_monotone_convergence_increasing)
- let ?B = "\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set"
- let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real"
- let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)"
-
- show "\<And>n::nat. (?f n has_integral ?M n) A"
- using * by (subst has_integral_restrict) simp_all
- show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
- by (auto simp: box_def)
- { fix x assume "x \<in> A"
- moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x"
- by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
- ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1"
- by (simp add: indicator_def UN_box_eq_UNIV) }
-
- have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
- by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
- also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))"
- proof (intro ext emeasure_eq_ennreal_measure)
- fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)"
- by (intro emeasure_mono) auto
- then show "emeasure lborel (A \<inter> ?B n) \<noteq> top"
- by (auto simp: top_unique)
- qed
- finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A"
- using emeasure_eq_ennreal_measure[of lborel A] finite
- by (simp add: UN_box_eq_UNIV less_top)
- qed
-qed
-
-lemma nn_integral_has_integral:
- fixes f::"'a::euclidean_space \<Rightarrow> real"
- assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
- shows "(f has_integral r) UNIV"
-using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
- case (set A)
- then have "((\<lambda>x. 1) has_integral measure lborel A) A"
- by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
- with set show ?case
- by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
-next
- case (mult g c)
- then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r"
- by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult)
- with \<open>0 \<le> r\<close> \<open>0 \<le> c\<close>
- obtain r' where "(c = 0 \<and> r = 0) \<or> (0 \<le> r' \<and> (\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel) = ennreal r' \<and> r = c * r')"
- by (cases "\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel" rule: ennreal_cases)
- (auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric])
- with mult show ?case
- by (auto intro!: has_integral_cmult_real)
-next
- case (add g h)
- then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
- by (simp add: nn_integral_add)
- with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
- by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
- (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
- with add show ?case
- by (auto intro!: has_integral_add)
-next
- case (seq U)
- note seq(1)[measurable] and f[measurable]
-
- { fix i x
- have "U i x \<le> f x"
- using seq(5)
- apply (rule LIMSEQ_le_const)
- using seq(4)
- apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
- done }
- note U_le_f = this
-
- { fix i
- have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
- using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp
- then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p" "p \<le> r" "0 \<le> p"
- using seq(6) \<open>0\<le>r\<close> by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel" rule: ennreal_cases) (auto simp: top_unique)
- moreover note seq
- ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
- by auto }
- then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ennreal (U i x) \<partial>lborel) = ennreal (p i)"
- and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i"
- and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis
-
- have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique)
-
- have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
- proof (rule monotone_convergence_increasing)
- show "\<forall>k. U k integrable_on UNIV" using U_int by auto
- show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
- then show "bounded {integral UNIV (U k) |k. True}"
- using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
- show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
- using seq by auto
- qed
- moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"
- using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
- ultimately have "integral UNIV f = r"
- by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique)
- with * show ?case
- by (simp add: has_integral_integral)
-qed
-
-lemma nn_integral_lborel_eq_integral:
- fixes f::"'a::euclidean_space \<Rightarrow> real"
- assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
- shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f"
-proof -
- from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
- by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
- then show ?thesis
- using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique)
-qed
-
-lemma nn_integral_integrable_on:
- fixes f::"'a::euclidean_space \<Rightarrow> real"
- assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
- shows "f integrable_on UNIV"
-proof -
- from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
- by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
- then show ?thesis
- by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
-qed
-
-lemma nn_integral_has_integral_lborel:
- fixes f :: "'a::euclidean_space \<Rightarrow> real"
- assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
- assumes I: "(f has_integral I) UNIV"
- shows "integral\<^sup>N lborel f = I"
-proof -
- from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
- from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
- let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"
-
- note F(1)[THEN borel_measurable_simple_function, measurable]
-
- have "0 \<le> I"
- using I by (rule has_integral_nonneg) (simp add: nonneg)
-
- have F_le_f: "enn2real (F i x) \<le> f x" for i x
- using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "\<lambda>i. F i x"]
- by (cases "F i x" rule: ennreal_cases) auto
- let ?F = "\<lambda>i x. F i x * indicator (?B i) x"
- have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))"
- proof (subst nn_integral_monotone_convergence_SUP[symmetric])
- { fix x
- obtain j where j: "x \<in> ?B j"
- using UN_box_eq_UNIV by auto
-
- have "ennreal (f x) = (SUP i. F i x)"
- using F(4)[of x] nonneg[of x] by (simp add: max_def)
- also have "\<dots> = (SUP i. ?F i x)"
- proof (rule SUP_eq)
- fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x"
- using j F(2)
- by (intro bexI[of _ "max i j"])
- (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def)
- qed (auto intro!: F split: split_indicator)
- finally have "ennreal (f x) = (SUP i. ?F i x)" . }
- then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>lborel)"
- by simp
- qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator)
- also have "\<dots> \<le> ennreal I"
- proof (rule SUP_least)
- fix i :: nat
- have finite_F: "(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>"
- proof (rule nn_integral_bound_simple_function)
- have "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} \<le>
- emeasure lborel (?B i)"
- by (intro emeasure_mono) (auto split: split_indicator)
- then show "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"
- by (auto simp: less_top[symmetric] top_unique)
- qed (auto split: split_indicator
- intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal)
-
- have int_F: "(\<lambda>x. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV"
- using F(4) finite_F
- by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg)
-
- have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) =
- (\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel)"
- using F(3,4)
- by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator)
- also have "\<dots> = ennreal (integral UNIV (\<lambda>x. enn2real (F i x) * indicator (?B i) x))"
- using F
- by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F])
- (auto split: split_indicator intro: enn2real_nonneg)
- also have "\<dots> \<le> ennreal I"
- by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f
- simp: \<open>0 \<le> I\<close> split: split_indicator )
- finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ennreal I" .
- qed
- finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) < \<infinity>"
- by (auto simp: less_top[symmetric] top_unique)
- from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis
- by (simp add: integral_unique)
-qed
-
-lemma has_integral_iff_emeasure_lborel:
- fixes A :: "'a::euclidean_space set"
- assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
- shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
-proof (cases "emeasure lborel A = \<infinity>")
- case emeasure_A: True
- have "\<not> (\<lambda>x. 1::real) integrable_on A"
- proof
- assume int: "(\<lambda>x. 1::real) integrable_on A"
- then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
- unfolding indicator_def[abs_def] integrable_restrict_univ .
- then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
- by auto
- from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
- by (simp add: ennreal_indicator)
- qed
- with emeasure_A show ?thesis
- by auto
-next
- case False
- then have "((\<lambda>x. 1) has_integral measure lborel A) A"
- by (simp add: has_integral_measure_lborel less_top)
- with False show ?thesis
- by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
-qed
-
-lemma has_integral_integral_real:
- fixes f::"'a::euclidean_space \<Rightarrow> real"
- assumes f: "integrable lborel f"
- shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
-using f proof induct
- case (base A c) then show ?case
- by (auto intro!: has_integral_mult_left simp: )
- (simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel)
-next
- case (add f g) then show ?case
- by (auto intro!: has_integral_add)
-next
- case (lim f s)
- show ?case
- proof (rule has_integral_dominated_convergence)
- show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact
- show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV"
- using \<open>integrable lborel f\<close>
- by (intro nn_integral_integrable_on)
- (auto simp: integrable_iff_bounded abs_mult nn_integral_cmult ennreal_mult ennreal_mult_less_top)
- show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
- using lim by (auto simp add: abs_mult)
- show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x"
- using lim by auto
- show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f"
- using lim lim(1)[THEN borel_measurable_integrable]
- by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
- qed
-qed
-
-context
- fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-begin
-
-lemma has_integral_integral_lborel:
- assumes f: "integrable lborel f"
- shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
-proof -
- have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV"
- using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto
- also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f"
- by (simp add: fun_eq_iff euclidean_representation)
- also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f"
- using f by (subst (2) eq_f[symmetric]) simp
- finally show ?thesis .
-qed
-
-lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV"
- using has_integral_integral_lborel by auto
-
-lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)"
- using has_integral_integral_lborel by auto
-
-end
-
-subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
-
lemma emeasure_bounded_finite:
assumes "bounded A" shows "emeasure lborel A < \<infinity>"
proof -
@@ -1149,233 +780,4 @@
by (auto simp: mult.commute)
qed
-text \<open>
-
-For the positive integral we replace continuity with Borel-measurability.
-
-\<close>
-
-lemma
- fixes f :: "real \<Rightarrow> real"
- assumes [measurable]: "f \<in> borel_measurable borel"
- assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"
- shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn)
- and has_bochner_integral_FTC_Icc_nonneg:
- "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
- and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
- and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int)
-proof -
- have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x"
- using f(2) by (auto split: split_indicator)
-
- have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b\<Longrightarrow> F x \<le> F y" for x y
- using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
-
- have "(f has_integral F b - F a) {a..b}"
- by (intro fundamental_theorem_of_calculus)
- (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
- intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
- then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
- unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a]
- by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
- then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
- by (rule nn_integral_has_integral_lborel[OF *])
- then show ?has
- by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono \<open>a \<le> b\<close>)
- then show ?eq ?int
- unfolding has_bochner_integral_iff by auto
- show ?nn
- by (subst nn[symmetric])
- (auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator)
-qed
-
-lemma
- fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
- assumes "a \<le> b"
- assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
- assumes cont: "continuous_on {a .. b} f"
- shows has_bochner_integral_FTC_Icc:
- "has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has)
- and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq)
-proof -
- let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
- have int: "integrable lborel ?f"
- using borel_integrable_compact[OF _ cont] by auto
- have "(f has_integral F b - F a) {a..b}"
- using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
- moreover
- have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
- using has_integral_integral_lborel[OF int]
- unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
- by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
- ultimately show ?eq
- by (auto dest: has_integral_unique)
- then show ?has
- using int by (auto simp: has_bochner_integral_iff)
-qed
-
-lemma
- fixes f :: "real \<Rightarrow> real"
- assumes "a \<le> b"
- assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
- assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
- shows has_bochner_integral_FTC_Icc_real:
- "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
- and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
-proof -
- have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
- unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
- using deriv by (auto intro: DERIV_subset)
- have 2: "continuous_on {a .. b} f"
- using cont by (intro continuous_at_imp_continuous_on) auto
- show ?has ?eq
- using has_bochner_integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2]
- by (auto simp: mult.commute)
-qed
-
-lemma nn_integral_FTC_atLeast:
- fixes f :: "real \<Rightarrow> real"
- assumes f_borel: "f \<in> borel_measurable borel"
- assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
- assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
- assumes lim: "(F \<longlongrightarrow> T) at_top"
- shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
-proof -
- let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x"
- let ?fR = "\<lambda>x. ennreal (f x) * indicator {a ..} x"
-
- have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
- using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
- then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
- by (intro tendsto_le_const[OF _ lim])
- (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
-
- have "(SUP i::nat. ?f i x) = ?fR x" for x
- proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
- from reals_Archimedean2[of "x - a"] guess n ..
- then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
- by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
- then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
- by (rule Lim_eventually)
- qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
- then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
- by simp
- also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
- proof (rule nn_integral_monotone_convergence_SUP)
- show "incseq ?f"
- using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
- show "\<And>i. (?f i) \<in> borel_measurable lborel"
- using f_borel by auto
- qed
- also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))"
- by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
- also have "\<dots> = T - F a"
- proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
- have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
- apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
- apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
- apply (rule filterlim_real_sequentially)
- done
- then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
- by (simp add: F_mono F_le_T tendsto_diff)
- qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
- finally show ?thesis .
-qed
-
-lemma integral_power:
- "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
-proof (subst integral_FTC_Icc_real)
- fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
- by (intro derivative_eq_intros) auto
-qed (auto simp: field_simps simp del: of_nat_Suc)
-
-subsection \<open>Integration by parts\<close>
-
-lemma integral_by_parts_integrable:
- fixes f g F G::"real \<Rightarrow> real"
- assumes "a \<le> b"
- assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
- assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
- assumes [intro]: "!!x. DERIV F x :> f x"
- assumes [intro]: "!!x. DERIV G x :> g x"
- shows "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
- by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)
-
-lemma integral_by_parts:
- fixes f g F G::"real \<Rightarrow> real"
- assumes [arith]: "a \<le> b"
- assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
- assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
- assumes [intro]: "!!x. DERIV F x :> f x"
- assumes [intro]: "!!x. DERIV G x :> g x"
- shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
- = F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
-proof-
- have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
- by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
- (auto intro!: DERIV_isCont)
-
- have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
- (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
- apply (subst integral_add[symmetric])
- apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
- by (auto intro!: DERIV_isCont integral_cong split:split_indicator)
-
- thus ?thesis using 0 by auto
-qed
-
-lemma integral_by_parts':
- fixes f g F G::"real \<Rightarrow> real"
- assumes "a \<le> b"
- assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
- assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
- assumes "!!x. DERIV F x :> f x"
- assumes "!!x. DERIV G x :> g x"
- shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
- = F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
- using integral_by_parts[OF assms] by (simp add: ac_simps)
-
-lemma has_bochner_integral_even_function:
- fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
- assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
- assumes even: "\<And>x. f (- x) = f x"
- shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
-proof -
- have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
- by (auto split: split_indicator)
- have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
- by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
- (auto simp: indicator even f)
- with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)"
- by (rule has_bochner_integral_add)
- then have "has_bochner_integral lborel f (x + x)"
- by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
- (auto split: split_indicator)
- then show ?thesis
- by (simp add: scaleR_2)
-qed
-
-lemma has_bochner_integral_odd_function:
- fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
- assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
- assumes odd: "\<And>x. f (- x) = - f x"
- shows "has_bochner_integral lborel f 0"
-proof -
- have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
- by (auto split: split_indicator)
- have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
- by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
- (auto simp: indicator odd f)
- from has_bochner_integral_minus[OF this]
- have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
- by simp
- with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
- by (rule has_bochner_integral_add)
- then have "has_bochner_integral lborel f (x + - x)"
- by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
- (auto split: split_indicator)
- then show ?thesis
- by simp
-qed
-
end
--- a/src/HOL/Analysis/Linear_Algebra.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Fri Sep 16 13:56:51 2016 +0200
@@ -10,6 +10,30 @@
"~~/src/HOL/Library/Infinite_Set"
begin
+lemma linear_simps:
+ assumes "bounded_linear f"
+ shows
+ "f (a + b) = f a + f b"
+ "f (a - b) = f a - f b"
+ "f 0 = 0"
+ "f (- a) = - f a"
+ "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
+proof -
+ interpret f: bounded_linear f by fact
+ show "f (a + b) = f a + f b" by (rule f.add)
+ show "f (a - b) = f a - f b" by (rule f.diff)
+ show "f 0 = 0" by (rule f.zero)
+ show "f (- a) = - f a" by (rule f.minus)
+ show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
+qed
+
+lemma bounded_linearI:
+ assumes "\<And>x y. f (x + y) = f x + f y"
+ and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
+ and "\<And>x. norm (f x) \<le> norm x * K"
+ shows "bounded_linear f"
+ using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
+
subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75)
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Fri Sep 16 13:56:51 2016 +0200
@@ -243,27 +243,6 @@
lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
by (auto intro: setsum_nonneg)
-lemma content_closed_interval:
- fixes a :: "'a::ordered_euclidean_space"
- assumes "a \<le> b"
- shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
- using content_cbox[of a b] assms
- by (simp add: cbox_interval eucl_le[where 'a='a])
-
-lemma integrable_const_ivl[intro]:
- fixes a::"'a::ordered_euclidean_space"
- shows "(\<lambda>x. c) integrable_on {a .. b}"
- unfolding cbox_interval[symmetric]
- by (rule integrable_const)
-
-lemma integrable_on_subinterval:
- fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
- assumes "f integrable_on s"
- and "{a .. b} \<subseteq> s"
- shows "f integrable_on {a .. b}"
- using integrable_on_subcbox[of f s a b] assms
- by (simp add: cbox_interval)
-
lemma
fixes a b::"'a::ordered_euclidean_space"
shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
--- a/src/HOL/Analysis/Set_Integral.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Sep 16 13:56:51 2016 +0200
@@ -7,7 +7,7 @@
*)
theory Set_Integral
- imports Bochner_Integration Lebesgue_Measure
+ imports Equivalence_Lebesgue_Henstock_Integration
begin
(*
@@ -85,7 +85,7 @@
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)
+ using assms by (auto intro!: Bochner_Integration.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"
@@ -118,22 +118,22 @@
(* 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)
+ by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.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)
+ by (subst integral_mult_right_zero[symmetric]) auto
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)
+ by (subst integral_mult_left_zero[symmetric]) auto
lemma set_integral_divide_zero [simp]:
fixes a :: "'a::{real_normed_field, field, 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)
+ by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
(auto split: split_indicator)
lemma set_integrable_scaleR_right [simp, intro]:
@@ -184,7 +184,7 @@
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))"
by (subst lborel_integral_real_affine[where c="-1" and t=0])
- (auto intro!: integral_cong split: split_indicator)
+ (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
(* question: why do we have this for negation, but multiplication by a constant
requires an integrability assumption? *)
@@ -194,7 +194,7 @@
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)
+ (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
lemma set_integral_mono:
fixes f g :: "_ \<Rightarrow> real"
@@ -254,7 +254,7 @@
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
+ from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
qed
@@ -410,7 +410,7 @@
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 (rule Bochner_Integration.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
--- a/src/HOL/Library/Inner_Product.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Library/Inner_Product.thy Fri Sep 16 13:56:51 2016 +0200
@@ -260,6 +260,11 @@
end
+lemma
+ shows real_inner_1_left[simp]: "inner 1 x = x"
+ and real_inner_1_right[simp]: "inner x 1 = x"
+ by simp_all
+
instantiation complex :: real_inner
begin
--- a/src/HOL/Probability/Characteristic_Functions.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy Fri Sep 16 13:56:51 2016 +0200
@@ -316,13 +316,13 @@
then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
by (simp add: integ_c)
also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
- unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
+ unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
- by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
+ by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
proof (rule integral_mono)
show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
- by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
+ by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
show "integrable M (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
unfolding power_abs[symmetric]
by (intro integrable_mult_right integrable_abs integrable_moments) simp
@@ -360,16 +360,16 @@
then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
by (simp add: integ_c)
also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
- unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
+ unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
- by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
+ by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
also have "\<dots> \<le> expectation (\<lambda>x. min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^(Suc n) / fact (Suc n)))"
(is "_ \<le> expectation ?f")
proof (rule integral_mono)
show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
- by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
+ by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
show "integrable M ?f"
- by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"])
+ by (rule Bochner_Integration.integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"])
(auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
show "cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)) \<le> ?f x" for x
using iexp_approx1[of "t * x" n] iexp_approx2[of "t * x" n]
@@ -377,9 +377,9 @@
qed
also have "\<dots> = (\<bar>t\<bar>^n / fact (Suc n)) * expectation (\<lambda>x. min (2 * \<bar>x\<bar>^n * Suc n) (\<bar>t\<bar> * \<bar>x\<bar>^Suc n))"
unfolding *
- proof (rule integral_mult_right)
+ proof (rule Bochner_Integration.integral_mult_right)
show "integrable M (\<lambda>x. min (2 * \<bar>x\<bar> ^ n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar> ^ Suc n))"
- by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"])
+ by (rule Bochner_Integration.integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"])
(auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
qed
finally show ?thesis
--- a/src/HOL/Probability/Distributions.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Distributions.thy Fri Sep 16 13:56:51 2016 +0200
@@ -608,7 +608,7 @@
using D by (rule entropy_distr) simp
also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) =
(\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
- by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
+ by (intro Bochner_Integration.integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
also have "\<dots> = (ln l - 1) / ln b"
by simp
finally show ?thesis
@@ -750,7 +750,7 @@
uniform_distributed_bounds[of X a b]
uniform_distributed_measure[of X a b]
distributed_measurable[of M lborel X]
- by (auto intro!: uniform_distrI_borel_atLeastAtMost)
+ by (auto intro!: uniform_distrI_borel_atLeastAtMost simp del: content_real_if)
lemma (in prob_space) uniform_distributed_expectation:
fixes a b :: real
@@ -762,13 +762,13 @@
have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) =
(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
- by (intro integral_cong) auto
+ by (intro Bochner_Integration.integral_cong) auto
also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
proof (subst integral_FTC_Icc_real)
fix x
show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
using uniform_distributed_params[OF D]
- by (auto intro!: derivative_eq_intros)
+ by (auto intro!: derivative_eq_intros simp del: content_real_if)
show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
using uniform_distributed_params[OF D]
by (auto intro!: isCont_divide)
@@ -791,12 +791,12 @@
have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
have "(\<integral>x. x\<^sup>2 * (?D x) \<partial>lborel) = (\<integral>x. x\<^sup>2 * (indicator {a - ?\<mu> .. b - ?\<mu>} x) / measure lborel {a .. b} \<partial>lborel)"
- by (intro integral_cong) (auto split: split_indicator)
+ by (intro Bochner_Integration.integral_cong) (auto split: split_indicator)
also have "\<dots> = (b - a)\<^sup>2 / 12"
by (simp add: integral_power uniform_distributed_expectation[OF D])
(simp add: eval_nat_numeral field_simps )
finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
-qed (auto intro: D simp: measure_nonneg)
+qed (auto intro: D simp del: content_real_if)
subsection \<open>Normal distribution\<close>
@@ -949,7 +949,7 @@
proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI)
fix b :: real assume b: "0 \<le> b"
have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = (\<integral>x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \<partial>lborel)"
- unfolding integral_mult_right_zero[symmetric] by (intro integral_cong) auto
+ unfolding integral_mult_right_zero[symmetric] by (intro Bochner_Integration.integral_cong) auto
also have "\<dots> = exp (- b\<^sup>2) * b ^ (Suc k) - exp (- 0\<^sup>2) * 0 ^ (Suc k) -
(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel)"
by (rule integral_by_parts')
@@ -957,7 +957,7 @@
simp: diff_Suc of_nat_Suc field_simps split: nat.split)
also have "(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel) =
(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
- by (intro integral_cong) auto
+ by (intro Bochner_Integration.integral_cong) auto
finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) =
exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
by (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
@@ -1361,10 +1361,10 @@
have "entropy b lborel X = - (\<integral> x. normal_density \<mu> \<sigma> x * log b (normal_density \<mu> \<sigma> x) \<partial>lborel)"
using D by (rule entropy_distr) simp
also have "\<dots> = - (\<integral> x. normal_density \<mu> \<sigma> x * (- ln (2 * pi * \<sigma>\<^sup>2) - (x - \<mu>)\<^sup>2 / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
- by (intro arg_cong[where f="uminus"] integral_cong)
+ by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong)
(auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt)
also have "\<dots> = - (\<integral>x. - (normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
- by (intro arg_cong[where f="uminus"] integral_cong) (auto simp: divide_simps field_simps)
+ by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) (auto simp: divide_simps field_simps)
also have "\<dots> = (\<integral>x. normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2 \<partial>lborel) / (2 * ln b)"
by (simp del: minus_add_distrib)
also have "\<dots> = (ln (2 * pi * \<sigma>\<^sup>2) + 1) / (2 * ln b)"
--- a/src/HOL/Probability/Giry_Monad.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Fri Sep 16 13:56:51 2016 +0200
@@ -862,15 +862,15 @@
show ?integrable
using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
- proof(rule integral_cong)
+ proof(rule Bochner_Integration.integral_cong)
fix M'
assume "M' \<in> space M"
with sets_eq_imp_space_eq[OF M] have "space M' = space N"
by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
- with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
+ with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: Bochner_Integration.integral_empty)
qed simp
then show ?integral
- using M * by(simp add: integral_empty)
+ using M * by(simp add: Bochner_Integration.integral_empty)
next
assume *: "space N \<noteq> {}"
@@ -1213,7 +1213,7 @@
also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _])
finally show ?integral by(simp add: bind_nonempty''[where N=K])
-qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
+qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite Bochner_Integration.integral_empty)
lemma (in prob_space) prob_space_bind:
assumes ae: "AE x in M. prob_space (N x)"
--- a/src/HOL/Probability/Information.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Information.thy Fri Sep 16 13:56:51 2016 +0200
@@ -840,7 +840,7 @@
also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
unfolding distributed_distr_eq_density[OF X] using Px Px_nn
apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
- by (subst integral_density) (auto simp del: integral_indicator intro!: integral_cong)
+ by (subst integral_density) (auto simp del: integral_indicator intro!: Bochner_Integration.integral_cong)
also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
@@ -901,11 +901,11 @@
have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
(\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
using uniform_distributed_params[OF X]
- by (intro integral_cong) (auto split: split_indicator simp: log_divide_eq zero_less_measure_iff)
+ by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: log_divide_eq zero_less_measure_iff)
show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
log b (measure MX A)"
unfolding eq using uniform_distributed_params[OF X]
- by (subst integral_mult_right) (auto simp: measure_def less_top[symmetric] intro!: integrable_real_indicator)
+ by (subst Bochner_Integration.integral_mult_right) (auto simp: measure_def less_top[symmetric] intro!: integrable_real_indicator)
qed simp
lemma (in information_space) entropy_simple_distributed:
@@ -1038,8 +1038,8 @@
apply (subst mi_eq)
apply (subst mutual_information_distr[OF S TP Px Px_nn Pyz _ Pxyz])
apply (auto simp: space_pair_measure)
- apply (subst integral_diff[symmetric])
- apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
+ apply (subst Bochner_Integration.integral_diff[symmetric])
+ apply (auto intro!: integral_cong_AE simp: split_beta' simp del: Bochner_Integration.integral_diff)
done
let ?P = "density (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) Pxyz"
@@ -1112,7 +1112,7 @@
done
have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
- apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integrable_diff[OF I1 I2]])
+ apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ Bochner_Integration.integrable_diff[OF I1 I2]])
using ae
apply (auto simp: split_beta')
done
@@ -1297,8 +1297,8 @@
apply simp
apply simp
apply (simp add: space_pair_measure)
- apply (subst integral_diff[symmetric])
- apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
+ apply (subst Bochner_Integration.integral_diff[symmetric])
+ apply (auto intro!: integral_cong_AE simp: split_beta' simp del: Bochner_Integration.integral_diff)
done
let ?P = "density (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) Pxyz"
@@ -1373,7 +1373,7 @@
(auto simp: split_beta' AE_density space_pair_measure intro!: AE_I2 ennreal_neg)
have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
- apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integrable_diff[OF I1 I2]])
+ apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ Bochner_Integration.integrable_diff[OF I1 I2]])
using ae
apply (auto simp: split_beta')
done
@@ -1593,7 +1593,7 @@
also have "\<dots> = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^sub>M T))"
using b_gt_1
by (subst distributed_transform_integral[OF Pxy _ Py, where T=snd])
- (auto intro!: integral_cong simp: space_pair_measure)
+ (auto intro!: Bochner_Integration.integral_cong simp: space_pair_measure)
finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^sub>M T))" .
have **: "\<And>x. x \<in> space (S \<Otimes>\<^sub>M T) \<Longrightarrow> 0 \<le> Pxy x"
@@ -1618,7 +1618,7 @@
apply auto
done
also have "\<dots> = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) - - (\<integral>x. Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
- by (simp add: integral_diff[OF I1 I2])
+ by (simp add: Bochner_Integration.integral_diff[OF I1 I2])
finally show ?thesis
using conditional_entropy_generic_eq[OF S T Py Py_nn Pxy Pxy_nn, simplified]
entropy_distr[OF Pxy **, simplified] e_eq
@@ -1785,9 +1785,9 @@
have "entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) = integral\<^sup>L (S \<Otimes>\<^sub>M T) ?f"
unfolding X Y XY
- apply (subst integral_diff)
- apply (intro integrable_diff Ixy Ix Iy)+
- apply (subst integral_diff)
+ apply (subst Bochner_Integration.integral_diff)
+ apply (intro Bochner_Integration.integrable_diff Ixy Ix Iy)+
+ apply (subst Bochner_Integration.integral_diff)
apply (intro Ixy Ix Iy)+
apply (simp add: field_simps)
done
--- a/src/HOL/Probability/Levy.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Levy.thy Fri Sep 16 13:56:51 2016 +0200
@@ -136,9 +136,9 @@
have "(CLBINT t=-T..T. ?F t * \<phi> t) =
(CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))"
using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def
- by (auto split: split_indicator intro!: integral_cong)
+ by (auto split: split_indicator intro!: Bochner_Integration.integral_cong)
also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))"
- by (auto intro!: integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
+ by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
also have "\<dots> = (CLINT x | M. (CLBINT t. ?f' (t, x)))"
proof (intro P.Fubini_integral [symmetric] integrableI_bounded_set [where B="b - a"])
show "emeasure (lborel \<Otimes>\<^sub>M M) ({- T<..<T} \<times> space M) < \<infinity>"
@@ -151,7 +151,7 @@
qed (auto split: split_indicator split_indicator_asm)
also have "\<dots> = (CLINT x | M. (complex_of_real (2 * (sgn (x - a) *
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))))"
- using main_eq by (intro integral_cong, auto)
+ using main_eq by (intro Bochner_Integration.integral_cong, auto)
also have "\<dots> = complex_of_real (LINT x | M. (2 * (sgn (x - a) *
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))"
by (rule integral_complex_of_real)
@@ -336,11 +336,11 @@
(CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))"
unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult)
also have "\<dots> = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))"
- by (rule integral_cong) (auto split: split_indicator)
+ by (rule Bochner_Integration.integral_cong) (auto split: split_indicator)
also have "\<dots> = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))"
using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta')
also have "\<dots> = (CLINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))"
- using \<open>u > 0\<close> by (intro integral_cong, auto simp add: * simp del: of_real_mult)
+ using \<open>u > 0\<close> by (intro Bochner_Integration.integral_cong, auto simp add: * simp del: of_real_mult)
also have "\<dots> = (LINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))"
by (rule integral_complex_of_real)
finally have "Re (CLBINT t:{-u..u}. 1 - char (M n) t) =
--- a/src/HOL/Probability/Probability_Mass_Function.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Sep 16 13:56:51 2016 +0200
@@ -167,7 +167,7 @@
lemma pmf_nonneg[simp]: "0 \<le> pmf p x"
by transfer simp
-
+
lemma pmf_not_neg [simp]: "\<not>pmf p x < 0"
by (simp add: not_less pmf_nonneg)
@@ -546,7 +546,7 @@
lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x"
proof -
- have "ennreal (measure_pmf.prob (return_pmf x) A) =
+ have "ennreal (measure_pmf.prob (return_pmf x) A) =
emeasure (measure_pmf (return_pmf x)) A"
by (simp add: measure_pmf.emeasure_eq_measure)
also have "\<dots> = ennreal (indicator A x)" by (simp add: ennreal_indicator)
@@ -778,10 +778,10 @@
have "1 = measure (measure_pmf M) UNIV" by simp
also have "\<dots> = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})"
by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
- also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}"
+ also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}"
by (simp add: measure_pmf_single)
also have "measure (measure_pmf N) (UNIV - {x}) \<le> measure (measure_pmf M) (UNIV - {x})"
- by (subst (1 2) integral_pmf [symmetric])
+ by (subst (1 2) integral_pmf [symmetric])
(intro integral_mono integrable_pmf, simp_all add: ge)
also have "measure (measure_pmf M) {x} + \<dots> = 1"
by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
@@ -803,7 +803,7 @@
by unfold_locales
have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)"
- by (rule integral_cong) (auto intro!: integral_pmf_restrict)
+ by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict)
also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)"
by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
countable_set_pmf borel_measurable_count_space)
@@ -815,7 +815,7 @@
by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
countable_set_pmf borel_measurable_count_space)
also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)"
- by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
+ by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" .
qed
@@ -1629,7 +1629,7 @@
lemma map_pmf_of_set:
assumes "finite A" "A \<noteq> {}"
- shows "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))"
+ shows "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))"
(is "?lhs = ?rhs")
proof (intro pmf_eqI)
fix x
@@ -1641,13 +1641,13 @@
lemma pmf_bind_pmf_of_set:
assumes "A \<noteq> {}" "finite A"
- shows "pmf (bind_pmf (pmf_of_set A) f) x =
+ shows "pmf (bind_pmf (pmf_of_set A) f) x =
(\<Sum>xa\<in>A. pmf (f xa) x) / real_of_nat (card A)" (is "?lhs = ?rhs")
proof -
from assms have "card A > 0" by auto
with assms have "ennreal ?lhs = ennreal ?rhs"
- by (subst ennreal_pmf_bind)
- (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric]
+ by (subst ennreal_pmf_bind)
+ (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric]
setsum_nonneg ennreal_of_nat_eq_real_of_nat)
thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: setsum_nonneg divide_nonneg_nonneg)
qed
@@ -1675,10 +1675,10 @@
qed
text \<open>
- Choosing an element uniformly at random from the union of a disjoint family
- of finite non-empty sets with the same size is the same as first choosing a set
- from the family uniformly at random and then choosing an element from the chosen set
- uniformly at random.
+ Choosing an element uniformly at random from the union of a disjoint family
+ of finite non-empty sets with the same size is the same as first choosing a set
+ from the family uniformly at random and then choosing an element from the chosen set
+ uniformly at random.
\<close>
lemma pmf_of_set_UN:
assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
@@ -1694,8 +1694,8 @@
by (subst pmf_of_set) auto
also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def)
- also from assms
- have "indicator (\<Union>x\<in>A. f x) x / real \<dots> =
+ also from assms
+ have "indicator (\<Union>x\<in>A. f x) x / real \<dots> =
indicator (\<Union>x\<in>A. f x) x / (n * real (card A))"
by (simp add: setsum_divide_distrib [symmetric] mult_ac)
also from assms have "indicator (\<Union>x\<in>A. f x) x = (\<Sum>y\<in>A. indicator (f y) x)"
@@ -1794,17 +1794,17 @@
lemma replicate_pmf_1: "replicate_pmf 1 p = map_pmf (\<lambda>x. [x]) p"
by (simp add: map_pmf_def bind_return_pmf)
-
-lemma set_replicate_pmf:
+
+lemma set_replicate_pmf:
"set_pmf (replicate_pmf n p) = {xs\<in>lists (set_pmf p). length xs = n}"
by (induction n) (auto simp: length_Suc_conv)
lemma replicate_pmf_distrib:
- "replicate_pmf (m + n) p =
+ "replicate_pmf (m + n) p =
do {xs \<leftarrow> replicate_pmf m p; ys \<leftarrow> replicate_pmf n p; return_pmf (xs @ ys)}"
by (induction m) (simp_all add: bind_return_pmf bind_return_pmf' bind_assoc_pmf)
-lemma power_diff':
+lemma power_diff':
assumes "b \<le> a"
shows "x ^ (a - b) = (if x = 0 \<and> a = b then 1 else x ^ a / (x::'a::field) ^ b)"
proof (cases "x = 0")
@@ -1812,12 +1812,12 @@
with assms show ?thesis by (cases "a - b") simp_all
qed (insert assms, simp_all add: power_diff)
-
+
lemma binomial_pmf_Suc:
assumes "p \<in> {0..1}"
- shows "binomial_pmf (Suc n) p =
- do {b \<leftarrow> bernoulli_pmf p;
- k \<leftarrow> binomial_pmf n p;
+ shows "binomial_pmf (Suc n) p =
+ do {b \<leftarrow> bernoulli_pmf p;
+ k \<leftarrow> binomial_pmf n p;
return_pmf ((if b then 1 else 0) + k)}" (is "_ = ?rhs")
proof (intro pmf_eqI)
fix k
@@ -1835,14 +1835,14 @@
lemma binomial_pmf_altdef:
assumes "p \<in> {0..1}"
shows "binomial_pmf n p = map_pmf (length \<circ> filter id) (replicate_pmf n (bernoulli_pmf p))"
- by (induction n)
- (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf
+ by (induction n)
+ (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf
bind_return_pmf' binomial_pmf_0 intro!: bind_pmf_cong)
subsection \<open>PMFs from assiciation lists\<close>
-definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where
+definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where
"pmf_of_list xs = embed_pmf (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
definition pmf_of_list_wf where
@@ -1870,12 +1870,12 @@
from Cons.prems have "snd x \<ge> 0" by simp
moreover have "b \<ge> 0" if "(a,b) \<in> set xs" for a b
using Cons.prems[of b] that by force
- ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) =
- (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) +
+ ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) =
+ (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) +
ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
- by (intro nn_integral_cong, subst ennreal_plus [symmetric])
+ by (intro nn_integral_cong, subst ennreal_plus [symmetric])
(auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg)
- also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) +
+ also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) +
(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
by (intro nn_integral_add)
(force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+
@@ -1934,20 +1934,20 @@
proof -
have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
by simp
- also from assms
+ also from assms
have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
- also from assms
+ also from assms
have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
- also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
+ also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
also have "?S = (\<Sum>x\<in>set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)"
using assms by (intro setsum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
- also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
+ also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
using assms by (simp add: pmf_pmf_of_list)
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). sum_list (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
@@ -1955,17 +1955,17 @@
also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
by (intro setsum.cong refl, subst sum_list_map_filter', subst sum_list_setsum_nth) simp
- also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
+ also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
by (rule setsum.commute)
- also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
+ also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
(\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
by (auto intro!: setsum.cong setsum.neutral)
also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
by (intro setsum.cong refl) (simp_all add: setsum.delta)
also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all
- finally show ?thesis .
+ finally show ?thesis .
qed
lemma measure_pmf_of_list:
@@ -1989,7 +1989,7 @@
"sum_list (filter (\<lambda>x. x \<noteq> 0) xs) = sum_list xs"
by (induction xs) simp_all
(* END MOVE *)
-
+
lemma set_pmf_of_list_eq:
assumes "pmf_of_list_wf xs" "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0"
shows "set_pmf (pmf_of_list xs) = fst ` set xs"
@@ -2000,13 +2000,13 @@
from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
- ultimately have "y = 0" using assms(1)
+ ultimately have "y = 0" using assms(1)
by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
with assms(2) y have False by force
}
thus "fst ` set xs \<subseteq> set_pmf (pmf_of_list xs)" by blast
qed (insert set_pmf_of_list[OF assms(1)], simp_all)
-
+
lemma pmf_of_list_remove_zeros:
assumes "pmf_of_list_wf xs"
defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
--- a/src/HOL/Probability/Probability_Measure.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Fri Sep 16 13:56:51 2016 +0200
@@ -225,7 +225,7 @@
using prob_space by (simp add: X)
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
using \<open>x \<in> I\<close> \<open>open I\<close> X(2)
- apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff
+ apply (intro integral_mono_AE Bochner_Integration.integrable_add Bochner_Integration.integrable_mult_right Bochner_Integration.integrable_diff
integrable_const X q)
apply (elim eventually_mono)
apply (intro convex_le_Inf_differential)
--- a/src/HOL/Probability/SPMF.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy Fri Sep 16 13:56:51 2016 +0200
@@ -554,11 +554,11 @@
have "?lhs = \<integral> x. ?f x \<partial>measure_pmf p"
by(simp add: bind_spmf_def pmf_bind)
also have "\<dots> = \<integral> x. ?f None * indicator {None} x + ?f x * indicator (range Some) x \<partial>measure_pmf p"
- by(rule integral_cong)(auto simp add: indicator_def)
+ by(rule Bochner_Integration.integral_cong)(auto simp add: indicator_def)
also have "\<dots> = (\<integral> x. ?f None * indicator {None} x \<partial>measure_pmf p) + (\<integral> x. ?f x * indicator (range Some) x \<partial>measure_pmf p)"
- by(rule integral_add)(auto 4 3 intro: integrable_real_mult_indicator measure_pmf.integrable_const_bound[where B=1] simp add: AE_measure_pmf_iff pmf_le_1)
+ by(rule Bochner_Integration.integral_add)(auto 4 3 intro: integrable_real_mult_indicator measure_pmf.integrable_const_bound[where B=1] simp add: AE_measure_pmf_iff pmf_le_1)
also have "\<dots> = pmf p None + \<integral> x. indicator (range Some) x * pmf (f (the x)) None \<partial>measure_pmf p"
- by(auto simp add: measure_measure_pmf_finite indicator_eq_0_iff intro!: integral_cong)
+ by(auto simp add: measure_measure_pmf_finite indicator_eq_0_iff intro!: Bochner_Integration.integral_cong)
also have "\<dots> = ?rhs" unfolding measure_spmf_def
by(subst integral_distr)(auto simp add: integral_restrict_space)
finally show ?thesis .
@@ -566,7 +566,7 @@
lemma spmf_bind: "spmf (p \<bind> f) y = \<integral> x. spmf (f x) y \<partial>measure_spmf p"
unfolding measure_spmf_def
-by(subst integral_distr)(auto simp add: bind_spmf_def pmf_bind integral_restrict_space indicator_eq_0_iff intro!: integral_cong split: option.split)
+by(subst integral_distr)(auto simp add: bind_spmf_def pmf_bind integral_restrict_space indicator_eq_0_iff intro!: Bochner_Integration.integral_cong split: option.split)
lemma ennreal_spmf_bind: "ennreal (spmf (p \<bind> f) x) = \<integral>\<^sup>+ y. spmf (f y) x \<partial>measure_spmf p"
by(auto simp add: bind_spmf_def ennreal_pmf_bind nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space intro: nn_integral_cong split: split_indicator option.split)
@@ -2688,7 +2688,7 @@
lemma pmf_try_spmf_None [simp]: "pmf (TRY p ELSE q) None = pmf p None * pmf q None" (is "?lhs = ?rhs")
proof -
have "?lhs = \<integral> x. pmf q None * indicator {None} x \<partial>measure_pmf p"
- unfolding try_spmf_def pmf_bind by(rule integral_cong)(simp_all split: option.split)
+ unfolding try_spmf_def pmf_bind by(rule Bochner_Integration.integral_cong)(simp_all split: option.split)
also have "\<dots> = ?rhs" by(simp add: measure_pmf_single)
finally show ?thesis .
qed
--- a/src/HOL/Probability/Sinc_Integral.thy Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy Fri Sep 16 13:56:51 2016 +0200
@@ -263,7 +263,7 @@
from lborel_integrable_real_affine[OF this, of t 0]
show ?thesis
unfolding interval_lebesgue_integral_0_infty
- by (rule integrable_bound) (auto simp: field_simps * split: split_indicator)
+ by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
qed
lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top"
@@ -291,7 +291,7 @@
fix x :: real assume x: "x \<noteq> 0" "x \<noteq> t"
have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> =
LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x"
- by (intro integral_cong) (auto split: split_indicator simp: abs_mult)
+ by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>. exp (- (y * x)))"
by (cases "x > 0")
(auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
@@ -315,7 +315,7 @@
also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
using \<open>0\<le>t\<close>
by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
- split: split_indicator intro!: integral_cong)
+ split: split_indicator intro!: Bochner_Integration.integral_cong)
also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
also have "... = pi / 2 - (LBINT u=0..\<infinity>. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))"