new material on eqiintegrable functions, etc.
--- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Aug 15 21:46:43 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Fri Aug 16 12:53:36 2019 +0100
@@ -490,126 +490,6 @@
qed
qed
-proposition lebesgue_regular_inner:
- assumes "S \<in> sets lebesgue"
- obtains K C where "negligible K" "\<And>n::nat. compact(C n)" "S = (\<Union>n. C n) \<union> K"
-proof -
- have "\<exists>T. closed T \<and> T \<subseteq> S \<and> (S - T) \<in> lmeasurable \<and> emeasure lebesgue (S - T) < ennreal ((1/2)^n)" for n
- using sets_lebesgue_inner_closed assms
- by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power)
- then obtain C where clo: "\<And>n. closed (C n)" and subS: "\<And>n. C n \<subseteq> S"
- and mea: "\<And>n. (S - C n) \<in> lmeasurable"
- and less: "\<And>n. emeasure lebesgue (S - C n) < ennreal ((1/2)^n)"
- by metis
- have "\<exists>F. (\<forall>n::nat. compact(F n)) \<and> (\<Union>n. F n) = C m" for m::nat
- by (metis clo closed_Union_compact_subsets)
- then obtain D :: "[nat,nat] \<Rightarrow> 'a set" where D: "\<And>m n. compact(D m n)" "\<And>m. (\<Union>n. D m n) = C m"
- by metis
- let ?C = "from_nat_into (\<Union>m. range (D m))"
- have "countable (\<Union>m. range (D m))"
- by blast
- have "range (from_nat_into (\<Union>m. range (D m))) = (\<Union>m. range (D m))"
- using range_from_nat_into by simp
- then have CD: "\<exists>m n. ?C k = D m n" for k
- by (metis (mono_tags, lifting) UN_iff rangeE range_eqI)
- show thesis
- proof
- show "negligible (S - (\<Union>n. C n))"
- proof (clarsimp simp: negligible_outer_le)
- fix e :: "real"
- assume "e > 0"
- then obtain n where n: "(1/2)^n < e"
- using real_arch_pow_inv [of e "1/2"] by auto
- show "\<exists>T. S - (\<Union>n. C n) \<subseteq> T \<and> T \<in> lmeasurable \<and> measure lebesgue T \<le> e"
- proof (intro exI conjI)
- show "S - (\<Union>n. C n) \<subseteq> S - C n"
- by blast
- show "S - C n \<in> lmeasurable"
- by (simp add: mea)
- show "measure lebesgue (S - C n) \<le> e"
- using less [of n] n
- by (simp add: emeasure_eq_measure2 less_le mea)
- qed
- qed
- show "compact (?C n)" for n
- using CD D by metis
- show "S = (\<Union>n. ?C n) \<union> (S - (\<Union>n. C n))" (is "_ = ?rhs")
- proof
- show "S \<subseteq> ?rhs"
- using D by fastforce
- show "?rhs \<subseteq> S"
- using subS D CD by auto (metis Sup_upper range_eqI subsetCE)
- qed
- qed
-qed
-
-
-lemma sets_lebesgue_continuous_image:
- assumes T: "T \<in> sets lebesgue" and contf: "continuous_on S f"
- and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)" and "T \<subseteq> S"
- shows "f ` T \<in> sets lebesgue"
-proof -
- obtain K C where "negligible K" and com: "\<And>n::nat. compact(C n)" and Teq: "T = (\<Union>n. C n) \<union> K"
- using lebesgue_regular_inner [OF T] by metis
- then have comf: "\<And>n::nat. compact(f ` C n)"
- by (metis Un_subset_iff Union_upper \<open>T \<subseteq> S\<close> compact_continuous_image contf continuous_on_subset rangeI)
- have "((\<Union>n. f ` C n) \<union> f ` K) \<in> sets lebesgue"
- proof (rule sets.Un)
- have "K \<subseteq> S"
- using Teq \<open>T \<subseteq> S\<close> by blast
- show "(\<Union>n. f ` C n) \<in> sets lebesgue"
- proof (rule sets.countable_Union)
- show "range (\<lambda>n. f ` C n) \<subseteq> sets lebesgue"
- using borel_compact comf by (auto simp: borel_compact)
- qed auto
- show "f ` K \<in> sets lebesgue"
- by (simp add: \<open>K \<subseteq> S\<close> \<open>negligible K\<close> negim negligible_imp_sets)
- qed
- then show ?thesis
- by (simp add: Teq image_Un image_Union)
-qed
-
-lemma differentiable_image_in_sets_lebesgue:
- fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
- assumes S: "S \<in> sets lebesgue" and dim: "DIM('m) \<le> DIM('n)" and f: "f differentiable_on S"
- shows "f`S \<in> sets lebesgue"
-proof (rule sets_lebesgue_continuous_image [OF S])
- show "continuous_on S f"
- by (meson differentiable_imp_continuous_on f)
- show "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible (f ` T)"
- using differentiable_on_subset f
- by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim])
-qed auto
-
-lemma sets_lebesgue_on_continuous_image:
- assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and contf: "continuous_on S f"
- and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)"
- shows "f ` X \<in> sets (lebesgue_on (f ` S))"
-proof -
- have "X \<subseteq> S"
- by (metis S X sets.Int_space_eq2 sets_restrict_space_iff)
- moreover have "f ` S \<in> sets lebesgue"
- using S contf negim sets_lebesgue_continuous_image by blast
- moreover have "f ` X \<in> sets lebesgue"
- by (metis S X contf negim sets_lebesgue_continuous_image sets_restrict_space_iff space_restrict_space space_restrict_space2)
- ultimately show ?thesis
- by (auto simp: sets_restrict_space_iff)
-qed
-
-lemma differentiable_image_in_sets_lebesgue_on:
- fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
- assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and dim: "DIM('m) \<le> DIM('n)"
- and f: "f differentiable_on S"
- shows "f ` X \<in> sets (lebesgue_on (f`S))"
-proof (rule sets_lebesgue_on_continuous_image [OF S X])
- show "continuous_on S f"
- by (meson differentiable_imp_continuous_on f)
- show "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible (f ` T)"
- using differentiable_on_subset f
- by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim])
-qed
-
-
proposition
fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
assumes S: "S \<in> lmeasurable"
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Aug 15 21:46:43 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Aug 16 12:53:36 2019 +0100
@@ -4466,6 +4466,194 @@
apply (auto simp: in_borel_measurable_borel vimage_def)
done
+subsection \<open>Lebesgue sets and continuous images\<close>
+
+proposition lebesgue_regular_inner:
+ assumes "S \<in> sets lebesgue"
+ obtains K C where "negligible K" "\<And>n::nat. compact(C n)" "S = (\<Union>n. C n) \<union> K"
+proof -
+ have "\<exists>T. closed T \<and> T \<subseteq> S \<and> (S - T) \<in> lmeasurable \<and> emeasure lebesgue (S - T) < ennreal ((1/2)^n)" for n
+ using sets_lebesgue_inner_closed assms
+ by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power)
+ then obtain C where clo: "\<And>n. closed (C n)" and subS: "\<And>n. C n \<subseteq> S"
+ and mea: "\<And>n. (S - C n) \<in> lmeasurable"
+ and less: "\<And>n. emeasure lebesgue (S - C n) < ennreal ((1/2)^n)"
+ by metis
+ have "\<exists>F. (\<forall>n::nat. compact(F n)) \<and> (\<Union>n. F n) = C m" for m::nat
+ by (metis clo closed_Union_compact_subsets)
+ then obtain D :: "[nat,nat] \<Rightarrow> 'a set" where D: "\<And>m n. compact(D m n)" "\<And>m. (\<Union>n. D m n) = C m"
+ by metis
+ let ?C = "from_nat_into (\<Union>m. range (D m))"
+ have "countable (\<Union>m. range (D m))"
+ by blast
+ have "range (from_nat_into (\<Union>m. range (D m))) = (\<Union>m. range (D m))"
+ using range_from_nat_into by simp
+ then have CD: "\<exists>m n. ?C k = D m n" for k
+ by (metis (mono_tags, lifting) UN_iff rangeE range_eqI)
+ show thesis
+ proof
+ show "negligible (S - (\<Union>n. C n))"
+ proof (clarsimp simp: negligible_outer_le)
+ fix e :: "real"
+ assume "e > 0"
+ then obtain n where n: "(1/2)^n < e"
+ using real_arch_pow_inv [of e "1/2"] by auto
+ show "\<exists>T. S - (\<Union>n. C n) \<subseteq> T \<and> T \<in> lmeasurable \<and> measure lebesgue T \<le> e"
+ proof (intro exI conjI)
+ show "S - (\<Union>n. C n) \<subseteq> S - C n"
+ by blast
+ show "S - C n \<in> lmeasurable"
+ by (simp add: mea)
+ show "measure lebesgue (S - C n) \<le> e"
+ using less [of n] n
+ by (simp add: emeasure_eq_measure2 less_le mea)
+ qed
+ qed
+ show "compact (?C n)" for n
+ using CD D by metis
+ show "S = (\<Union>n. ?C n) \<union> (S - (\<Union>n. C n))" (is "_ = ?rhs")
+ proof
+ show "S \<subseteq> ?rhs"
+ using D by fastforce
+ show "?rhs \<subseteq> S"
+ using subS D CD by auto (metis Sup_upper range_eqI subsetCE)
+ qed
+ qed
+qed
+
+lemma sets_lebesgue_continuous_image:
+ assumes T: "T \<in> sets lebesgue" and contf: "continuous_on S f"
+ and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)" and "T \<subseteq> S"
+ shows "f ` T \<in> sets lebesgue"
+proof -
+ obtain K C where "negligible K" and com: "\<And>n::nat. compact(C n)" and Teq: "T = (\<Union>n. C n) \<union> K"
+ using lebesgue_regular_inner [OF T] by metis
+ then have comf: "\<And>n::nat. compact(f ` C n)"
+ by (metis Un_subset_iff Union_upper \<open>T \<subseteq> S\<close> compact_continuous_image contf continuous_on_subset rangeI)
+ have "((\<Union>n. f ` C n) \<union> f ` K) \<in> sets lebesgue"
+ proof (rule sets.Un)
+ have "K \<subseteq> S"
+ using Teq \<open>T \<subseteq> S\<close> by blast
+ show "(\<Union>n. f ` C n) \<in> sets lebesgue"
+ proof (rule sets.countable_Union)
+ show "range (\<lambda>n. f ` C n) \<subseteq> sets lebesgue"
+ using borel_compact comf by (auto simp: borel_compact)
+ qed auto
+ show "f ` K \<in> sets lebesgue"
+ by (simp add: \<open>K \<subseteq> S\<close> \<open>negligible K\<close> negim negligible_imp_sets)
+ qed
+ then show ?thesis
+ by (simp add: Teq image_Un image_Union)
+qed
+
+lemma differentiable_image_in_sets_lebesgue:
+ fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
+ assumes S: "S \<in> sets lebesgue" and dim: "DIM('m) \<le> DIM('n)" and f: "f differentiable_on S"
+ shows "f`S \<in> sets lebesgue"
+proof (rule sets_lebesgue_continuous_image [OF S])
+ show "continuous_on S f"
+ by (meson differentiable_imp_continuous_on f)
+ show "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible (f ` T)"
+ using differentiable_on_subset f
+ by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim])
+qed auto
+
+lemma sets_lebesgue_on_continuous_image:
+ assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and contf: "continuous_on S f"
+ and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)"
+ shows "f ` X \<in> sets (lebesgue_on (f ` S))"
+proof -
+ have "X \<subseteq> S"
+ by (metis S X sets.Int_space_eq2 sets_restrict_space_iff)
+ moreover have "f ` S \<in> sets lebesgue"
+ using S contf negim sets_lebesgue_continuous_image by blast
+ moreover have "f ` X \<in> sets lebesgue"
+ by (metis S X contf negim sets_lebesgue_continuous_image sets_restrict_space_iff space_restrict_space space_restrict_space2)
+ ultimately show ?thesis
+ by (auto simp: sets_restrict_space_iff)
+qed
+
+lemma differentiable_image_in_sets_lebesgue_on:
+ fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
+ assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and dim: "DIM('m) \<le> DIM('n)"
+ and f: "f differentiable_on S"
+ shows "f ` X \<in> sets (lebesgue_on (f`S))"
+proof (rule sets_lebesgue_on_continuous_image [OF S X])
+ show "continuous_on S f"
+ by (meson differentiable_imp_continuous_on f)
+ show "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible (f ` T)"
+ using differentiable_on_subset f
+ by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim])
+qed
+
+subsection \<open>Affine lemmas\<close>
+
+lemma borel_measurable_affine:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
+ assumes f: "f \<in> borel_measurable lebesgue" and "c \<noteq> 0"
+ shows "(\<lambda>x. f(t + c *\<^sub>R x)) \<in> borel_measurable lebesgue"
+proof -
+ { fix a b
+ have "{x. f x \<in> cbox a b} \<in> sets lebesgue"
+ using f cbox_borel lebesgue_measurable_vimage_borel by blast
+ then have "(\<lambda>x. (x - t) /\<^sub>R c) ` {x. f x \<in> cbox a b} \<in> sets lebesgue"
+ proof (rule differentiable_image_in_sets_lebesgue)
+ show "(\<lambda>x. (x - t) /\<^sub>R c) differentiable_on {x. f x \<in> cbox a b}"
+ unfolding differentiable_on_def differentiable_def
+ by (rule \<open>c \<noteq> 0\<close> derivative_eq_intros strip exI | simp)+
+ qed auto
+ moreover
+ have "{x. f(t + c *\<^sub>R x) \<in> cbox a b} = (\<lambda>x. (x-t) /\<^sub>R c) ` {x. f x \<in> cbox a b}"
+ using \<open>c \<noteq> 0\<close> by (auto simp: image_def)
+ ultimately have "{x. f(t + c *\<^sub>R x) \<in> cbox a b} \<in> sets lebesgue"
+ by (auto simp: borel_measurable_vimage_closed_interval) }
+ then show ?thesis
+ by (subst lebesgue_on_UNIV_eq [symmetric]; auto simp: borel_measurable_vimage_closed_interval)
+qed
+
+lemma lebesgue_integrable_real_affine:
+ fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
+ assumes f: "integrable lebesgue f" and "c \<noteq> 0"
+ shows "integrable lebesgue (\<lambda>x. f(t + c * x))"
+proof -
+ have "(\<lambda>x. norm (f x)) \<in> borel_measurable lebesgue"
+ by (simp add: borel_measurable_integrable f)
+ then show ?thesis
+ using assms borel_measurable_affine [of f c]
+ unfolding integrable_iff_bounded
+ by (subst (asm) nn_integral_real_affine_lebesgue[where c=c and t=t]) (auto simp: ennreal_mult_less_top)
+qed
+
+lemma lebesgue_integrable_real_affine_iff:
+ fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
+ shows "c \<noteq> 0 \<Longrightarrow> integrable lebesgue (\<lambda>x. f(t + c * x)) \<longleftrightarrow> integrable lebesgue f"
+ using lebesgue_integrable_real_affine[of f c t]
+ lebesgue_integrable_real_affine[of "\<lambda>x. f(t + c * x)" "1/c" "-t/c"]
+ by (auto simp: field_simps)
+
+lemma\<^marker>\<open>tag important\<close> lebesgue_integral_real_affine:
+ fixes f :: "real \<Rightarrow> 'a :: euclidean_space" and c :: real
+ assumes c: "c \<noteq> 0" shows "(\<integral>x. f x \<partial> lebesgue) = \<bar>c\<bar> *\<^sub>R (\<integral>x. f(t + c * x) \<partial>lebesgue)"
+proof cases
+ have "(\<lambda>x. t + c * x) \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
+ using lebesgue_affine_measurable[where c= "\<lambda>x::real. c"] \<open>c \<noteq> 0\<close> by simp
+ moreover
+ assume "integrable lebesgue f"
+ ultimately show ?thesis
+ by (subst lebesgue_real_affine[OF c, of t]) (auto simp: integral_density integral_distr)
+next
+ assume "\<not> integrable lebesgue f" with c show ?thesis
+ by (simp add: lebesgue_integrable_real_affine_iff not_integrable_integral_eq)
+qed
+
+lemma has_bochner_integral_lebesgue_real_affine_iff:
+ fixes i :: "'a :: euclidean_space"
+ shows "c \<noteq> 0 \<Longrightarrow>
+ has_bochner_integral lebesgue f i \<longleftrightarrow>
+ has_bochner_integral lebesgue (\<lambda>x. f(t + c * x)) (i /\<^sub>R \<bar>c\<bar>)"
+ unfolding has_bochner_integral_iff lebesgue_integrable_real_affine_iff
+ by (simp_all add: lebesgue_integral_real_affine[symmetric] divideR_right cong: conj_cong)
+
subsection\<open>More results on integrability\<close>
lemma integrable_on_all_intervals_UNIV:
--- a/src/HOL/Analysis/Improper_Integral.thy Thu Aug 15 21:46:43 2019 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy Fri Aug 16 12:53:36 2019 +0100
@@ -1,3 +1,7 @@
+(* Title: HOL/Analysis/Improper_Integral.thy
+ Author: LC Paulson (ported from HOL Light)
+*)
+
section \<open>Continuity of the indefinite integral; improper integral theorem\<close>
theory "Improper_Integral"
@@ -66,6 +70,180 @@
by (metis assms equiintegrable_on_Un equiintegrable_on_sing insert_is_Un)
+lemma equiintegrable_cmul:
+ assumes F: "F equiintegrable_on I"
+ shows "(\<Union>c \<in> {-k..k}. \<Union>f \<in> F. {(\<lambda>x. c *\<^sub>R f x)}) equiintegrable_on I"
+ unfolding equiintegrable_on_def
+ proof (intro conjI impI allI ballI)
+ show "f integrable_on I"
+ if "f \<in> (\<Union>c\<in>{- k..k}. \<Union>f\<in>F. {\<lambda>x. c *\<^sub>R f x})"
+ for f :: "'a \<Rightarrow> 'b"
+ using that assms equiintegrable_on_integrable integrable_cmul by blast
+ show "\<exists>\<gamma>. gauge \<gamma> \<and> (\<forall>f \<D>. f \<in> (\<Union>c\<in>{- k..k}. \<Union>f\<in>F. {\<lambda>x. c *\<^sub>R f x}) \<and> \<D> tagged_division_of I
+ \<and> \<gamma> fine \<D> \<longrightarrow> norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>)"
+ if "\<epsilon> > 0" for \<epsilon>
+ proof -
+ obtain \<gamma> where "gauge \<gamma>"
+ and \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of I; \<gamma> fine \<D>\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon> / (\<bar>k\<bar> + 1)"
+ using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def
+ by (metis add.commute add.right_neutral add_strict_mono divide_pos_pos norm_eq_zero real_norm_def zero_less_norm_iff zero_less_one)
+ moreover have "norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R c *\<^sub>R (f x)) - integral I (\<lambda>x. c *\<^sub>R f x)) < \<epsilon>"
+ if c: "c \<in> {- k..k}"
+ and "f \<in> F" "\<D> tagged_division_of I" "\<gamma> fine \<D>"
+ for \<D> c f
+ proof -
+ have "norm ((\<Sum>x\<in>\<D>. case x of (x, K) \<Rightarrow> content K *\<^sub>R c *\<^sub>R f x) - integral I (\<lambda>x. c *\<^sub>R f x))
+ = \<bar>c\<bar> * norm ((\<Sum>x\<in>\<D>. case x of (x, K) \<Rightarrow> content K *\<^sub>R f x) - integral I f)"
+ by (simp add: algebra_simps scale_sum_right case_prod_unfold flip: norm_scaleR)
+ also have "\<dots> \<le> (\<bar>k\<bar> + 1) * norm ((\<Sum>x\<in>\<D>. case x of (x, K) \<Rightarrow> content K *\<^sub>R f x) - integral I f)"
+ using c by (auto simp: mult_right_mono)
+ also have "\<dots> < (\<bar>k\<bar> + 1) * (\<epsilon> / (\<bar>k\<bar> + 1))"
+ by (rule mult_strict_left_mono) (use \<gamma> less_eq_real_def that in auto)
+ also have "\<dots> = \<epsilon>"
+ by auto
+ finally show ?thesis .
+ qed
+ ultimately show ?thesis
+ by (rule_tac x="\<gamma>" in exI) auto
+ qed
+qed
+
+
+lemma equiintegrable_add:
+ assumes F: "F equiintegrable_on I" and G: "G equiintegrable_on I"
+ shows "(\<Union>f \<in> F. \<Union>g \<in> G. {(\<lambda>x. f x + g x)}) equiintegrable_on I"
+ unfolding equiintegrable_on_def
+proof (intro conjI impI allI ballI)
+ show "f integrable_on I"
+ if "f \<in> (\<Union>f\<in>F. \<Union>g\<in>G. {\<lambda>x. f x + g x})" for f
+ using that equiintegrable_on_integrable assms by (auto intro: integrable_add)
+ show "\<exists>\<gamma>. gauge \<gamma> \<and> (\<forall>f \<D>. f \<in> (\<Union>f\<in>F. \<Union>g\<in>G. {\<lambda>x. f x + g x}) \<and> \<D> tagged_division_of I
+ \<and> \<gamma> fine \<D> \<longrightarrow> norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>)"
+ if "\<epsilon> > 0" for \<epsilon>
+ proof -
+ obtain \<gamma>1 where "gauge \<gamma>1"
+ and \<gamma>1: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of I; \<gamma>1 fine \<D>\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) < \<epsilon>/2"
+ using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
+ obtain \<gamma>2 where "gauge \<gamma>2"
+ and \<gamma>2: "\<And>g \<D>. \<lbrakk>g \<in> G; \<D> tagged_division_of I; \<gamma>2 fine \<D>\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral I g) < \<epsilon>/2"
+ using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
+ have "gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
+ using \<open>gauge \<gamma>1\<close> \<open>gauge \<gamma>2\<close> by blast
+ moreover have "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R h x) - integral I h) < \<epsilon>"
+ if h: "h \<in> (\<Union>f\<in>F. \<Union>g\<in>G. {\<lambda>x. f x + g x})"
+ and \<D>: "\<D> tagged_division_of I" and fine: "(\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x) fine \<D>"
+ for h \<D>
+ proof -
+ obtain f g where "f \<in> F" "g \<in> G" and heq: "h = (\<lambda>x. f x + g x)"
+ using h by blast
+ then have int: "f integrable_on I" "g integrable_on I"
+ using F G equiintegrable_on_def by blast+
+ have "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R h x) - integral I h)
+ = norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x + content K *\<^sub>R g x) - (integral I f + integral I g))"
+ by (simp add: heq algebra_simps integral_add int)
+ also have "\<dots> = norm (((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f + (\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral I g))"
+ by (simp add: sum.distrib algebra_simps case_prod_unfold)
+ also have "\<dots> \<le> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral I f) + norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral I g)"
+ by (metis (mono_tags) add_diff_eq norm_triangle_ineq)
+ also have "\<dots> < \<epsilon>/2 + \<epsilon>/2"
+ using \<gamma>1 [OF \<open>f \<in> F\<close> \<D>] \<gamma>2 [OF \<open>g \<in> G\<close> \<D>] fine by (simp add: fine_Int)
+ finally show ?thesis by simp
+ qed
+ ultimately show ?thesis
+ by meson
+ qed
+qed
+
+lemma equiintegrable_minus:
+ assumes "F equiintegrable_on I"
+ shows "(\<Union>f \<in> F. {(\<lambda>x. - f x)}) equiintegrable_on I"
+ by (force intro: equiintegrable_on_subset [OF equiintegrable_cmul [OF assms, of 1]])
+
+lemma equiintegrable_diff:
+ assumes F: "F equiintegrable_on I" and G: "G equiintegrable_on I"
+ shows "(\<Union>f \<in> F. \<Union>g \<in> G. {(\<lambda>x. f x - g x)}) equiintegrable_on I"
+ by (rule equiintegrable_on_subset [OF equiintegrable_add [OF F equiintegrable_minus [OF G]]]) auto
+
+
+lemma equiintegrable_sum:
+ fixes F :: "('a::euclidean_space \<Rightarrow> 'b::euclidean_space) set"
+ assumes "F equiintegrable_on cbox a b"
+ shows "(\<Union>I \<in> Collect finite. \<Union>c \<in> {c. (\<forall>i \<in> I. c i \<ge> 0) \<and> sum c I = 1}.
+ \<Union>f \<in> I \<rightarrow> F. {(\<lambda>x. sum (\<lambda>i::'j. c i *\<^sub>R f i x) I)}) equiintegrable_on cbox a b"
+ (is "?G equiintegrable_on _")
+ unfolding equiintegrable_on_def
+proof (intro conjI impI allI ballI)
+ show "f integrable_on cbox a b" if "f \<in> ?G" for f
+ using that assms by (auto simp: equiintegrable_on_def intro!: integrable_sum integrable_cmul)
+ show "\<exists>\<gamma>. gauge \<gamma>
+ \<and> (\<forall>g \<D>. g \<in> ?G \<and> \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D>
+ \<longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral (cbox a b) g) < \<epsilon>)"
+ if "\<epsilon> > 0" for \<epsilon>
+ proof -
+ obtain \<gamma> where "gauge \<gamma>"
+ and \<gamma>: "\<And>f \<D>. \<lbrakk>f \<in> F; \<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox a b) f) < \<epsilon> / 2"
+ using assms \<open>\<epsilon> > 0\<close> unfolding equiintegrable_on_def by (meson half_gt_zero_iff)
+ moreover have "norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R g x) - integral (cbox a b) g) < \<epsilon>"
+ if g: "g \<in> ?G"
+ and \<D>: "\<D> tagged_division_of cbox a b"
+ and fine: "\<gamma> fine \<D>"
+ for \<D> g
+ proof -
+ obtain I c f where "finite I" and 0: "\<And>i::'j. i \<in> I \<Longrightarrow> 0 \<le> c i"
+ and 1: "sum c I = 1" and f: "f \<in> I \<rightarrow> F" and geq: "g = (\<lambda>x. \<Sum>i\<in>I. c i *\<^sub>R f i x)"
+ using g by auto
+ have fi_int: "f i integrable_on cbox a b" if "i \<in> I" for i
+ by (metis Pi_iff assms equiintegrable_on_def f that)
+ have *: "integral (cbox a b) (\<lambda>x. c i *\<^sub>R f i x) = (\<Sum>(x, K)\<in>\<D>. integral K (\<lambda>x. c i *\<^sub>R f i x))"
+ if "i \<in> I" for i
+ proof -
+ have "f i integrable_on cbox a b"
+ by (metis Pi_iff assms equiintegrable_on_def f that)
+ then show ?thesis
+ by (intro \<D> integrable_cmul integral_combine_tagged_division_topdown)
+ qed
+ have "finite \<D>"
+ using \<D> by blast
+ have swap: "(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R (\<Sum>i\<in>I. c i *\<^sub>R f i x))
+ = (\<Sum>i\<in>I. c i *\<^sub>R (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f i x))"
+ by (simp add: scale_sum_right case_prod_unfold algebra_simps) (rule sum.swap)
+ have "norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R g x) - integral (cbox a b) g)
+ = norm ((\<Sum>i\<in>I. c i *\<^sub>R ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f i x) - integral (cbox a b) (f i))))"
+ unfolding geq swap
+ by (simp add: scaleR_right.sum algebra_simps integral_sum fi_int integrable_cmul \<open>finite I\<close> sum_subtractf flip: sum_diff)
+ also have "\<dots> \<le> (\<Sum>i\<in>I. c i * \<epsilon> / 2)"
+ proof (rule sum_norm_le)
+ show "norm (c i *\<^sub>R ((\<Sum>(xa, K)\<in>\<D>. content K *\<^sub>R f i xa) - integral (cbox a b) (f i))) \<le> c i * \<epsilon> / 2"
+ if "i \<in> I" for i
+ proof -
+ have "norm ((\<Sum>(x, K)\<in>\<D>. content K *\<^sub>R f i x) - integral (cbox a b) (f i)) \<le> \<epsilon>/2"
+ using \<gamma> [OF _ \<D> fine, of "f i"] funcset_mem [OF f] that by auto
+ then show ?thesis
+ using that by (auto simp: 0 mult.assoc intro: mult_left_mono)
+ qed
+ qed
+ also have "\<dots> < \<epsilon>"
+ using 1 \<open>\<epsilon> > 0\<close> by (simp add: flip: sum_divide_distrib sum_distrib_right)
+ finally show ?thesis .
+ qed
+ ultimately show ?thesis
+ by (rule_tac x="\<gamma>" in exI) auto
+ qed
+qed
+
+corollary equiintegrable_sum_real:
+ fixes F :: "(real \<Rightarrow> 'b::euclidean_space) set"
+ assumes "F equiintegrable_on {a..b}"
+ shows "(\<Union>I \<in> Collect finite. \<Union>c \<in> {c. (\<forall>i \<in> I. c i \<ge> 0) \<and> sum c I = 1}.
+ \<Union>f \<in> I \<rightarrow> F. {(\<lambda>x. sum (\<lambda>i. c i *\<^sub>R f i x) I)})
+ equiintegrable_on {a..b}"
+ using equiintegrable_sum [of F a b] assms by auto
+
+
text\<open> Basic combining theorems for the interval of integration.\<close>
lemma equiintegrable_on_null [simp]:
@@ -1171,7 +1349,6 @@
qed
-
corollary equiintegrable_halfspace_restrictions_ge:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
@@ -1202,6 +1379,37 @@
using equiintegrable_reflect [OF *] by (auto simp: eq)
qed
+corollary equiintegrable_halfspace_restrictions_lt:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
+ and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
+ shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i < c then h x else 0)}) equiintegrable_on cbox a b"
+ (is "?G equiintegrable_on cbox a b")
+proof -
+ have *: "(\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>F. {\<lambda>x. if c \<le> x \<bullet> i then h x else 0}) equiintegrable_on cbox a b"
+ using equiintegrable_halfspace_restrictions_ge [OF F f] norm_f by auto
+ have "(\<lambda>x. if x \<bullet> i < c then h x else 0) = (\<lambda>x. h x - (if c \<le> x \<bullet> i then h x else 0))"
+ if "i \<in> Basis" "h \<in> F" for i c h
+ using that by force
+ then show ?thesis
+ by (blast intro: equiintegrable_on_subset [OF equiintegrable_diff [OF F *]])
+qed
+
+corollary equiintegrable_halfspace_restrictions_gt:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
+ and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
+ shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i > c then h x else 0)}) equiintegrable_on cbox a b"
+ (is "?G equiintegrable_on cbox a b")
+proof -
+ have *: "(\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>F. {\<lambda>x. if c \<ge> x \<bullet> i then h x else 0}) equiintegrable_on cbox a b"
+ using equiintegrable_halfspace_restrictions_le [OF F f] norm_f by auto
+ have "(\<lambda>x. if x \<bullet> i > c then h x else 0) = (\<lambda>x. h x - (if c \<ge> x \<bullet> i then h x else 0))"
+ if "i \<in> Basis" "h \<in> F" for i c h
+ using that by force
+ then show ?thesis
+ by (blast intro: equiintegrable_on_subset [OF equiintegrable_diff [OF F *]])
+qed
proposition equiintegrable_closed_interval_restrictions:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -1662,5 +1870,404 @@
qed
qed
+subsection\<open>Second Mean Value Theorem\<close>
+
+
+
+subsection\<open>Second mean value theorem and corollaries\<close>
+
+lemma level_approx:
+ fixes f :: "real \<Rightarrow> real" and n::nat
+ assumes f: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x \<and> f x \<le> 1" and "x \<in> S" "n \<noteq> 0"
+ shows "\<bar>f x - (\<Sum>k = Suc 0..n. if k / n \<le> f x then inverse n else 0)\<bar> < inverse n"
+ (is "?lhs < _")
+proof -
+ have "n * f x \<ge> 0"
+ using assms by auto
+ then obtain m::nat where m: "floor(n * f x) = int m"
+ using nonneg_int_cases zero_le_floor by blast
+ then have kn: "real k / real n \<le> f x \<longleftrightarrow> k \<le> m" for k
+ using \<open>n \<noteq> 0\<close> by (simp add: divide_simps mult.commute) linarith
+ then have "Suc n / real n \<le> f x \<longleftrightarrow> Suc n \<le> m"
+ by blast
+ have "real n * f x \<le> real n"
+ by (simp add: \<open>x \<in> S\<close> f mult_left_le)
+ then have "m \<le> n"
+ using m by linarith
+ have "?lhs = \<bar>f x - (\<Sum>k \<in> {Suc 0..n} \<inter> {..m}. inverse n)\<bar>"
+ by (subst sum.inter_restrict) (auto simp: kn)
+ also have "\<dots> < inverse n"
+ using \<open>m \<le> n\<close> \<open>n \<noteq> 0\<close> m
+ by (simp add: min_absorb2 divide_simps mult.commute) linarith
+ finally show ?thesis .
+qed
+
+
+lemma SMVT_lemma2:
+ fixes f :: "real \<Rightarrow> real"
+ assumes f: "f integrable_on {a..b}"
+ and g: "\<And>x y. x \<le> y \<Longrightarrow> g x \<le> g y"
+ shows "(\<Union>y::real. {\<lambda>x. if g x \<ge> y then f x else 0}) equiintegrable_on {a..b}"
+proof -
+ have ffab: "{f} equiintegrable_on {a..b}"
+ by (metis equiintegrable_on_sing f interval_cbox)
+ then have ff: "{f} equiintegrable_on (cbox a b)"
+ by simp
+ have ge: "(\<Union>c. {\<lambda>x. if x \<ge> c then f x else 0}) equiintegrable_on {a..b}"
+ using equiintegrable_halfspace_restrictions_ge [OF ff] by auto
+ have gt: "(\<Union>c. {\<lambda>x. if x > c then f x else 0}) equiintegrable_on {a..b}"
+ using equiintegrable_halfspace_restrictions_gt [OF ff] by auto
+ have 0: "{(\<lambda>x. 0)} equiintegrable_on {a..b}"
+ by (metis box_real(2) equiintegrable_on_sing integrable_0)
+ have \<dagger>: "(\<lambda>x. if g x \<ge> y then f x else 0) \<in> {(\<lambda>x. 0), f} \<union> (\<Union>z. {\<lambda>x. if z < x then f x else 0}) \<union> (\<Union>z. {\<lambda>x. if z \<le> x then f x else 0})"
+ for y
+ proof (cases "(\<forall>x. g x \<ge> y) \<or> (\<forall>x. \<not> (g x \<ge> y))")
+ let ?\<mu> = "Inf {x. g x \<ge> y}"
+ case False
+ have lower: "?\<mu> \<le> x" if "g x \<ge> y" for x
+ apply (rule cInf_lower)
+ using False
+ apply (auto simp: that bdd_below_def)
+ by (meson dual_order.trans g linear)
+ have greatest: "?\<mu> \<ge> z" if "(\<And>x. g x \<ge> y \<Longrightarrow> z \<le> x)" for z
+ by (metis False cInf_greatest empty_iff mem_Collect_eq that)
+ show ?thesis
+ proof (cases "g ?\<mu> \<ge> y")
+ case True
+ then obtain \<zeta> where \<zeta>: "\<And>x. g x \<ge> y \<longleftrightarrow> x \<ge> \<zeta>"
+ by (metis g lower order.trans) \<comment> \<open>in fact y is @{term ?\<mu>}}\<close>
+ then show ?thesis
+ by (force simp: \<zeta>)
+ next
+ case False
+ have "(y \<le> g x) = (?\<mu> < x)" for x
+ proof
+ show "?\<mu> < x" if "y \<le> g x"
+ using that False less_eq_real_def lower by blast
+ show "y \<le> g x" if "?\<mu> < x"
+ by (metis g greatest le_less_trans that less_le_trans linear not_less)
+ qed
+ then obtain \<zeta> where \<zeta>: "\<And>x. g x \<ge> y \<longleftrightarrow> x > \<zeta>" ..
+ then show ?thesis
+ by (force simp: \<zeta>)
+ qed
+ qed auto
+ show ?thesis
+ apply (rule equiintegrable_on_subset [OF equiintegrable_on_Un [OF gt equiintegrable_on_Un [OF ge equiintegrable_on_Un [OF ffab 0]]]])
+ using \<dagger> apply (simp add: UN_subset_iff)
+ done
+qed
+
+
+lemma SMVT_lemma4:
+ fixes f :: "real \<Rightarrow> real"
+ assumes f: "f integrable_on {a..b}"
+ and "a \<le> b"
+ and g: "\<And>x y. x \<le> y \<Longrightarrow> g x \<le> g y"
+ and 01: "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> 0 \<le> g x \<and> g x \<le> 1"
+ obtains c where "a \<le> c" "c \<le> b" "((\<lambda>x. g x *\<^sub>R f x) has_integral integral {c..b} f) {a..b}"
+proof -
+ have "connected ((\<lambda>x. integral {x..b} f) ` {a..b})"
+ by (simp add: f indefinite_integral_continuous_1' connected_continuous_image)
+ moreover have "compact ((\<lambda>x. integral {x..b} f) ` {a..b})"
+ by (simp add: compact_continuous_image f indefinite_integral_continuous_1')
+ ultimately obtain m M where int_fab: "(\<lambda>x. integral {x..b} f) ` {a..b} = {m..M}"
+ using connected_compact_interval_1 by meson
+ have "\<exists>c. c \<in> {a..b} \<and>
+ integral {c..b} f =
+ integral {a..b} (\<lambda>x. (\<Sum>k = 1..n. if g x \<ge> real k / real n then inverse n *\<^sub>R f x else 0))" for n
+ proof (cases "n=0")
+ case True
+ then show ?thesis
+ using \<open>a \<le> b\<close> by auto
+ next
+ case False
+ have "(\<Union>c::real. {\<lambda>x. if g x \<ge> c then f x else 0}) equiintegrable_on {a..b}"
+ using SMVT_lemma2 [OF f g] .
+ then have int: "(\<lambda>x. if g x \<ge> c then f x else 0) integrable_on {a..b}" for c
+ by (simp add: equiintegrable_on_def)
+ have int': "(\<lambda>x. if g x \<ge> c then u * f x else 0) integrable_on {a..b}" for c u
+ proof -
+ have "(\<lambda>x. if g x \<ge> c then u * f x else 0) = (\<lambda>x. u * (if g x \<ge> c then f x else 0))"
+ by (force simp: if_distrib)
+ then show ?thesis
+ using integrable_on_cmult_left [OF int] by simp
+ qed
+ have "\<exists>d. d \<in> {a..b} \<and> integral {a..b} (\<lambda>x. if g x \<ge> y then f x else 0) = integral {d..b} f" for y
+ proof -
+ let ?X = "{x. g x \<ge> y}"
+ have *: "\<exists>a. ?X = {x. a \<le> x} \<or> ?X = {x. a < x}"
+ if 1: "?X \<noteq> {}" and 2: "?X \<noteq> UNIV"
+ proof -
+ let ?\<mu> = "Inf{x. g x \<ge> y}"
+ have lower: "?\<mu> \<le> x" if "g x \<ge> y" for x
+ apply (rule cInf_lower)
+ using 1 2 apply (auto simp: that bdd_below_def)
+ by (meson dual_order.trans g linear)
+ have greatest: "?\<mu> \<ge> z" if "(\<And>x. g x \<ge> y \<Longrightarrow> z \<le> x)" for z
+ by (metis cInf_greatest mem_Collect_eq that 1)
+ show ?thesis
+ proof (cases "g ?\<mu> \<ge> y")
+ case True
+ then obtain \<zeta> where \<zeta>: "\<And>x. g x \<ge> y \<longleftrightarrow> x \<ge> \<zeta>"
+ by (metis g lower order.trans) \<comment> \<open>in fact y is @{term ?\<mu>}}\<close>
+ then show ?thesis
+ by (force simp: \<zeta>)
+ next
+ case False
+ have "(y \<le> g x) = (?\<mu> < x)" for x
+ proof
+ show "?\<mu> < x" if "y \<le> g x"
+ using that False less_eq_real_def lower by blast
+ show "y \<le> g x" if "?\<mu> < x"
+ by (metis g greatest le_less_trans that less_le_trans linear not_less)
+ qed
+ then obtain \<zeta> where \<zeta>: "\<And>x. g x \<ge> y \<longleftrightarrow> x > \<zeta>" ..
+ then show ?thesis
+ by (force simp: \<zeta>)
+ qed
+ qed
+ then consider "?X = {}" | "?X = UNIV" | d where "?X = {x. d \<le> x} \<or>?X = {x. d < x}"
+ by metis
+ then have "\<exists>d. d \<in> {a..b} \<and> integral {a..b} (\<lambda>x. if x \<in> ?X then f x else 0) = integral {d..b} f"
+ proof cases
+ case 1
+ then show ?thesis
+ using \<open>a \<le> b\<close> by auto
+ next
+ case 2
+ then show ?thesis
+ using \<open>a \<le> b\<close> by auto
+ next
+ case (3 d)
+ show ?thesis
+ proof (cases "d < a")
+ case True
+ with 3 show ?thesis
+ apply (rule_tac x=a in exI)
+ apply (auto simp: \<open>a \<le> b\<close> iff del: mem_Collect_eq intro!: Henstock_Kurzweil_Integration.integral_cong, simp_all)
+ done
+ next
+ case False
+ show ?thesis
+ proof (cases "b < d")
+ case True
+ have "integral {a..b} (\<lambda>x. if x \<in> {x. y \<le> g x} then f x else 0) = integral {a..b} (\<lambda>x. 0)"
+ by (rule Henstock_Kurzweil_Integration.integral_cong) (use 3 True in fastforce)
+ then show ?thesis
+ using \<open>a \<le> b\<close> by auto
+ next
+ case False
+ with \<open>\<not> d < a\<close> have eq: "Collect ((\<le>) d) \<inter> {a..b} = {d..b}" "Collect ((<) d) \<inter> {a..b} = {d<..b}"
+ by force+
+ moreover have "integral {d<..b} f = integral {d..b} f"
+ by (rule integral_spike_set [OF empty_imp_negligible negligible_subset [OF negligible_sing [of d]]]) auto
+ ultimately
+ show ?thesis
+ using \<open>\<not> d < a\<close> False 3
+ apply (rule_tac x=d in exI)
+ apply (auto simp: \<open>a \<le> b\<close> iff del: mem_Collect_eq; subst Henstock_Kurzweil_Integration.integral_restrict_Int)
+ apply (simp_all add: \<open>a \<le> b\<close> not_less eq)
+ done
+ qed
+ qed
+ qed
+ then show ?thesis
+ by auto
+ qed
+ then have "\<forall>k. \<exists>d. d \<in> {a..b} \<and> integral {a..b} (\<lambda>x. if real k / real n \<le> g x then f x else 0) = integral {d..b} f"
+ by meson
+ then obtain d where dab: "\<And>k. d k \<in> {a..b}"
+ and deq: "\<And>k::nat. integral {a..b} (\<lambda>x. if k/n \<le> g x then f x else 0) = integral {d k..b} f"
+ by metis
+ have "(\<Sum>k = 1..n. integral {a..b} (\<lambda>x. if real k / real n \<le> g x then f x else 0)) /\<^sub>R n \<in> {m..M}"
+ unfolding scaleR_right.sum
+ proof (intro conjI allI impI convex [THEN iffD1, rule_format])
+ show "integral {a..b} (\<lambda>xa. if real k / real n \<le> g xa then f xa else 0) \<in> {m..M}" for k
+ by (metis (no_types, lifting) deq image_eqI int_fab dab)
+ qed (use \<open>n \<noteq> 0\<close> in auto)
+ then have "\<exists>c. c \<in> {a..b} \<and>
+ integral {c..b} f = inverse n *\<^sub>R (\<Sum>k = 1..n. integral {a..b} (\<lambda>x. if g x \<ge> real k / real n then f x else 0))"
+ by (metis (no_types, lifting) int_fab imageE)
+ then show ?thesis
+ by (simp add: sum_distrib_left if_distrib integral_sum int' flip: integral_mult_right cong: if_cong)
+ qed
+ then obtain c where cab: "\<And>n. c n \<in> {a..b}"
+ and c: "\<And>n. integral {c n..b} f = integral {a..b} (\<lambda>x. (\<Sum>k = 1..n. if g x \<ge> real k / real n then f x /\<^sub>R n else 0))"
+ by metis
+ obtain d and \<sigma> :: "nat\<Rightarrow>nat"
+ where "d \<in> {a..b}" and \<sigma>: "strict_mono \<sigma>" and d: "(c \<circ> \<sigma>) \<longlonglongrightarrow> d" and non0: "\<And>n. \<sigma> n \<ge> Suc 0"
+ proof -
+ have "compact{a..b}"
+ by auto
+ with cab obtain d and s0
+ where "d \<in> {a..b}" and s0: "strict_mono s0" and tends: "(c \<circ> s0) \<longlonglongrightarrow> d"
+ unfolding compact_def
+ using that by blast
+ show thesis
+ proof
+ show "d \<in> {a..b}"
+ by fact
+ show "strict_mono (s0 \<circ> Suc)"
+ using s0 by (auto simp: strict_mono_def)
+ show "(c \<circ> (s0 \<circ> Suc)) \<longlonglongrightarrow> d"
+ by (metis tends LIMSEQ_subseq_LIMSEQ Suc_less_eq comp_assoc strict_mono_def)
+ show "\<And>n. (s0 \<circ> Suc) n \<ge> Suc 0"
+ by (metis comp_apply le0 not_less_eq_eq old.nat.exhaust s0 seq_suble)
+ qed
+ qed
+ define \<phi> where "\<phi> \<equiv> \<lambda>n x. \<Sum>k = Suc 0..\<sigma> n. if k/(\<sigma> n) \<le> g x then f x /\<^sub>R (\<sigma> n) else 0"
+ define \<psi> where "\<psi> \<equiv> \<lambda>n x. \<Sum>k = Suc 0..\<sigma> n. if k/(\<sigma> n) \<le> g x then inverse (\<sigma> n) else 0"
+ have **: "(\<lambda>x. g x *\<^sub>R f x) integrable_on cbox a b \<and>
+ (\<lambda>n. integral (cbox a b) (\<phi> n)) \<longlonglongrightarrow> integral (cbox a b) (\<lambda>x. g x *\<^sub>R f x)"
+ proof (rule equiintegrable_limit)
+ have \<dagger>: "((\<lambda>n. \<lambda>x. (\<Sum>k = Suc 0..n. if k / n \<le> g x then inverse n *\<^sub>R f x else 0)) ` {Suc 0..}) equiintegrable_on {a..b}"
+ proof -
+ have *: "(\<Union>c::real. {\<lambda>x. if g x \<ge> c then f x else 0}) equiintegrable_on {a..b}"
+ using SMVT_lemma2 [OF f g] .
+ show ?thesis
+ apply (rule equiintegrable_on_subset [OF equiintegrable_sum_real [OF *]], clarify)
+ apply (rule_tac a="{Suc 0..n}" in UN_I, force)
+ apply (rule_tac a="\<lambda>k. inverse n" in UN_I, auto)
+ apply (rule_tac x="\<lambda>k x. if real k / real n \<le> g x then f x else 0" in bexI)
+ apply (force intro: sum.cong)+
+ done
+ qed
+ show "range \<phi> equiintegrable_on cbox a b"
+ unfolding \<phi>_def
+ by (auto simp: non0 intro: equiintegrable_on_subset [OF \<dagger>])
+ show "(\<lambda>n. \<phi> n x) \<longlonglongrightarrow> g x *\<^sub>R f x"
+ if x: "x \<in> cbox a b" for x
+ proof -
+ have eq: "\<phi> n x = \<psi> n x *\<^sub>R f x" for n
+ by (auto simp: \<phi>_def \<psi>_def sum_distrib_right if_distrib intro: sum.cong)
+ show ?thesis
+ unfolding eq
+ proof (rule tendsto_scaleR [OF _ tendsto_const])
+ show "(\<lambda>n. \<psi> n x) \<longlonglongrightarrow> g x"
+ unfolding lim_sequentially dist_real_def
+ proof (intro allI impI)
+ fix e :: real
+ assume "e > 0"
+ then obtain N where "N \<noteq> 0" "0 < inverse (real N)" and N: "inverse (real N) < e"
+ using real_arch_inverse by metis
+ moreover have "\<bar>\<psi> n x - g x\<bar> < inverse (real N)" if "n\<ge>N" for n
+ proof -
+ have "\<bar>g x - \<psi> n x\<bar> < inverse (real (\<sigma> n))"
+ unfolding \<psi>_def
+ proof (rule level_approx [of "{a..b}" g])
+ show "\<sigma> n \<noteq> 0"
+ by (metis Suc_n_not_le_n non0)
+ qed (use x 01 non0 in auto)
+ also have "\<dots> \<le> inverse N"
+ using seq_suble [OF \<sigma>] \<open>N \<noteq> 0\<close> non0 that by (auto intro: order_trans simp: divide_simps)
+ finally show ?thesis
+ by linarith
+ qed
+ ultimately show "\<exists>N. \<forall>n\<ge>N. \<bar>\<psi> n x - g x\<bar> < e"
+ using less_trans by blast
+ qed
+ qed
+ qed
+ qed
+ show thesis
+ proof
+ show "a \<le> d" "d \<le> b"
+ using \<open>d \<in> {a..b}\<close> atLeastAtMost_iff by blast+
+ show "((\<lambda>x. g x *\<^sub>R f x) has_integral integral {d..b} f) {a..b}"
+ unfolding has_integral_iff
+ proof
+ show "(\<lambda>x. g x *\<^sub>R f x) integrable_on {a..b}"
+ using ** by simp
+ show "integral {a..b} (\<lambda>x. g x *\<^sub>R f x) = integral {d..b} f"
+ proof (rule tendsto_unique)
+ show "(\<lambda>n. integral {c(\<sigma> n)..b} f) \<longlonglongrightarrow> integral {a..b} (\<lambda>x. g x *\<^sub>R f x)"
+ using ** by (simp add: c \<phi>_def)
+ show "(\<lambda>n. integral {c(\<sigma> n)..b} f) \<longlonglongrightarrow> integral {d..b} f"
+ using indefinite_integral_continuous_1' [OF f]
+ using d unfolding o_def
+ apply (simp add: continuous_on_eq_continuous_within)
+ apply (drule_tac x=d in bspec)
+ using \<open>d \<in> {a..b}\<close> apply blast
+ apply (simp add: continuous_within_sequentially o_def)
+ using cab by auto
+ qed auto
+ qed
+ qed
+qed
+
+
+theorem second_mean_value_theorem_full:
+ fixes f :: "real \<Rightarrow> real"
+ assumes f: "f integrable_on {a..b}" and "a \<le> b"
+ and g: "\<And>x y. \<lbrakk>a \<le> x; x \<le> y; y \<le> b\<rbrakk> \<Longrightarrow> g x \<le> g y"
+ obtains c where "c \<in> {a..b}"
+ and "((\<lambda>x. g x * f x) has_integral (g a * integral {a..c} f + g b * integral {c..b} f)) {a..b}"
+proof -
+ have gab: "g a \<le> g b"
+ using \<open>a \<le> b\<close> g by blast
+ then consider "g a < g b" | "g a = g b"
+ by linarith
+ then show thesis
+ proof cases
+ case 1
+ define h where "h \<equiv> \<lambda>x. if x < a then 0 else if b < x then 1
+ else (g x - g a) / (g b - g a)"
+ obtain c where "a \<le> c" "c \<le> b" and c: "((\<lambda>x. h x *\<^sub>R f x) has_integral integral {c..b} f) {a..b}"
+ proof (rule SMVT_lemma4 [OF f \<open>a \<le> b\<close>, of h])
+ show "h x \<le> h y" "0 \<le> h x \<and> h x \<le> 1" if "x \<le> y" for x y
+ using that gab by (auto simp: divide_simps g h_def)
+ qed
+ show ?thesis
+ proof
+ show "c \<in> {a..b}"
+ using \<open>a \<le> c\<close> \<open>c \<le> b\<close> by auto
+ have I: "((\<lambda>x. g x * f x - g a * f x) has_integral (g b - g a) * integral {c..b} f) {a..b}"
+ proof (subst has_integral_cong)
+ show "g x * f x - g a * f x = (g b - g a) * h x *\<^sub>R f x"
+ if "x \<in> {a..b}" for x
+ using 1 that by (simp add: h_def divide_simps algebra_simps)
+ show "((\<lambda>x. (g b - g a) * h x *\<^sub>R f x) has_integral (g b - g a) * integral {c..b} f) {a..b}"
+ using has_integral_mult_right [OF c, of "g b - g a"] .
+ qed
+ have II: "((\<lambda>x. g a * f x) has_integral g a * integral {a..b} f) {a..b}"
+ using has_integral_mult_right [where c = "g a", OF integrable_integral [OF f]] .
+ have "((\<lambda>x. g x * f x) has_integral (g b - g a) * integral {c..b} f + g a * integral {a..b} f) {a..b}"
+ using has_integral_add [OF I II] by simp
+ then show "((\<lambda>x. g x * f x) has_integral g a * integral {a..c} f + g b * integral {c..b} f) {a..b}"
+ by (simp add: algebra_simps flip: integral_combine [OF \<open>a \<le> c\<close> \<open>c \<le> b\<close> f])
+ qed
+ next
+ case 2
+ show ?thesis
+ proof
+ show "a \<in> {a..b}"
+ by (simp add: \<open>a \<le> b\<close>)
+ have "((\<lambda>x. g x * f x) has_integral g a * integral {a..b} f) {a..b}"
+ proof (rule has_integral_eq)
+ show "((\<lambda>x. g a * f x) has_integral g a * integral {a..b} f) {a..b}"
+ using f has_integral_mult_right by blast
+ show "g a * f x = g x * f x"
+ if "x \<in> {a..b}" for x
+ by (metis atLeastAtMost_iff g less_eq_real_def not_le that 2)
+ qed
+ then show "((\<lambda>x. g x * f x) has_integral g a * integral {a..a} f + g b * integral {a..b} f) {a..b}"
+ by (simp add: 2)
+ qed
+ qed
+qed
+
+
+corollary second_mean_value_theorem:
+ fixes f :: "real \<Rightarrow> real"
+ assumes f: "f integrable_on {a..b}" and "a \<le> b"
+ and g: "\<And>x y. \<lbrakk>a \<le> x; x \<le> y; y \<le> b\<rbrakk> \<Longrightarrow> g x \<le> g y"
+ obtains c where "c \<in> {a..b}"
+ "integral {a..b} (\<lambda>x. g x * f x)
+ = g a * integral {a..c} f + g b * integral {c..b} f"
+ using second_mean_value_theorem_full [where g=g, OF assms]
+ by (metis (full_types) integral_unique)
+
+
end
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Aug 15 21:46:43 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Fri Aug 16 12:53:36 2019 +0100
@@ -396,6 +396,14 @@
using major by auto
qed
+lemma integral_eq_zero_null_sets:
+ assumes "S \<in> null_sets lebesgue"
+ shows "integral\<^sup>L (lebesgue_on S) f = 0"
+proof (rule integral_eq_zero_AE)
+ show "AE x in lebesgue_on S. f x = 0"
+ by (metis (no_types, lifting) assms AE_not_in lebesgue_on_mono null_setsD2 null_sets_restrict_space order_refl)
+qed
+
lemma
shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel"
and space_lborel[simp]: "space lborel = space borel"
@@ -846,6 +854,26 @@
finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
qed
+corollary lebesgue_real_affine:
+ "c \<noteq> 0 \<Longrightarrow> lebesgue = density (distr lebesgue lebesgue (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))"
+ using lebesgue_affine_euclidean [where c= "\<lambda>x::real. c"] by simp
+
+lemma nn_integral_real_affine_lebesgue:
+ fixes c :: real assumes f[measurable]: "f \<in> borel_measurable lebesgue" and c: "c \<noteq> 0"
+ shows "(\<integral>\<^sup>+x. f x \<partial>lebesgue) = ennreal\<bar>c\<bar> * (\<integral>\<^sup>+x. f(t + c * x) \<partial>lebesgue)"
+proof -
+ have "(\<integral>\<^sup>+x. f x \<partial>lebesgue) = (\<integral>\<^sup>+x. f x \<partial>density (distr lebesgue lebesgue (\<lambda>x. t + c * x)) (\<lambda>x. ennreal \<bar>c\<bar>))"
+ using lebesgue_real_affine c by auto
+ also have "\<dots> = \<integral>\<^sup>+ x. ennreal \<bar>c\<bar> * f x \<partial>distr lebesgue lebesgue (\<lambda>x. t + c * x)"
+ by (subst nn_integral_density) auto
+ also have "\<dots> = ennreal \<bar>c\<bar> * integral\<^sup>N (distr lebesgue lebesgue (\<lambda>x. t + c * x)) f"
+ using f measurable_distr_eq1 nn_integral_cmult by blast
+ also have "\<dots> = \<bar>c\<bar> * (\<integral>\<^sup>+x. f(t + c * x) \<partial>lebesgue)"
+ using lebesgue_affine_measurable[where c= "\<lambda>x::real. c"]
+ by (subst nn_integral_distr) (force+)
+ finally show ?thesis .
+qed
+
lemma lebesgue_measurable_scaling[measurable]: "(*\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
proof cases
assume "x = 0"