move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
--- a/src/HOL/Analysis/Bochner_Integration.thy Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Fri Sep 23 18:34:34 2016 +0200
@@ -2311,7 +2311,7 @@
lemma integrableE:
assumes "integrable M f"
- obtains r q where
+ obtains r q where "0 \<le> r" "0 \<le> q"
"(\<integral>\<^sup>+x. ennreal (f x)\<partial>M) = ennreal r"
"(\<integral>\<^sup>+x. ennreal (-f x)\<partial>M) = ennreal q"
"f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
--- a/src/HOL/Analysis/Complete_Measure.thy Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Complete_Measure.thy Fri Sep 23 18:34:34 2016 +0200
@@ -342,6 +342,7 @@
lemma null_sets_restrict_space:
"\<Omega> \<in> sets M \<Longrightarrow> A \<in> null_sets (restrict_space M \<Omega>) \<longleftrightarrow> A \<subseteq> \<Omega> \<and> A \<in> null_sets M"
by (auto simp: null_sets_def emeasure_restrict_space sets_restrict_space)
+
lemma completion_ex_borel_measurable_real:
fixes g :: "'a \<Rightarrow> real"
assumes g: "g \<in> borel_measurable (completion M)"
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Fri Sep 23 18:34:34 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Complex Analysis Basics\<close>
theory Complex_Analysis_Basics
-imports Henstock_Kurzweil_Integration "~~/src/HOL/Library/Nonpos_Ints"
+imports Equivalence_Lebesgue_Henstock_Integration "~~/src/HOL/Library/Nonpos_Ints"
begin
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Sep 23 18:34:34 2016 +0200
@@ -1,5 +1,10 @@
+(* Title: HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
+ Author: Johannes Hölzl, TU München
+ Author: Robert Himmelmann, TU München
+*)
+
theory Equivalence_Lebesgue_Henstock_Integration
- imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure
+ imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
begin
lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
@@ -650,34 +655,27 @@
by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
qed
+lemma ennreal_max_0: "ennreal (max 0 x) = ennreal x"
+ by (auto simp: max_def ennreal_neg)
+
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
+proof -
+ from integrableE[OF f] obtain r q
+ where "0 \<le> r" "0 \<le> q"
+ and r: "(\<integral>\<^sup>+ x. ennreal (max 0 (f x)) \<partial>lborel) = ennreal r"
+ and q: "(\<integral>\<^sup>+ x. ennreal (max 0 (- f x)) \<partial>lborel) = ennreal q"
+ and f: "f \<in> borel_measurable lborel" and eq: "integral\<^sup>L lborel f = r - q"
+ unfolding ennreal_max_0 by auto
+ then have "((\<lambda>x. max 0 (f x)) has_integral r) UNIV" "((\<lambda>x. max 0 (- f x)) has_integral q) UNIV"
+ using nn_integral_has_integral[OF _ _ r] nn_integral_has_integral[OF _ _ q] by auto
+ note has_integral_sub[OF this]
+ moreover have "(\<lambda>x. max 0 (f x) - max 0 (- f x)) = f"
+ by auto
+ ultimately show ?thesis
+ by (simp add: eq)
qed
lemma has_integral_AE:
@@ -781,6 +779,997 @@
end
+lemma measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
+ by (auto simp: measurable_def)
+
+lemma integrable_completion:
+ fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+ shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> integrable (completion M) f \<longleftrightarrow> integrable M f"
+ by (rule integrable_subalgebra[symmetric]) auto
+
+lemma integral_completion:
+ fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+ assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "integral\<^sup>L (completion M) f = integral\<^sup>L M f"
+ by (rule integral_subalgebra[symmetric]) (auto intro: f)
+
+context
+begin
+
+private lemma has_integral_integral_lebesgue_real:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes f: "integrable lebesgue f"
+ shows "(f has_integral (integral\<^sup>L lebesgue f)) UNIV"
+proof -
+ obtain f' where f': "f' \<in> borel \<rightarrow>\<^sub>M borel" "AE x in lborel. f x = f' x"
+ using completion_ex_borel_measurable_real[OF borel_measurable_integrable[OF f]] by auto
+ moreover have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>lborel) = (\<integral>\<^sup>+ x. ennreal (norm (f' x)) \<partial>lborel)"
+ using f' by (intro nn_integral_cong_AE) auto
+ ultimately have "integrable lborel f'"
+ using f by (auto simp: integrable_iff_bounded nn_integral_completion cong: nn_integral_cong_AE)
+ note has_integral_integral_real[OF this]
+ moreover have "integral\<^sup>L lebesgue f = integral\<^sup>L lebesgue f'"
+ using f' f by (intro integral_cong_AE) (auto intro: AE_completion measurable_completion)
+ moreover have "integral\<^sup>L lebesgue f' = integral\<^sup>L lborel f'"
+ using f' by (simp add: integral_completion)
+ moreover have "(f' has_integral integral\<^sup>L lborel f') UNIV \<longleftrightarrow> (f has_integral integral\<^sup>L lborel f') UNIV"
+ using f' by (intro has_integral_AE) auto
+ ultimately show ?thesis
+ by auto
+qed
+
+lemma has_integral_integral_lebesgue:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "integrable lebesgue f"
+ shows "(f has_integral (integral\<^sup>L lebesgue 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 lebesgue (\<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_lebesgue_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 lebesgue (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lebesgue f"
+ using f by (subst (2) eq_f[symmetric]) simp
+ finally show ?thesis .
+qed
+
+lemma integrable_on_lebesgue:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "integrable lebesgue f \<Longrightarrow> f integrable_on UNIV"
+ using has_integral_integral_lebesgue by auto
+
+lemma integral_lebesgue:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "integrable lebesgue f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lebesgue)"
+ using has_integral_integral_lebesgue by auto
+
+end
+
+subsection \<open>Absolute integrability (this is the same as Lebesgue integrability)\<close>
+
+translations
+"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
+
+translations
+"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
+
+lemma set_integral_reflect:
+ fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+ shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
+ by (subst lborel_integral_real_affine[where c="-1" and t=0])
+ (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
+
+lemma borel_integrable_atLeastAtMost':
+ fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+ assumes f: "continuous_on {a..b} f"
+ shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
+ by (intro borel_integrable_compact compact_Icc f)
+
+lemma integral_FTC_atLeastAtMost:
+ fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
+ assumes "a \<le> b"
+ and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+ and f: "continuous_on {a .. b} f"
+ shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
+proof -
+ let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
+ have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
+ using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
+ moreover
+ have "(f has_integral F b - F a) {a .. b}"
+ by (intro fundamental_theorem_of_calculus ballI assms) auto
+ then have "(?f has_integral F b - F a) {a .. b}"
+ by (subst has_integral_cong[where g=f]) auto
+ then have "(?f has_integral F b - F a) UNIV"
+ by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
+ ultimately show "integral\<^sup>L lborel ?f = F b - F a"
+ by (rule has_integral_unique)
+qed
+
+lemma set_borel_integral_eq_integral:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "set_integrable lborel S f"
+ shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
+proof -
+ let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
+ have "(?f has_integral LINT x : S | lborel. f x) UNIV"
+ by (rule has_integral_integral_lborel) fact
+ hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
+ apply (subst has_integral_restrict_univ [symmetric])
+ apply (rule has_integral_eq)
+ by auto
+ thus "f integrable_on S"
+ by (auto simp add: integrable_on_def)
+ with 1 have "(f has_integral (integral S f)) S"
+ by (intro integrable_integral, auto simp add: integrable_on_def)
+ thus "LINT x : S | lborel. f x = integral S f"
+ by (intro has_integral_unique [OF 1])
+qed
+
+lemma has_integral_set_lebesgue:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "set_integrable lebesgue S f"
+ shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
+ using has_integral_integral_lebesgue[OF f]
+ by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_univ cong: if_cong)
+
+lemma set_lebesgue_integral_eq_integral:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "set_integrable lebesgue S f"
+ shows "f integrable_on S" "LINT x:S | lebesgue. f x = integral S f"
+ using has_integral_set_lebesgue[OF f] by (auto simp: integral_unique integrable_on_def)
+
+abbreviation
+ absolutely_integrable_on :: "('a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
+ (infixr "absolutely'_integrable'_on" 46)
+ where "f absolutely_integrable_on s \<equiv> set_integrable lebesgue s f"
+
+lemma absolutely_integrable_on_def:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. norm (f x)) integrable_on s"
+proof safe
+ assume f: "f absolutely_integrable_on s"
+ then have nf: "integrable lebesgue (\<lambda>x. norm (indicator s x *\<^sub>R f x))"
+ by (intro integrable_norm)
+ note integrable_on_lebesgue[OF f] integrable_on_lebesgue[OF nf]
+ moreover have
+ "(\<lambda>x. indicator s x *\<^sub>R f x) = (\<lambda>x. if x \<in> s then f x else 0)"
+ "(\<lambda>x. norm (indicator s x *\<^sub>R f x)) = (\<lambda>x. if x \<in> s then norm (f x) else 0)"
+ by auto
+ ultimately show "f integrable_on s" "(\<lambda>x. norm (f x)) integrable_on s"
+ by (simp_all add: integrable_restrict_univ)
+next
+ assume f: "f integrable_on s" and nf: "(\<lambda>x. norm (f x)) integrable_on s"
+ show "f absolutely_integrable_on s"
+ proof (rule integrableI_bounded)
+ show "(\<lambda>x. indicator s x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+ using f has_integral_implies_lebesgue_measurable[of f _ s] by (auto simp: integrable_on_def)
+ show "(\<integral>\<^sup>+ x. ennreal (norm (indicator s x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
+ using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ s]
+ by (auto simp: integrable_on_def nn_integral_completion)
+ qed
+qed
+
+lemma absolutely_integrable_onI:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "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 set_integral_norm_bound:
+ fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
+ shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
+ using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by simp
+
+lemma set_integral_finite_UN_AE:
+ fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+ assumes "finite I"
+ and ae: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> AE x in M. (x \<in> A i \<and> x \<in> A j) \<longrightarrow> i = j"
+ and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
+ and f: "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f"
+ shows "LINT x:(\<Union>i\<in>I. A i)|M. f x = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
+ using \<open>finite I\<close> order_refl[of I]
+proof (induction I rule: finite_subset_induct')
+ case (insert i I')
+ have "AE x in M. (\<forall>j\<in>I'. x \<in> A i \<longrightarrow> x \<notin> A j)"
+ proof (intro AE_ball_countable[THEN iffD2] ballI)
+ fix j assume "j \<in> I'"
+ with \<open>I' \<subseteq> I\<close> \<open>i \<notin> I'\<close> have "i \<noteq> j" "j \<in> I"
+ by auto
+ then show "AE x in M. x \<in> A i \<longrightarrow> x \<notin> A j"
+ using ae[of i j] \<open>i \<in> I\<close> by auto
+ qed (use \<open>finite I'\<close> in \<open>rule countable_finite\<close>)
+ then have "AE x\<in>A i in M. \<forall>xa\<in>I'. x \<notin> A xa "
+ by auto
+ with insert.hyps insert.IH[symmetric]
+ show ?case
+ by (auto intro!: set_integral_Un_AE sets.finite_UN f set_integrable_UN)
+qed simp
+
+lemma set_integrable_norm:
+ fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+ assumes f: "set_integrable M k f" shows "set_integrable M k (\<lambda>x. norm (f x))"
+ using integrable_norm[OF f] by simp
+
+lemma absolutely_integrable_bounded_variation:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "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"
+proof (rule that[of "integral UNIV (\<lambda>x. norm (f x))"]; safe)
+ fix d :: "'a set set" assume d: "d division_of \<Union>d"
+ have *: "k \<in> d \<Longrightarrow> f absolutely_integrable_on k" for k
+ using f[THEN set_integrable_subset, of k] division_ofD(2,4)[OF d, of k] by auto
+ note d' = division_ofD[OF d]
+
+ have "(\<Sum>k\<in>d. norm (integral k f)) = (\<Sum>k\<in>d. norm (LINT x:k|lebesgue. f x))"
+ by (intro setsum.cong refl arg_cong[where f=norm] set_lebesgue_integral_eq_integral(2)[symmetric] *)
+ also have "\<dots> \<le> (\<Sum>k\<in>d. LINT x:k|lebesgue. norm (f x))"
+ by (intro setsum_mono set_integral_norm_bound *)
+ also have "\<dots> = (\<Sum>k\<in>d. integral k (\<lambda>x. norm (f x)))"
+ by (intro setsum.cong refl set_lebesgue_integral_eq_integral(2) set_integrable_norm *)
+ also have "\<dots> \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
+ using integrable_on_subdivision[OF d] assms f unfolding absolutely_integrable_on_def
+ by (subst integral_combine_division_topdown[OF _ d]) auto
+ also have "\<dots> \<le> integral UNIV (\<lambda>x. norm (f x))"
+ using integrable_on_subdivision[OF d] assms unfolding absolutely_integrable_on_def
+ by (intro integral_subset_le) auto
+ finally show "(\<Sum>k\<in>d. norm (integral k f)) \<le> integral UNIV (\<lambda>x. norm (f x))" .
+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] unfolding absolutely_integrable_on_def 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 (intro setsum_mono)
+ subgoal for k
+ using d'(4)[of k] f_int
+ by (auto simp: absolutely_integrable_on_def integral_norm_bound_integral)
+ 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 unfolding absolutely_integrable_on_def
+ 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] unfolding absolutely_integrable_on_def
+ apply auto
+ done
+ qed
+ finally show ?case .
+ next
+ note f' = f_int[of a b, unfolded absolutely_integrable_on_def]
+ note f = f'[THEN conjunct1] f'[THEN conjunct2]
+ 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) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
+ by (intro arg_cong2[where f=integrable]) auto
+
+lemma absolutely_integrable_add[intro]:
+ fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+ shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on s"
+ by (rule set_integral_add)
+
+lemma absolutely_integrable_sub[intro]:
+ fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+ shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) absolutely_integrable_on s"
+ by (rule set_integral_diff)
+
+lemma absolutely_integrable_linear:
+ fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
+ and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
+ shows "f absolutely_integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on s"
+ using integrable_bounded_linear[of h lebesgue "\<lambda>x. indicator s x *\<^sub>R f x"]
+ by (simp add: linear_simps[of h])
+
+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_integrable_bound:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+ assumes le: "\<forall>x\<in>s. norm (f x) \<le> g x" and f: "f integrable_on s" and g: "g integrable_on s"
+ shows "f absolutely_integrable_on s"
+proof (rule Bochner_Integration.integrable_bound)
+ show "g absolutely_integrable_on s"
+ unfolding absolutely_integrable_on_def
+ proof
+ show "(\<lambda>x. norm (g x)) integrable_on s"
+ using le norm_ge_zero[of "f _"]
+ by (intro integrable_spike_finite[OF _ _ g, where s="{}"])
+ (auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
+ qed fact
+ show "set_borel_measurable lebesgue s f"
+ using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
+qed (use le in \<open>auto intro!: always_eventually split: split_indicator\<close>)
+
+subsection \<open>Dominated convergence\<close>
+
+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) \<longlonglongrightarrow> g x"
+ shows "g integrable_on s" "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+proof -
+ have 3: "h absolutely_integrable_on s"
+ unfolding absolutely_integrable_on_def
+ proof
+ show "(\<lambda>x. norm (h x)) integrable_on s"
+ proof (intro integrable_spike_finite[OF _ _ h, where s="{}"] ballI)
+ fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
+ using order_trans[OF norm_ge_zero le[THEN bspec, of x]] by auto
+ qed auto
+ qed fact
+ have 2: "set_borel_measurable lebesgue s (f k)" for k
+ using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
+ then have 1: "set_borel_measurable lebesgue s g"
+ by (rule borel_measurable_LIMSEQ_metric) (use conv in \<open>auto split: split_indicator\<close>)
+ have 4: "AE x in lebesgue. (\<lambda>i. indicator s x *\<^sub>R f i x) \<longlonglongrightarrow> indicator s x *\<^sub>R g x"
+ "AE x in lebesgue. norm (indicator s x *\<^sub>R f k x) \<le> indicator s x *\<^sub>R h x" for k
+ using conv le by (auto intro!: always_eventually split: split_indicator)
+
+ have g: "g absolutely_integrable_on s"
+ using 1 2 3 4 by (rule integrable_dominated_convergence)
+ then show "g integrable_on s"
+ by (auto simp: absolutely_integrable_on_def)
+ have "(\<lambda>k. (LINT x:s|lebesgue. f k x)) \<longlonglongrightarrow> (LINT x:s|lebesgue. g x)"
+ using 1 2 3 4 by (rule integral_dominated_convergence)
+ then show "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+ using g absolutely_integrable_integrable_bound[OF le f h]
+ by (subst (asm) (1 2) set_lebesgue_integral_eq_integral) auto
+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
+
subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
text \<open>
--- 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:
--- a/src/HOL/Analysis/Interval_Integral.thy Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Fri Sep 23 18:34:34 2016 +0200
@@ -5,7 +5,7 @@
*)
theory Interval_Integral
- imports Set_Integral
+ imports Equivalence_Lebesgue_Henstock_Integration
begin
lemma continuous_on_vector_derivative:
@@ -1062,19 +1062,16 @@
qed
-syntax
-"_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
-("(2CLBINT _. _)" [0,60] 60)
+syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
+ ("(2CLBINT _. _)" [0,60] 60)
+
+translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
+
+syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
+ ("(3CLBINT _:_. _)" [0,60,61] 60)
translations
-"CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
-
-syntax
-"_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
-("(3CLBINT _:_. _)" [0,60,61] 60)
-
-translations
-"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
+ "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
abbreviation complex_interval_lebesgue_integral ::
"real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> complex" where
--- a/src/HOL/Analysis/Set_Integral.thy Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Sep 23 18:34:34 2016 +0200
@@ -7,7 +7,7 @@
*)
theory Set_Integral
- imports Equivalence_Lebesgue_Henstock_Integration
+ imports Bochner_Integration
begin
(*
@@ -50,16 +50,10 @@
"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
("(2LBINT _./ _)" [0,60] 60)
-translations
-"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
-
syntax
"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
("(3LBINT _:_./ _)" [0,60,61] 60)
-translations
-"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
-
(*
Basic properties
*)
@@ -180,12 +174,6 @@
(LINT x:A|M. f x) - (LINT x:A|M. g x)"
using assms by (simp_all add: scaleR_diff_right)
-lemma set_integral_reflect:
- fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
- shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
- by (subst lborel_integral_real_affine[where c="-1" and t=0])
- (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? *)
lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
@@ -528,59 +516,6 @@
translations
"CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
-(*
-lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x"
- apply (simp add: norm_mult)
- by (subst norm_mult, auto)
-*)
-
-lemma borel_integrable_atLeastAtMost':
- fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
- assumes f: "continuous_on {a..b} f"
- shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
- by (intro borel_integrable_compact compact_Icc f)
-
-lemma integral_FTC_atLeastAtMost:
- fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
- assumes "a \<le> b"
- and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
- and f: "continuous_on {a .. b} f"
- shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
-proof -
- let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
- have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
- using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
- moreover
- have "(f has_integral F b - F a) {a .. b}"
- by (intro fundamental_theorem_of_calculus ballI assms) auto
- then have "(?f has_integral F b - F a) {a .. b}"
- by (subst has_integral_cong[where g=f]) auto
- then have "(?f has_integral F b - F a) UNIV"
- by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
- ultimately show "integral\<^sup>L lborel ?f = F b - F a"
- by (rule has_integral_unique)
-qed
-
-lemma set_borel_integral_eq_integral:
- fixes f :: "real \<Rightarrow> 'a::euclidean_space"
- assumes "set_integrable lborel S f"
- shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
-proof -
- let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
- have "(?f has_integral LINT x : S | lborel. f x) UNIV"
- by (rule has_integral_integral_lborel) fact
- hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
- apply (subst has_integral_restrict_univ [symmetric])
- apply (rule has_integral_eq)
- by auto
- thus "f integrable_on S"
- by (auto simp add: integrable_on_def)
- with 1 have "(f has_integral (integral S f)) S"
- by (intro integrable_integral, auto simp add: integrable_on_def)
- thus "LINT x : S | lborel. f x = integral S f"
- by (intro has_integral_unique [OF 1])
-qed
-
lemma set_borel_measurable_continuous:
fixes f :: "_ \<Rightarrow> _::real_normed_vector"
assumes "S \<in> sets borel" "continuous_on S f"