--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Sep 23 18:34:34 2016 +0200
@@ -6180,7 +6180,7 @@
unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
using assms
by auto
-
+
lemma integrable_stretch:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -9608,31 +9608,6 @@
by auto
qed
-
-subsection \<open>Absolute integrability (this is the same as Lebesgue integrability)\<close>
-
-definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46)
- where "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. (norm(f x))) integrable_on s"
-
-lemma absolutely_integrable_onI[intro?]:
- "f integrable_on s \<Longrightarrow>
- (\<lambda>x. (norm(f x))) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
- unfolding absolutely_integrable_on_def
- by auto
-
-lemma absolutely_integrable_onD[dest]:
- assumes "f absolutely_integrable_on s"
- shows "f integrable_on s"
- and "(\<lambda>x. norm (f x)) integrable_on s"
- using assms
- unfolding absolutely_integrable_on_def
- by auto
-
-(*lemma absolutely_integrable_on_trans[simp]:
- fixes f::"'n::euclidean_space \<Rightarrow> real"
- shows "(vec1 \<circ> f) absolutely_integrable_on s \<longleftrightarrow> f absolutely_integrable_on s"
- unfolding absolutely_integrable_on_def o_def by auto*)
-
lemma integral_norm_bound_integral:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "f integrable_on s"
@@ -9768,1174 +9743,6 @@
using assms
by auto
-lemma absolutely_integrable_le:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "f absolutely_integrable_on s"
- shows "norm (integral s f) \<le> integral s (\<lambda>x. norm (f x))"
- apply (rule integral_norm_bound_integral)
- using assms
- apply auto
- done
-
-lemma absolutely_integrable_0[intro]:
- "(\<lambda>x. 0) absolutely_integrable_on s"
- unfolding absolutely_integrable_on_def
- by auto
-
-lemma absolutely_integrable_cmul[intro]:
- "f absolutely_integrable_on s \<Longrightarrow>
- (\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s"
- unfolding absolutely_integrable_on_def
- using integrable_cmul[of f s c]
- using integrable_cmul[of "\<lambda>x. norm (f x)" s "\<bar>c\<bar>"]
- by auto
-
-lemma absolutely_integrable_neg[intro]:
- "f absolutely_integrable_on s \<Longrightarrow>
- (\<lambda>x. -f(x)) absolutely_integrable_on s"
- apply (drule absolutely_integrable_cmul[where c="-1"])
- apply auto
- done
-
-lemma absolutely_integrable_norm[intro]:
- "f absolutely_integrable_on s \<Longrightarrow>
- (\<lambda>x. norm (f x)) absolutely_integrable_on s"
- unfolding absolutely_integrable_on_def
- by auto
-
-lemma absolutely_integrable_abs[intro]:
- "f absolutely_integrable_on s \<Longrightarrow>
- (\<lambda>x. \<bar>f x::real\<bar>) absolutely_integrable_on s"
- apply (drule absolutely_integrable_norm)
- unfolding real_norm_def
- apply assumption
- done
-
-lemma absolutely_integrable_on_subinterval:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- shows "f absolutely_integrable_on s \<Longrightarrow>
- cbox a b \<subseteq> s \<Longrightarrow> f absolutely_integrable_on cbox a b"
- unfolding absolutely_integrable_on_def
- by (metis integrable_on_subcbox)
-
-lemma absolutely_integrable_bounded_variation:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "f absolutely_integrable_on UNIV"
- obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
- apply (rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
- apply safe
-proof goal_cases
- case prems: (1 d)
- note d = division_ofD[OF prems(2)]
- have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
- apply (rule setsum_mono,rule absolutely_integrable_le)
- apply (drule d(4))
- apply safe
- apply (rule absolutely_integrable_on_subinterval[OF assms])
- apply auto
- done
- also have "\<dots> \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
- apply (subst integral_combine_division_topdown[OF _ prems(2)])
- using integrable_on_subdivision[OF prems(2)]
- using assms
- apply auto
- done
- also have "\<dots> \<le> integral UNIV (\<lambda>x. norm (f x))"
- apply (rule integral_subset_le)
- using integrable_on_subdivision[OF prems(2)]
- using assms
- apply auto
- done
- finally show ?case .
-qed
-
-lemma helplemma:
- assumes "setsum (\<lambda>x. norm (f x - g x)) s < e"
- and "finite s"
- shows "\<bar>setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s\<bar> < e"
- unfolding setsum_subtractf[symmetric]
- apply (rule le_less_trans[OF setsum_abs])
- apply (rule le_less_trans[OF _ assms(1)])
- apply (rule setsum_mono)
- apply (rule norm_triangle_ineq3)
- done
-
-lemma bounded_variation_absolutely_integrable_interval:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes f: "f integrable_on cbox a b"
- and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
- shows "f absolutely_integrable_on cbox a b"
-proof -
- let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}"
- have D_1: "?D \<noteq> {}"
- by (rule elementary_interval[of a b]) auto
- have D_2: "bdd_above (?f`?D)"
- by (metis * mem_Collect_eq bdd_aboveI2)
- note D = D_1 D_2
- let ?S = "SUP x:?D. ?f x"
- show ?thesis
- apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
- apply (subst has_integral[of _ ?S])
- apply safe
- proof goal_cases
- case e: (1 e)
- then have "?S - e / 2 < ?S" by simp
- then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
- unfolding less_cSUP_iff[OF D] by auto
- note d' = division_ofD[OF this(1)]
-
- have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
- proof
- fix x
- have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
- apply (rule separate_point_closed)
- apply (rule closed_Union)
- apply (rule finite_subset[OF _ d'(1)])
- using d'(4)
- apply auto
- done
- then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
- by force
- qed
- from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
-
- have "e/2 > 0"
- using e by auto
- from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
- let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
- show ?case
- apply (rule_tac x="?g" in exI)
- apply safe
- proof -
- show "gauge ?g"
- using g(1) k(1)
- unfolding gauge_def
- by auto
- fix p
- assume "p tagged_division_of (cbox a b)" and "?g fine p"
- note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
- note p' = tagged_division_ofD[OF p(1)]
- define p' where "p' = {(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}"
- have gp': "g fine p'"
- using p(2)
- unfolding p'_def fine_def
- by auto
- have p'': "p' tagged_division_of (cbox a b)"
- apply (rule tagged_division_ofI)
- proof -
- show "finite p'"
- apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
- {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
- unfolding p'_def
- defer
- apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
- apply safe
- unfolding image_iff
- apply (rule_tac x="(i,x,l)" in bexI)
- apply auto
- done
- fix x k
- assume "(x, k) \<in> p'"
- then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
- unfolding p'_def by auto
- then guess i l by (elim exE) note il=conjunctD4[OF this]
- show "x \<in> k" and "k \<subseteq> cbox a b"
- using p'(2-3)[OF il(3)] il by auto
- show "\<exists>a b. k = cbox a b"
- unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
- apply safe
- unfolding inter_interval
- apply auto
- done
- next
- fix x1 k1
- assume "(x1, k1) \<in> p'"
- then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
- unfolding p'_def by auto
- then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this]
- fix x2 k2
- assume "(x2,k2)\<in>p'"
- then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
- unfolding p'_def by auto
- then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this]
- assume "(x1, k1) \<noteq> (x2, k2)"
- then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
- using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
- unfolding il1 il2
- by auto
- then show "interior k1 \<inter> interior k2 = {}"
- unfolding il1 il2 by auto
- next
- have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
- unfolding p'_def using d' by auto
- show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
- apply rule
- apply (rule Union_least)
- unfolding mem_Collect_eq
- apply (erule exE)
- apply (drule *[rule_format])
- apply safe
- proof -
- fix y
- assume y: "y \<in> cbox a b"
- then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
- unfolding p'(6)[symmetric] by auto
- then guess x l by (elim exE) note xl=conjunctD2[OF this]
- then have "\<exists>k. k \<in> d \<and> y \<in> k"
- using y unfolding d'(6)[symmetric] by auto
- then guess i .. note i = conjunctD2[OF this]
- have "x \<in> i"
- using fineD[OF p(3) xl(1)]
- using k(2)[OF i(1), of x]
- using i(2) xl(2)
- by auto
- then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
- unfolding p'_def Union_iff
- apply (rule_tac x="i \<inter> l" in bexI)
- using i xl
- apply auto
- done
- qed
- qed
-
- then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
- apply -
- apply (rule g(2)[rule_format])
- unfolding tagged_division_of_def
- apply safe
- apply (rule gp')
- done
- then have **: "\<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
- unfolding split_def
- using p''
- by (force intro!: helplemma)
-
- have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
- proof (safe, goal_cases)
- case prems: (2 _ _ x i l)
- have "x \<in> i"
- using fineD[OF p(3) prems(1)] k(2)[OF prems(2), of x] prems(4-)
- by auto
- then have "(x, i \<inter> l) \<in> p'"
- unfolding p'_def
- using prems
- apply safe
- apply (rule_tac x=x in exI)
- apply (rule_tac x="i \<inter> l" in exI)
- apply safe
- using prems
- apply auto
- done
- then show ?case
- using prems(3) by auto
- next
- fix x k
- assume "(x, k) \<in> p'"
- then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
- unfolding p'_def by auto
- then guess i l by (elim exE) note il=conjunctD4[OF this]
- then show "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
- apply (rule_tac x=x in exI)
- apply (rule_tac x=i in exI)
- apply (rule_tac x=l in exI)
- using p'(2)[OF il(3)]
- apply auto
- done
- qed
- have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
- apply (subst setsum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
- unfolding norm_eq_zero
- apply (rule integral_null)
- apply assumption
- apply rule
- done
- note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
-
- have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
- sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
- by arith
- show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
- unfolding real_norm_def
- apply (rule *[rule_format,OF **])
- apply safe
- apply(rule d(2))
- proof goal_cases
- case 1
- show ?case
- by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
- next
- case 2
- have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
- (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
- by auto
- have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
- proof (rule setsum_mono, goal_cases)
- case k: (1 k)
- from d'(4)[OF this] guess u v by (elim exE) note uv=this
- define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}"
- note uvab = d'(2)[OF k[unfolded uv]]
- have "d' division_of cbox u v"
- apply (subst d'_def)
- apply (rule division_inter_1)
- apply (rule division_of_tagged_division[OF p(1)])
- apply (rule uvab)
- done
- then have "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'"
- unfolding uv
- apply (subst integral_combine_division_topdown[of _ _ d'])
- apply (rule integrable_on_subcbox[OF assms(1) uvab])
- apply assumption
- apply (rule setsum_norm_le)
- apply auto
- 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 Setcompr_eq_image)
- apply (rule finite_imageI)+
- apply fact
- unfolding d'_def uv
- apply blast
- proof (rule, goal_cases)
- case prems: (1 i)
- then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
- by auto
- from this[unfolded mem_Collect_eq] guess l .. note l=this
- then have "cbox u v \<inter> l = {}"
- using prems by auto
- then show ?case
- using l by auto
- qed
- also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
- unfolding Setcompr_eq_image
- apply (rule setsum.reindex_nontrivial [unfolded o_def])
- apply (rule finite_imageI)
- apply (rule p')
- proof goal_cases
- case prems: (1 l y)
- have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
- apply (subst(2) interior_Int)
- apply (rule Int_greatest)
- defer
- apply (subst prems(4))
- apply auto
- done
- then have *: "interior (k \<inter> l) = {}"
- using snd_p(5)[OF prems(1-3)] by auto
- from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
- show ?case
- using *
- unfolding uv inter_interval content_eq_0_interior[symmetric]
- by auto
- qed
- finally show ?case .
- qed
- also have "\<dots> = (\<Sum>(i,l)\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (i\<inter>l) f))"
- apply (subst sum_sum_product[symmetric])
- apply fact
- using p'(1)
- apply auto
- done
- also have "\<dots> = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (case_prod op \<inter> x) f))"
- unfolding split_def ..
- also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
- unfolding *
- apply (rule setsum.reindex_nontrivial [symmetric, unfolded o_def])
- apply (rule finite_product_dependent)
- apply fact
- apply (rule finite_imageI)
- apply (rule p')
- unfolding split_paired_all mem_Collect_eq split_conv o_def
- proof -
- note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
- fix l1 l2 k1 k2
- assume as:
- "(l1, k1) \<noteq> (l2, k2)"
- "l1 \<inter> k1 = l2 \<inter> k2"
- "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
- "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
- then have "l1 \<in> d" and "k1 \<in> snd ` p"
- by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
- guess u1 v1 u2 v2 by (elim exE) note uv=this
- have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
- using as by auto
- then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
- apply -
- apply (erule disjE)
- apply (rule disjI2)
- apply (rule d'(5))
- prefer 4
- apply (rule disjI1)
- apply (rule *)
- using as
- apply auto
- done
- moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
- using as(2) by auto
- ultimately have "interior(l1 \<inter> k1) = {}"
- by auto
- then show "norm (integral (l1 \<inter> k1) f) = 0"
- unfolding uv inter_interval
- unfolding content_eq_0_interior[symmetric]
- by auto
- qed
- also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
- unfolding sum_p'
- apply (rule setsum.mono_neutral_right)
- apply (subst *)
- apply (rule finite_imageI[OF finite_product_dependent])
- apply fact
- apply (rule finite_imageI[OF p'(1)])
- apply safe
- proof goal_cases
- case (2 i ia l a b)
- then have "ia \<inter> b = {}"
- unfolding p'alt image_iff Bex_def not_ex
- apply (erule_tac x="(a, ia \<inter> b)" in allE)
- apply auto
- done
- then show ?case
- by auto
- next
- case (1 x a b)
- then show ?case
- unfolding p'_def
- apply safe
- apply (rule_tac x=i in exI)
- apply (rule_tac x=l in exI)
- unfolding snd_conv image_iff
- apply safe
- apply (rule_tac x="(a,l)" in bexI)
- apply auto
- done
- qed
- finally show ?case .
- next
- case 3
- let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
- have Sigma_alt: "\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}"
- by auto
- have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
- apply safe
- unfolding image_iff
- apply (rule_tac x="((x,l),i)" in bexI)
- apply auto
- done
- note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
- have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))"
- unfolding norm_scaleR
- apply (rule setsum.mono_neutral_left)
- apply (subst *)
- apply (rule finite_imageI)
- apply fact
- unfolding p'alt
- apply blast
- apply safe
- apply (rule_tac x=x in exI)
- apply (rule_tac x=i in exI)
- apply (rule_tac x=l in exI)
- apply auto
- done
- also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
- unfolding *
- apply (subst setsum.reindex_nontrivial)
- apply fact
- unfolding split_paired_all
- unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
- apply (elim conjE)
- proof -
- fix x1 l1 k1 x2 l2 k2
- assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
- "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
- from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
- from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
- by auto
- then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
- apply -
- apply (erule disjE)
- apply (rule disjI2)
- defer
- apply (rule disjI1)
- apply (rule d'(5)[OF as(3-4)])
- apply assumption
- apply (rule p'(5)[OF as(1-2)])
- apply auto
- done
- moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
- unfolding as ..
- ultimately have "interior (l1 \<inter> k1) = {}"
- by auto
- then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
- unfolding uv inter_interval
- unfolding content_eq_0_interior[symmetric]
- by auto
- qed safe
- also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
- unfolding Sigma_alt
- apply (subst sum_sum_product[symmetric])
- apply (rule p')
- apply rule
- apply (rule d')
- apply (rule setsum.cong)
- apply (rule refl)
- unfolding split_paired_all split_conv
- proof -
- fix x l
- assume as: "(x, l) \<in> p"
- note xl = p'(2-4)[OF this]
- from this(3) guess u v by (elim exE) note uv=this
- have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
- apply (rule setsum.cong)
- apply (rule refl)
- apply (drule d'(4))
- apply safe
- apply (subst Int_commute)
- unfolding inter_interval uv
- apply (subst abs_of_nonneg)
- apply auto
- done
- also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
- unfolding Setcompr_eq_image
- apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
- apply (rule d')
- proof goal_cases
- case prems: (1 k y)
- from d'(4)[OF this(1)] d'(4)[OF this(2)]
- guess u1 v1 u2 v2 by (elim exE) note uv=this
- have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
- apply (subst interior_Int)
- using d'(5)[OF prems(1-3)]
- apply auto
- done
- also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
- by auto
- also have "\<dots> = interior (k \<inter> cbox u v)"
- unfolding prems(4) by auto
- finally show ?case
- unfolding uv inter_interval content_eq_0_interior ..
- 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 Setcompr_eq_image
- apply (rule finite_imageI)
- apply (rule d')
- apply blast
- apply safe
- apply (rule_tac x=k in exI)
- proof goal_cases
- case prems: (1 i k)
- from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
- have "interior (k \<inter> cbox u v) \<noteq> {}"
- using prems(2)
- unfolding ab inter_interval content_eq_0_interior
- by auto
- then show ?case
- using prems(1)
- using interior_subset[of "k \<inter> cbox u v"]
- by auto
- qed
- finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
- unfolding setsum_distrib_right[symmetric] real_scaleR_def
- apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
- using xl(2)[unfolded uv]
- unfolding uv
- apply auto
- done
- qed
- finally show ?case .
- qed
- qed
- qed
-qed
-
-lemma bounded_variation_absolutely_integrable:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "f integrable_on UNIV"
- and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
- shows "f absolutely_integrable_on UNIV"
-proof (rule absolutely_integrable_onI, fact, rule)
- let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
- have D_1: "?D \<noteq> {}"
- by (rule elementary_interval) auto
- have D_2: "bdd_above (?f`?D)"
- by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
- note D = D_1 D_2
- let ?S = "SUP d:?D. ?f d"
- have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
- apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
- apply (rule integrable_on_subcbox[OF assms(1)])
- defer
- apply safe
- apply (rule assms(2)[rule_format])
- apply auto
- done
- show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
- apply (subst has_integral_alt')
- apply safe
- proof goal_cases
- case (1 a b)
- show ?case
- using f_int[of a b] by auto
- next
- case prems: (2 e)
- have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have "?S \<le> ?S - e"
- by (intro cSUP_least[OF D(1)]) auto
- then show False
- using prems by auto
- qed
- then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
- "SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
- by (auto simp add: image_iff not_le)
- from this(1) obtain d where "d division_of \<Union>d"
- and "K = (\<Sum>k\<in>d. norm (integral k f))"
- by auto
- note d = this(1) *(2)[unfolded this(2)]
- note d'=division_ofD[OF this(1)]
- have "bounded (\<Union>d)"
- by (rule elementary_bounded,fact)
- from this[unfolded bounded_pos] obtain K where
- K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
- show ?case
- apply (rule_tac x="K + 1" in exI)
- apply safe
- proof -
- fix a b :: 'n
- assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
- have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
- by arith
- show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
- unfolding real_norm_def
- apply (rule *[rule_format])
- apply safe
- apply (rule d(2))
- proof goal_cases
- case 1
- have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
- apply (rule setsum_mono)
- apply (rule absolutely_integrable_le)
- apply (drule d'(4))
- apply safe
- apply (rule f_int)
- done
- also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
- apply (rule integral_combine_division_bottomup[symmetric])
- apply (rule d)
- unfolding forall_in_division[OF d(1)]
- using f_int
- apply auto
- done
- also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
- proof -
- have "\<Union>d \<subseteq> cbox a b"
- apply rule
- apply (drule K(2)[rule_format])
- apply (rule ab[unfolded subset_eq,rule_format])
- apply (auto simp add: dist_norm)
- done
- then show ?thesis
- apply -
- apply (subst if_P)
- apply rule
- apply (rule integral_subset_le)
- defer
- apply (rule integrable_on_subdivision[of _ _ _ "cbox a b"])
- apply (rule d)
- using f_int[of a b]
- apply auto
- done
- qed
- finally show ?case .
- next
- note f = absolutely_integrable_onD[OF f_int[of a b]]
- note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
- have "e/2>0"
- using \<open>e > 0\<close> by auto
- from * [OF this] obtain d1 where
- d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
- norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e / 2"
- by auto
- from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
- d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
- (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
- obtain p where
- p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
- by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
- (auto simp add: fine_inter)
- have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
- \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
- by arith
- show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
- apply (subst if_P)
- apply rule
- proof (rule *[rule_format])
- show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e / 2"
- unfolding split_def
- apply (rule helplemma)
- using d2(2)[rule_format,of p]
- using p(1,3)
- unfolding tagged_division_of_def split_def
- apply auto
- done
- show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e / 2"
- using d1(2)[rule_format,OF conjI[OF p(1,2)]]
- by (simp only: real_norm_def)
- show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
- apply (rule setsum.cong)
- apply (rule refl)
- unfolding split_paired_all split_conv
- apply (drule tagged_division_ofD(4)[OF p(1)])
- unfolding norm_scaleR
- apply (subst abs_of_nonneg)
- apply auto
- done
- show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
- using partial_division_of_tagged_division[of p "cbox a b"] p(1)
- apply (subst setsum.over_tagged_division_lemma[OF p(1)])
- apply (simp add: integral_null)
- apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
- apply (auto simp: tagged_partial_division_of_def)
- done
- qed
- qed
- qed (insert K, auto)
- qed
-qed
-
-lemma absolutely_integrable_restrict_univ:
- "(\<lambda>x. if x \<in> s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \<longleftrightarrow>
- f absolutely_integrable_on s"
- unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ ..
-
-lemma absolutely_integrable_add[intro]:
- fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "f absolutely_integrable_on s"
- and "g absolutely_integrable_on s"
- shows "(\<lambda>x. f x + g x) absolutely_integrable_on s"
-proof -
- let ?P = "\<And>f g::'n \<Rightarrow> 'm. f absolutely_integrable_on UNIV \<Longrightarrow>
- g absolutely_integrable_on UNIV \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on UNIV"
- {
- presume as: "PROP ?P"
- note a = absolutely_integrable_restrict_univ[symmetric]
- have *: "\<And>x. (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0) =
- (if x \<in> s then f x + g x else 0)" by auto
- show ?thesis
- apply (subst a)
- using as[OF assms[unfolded a[of f] a[of g]]]
- apply (simp only: *)
- done
- }
- fix f g :: "'n \<Rightarrow> 'm"
- assume assms: "f absolutely_integrable_on UNIV" "g absolutely_integrable_on UNIV"
- note absolutely_integrable_bounded_variation
- from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format]
- show "(\<lambda>x. f x + g x) absolutely_integrable_on UNIV"
- apply (rule bounded_variation_absolutely_integrable[of _ "B1+B2"])
- apply (rule integrable_add)
- prefer 3
- apply safe
- proof goal_cases
- case prems: (1 d)
- have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
- apply (drule division_ofD(4)[OF prems])
- apply safe
- apply (rule_tac[!] integrable_on_subcbox[of _ UNIV])
- using assms
- apply auto
- done
- then have "(\<Sum>k\<in>d. norm (integral k (\<lambda>x. f x + g x))) \<le>
- (\<Sum>k\<in>d. norm (integral k f)) + (\<Sum>k\<in>d. norm (integral k g))"
- apply -
- unfolding setsum.distrib [symmetric]
- apply (rule setsum_mono)
- apply (subst integral_add)
- prefer 3
- apply (rule norm_triangle_ineq)
- apply auto
- done
- also have "\<dots> \<le> B1 + B2"
- using B(1)[OF prems] B(2)[OF prems] by auto
- finally show ?case .
- qed (insert assms, auto)
-qed
-
-lemma absolutely_integrable_sub[intro]:
- fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "f absolutely_integrable_on s"
- and "g absolutely_integrable_on s"
- shows "(\<lambda>x. f x - g x) absolutely_integrable_on s"
- using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
- by (simp add: algebra_simps)
-
-lemma absolutely_integrable_linear:
- fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
- and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
- assumes "f absolutely_integrable_on s"
- and "bounded_linear h"
- shows "(h \<circ> f) absolutely_integrable_on s"
-proof -
- {
- presume as: "\<And>f::'m \<Rightarrow> 'n. \<And>h::'n \<Rightarrow> 'p. f absolutely_integrable_on UNIV \<Longrightarrow>
- bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on UNIV"
- note a = absolutely_integrable_restrict_univ[symmetric]
- show ?thesis
- apply (subst a)
- using as[OF assms[unfolded a[of f] a[of g]]]
- apply (simp only: o_def if_distrib linear_simps[OF assms(2)])
- done
- }
- fix f :: "'m \<Rightarrow> 'n"
- fix h :: "'n \<Rightarrow> 'p"
- assume assms: "f absolutely_integrable_on UNIV" "bounded_linear h"
- from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this
- from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this]
- show "(h \<circ> f) absolutely_integrable_on UNIV"
- apply (rule bounded_variation_absolutely_integrable[of _ "B * b"])
- apply (rule integrable_linear[OF _ assms(2)])
- apply safe
- proof goal_cases
- case prems: (2 d)
- have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
- unfolding setsum_distrib_right
- apply (rule setsum_mono)
- proof goal_cases
- case (1 k)
- from division_ofD(4)[OF prems this]
- guess u v by (elim exE) note uv=this
- have *: "f integrable_on k"
- unfolding uv
- apply (rule integrable_on_subcbox[of _ UNIV])
- using assms
- apply auto
- done
- note this[unfolded has_integral_integral]
- note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)]
- note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)]
- show ?case
- unfolding * using b by auto
- qed
- also have "\<dots> \<le> B * b"
- apply (rule mult_right_mono)
- using B prems b
- apply auto
- done
- finally show ?case .
- qed (insert assms, auto)
-qed
-
-lemma absolutely_integrable_setsum:
- fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "finite t"
- and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
- shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
- using assms(1,2)
- by induct auto
-
-lemma absolutely_integrable_vector_abs:
- fixes f :: "'a::euclidean_space => 'b::euclidean_space"
- and T :: "'c::euclidean_space \<Rightarrow> 'b"
- assumes f: "f absolutely_integrable_on s"
- shows "(\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>T i\<bar> *\<^sub>R i)) absolutely_integrable_on s"
- (is "?Tf absolutely_integrable_on s")
-proof -
- have if_distrib: "\<And>P A B x. (if P then A else B) *\<^sub>R x = (if P then A *\<^sub>R x else B *\<^sub>R x)"
- by simp
- have *: "\<And>x. ?Tf x = (\<Sum>i\<in>Basis.
- ((\<lambda>y. (\<Sum>j\<in>Basis. (if j = i then y else 0) *\<^sub>R j)) o
- (\<lambda>x. (norm (\<Sum>j\<in>Basis. (if j = i then f x\<bullet>T i else 0) *\<^sub>R j)))) x)"
- by (simp add: comp_def if_distrib setsum.If_cases)
- show ?thesis
- unfolding *
- apply (rule absolutely_integrable_setsum[OF finite_Basis])
- apply (rule absolutely_integrable_linear)
- apply (rule absolutely_integrable_norm)
- apply (rule absolutely_integrable_linear[OF f, unfolded o_def])
- apply (auto simp: linear_linear euclidean_eq_iff[where 'a='c] inner_simps intro!: linearI)
- done
-qed
-
-lemma absolutely_integrable_max:
- fixes f g :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
- assumes "f absolutely_integrable_on s"
- and "g absolutely_integrable_on s"
- shows "(\<lambda>x. (\<Sum>i\<in>Basis. max (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)::'n) absolutely_integrable_on s"
-proof -
- have *:"\<And>x. (1 / 2) *\<^sub>R (((\<Sum>i\<in>Basis. \<bar>(f x - g x) \<bullet> i\<bar> *\<^sub>R i)::'n) + (f x + g x)) =
- (\<Sum>i\<in>Basis. max (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)"
- unfolding euclidean_eq_iff[where 'a='n] by (auto simp: inner_simps)
- note absolutely_integrable_sub[OF assms] absolutely_integrable_add[OF assms]
- note absolutely_integrable_vector_abs[OF this(1), where T="\<lambda>x. x"] this(2)
- note absolutely_integrable_add[OF this]
- note absolutely_integrable_cmul[OF this, of "1/2"]
- then show ?thesis unfolding * .
-qed
-
-lemma absolutely_integrable_min:
- fixes f g::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
- assumes "f absolutely_integrable_on s"
- and "g absolutely_integrable_on s"
- shows "(\<lambda>x. (\<Sum>i\<in>Basis. min (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)::'n) absolutely_integrable_on s"
-proof -
- have *:"\<And>x. (1 / 2) *\<^sub>R ((f x + g x) - (\<Sum>i\<in>Basis. \<bar>(f x - g x) \<bullet> i\<bar> *\<^sub>R i::'n)) =
- (\<Sum>i\<in>Basis. min (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)"
- unfolding euclidean_eq_iff[where 'a='n] by (auto simp: inner_simps)
-
- note absolutely_integrable_add[OF assms] absolutely_integrable_sub[OF assms]
- note this(1) absolutely_integrable_vector_abs[OF this(2), where T="\<lambda>x. x"]
- note absolutely_integrable_sub[OF this]
- note absolutely_integrable_cmul[OF this,of "1/2"]
- then show ?thesis unfolding * .
-qed
-
-lemma absolutely_integrable_abs_eq:
- fixes f::"'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and>
- (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on s"
- (is "?l = ?r")
-proof
- assume ?l
- then show ?r
- apply -
- apply rule
- defer
- apply (drule absolutely_integrable_vector_abs)
- apply auto
- done
-next
- assume ?r
- {
- presume lem: "\<And>f::'n \<Rightarrow> 'm. f integrable_on UNIV \<Longrightarrow>
- (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on UNIV \<Longrightarrow>
- f absolutely_integrable_on UNIV"
- have *: "\<And>x. (\<Sum>i\<in>Basis. \<bar>(if x \<in> s then f x else 0) \<bullet> i\<bar> *\<^sub>R i) =
- (if x \<in> s then (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) else (0::'m))"
- unfolding euclidean_eq_iff[where 'a='m]
- by auto
- show ?l
- apply (subst absolutely_integrable_restrict_univ[symmetric])
- apply (rule lem)
- unfolding integrable_restrict_univ *
- using \<open>?r\<close>
- apply auto
- done
- }
- fix f :: "'n \<Rightarrow> 'm"
- assume assms: "f integrable_on UNIV" "(\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on UNIV"
- let ?B = "\<Sum>i\<in>Basis. integral UNIV (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) \<bullet> i"
- show "f absolutely_integrable_on UNIV"
- apply (rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"])
- apply safe
- proof goal_cases
- case d: (1 d)
- note d'=division_ofD[OF d]
- have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
- (\<Sum>k\<in>d. setsum (op \<bullet> (integral k (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m))) Basis)"
- apply (rule setsum_mono)
- apply (rule order_trans[OF norm_le_l1])
- apply (rule setsum_mono)
- unfolding lessThan_iff
- proof -
- fix k
- fix i :: 'm
- assume "k \<in> d" and i: "i \<in> Basis"
- from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
- show "\<bar>integral k f \<bullet> i\<bar> \<le> integral k (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) \<bullet> i"
- apply (rule abs_leI)
- unfolding inner_minus_left[symmetric]
- defer
- apply (subst integral_neg[symmetric])
- apply (rule_tac[1-2] integral_component_le[OF i])
- using integrable_on_subcbox[OF assms(1),of a b]
- integrable_on_subcbox[OF assms(2),of a b] i integrable_neg
- unfolding ab
- apply auto
- done
- qed
- also have "\<dots> \<le> setsum (op \<bullet> (integral UNIV (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m))) Basis"
- apply (subst setsum.commute)
- apply (rule setsum_mono)
- proof goal_cases
- case (1 j)
- have *: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) integrable_on \<Union>d"
- using integrable_on_subdivision[OF d assms(2)] by auto
- have "(\<Sum>i\<in>d. integral i (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j) =
- integral (\<Union>d) (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j"
- unfolding inner_setsum_left[symmetric] integral_combine_division_topdown[OF * d] ..
- also have "\<dots> \<le> integral UNIV (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j"
- apply (rule integral_subset_component_le)
- using assms * \<open>j \<in> Basis\<close>
- apply auto
- done
- finally show ?case .
- qed
- finally show ?case .
- qed
-qed
-
-lemma nonnegative_absolutely_integrable:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "\<forall>x\<in>s. \<forall>i\<in>Basis. 0 \<le> f x \<bullet> i"
- and "f integrable_on s"
- shows "f absolutely_integrable_on s"
- unfolding absolutely_integrable_abs_eq
- apply rule
- apply (rule assms)thm integrable_eq
- apply (rule integrable_eq[of _ f])
- using assms
- apply (auto simp: euclidean_eq_iff[where 'a='m])
- done
-
-lemma absolutely_integrable_integrable_bound:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "\<forall>x\<in>s. norm (f x) \<le> g x"
- and "f integrable_on s"
- and "g integrable_on s"
- shows "f absolutely_integrable_on s"
-proof -
- {
- presume *: "\<And>f::'n \<Rightarrow> 'm. \<And>g. \<forall>x. norm (f x) \<le> g x \<Longrightarrow> f integrable_on UNIV \<Longrightarrow>
- g integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV"
- show ?thesis
- apply (subst absolutely_integrable_restrict_univ[symmetric])
- apply (rule *[of _ "\<lambda>x. if x\<in>s then g x else 0"])
- using assms
- unfolding integrable_restrict_univ
- apply auto
- done
- }
- fix g
- fix f :: "'n \<Rightarrow> 'm"
- assume assms: "\<forall>x. norm (f x) \<le> g x" "f integrable_on UNIV" "g integrable_on UNIV"
- show "f absolutely_integrable_on UNIV"
- apply (rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
- apply safe
- proof goal_cases
- case d: (1 d)
- note d'=division_ofD[OF d]
- have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
- apply (rule setsum_mono)
- apply (rule integral_norm_bound_integral)
- apply (drule_tac[!] d'(4))
- apply safe
- apply (rule_tac[1-2] integrable_on_subcbox)
- using assms
- apply auto
- done
- also have "\<dots> = integral (\<Union>d) g"
- apply (rule integral_combine_division_bottomup[symmetric])
- apply (rule d)
- apply safe
- apply (drule d'(4))
- apply safe
- apply (rule integrable_on_subcbox[OF assms(3)])
- apply auto
- done
- also have "\<dots> \<le> integral UNIV g"
- apply (rule integral_subset_le)
- defer
- apply (rule integrable_on_subdivision[OF d,of _ UNIV])
- prefer 4
- apply rule
- apply (rule_tac y="norm (f x)" in order_trans)
- using assms
- apply auto
- done
- finally show ?case .
- qed
-qed
-
-lemma absolutely_integrable_absolutely_integrable_bound:
- fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- and g :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
- assumes "\<forall>x\<in>s. norm (f x) \<le> norm (g x)"
- and "f integrable_on s"
- and "g absolutely_integrable_on s"
- shows "f absolutely_integrable_on s"
- apply (rule absolutely_integrable_integrable_bound[of s f "\<lambda>x. norm (g x)"])
- using assms
- apply auto
- done
-
-lemma absolutely_integrable_inf_real:
- assumes "finite k"
- and "k \<noteq> {}"
- and "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
- shows "(\<lambda>x. (Inf ((fs x) ` k))) absolutely_integrable_on s"
- using assms
-proof induct
- case (insert a k)
- let ?P = "(\<lambda>x.
- if fs x ` k = {} then fs x a
- else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s"
- show ?case
- unfolding image_insert
- apply (subst Inf_insert_finite)
- apply (rule finite_imageI[OF insert(1)])
- proof (cases "k = {}")
- case True
- then show ?P
- apply (subst if_P)
- defer
- apply (rule insert(5)[rule_format])
- apply auto
- done
- next
- case False
- then show ?P
- apply (subst if_not_P)
- defer
- apply (rule absolutely_integrable_min[where 'n=real, unfolded Basis_real_def, simplified])
- defer
- apply(rule insert(3)[OF False])
- using insert(5)
- apply auto
- done
- qed
-next
- case empty
- then show ?case by auto
-qed
-
-lemma absolutely_integrable_sup_real:
- assumes "finite k"
- and "k \<noteq> {}"
- and "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
- shows "(\<lambda>x. (Sup ((fs x) ` k))) absolutely_integrable_on s"
- using assms
-proof induct
- case (insert a k)
- let ?P = "(\<lambda>x.
- if fs x ` k = {} then fs x a
- else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s"
- show ?case
- unfolding image_insert
- apply (subst Sup_insert_finite)
- apply (rule finite_imageI[OF insert(1)])
- proof (cases "k = {}")
- case True
- then show ?P
- apply (subst if_P)
- defer
- apply (rule insert(5)[rule_format])
- apply auto
- done
- next
- case False
- then show ?P
- apply (subst if_not_P)
- defer
- apply (rule absolutely_integrable_max[where 'n=real, unfolded Basis_real_def, simplified])
- defer
- apply (rule insert(3)[OF False])
- using insert(5)
- apply auto
- done
- qed
-qed auto
-
-
subsection \<open>differentiation under the integral sign\<close>
lemma tube_lemma:
@@ -11296,8 +10103,7 @@
by (simp add: integral_diff dist_norm)
also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))"
using elim
- by (intro integral_norm_bound_integral)
- (auto intro!: integrable_diff absolutely_integrable_onI)
+ by (intro integral_norm_bound_integral) (auto intro!: integrable_diff)
also have "\<dots> < e"
using \<open>0 < e\<close>
by (simp add: e'_def)
@@ -11309,358 +10115,6 @@
qed
-subsection \<open>Dominated convergence\<close>
-
-context
-begin
-
-private lemma dominated_convergence_real:
- fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
- assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
- and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
- and "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
- shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
-proof
- have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
- proof (safe intro!: bdd_belowI)
- fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
- using assms(3)[rule_format, of x n] by simp
- qed
- have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
- proof (safe intro!: bdd_aboveI)
- fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
- using assms(3)[rule_format, of x n] by simp
- qed
-
- have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
- integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
- proof (rule monotone_convergence_decreasing, safe)
- fix m :: nat
- show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}"
- unfolding bounded_iff
- apply (rule_tac x="integral s h" in exI)
- proof safe
- 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 Setcompr_eq_image
- apply (rule absolutely_integrable_onD)
- apply (rule absolutely_integrable_inf_real)
- prefer 5
- unfolding real_norm_def
- apply rule
- apply (rule cInf_abs_ge)
- prefer 5
- apply rule
- apply (rule_tac g = h in absolutely_integrable_integrable_bound)
- using assms
- unfolding real_norm_def
- apply auto
- done
- qed
- fix k :: nat
- show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
- unfolding Setcompr_eq_image
- apply (rule absolutely_integrable_onD)
- apply (rule absolutely_integrable_inf_real)
- prefer 3
- using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
- apply auto
- done
- fix x
- assume x: "x \<in> s"
- show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
- by (rule cInf_superset_mono) auto
- let ?S = "{f j x| j. m \<le> j}"
- show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Inf ?S) sequentially"
- proof (rule LIMSEQ_I, goal_cases)
- case r: (1 r)
-
- have "\<exists>y\<in>?S. y < Inf ?S + r"
- by (subst cInf_less_iff[symmetric]) (auto simp: \<open>x\<in>s\<close> r)
- then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
- by blast
-
- show ?case
- apply (rule_tac x=N in exI)
- apply safe
- proof goal_cases
- case prems: (1 n)
- have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> \<bar>ix - Inf ?S\<bar> < r"
- by arith
- show ?case
- unfolding real_norm_def
- apply (rule *[rule_format, OF N(1)])
- apply (rule cInf_superset_mono, auto simp: \<open>x\<in>s\<close>) []
- apply (rule cInf_lower)
- using N prems
- apply auto []
- apply simp
- done
- qed
- qed
- qed
- note dec1 = conjunctD2[OF this]
-
- have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
- integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
- proof (rule monotone_convergence_increasing,safe)
- fix m :: nat
- show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}"
- unfolding bounded_iff
- apply (rule_tac x="integral s h" in exI)
- 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 Setcompr_eq_image
- apply (rule absolutely_integrable_onD)
- apply(rule absolutely_integrable_sup_real)
- prefer 5 unfolding real_norm_def
- apply rule
- apply (rule cSup_abs_le)
- using assms
- apply (force simp add: )
- prefer 4
- apply rule
- apply (rule_tac g=h in absolutely_integrable_integrable_bound)
- using assms
- unfolding real_norm_def
- apply auto
- done
- qed
- fix k :: nat
- show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
- unfolding Setcompr_eq_image
- apply (rule absolutely_integrable_onD)
- apply (rule absolutely_integrable_sup_real)
- prefer 3
- using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
- apply auto
- done
- fix x
- assume x: "x\<in>s"
- show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
- by (rule cSup_subset_mono) auto
- let ?S = "{f j x| j. m \<le> j}"
- show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Sup ?S) sequentially"
- proof (rule LIMSEQ_I, goal_cases)
- case r: (1 r)
- have "\<exists>y\<in>?S. Sup ?S - r < y"
- by (subst less_cSup_iff[symmetric]) (auto simp: r \<open>x\<in>s\<close>)
- then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
- by blast
-
- show ?case
- apply (rule_tac x=N in exI)
- apply safe
- proof goal_cases
- case prems: (1 n)
- have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> \<bar>ix - Sup ?S\<bar> < r"
- by arith
- show ?case
- apply simp
- apply (rule *[rule_format, OF N(1)])
- apply (rule cSup_subset_mono, auto simp: \<open>x\<in>s\<close>) []
- apply (subst cSup_upper)
- using N prems
- apply auto
- done
- qed
- qed
- qed
- note inc1 = conjunctD2[OF this]
-
- have "g integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
- apply (rule monotone_convergence_increasing,safe)
- apply fact
- proof -
- show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
- unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
- proof safe
- fix k :: nat
- show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h"
- apply (rule integral_norm_bound_integral)
- apply fact+
- unfolding real_norm_def
- apply rule
- apply (rule cInf_abs_ge)
- using assms(3)
- apply auto
- done
- qed
- fix k :: nat and x
- assume x: "x \<in> s"
-
- have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
- show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
- by (intro cInf_superset_mono) (auto simp: \<open>x\<in>s\<close>)
-
- show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) \<longlonglongrightarrow> g x"
- proof (rule LIMSEQ_I, goal_cases)
- case r: (1 r)
- then have "0<r/2"
- by auto
- from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N = this
- show ?case
- apply (rule_tac x=N in exI)
- apply safe
- unfolding real_norm_def
- apply (rule le_less_trans[of _ "r/2"])
- apply (rule cInf_asclose)
- apply safe
- defer
- apply (rule less_imp_le)
- using N r
- apply auto
- done
- qed
- qed
- note inc2 = conjunctD2[OF this]
-
- have "g integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
- apply (rule monotone_convergence_decreasing,safe)
- apply fact
- proof -
- show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
- unfolding bounded_iff
- apply (rule_tac x="integral s h" in exI)
- proof safe
- fix k :: nat
- show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
- apply (rule integral_norm_bound_integral)
- apply fact+
- unfolding real_norm_def
- apply rule
- apply (rule cSup_abs_le)
- using assms(3)
- apply auto
- done
- qed
- fix k :: nat
- fix x
- assume x: "x \<in> s"
-
- show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
- by (rule cSup_subset_mono) (auto simp: \<open>x\<in>s\<close>)
- show "((\<lambda>k. Sup {f j x |j. k \<le> j}) \<longlongrightarrow> g x) sequentially"
- proof (rule LIMSEQ_I, goal_cases)
- case r: (1 r)
- then have "0<r/2"
- by auto
- from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
- show ?case
- apply (rule_tac x=N in exI,safe)
- unfolding real_norm_def
- apply (rule le_less_trans[of _ "r/2"])
- apply (rule cSup_asclose)
- apply safe
- defer
- apply (rule less_imp_le)
- using N r
- apply auto
- done
- qed
- qed
- note dec2 = conjunctD2[OF this]
-
- show "g integrable_on s" by fact
- show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
- proof (rule LIMSEQ_I, goal_cases)
- case r: (1 r)
- from LIMSEQ_D [OF inc2(2) r] guess N1 .. note N1=this[unfolded real_norm_def]
- from LIMSEQ_D [OF dec2(2) r] guess N2 .. note N2=this[unfolded real_norm_def]
- show ?case
- proof (rule_tac x="N1+N2" in exI, safe)
- fix n
- assume n: "n \<ge> N1 + N2"
- have *: "\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r"
- by arith
- show "norm (integral s (f n) - integral s g) < r"
- unfolding real_norm_def
- proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
- show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
- by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
- show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
- by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
- qed (insert n, auto)
- qed
- qed
-qed
-
-lemma dominated_convergence:
- fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
- and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
- and conv: "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
- shows "g integrable_on s"
- and "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
-proof -
- {
- fix b :: 'm assume b: "b \<in> Basis"
- have A: "(\<lambda>x. g x \<bullet> b) integrable_on s \<and>
- (\<lambda>k. integral s (\<lambda>x. f k x \<bullet> b)) \<longlonglongrightarrow> integral s (\<lambda>x. g x \<bullet> b)"
- proof (rule dominated_convergence_real)
- fix k :: nat
- from f show "(\<lambda>x. f k x \<bullet> b) integrable_on s" by (rule integrable_component)
- next
- from h show "h integrable_on s" .
- next
- fix k :: nat
- show "\<forall>x\<in>s. norm (f k x \<bullet> b) \<le> h x"
- proof
- fix x assume x: "x \<in> s"
- have "norm (f k x \<bullet> b) \<le> norm (f k x)" by (simp add: Basis_le_norm b)
- also have "\<dots> \<le> h x" using le[of k] x by simp
- finally show "norm (f k x \<bullet> b) \<le> h x" .
- qed
- next
- from conv show "\<forall>x\<in>s. (\<lambda>k. f k x \<bullet> b) \<longlonglongrightarrow> g x \<bullet> b"
- by (auto intro!: tendsto_inner)
- qed
- have B: "integral s ((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f k x \<bullet> b)) = integral s (\<lambda>x. f k x \<bullet> b) *\<^sub>R b"
- for k by (rule integral_linear)
- (simp_all add: f integrable_component bounded_linear_scaleR_left)
- have C: "integral s ((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. g x \<bullet> b)) = integral s (\<lambda>x. g x \<bullet> b) *\<^sub>R b"
- using A by (intro integral_linear)
- (simp_all add: integrable_component bounded_linear_scaleR_left)
- note A B C
- } note A = this
-
- show "g integrable_on s" by (rule integrable_componentwise) (insert A, blast)
- with A f show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
- by (subst (1 2) integral_componentwise)
- (auto intro!: tendsto_setsum tendsto_scaleR simp: o_def)
-qed
-
-lemma has_integral_dominated_convergence:
- fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
- assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
- "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
- and x: "y \<longlonglongrightarrow> x"
- shows "(g has_integral x) s"
-proof -
- have int_f: "\<And>k. (f k) integrable_on s"
- using assms by (auto simp: integrable_on_def)
- have "(g has_integral (integral s g)) s"
- by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
- moreover have "integral s g = x"
- proof (rule LIMSEQ_unique)
- show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
- using integral_unique[OF assms(1)] x by simp
- show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
- by (intro dominated_convergence[OF int_f assms(2)]) fact+
- qed
- ultimately show ?thesis
- by simp
-qed
-
-end
-
-
subsection \<open>Integration by parts\<close>
lemma integration_by_parts_interior_strong: