diff --git a/thys/Green/Integrals.thy b/thys/Green/Integrals.thy --- a/thys/Green/Integrals.thy +++ b/thys/Green/Integrals.thy @@ -1,946 +1,852 @@ theory Integrals imports "HOL-Analysis.Analysis" General_Utils begin lemma gauge_integral_Fubini_universe_x: fixes f :: "('a::euclidean_space * 'b::euclidean_space) \ 'c::euclidean_space" assumes fun_lesbegue_integrable: "integrable lborel f" and x_axis_integral_measurable: "(\x. integral UNIV (\y. f(x, y))) \ borel_measurable lborel" shows "integral UNIV f = integral UNIV (\x. integral UNIV (\y. f(x,y)))" "(\x. integral UNIV (\y. f(x,y))) integrable_on UNIV" proof - have f_is_measurable: "f \ borel_measurable lborel" using fun_lesbegue_integrable and borel_measurable_integrable by auto have fun_lborel_prod_integrable: "integrable (lborel \\<^sub>M lborel) f" using fun_lesbegue_integrable by (simp add: lborel_prod) then have region_integral_is_one_twoD_integral: - "(LBINT x. (LBINT y. f (x, y))) = integral\<^sup>L (lborel \\<^sub>M lborel) f" + "(LBINT x. LBINT y. f (x, y)) = integral\<^sup>L (lborel \\<^sub>M lborel) f" using lborel_pair.integral_fst' by auto then have AE_one_D_integrals_eq: "AE x in lborel. (LBINT y. f (x, y)) = integral UNIV (\y. f(x,y))" proof - have "AE x in lborel. integrable lborel (\y. f(x,y))" using lborel_pair.AE_integrable_fst' and fun_lborel_prod_integrable by blast then show ?thesis using integral_lborel and always_eventually and AE_mp by fastforce qed have one_D_integral_measurable: "(\x. LBINT y. f (x, y)) \ borel_measurable lborel" using f_is_measurable and lborel.borel_measurable_lebesgue_integral by auto then have second_lesbegue_integral_eq: - "(LBINT x. (LBINT y. f (x, y))) = (LBINT x. (integral UNIV (\y. f(x,y))))" + "(LBINT x. LBINT y. f (x, y)) = (LBINT x. integral UNIV (\y. f(x,y)))" using x_axis_integral_measurable and integral_cong_AE and AE_one_D_integrals_eq by blast have "integrable lborel (\x. LBINT y. f (x, y))" using fun_lborel_prod_integrable and lborel_pair.integrable_fst' by auto then have oneD_gauge_integral_lesbegue_integrable: "integrable lborel (\x. integral UNIV (\y. f(x,y)))" using x_axis_integral_measurable and AE_one_D_integrals_eq and integrable_cong_AE_imp by blast then show one_D_gauge_integral_integrable: "(\x. integral UNIV (\y. f(x,y))) integrable_on UNIV" using integrable_on_lborel by auto - have "(LBINT x. (integral UNIV (\y. f(x,y)))) = integral UNIV (\x. integral UNIV (\y. f(x, y)))" + have "(LBINT x. integral UNIV (\y. f(x,y))) = integral UNIV (\x. integral UNIV (\y. f(x, y)))" using integral_lborel oneD_gauge_integral_lesbegue_integrable by fastforce then have twoD_lesbeuge_eq_twoD_gauge: - "(LBINT x. (LBINT y. f (x, y))) = integral UNIV (\x. integral UNIV (\y. f(x, y)))" + "(LBINT x. LBINT y. f (x, y)) = integral UNIV (\x. integral UNIV (\y. f(x, y)))" using second_lesbegue_integral_eq by auto then show "integral UNIV f = integral UNIV (\x. integral UNIV (\y. f(x,y)))" using fun_lesbegue_integrable and integral_lborel and region_integral_is_one_twoD_integral by (metis lborel_prod) qed lemma gauge_integral_Fubini_universe_y: fixes f :: "('a::euclidean_space * 'b::euclidean_space) \ 'c::euclidean_space" assumes fun_lesbegue_integrable: "integrable lborel f" and y_axis_integral_measurable: "(\x. integral UNIV (\y. f(y, x))) \ borel_measurable lborel" shows "integral UNIV f = integral UNIV (\x. integral UNIV (\y. f(y, x)))" "(\x. integral UNIV (\y. f(y, x))) integrable_on UNIV" proof - have f_is_measurable: "f \ borel_measurable lborel" using fun_lesbegue_integrable and borel_measurable_integrable by auto have fun_lborel_prod_integrable: "integrable (lborel \\<^sub>M lborel) f" using fun_lesbegue_integrable by (simp add: lborel_prod) then have region_integral_is_one_twoD_integral: - "(LBINT x. (LBINT y. f (y, x))) = integral\<^sup>L (lborel \\<^sub>M lborel) f" - using lborel_pair.integral_fst' - f_is_measurable lborel_pair.integrable_product_swap lborel_pair.integral_fst lborel_pair.integral_product_swap lborel_prod - by force + "(LBINT x. LBINT y. f (y, x)) = integral\<^sup>L (lborel \\<^sub>M lborel) f" + by (simp add: lborel_pair.integrable_product_swap_iff lborel_pair.integral_fst lborel_pair.integral_product_swap) then have AE_one_D_integrals_eq: "AE x in lborel. (LBINT y. f (y, x)) = integral UNIV (\y. f(y,x))" proof - have "AE x in lborel. integrable lborel (\y. f(y,x))" using lborel_pair.AE_integrable_fst' and fun_lborel_prod_integrable lborel_pair.AE_integrable_fst lborel_pair.integrable_product_swap by blast then show ?thesis - using integral_lborel and always_eventually - and AE_mp - by fastforce + using integral_lborel always_eventually AE_mp by fastforce qed have one_D_integral_measurable: "(\x. LBINT y. f (y, x)) \ borel_measurable lborel" using f_is_measurable and lborel.borel_measurable_lebesgue_integral by auto then have second_lesbegue_integral_eq: - "(LBINT x. (LBINT y. f (y, x))) = (LBINT x. (integral UNIV (\y. f(y, x))))" + "(LBINT x. LBINT y. f (y, x)) = (LBINT x. integral UNIV (\y. f(y, x)))" using y_axis_integral_measurable and integral_cong_AE and AE_one_D_integrals_eq by blast have "integrable lborel (\x. LBINT y. f (y, x))" using fun_lborel_prod_integrable and lborel_pair.integrable_fst' by (simp add: lborel_pair.integrable_fst lborel_pair.integrable_product_swap) then have oneD_gauge_integral_lesbegue_integrable: "integrable lborel (\x. integral UNIV (\y. f(y, x)))" using y_axis_integral_measurable and AE_one_D_integrals_eq and integrable_cong_AE_imp by blast then show one_D_gauge_integral_integrable: "(\x. integral UNIV (\y. f(y, x))) integrable_on UNIV" - using integrable_on_lborel - by auto - have "(LBINT x. (integral UNIV (\y. f(y, x)))) = integral UNIV (\x. integral UNIV (\y. f(y, x)))" + using integrable_on_lborel by auto + have "(LBINT x. integral UNIV (\y. f(y, x))) = integral UNIV (\x. integral UNIV (\y. f(y, x)))" using integral_lborel oneD_gauge_integral_lesbegue_integrable by fastforce then have twoD_lesbeuge_eq_twoD_gauge: - "(LBINT x. (LBINT y. f (y, x))) = integral UNIV (\x. integral UNIV (\y. f(y, x)))" - using second_lesbegue_integral_eq - by auto + "(LBINT x. LBINT y. f (y, x)) = integral UNIV (\x. integral UNIV (\y. f(y, x)))" + using second_lesbegue_integral_eq by auto then show "integral UNIV f = integral UNIV (\x. integral UNIV (\y. f(y, x)))" using fun_lesbegue_integrable and integral_lborel and region_integral_is_one_twoD_integral by (metis lborel_prod) qed lemma gauge_integral_Fubini_curve_bounded_region_x: fixes f g :: "('a::euclidean_space * 'b::euclidean_space) \ 'c::euclidean_space" and g1 g2:: "'a \ 'b" and s:: "('a * 'b) set" assumes fun_lesbegue_integrable: "integrable lborel f" and x_axis_gauge_integrable: "\x. (\y. f(x, y)) integrable_on UNIV" and (*IS THIS redundant? NO IT IS NOT*) x_axis_integral_measurable: "(\x. integral UNIV (\y. f(x, y))) \ borel_measurable lborel" and f_is_g_indicator: "f = (\x. if x \ s then g x else 0)" and s_is_bounded_by_g1_and_g2: "s = {(x,y). (\i\Basis. a \ i \ x \ i \ x \ i \ b \ i) \ (\i\Basis. (g1 x) \ i \ y \ i \ y \ i \ (g2 x) \ i)}" shows "integral s g = integral (cbox a b) (\x. integral (cbox (g1 x) (g2 x)) (\y. g(x,y)))" proof - have two_D_integral_to_one_D: "integral UNIV f = integral UNIV (\x. integral UNIV (\y. f(x,y)))" using gauge_integral_Fubini_universe_x and fun_lesbegue_integrable and x_axis_integral_measurable by auto have one_d_integral_integrable: "(\x. integral UNIV (\y. f(x,y))) integrable_on UNIV" using gauge_integral_Fubini_universe_x(2) and assms by blast have case_x_in_range: "\ x \ cbox a b. integral (cbox (g1 x) (g2 x)) (\y. g(x,y)) = integral UNIV (\y. f(x,y))" proof fix x:: 'a assume within_range: "x \ (cbox a b)" let ?f_one_D_spec = "(\y. if y \ (cbox (g1 x) (g2 x)) then g(x,y) else 0)" have f_one_D_region: "(\y. f(x,y)) = (\y. if y \ cbox (g1 x) (g2 x) then g(x,y) else 0)" proof fix y::'b show "f (x, y) = (if y \ (cbox (g1 x) (g2 x)) then g (x, y) else 0)" - apply (simp add: f_is_g_indicator s_is_bounded_by_g1_and_g2) using within_range - apply (simp add: cbox_def) - by smt + by (force simp add: cbox_def f_is_g_indicator s_is_bounded_by_g1_and_g2) qed have zero_out_of_bound: "\ y. y \ cbox (g1 x) (g2 x) \ f (x,y) = 0" using f_is_g_indicator and s_is_bounded_by_g1_and_g2 by (auto simp add: cbox_def) have "(\y. f(x,y)) integrable_on cbox (g1 x) (g2 x)" proof - have "?f_one_D_spec integrable_on UNIV" using f_one_D_region and x_axis_gauge_integrable by metis then have "?f_one_D_spec integrable_on cbox(g1 x) (g2 x)" - using integrable_on_subcbox - by blast + using integrable_on_subcbox by blast then show ?thesis using f_one_D_region by auto qed then have f_integrale_x: "((\y. f(x,y)) has_integral (integral (cbox (g1 x) (g2 x)) (\y. f(x,y)))) (cbox (g1 x) (g2 x))" using integrable_integral and within_range and x_axis_gauge_integrable by auto have "integral (cbox (g1 x) (g2 x)) (\y. f (x, y)) = integral UNIV (\y. f (x, y))" using has_integral_on_superset[OF f_integrale_x _ Set.subset_UNIV] zero_out_of_bound by (simp add: integral_unique) then have "((\y. f(x, y)) has_integral integral UNIV (\y. f (x, y))) (cbox (g1 x) (g2 x))" using f_integrale_x by simp then have "((\y. g(x, y)) has_integral integral UNIV (\y. f (x, y))) (cbox (g1 x)(g2 x))" - using Henstock_Kurzweil_Integration.has_integral_restrict [OF subset_refl ] and - f_one_D_region - by (smt has_integral_eq) + by (simp add: f_one_D_region) then show "integral (cbox (g1 x) (g2 x)) (\y. g (x, y)) = integral UNIV (\y. f (x, y))" by auto qed have case_x_not_in_range: "\ x. x \ cbox a b \ integral UNIV (\y. f(x,y)) = 0" proof fix x::'a have "x \ (cbox a b) \ (\y. f(x,y) = 0)" - apply (simp add: s_is_bounded_by_g1_and_g2 f_is_g_indicator cbox_def) - by auto + by (auto simp add: s_is_bounded_by_g1_and_g2 f_is_g_indicator cbox_def) then show "x \ cbox a b \ integral UNIV (\y. f (x, y)) = 0" by (simp) qed have RHS: "integral UNIV (\x. integral UNIV (\y. f(x,y))) = integral (cbox a b) (\x. integral (cbox (g1 x) (g2 x)) (\y. g(x,y)))" proof - let ?first_integral = "(\x. integral (cbox (g1 x) (g2 x)) (\y. g(x,y)))" let ?x_integral_cases = "(\x. if x \ cbox a b then ?first_integral x else 0)" have x_integral_cases_integral: "(\x. integral UNIV (\y. f(x,y))) = ?x_integral_cases" using case_x_in_range and case_x_not_in_range by auto have "((\x. integral UNIV (\y. f(x,y))) has_integral (integral UNIV f)) UNIV" - using two_D_integral_to_one_D - one_d_integral_integrable - by auto + using two_D_integral_to_one_D one_d_integral_integrable by auto then have "(?x_integral_cases has_integral (integral UNIV f)) UNIV" using x_integral_cases_integral by auto then have "(?first_integral has_integral (integral UNIV f)) (cbox a b)" using has_integral_restrict_UNIV[of "cbox a b" "?first_integral" "integral UNIV f"] by auto then show ?thesis - using two_D_integral_to_one_D - by (simp add: integral_unique) + using two_D_integral_to_one_D by (simp add: integral_unique) qed have f_integrable:"f integrable_on UNIV" using fun_lesbegue_integrable and integrable_on_lborel by auto then have LHS: "integral UNIV f = integral s g" - apply (simp add: f_is_g_indicator) - using integrable_restrict_UNIV - integral_restrict_UNIV - by auto + using assms(4) integrable_integral by fastforce then show ?thesis using RHS and two_D_integral_to_one_D by auto qed lemma gauge_integral_Fubini_curve_bounded_region_y: fixes f g :: "('a::euclidean_space * 'b::euclidean_space) \ 'c::euclidean_space" and g1 g2:: "'b \ 'a" and s:: "('a * 'b) set" assumes fun_lesbegue_integrable: "integrable lborel f" and y_axis_gauge_integrable: "\x. (\y. f(y, x)) integrable_on UNIV" and (*IS THIS redundant? NO IT IS NOT*) y_axis_integral_measurable: "(\x. integral UNIV (\y. f(y, x))) \ borel_measurable lborel" and f_is_g_indicator: "f = (\x. if x \ s then g x else 0)" and s_is_bounded_by_g1_and_g2: "s = {(y, x). (\i\Basis. a \ i \ x \ i \ x \ i \ b \ i) \ (\i\Basis. (g1 x) \ i \ y \ i \ y \ i \ (g2 x) \ i)}" shows "integral s g = integral (cbox a b) (\x. integral (cbox (g1 x) (g2 x)) (\y. g(y, x)))" proof - have two_D_integral_to_one_D: "integral UNIV f = integral UNIV (\x. integral UNIV (\y. f(y, x)))" using gauge_integral_Fubini_universe_y and fun_lesbegue_integrable and y_axis_integral_measurable by auto have one_d_integral_integrable: "(\x. integral UNIV (\y. f(y, x))) integrable_on UNIV" using gauge_integral_Fubini_universe_y(2) and assms by blast have case_y_in_range: "\ x \ cbox a b. integral (cbox (g1 x) (g2 x)) (\y. g(y, x)) = integral UNIV (\y. f(y, x))" proof fix x:: 'b assume within_range: "x \ (cbox a b)" let ?f_one_D_spec = "(\y. if y \ (cbox (g1 x) (g2 x)) then g(y, x) else 0)" have f_one_D_region: "(\y. f(y, x)) = (\y. if y \ cbox (g1 x) (g2 x) then g(y, x) else 0)" proof fix y::'a show "f (y, x) = (if y \ (cbox (g1 x) (g2 x)) then g (y, x) else 0)" - apply (simp add: f_is_g_indicator s_is_bounded_by_g1_and_g2) using within_range - apply (simp add: cbox_def) - by smt + by (force simp add: cbox_def f_is_g_indicator s_is_bounded_by_g1_and_g2) qed have zero_out_of_bound: "\ y. y \ cbox (g1 x) (g2 x) \ f (y, x) = 0" using f_is_g_indicator and s_is_bounded_by_g1_and_g2 by (auto simp add: cbox_def) have "(\y. f(y, x)) integrable_on cbox (g1 x) (g2 x)" proof - have "?f_one_D_spec integrable_on UNIV" using f_one_D_region and y_axis_gauge_integrable by metis then have "?f_one_D_spec integrable_on cbox(g1 x) (g2 x)" using integrable_on_subcbox by blast then show ?thesis using f_one_D_region by auto qed then have f_integrale_y: "((\y. f(y, x)) has_integral (integral (cbox (g1 x) (g2 x)) (\y. f(y,x)))) (cbox (g1 x) (g2 x))" using integrable_integral and within_range and y_axis_gauge_integrable by auto have "integral (cbox (g1 x) (g2 x)) (\y. f (y, x)) = integral UNIV (\y. f (y, x))" using has_integral_on_superset[OF f_integrale_y _ Set.subset_UNIV] zero_out_of_bound by (simp add: integral_unique) then have "((\y. f(y, x)) has_integral integral UNIV (\y. f (y, x))) (cbox (g1 x) (g2 x))" using f_integrale_y by simp then have "((\y. g(y, x)) has_integral integral UNIV (\y. f (y, x))) (cbox (g1 x)(g2 x))" - using Henstock_Kurzweil_Integration.has_integral_restrict [OF subset_refl ] and - f_one_D_region - by (smt has_integral_eq) + using f_one_D_region by fastforce then show "integral (cbox (g1 x) (g2 x)) (\y. g (y, x)) = integral UNIV (\y. f (y, x))" by auto qed have case_y_not_in_range: "\ x. x \ cbox a b \ integral UNIV (\y. f(y, x)) = 0" proof fix x::'b have "x \ (cbox a b) \ (\y. f(y, x) = 0)" apply (simp add: s_is_bounded_by_g1_and_g2 f_is_g_indicator cbox_def) by auto then show "x \ cbox a b \ integral UNIV (\y. f (y, x)) = 0" by (simp) qed have RHS: "integral UNIV (\x. integral UNIV (\y. f(y, x))) = integral (cbox a b) (\x. integral (cbox (g1 x) (g2 x)) (\y. g(y, x)))" proof - let ?first_integral = "(\x. integral (cbox (g1 x) (g2 x)) (\y. g(y, x)))" let ?x_integral_cases = "(\x. if x \ cbox a b then ?first_integral x else 0)" have y_integral_cases_integral: "(\x. integral UNIV (\y. f(y, x))) = ?x_integral_cases" using case_y_in_range and case_y_not_in_range by auto have "((\x. integral UNIV (\y. f(y, x))) has_integral (integral UNIV f)) UNIV" using two_D_integral_to_one_D one_d_integral_integrable by auto then have "(?x_integral_cases has_integral (integral UNIV f)) UNIV" using y_integral_cases_integral by auto then have "(?first_integral has_integral (integral UNIV f)) (cbox a b)" using has_integral_restrict_UNIV[of "cbox a b" "?first_integral" "integral UNIV f"] by auto then show ?thesis using two_D_integral_to_one_D by (simp add: integral_unique) qed have f_integrable:"f integrable_on UNIV" using fun_lesbegue_integrable and integrable_on_lborel by auto then have LHS: "integral UNIV f = integral s g" apply (simp add: f_is_g_indicator) using integrable_restrict_UNIV integral_restrict_UNIV by auto then show ?thesis using RHS and two_D_integral_to_one_D by auto qed lemma gauge_integral_by_substitution: fixes f::"(real \ real)" and g::"(real \ real)" and g'::"real \ real" and a::"real" and b::"real" assumes a_le_b: "a \ b" and ga_le_gb: "g a \ g b" and g'_derivative: "\x \ {a..b}. (g has_vector_derivative (g' x)) (at x within {a..b})" and g'_continuous: "continuous_on {a..b} g'" and f_continuous: "continuous_on (g ` {a..b}) f" shows "integral {g a..g b} (f) = integral {a..b} (\x. f(g x) * (g' x))" proof - have "\x \ {a..b}. (g has_real_derivative (g' x)) (at x within {a..b})" using has_real_derivative_iff_has_vector_derivative[of "g"] and g'_derivative by auto then have 2: "interval_lebesgue_integral lborel (ereal (a)) (ereal (b)) (\x. g' x *\<^sub>R f (g x)) = interval_lebesgue_integral lborel (ereal (g a)) (ereal (g b)) f" using interval_integral_substitution_finite[of "a" "b" "g" "g'" "f"] and g'_continuous and a_le_b and f_continuous by auto have g_continuous: "continuous_on {a .. b} g" using Derivative.differentiable_imp_continuous_on apply (simp add: differentiable_on_def differentiable_def) by (metis continuous_on_vector_derivative g'_derivative) have "set_integrable lborel {a .. b} (\x. g' x *\<^sub>R f (g x))" proof - have "continuous_on {a .. b} (\x. g' x *\<^sub>R f (g x))" proof - have "continuous_on {a .. b} (\x. f (g x))" proof - show ?thesis using Topological_Spaces.continuous_on_compose f_continuous g_continuous by auto qed then show ?thesis using Limits.continuous_on_mult g'_continuous by auto qed then show ?thesis using borel_integrable_atLeastAtMost' by blast qed then have 0: "interval_lebesgue_integral lborel (ereal (a)) (ereal (b)) (\x. g' x *\<^sub>R f (g x)) = integral {a .. b} (\x. g' x *\<^sub>R f (g x))" using a_le_b and interval_integral_eq_integral by (metis (no_types)) have "set_integrable lborel {g a .. g b} f" proof - have "continuous_on {g a .. g b} f" proof - have "{g a .. g b} \ g ` {a .. b}" using g_continuous by (metis a_le_b atLeastAtMost_iff atLeastatMost_subset_iff continuous_image_closed_interval imageI order_refl) then show "continuous_on {g a .. g b} f" using f_continuous continuous_on_subset by blast qed then show ?thesis using borel_integrable_atLeastAtMost' by blast qed then have 1: "interval_lebesgue_integral lborel (ereal (g a)) (ereal (g b)) f = integral {g a .. g b} f" using ga_le_gb and interval_integral_eq_integral by (metis (no_types)) then show ?thesis using 0 and 1 and 2 by (metis (no_types, lifting) Henstock_Kurzweil_Integration.integral_cong mult.commute real_scaleR_def) qed lemma frontier_ic: assumes "a < (b::real)" shows "frontier {a<..b} = {a,b}" apply(simp add: frontier_def) using assms by auto lemma frontier_ci: assumes "a < (b::real)" shows "frontier {a<.. closed {a<..b}" using assms frontier_subset_eq frontier_ic greaterThanAtMost_iff by blast lemma closure_ic_union_ci: assumes "a < (b::real)" "b < c" shows "closure ({a.. {b<..c}) = {a .. c}" using frontier_ic[OF assms(1)] frontier_ci[OF assms(2)] closure_Un assms apply(simp add: frontier_def) by auto lemma interior_ic_ci_union: assumes "a < (b::real)" "b < c" shows "b \ (interior ({a.. {b<..c}))" proof- have "b \ ({a.. {b<..c})" by auto then show ?thesis using interior_subset by blast qed lemma frontier_ic_union_ci: assumes "a < (b::real)" "b < c" shows "b \ frontier ({a.. {b<..c})" using closure_ic_union_ci assms interior_ic_ci_union by(simp add: frontier_def) lemma ic_union_ci_not_closed: assumes "a < (b::real)" "b < c" shows "\ closed ({a.. {b<..c})" proof- have "b \ ({a.. {b<..c})" by auto then show ?thesis using assms frontier_subset_eq frontier_ic_union_ci[OF assms] by (auto simp only: subset_iff) qed lemma integrable_continuous_: fixes f :: "'b::euclidean_space \ 'a::banach" assumes "continuous_on (cbox a b) f" shows "f integrable_on cbox a b" by (simp add: assms integrable_continuous) lemma removing_singletons_from_div: assumes "\t\S. \c d::real. c < d \ {c..d} = t" "{x} \ \S = {a..b}" "a < x" "x < b" "finite S" shows "\t\S. x \ t" proof(rule ccontr) assume "\(\t\S. x \ t)" then have "\t\S. x \ t" by auto then have "x \ \S" by auto then have i: "\S = {a..b} - {x}" using assms (2) by auto have "x \ {a..b}" using assms by auto then have "{a .. b} - {x} = {a.. {x<..b}" by auto then have 0: "\S = {a.. {x<..b}" using i by auto have 1:"closed (\S)" apply(rule closed_Union) proof- show "finite S" using assms by auto show "\T\S. closed T" using assms by auto qed show False using 0 1 ic_union_ci_not_closed assms by auto qed lemma remove_singleton_from_division_of:(*By Manuel Eberl*) assumes "A division_of {a::real..b}" "a < b" assumes "x \ {a..b}" shows "\c d. c < d \ {c..d} \ A \ x \ {c..d}" proof - from assms have "x islimpt {a..b}" by (intro connected_imp_perfect) auto also have "{a..b} = {x. {x..x} \ A} \ ({a..b} - {x. {x..x} \ A})" using assms by auto also have "x islimpt \ \ x islimpt {a..b} - {x. {x..x} \ A}" proof (intro islimpt_Un_finite) have "{x. {x..x} \ A} \ Inf ` A" proof safe fix x assume "{x..x} \ A" thus "x \ Inf ` A" by (auto intro!: bexI[of _ "{x}"] simp: image_iff) qed moreover from assms have "finite A" by (auto simp: division_of_def) hence "finite (Inf ` A)" by auto ultimately show "finite {x. {x..x} \ A}" by (rule finite_subset) qed also have "{a..b} = \A" using assms by (auto simp: division_of_def) finally have "x islimpt \(A - range (\x. {x..x}))" by (rule islimpt_subset) auto moreover have "closed (\(A - range (\x. {x..x})))" using assms by (intro closed_Union) auto ultimately have "x \ (\(A - range (\x. {x..x})))" by (auto simp: closed_limpt) then obtain X where "x \ X" "X \ A" "X \ range (\x. {x..x})" by blast moreover from division_ofD(2)[OF assms(1) this(2)] division_ofD(3)[OF assms(1) this(2)] division_ofD(4)[OF assms(1) this(2)] obtain c d where "X = cbox c d" "X \ {a..b}" "X \ {}" by blast ultimately have "c \ d" by auto have "c \ d" proof assume "c = d" with \X = cbox c d\ have "X = {c..c}" by auto hence "X \ range (\x. {x..x})" by blast with \X \ range (\x. {x..x})\ show False by contradiction qed with \c \ d\ have "c < d" by simp with \X = cbox c d\ and \x \ X\ and \X \ A\ show ?thesis by auto qed lemma remove_singleton_from_tagged_division_of: assumes "A tagged_division_of {a::real..b}" "a < b" assumes "x \ {a..b}" shows "\k c d. c < d \ (k, {c..d}) \ A \ x \ {c..d}" using remove_singleton_from_division_of[OF division_of_tagged_division[OF assms(1)] assms(2)] - (*sledgehammer*) using assms(3) by fastforce lemma tagged_div_wo_singlestons: assumes "p tagged_division_of {a::real..b}" "a < b" shows "(p - {xk. \x y. xk = (x,{y})}) tagged_division_of cbox a b" using remove_singleton_from_tagged_division_of[OF assms] assms apply(auto simp add: tagged_division_of_def tagged_partial_division_of_def) apply blast apply blast apply blast by fastforce lemma tagged_div_wo_empty: assumes "p tagged_division_of {a::real..b}" "a < b" shows "(p - {xk. \x. xk = (x,{})}) tagged_division_of cbox a b" using remove_singleton_from_tagged_division_of[OF assms] assms apply(auto simp add: tagged_division_of_def tagged_partial_division_of_def) apply blast apply blast apply blast by fastforce lemma fine_diff: assumes "\ fine p" shows "\ fine (p - s)" apply (auto simp add: fine_def) using assms by auto lemma tagged_div_tage_notin_set: assumes "finite (s::real set)" "p tagged_division_of {a..b}" "\ fine p" "(\(x, K)\p. \c d::real. c < d \ K = {c..d})" "gauge \" shows "\p' \'. p' tagged_division_of {a..b} \ \' fine p' \ (\(x, K)\p'. x \ s) \ gauge \'" proof- have "(\(x::real, K)\p. \x'. x' \ s \ x'\ interior K)" proof- {fix x::real fix K assume ass: "(x::real,K) \ p" have "(\(x, K)\p. infinite (interior K))" using assms(4) infinite_Ioo interior_atLeastAtMost_real - by (smt split_beta) + by (smt (verit) split_beta) then have i: "infinite (interior K)" using ass by auto have "\x'. x' \ s \ x'\ interior K" using infinite_imp_nonempty[OF Diff_infinite_finite[OF assms(1) i]] by auto} then show ?thesis by auto qed then obtain f where f: "(\(x::real, K)\p. (f (x,K)) \ s \ (f (x,K)) \ interior K)" using choice_iff[where ?Q = "\(x,K) x'. (x::real, K)\p \ x' \ s \ x' \ interior K"] apply (auto simp add: case_prod_beta) by metis have f': "(\(x::real, K)\p. (f (x,K)) \ s \ (f (x,K)) \ K)" using f interior_subset by (auto simp add: case_prod_beta subset_iff) let ?p' = "{m. (\xK. m = ((f xK), snd xK) \ xK \ p)}" have 0: "(\(x, K)\?p'. x \ s)" using f by (auto simp add: case_prod_beta) have i: "finite {(f (a, b), b) |a b. (a, b) \ p}" proof- have a: "{(f (a, b), b) |a b. (a, b) \ p} = (%(a,b). (f(a,b),b)) ` p" by auto have b: "finite p" using assms(2) by auto show ?thesis using a b by auto qed have 1: "?p' tagged_division_of {a..b}" using assms(2) f' apply(auto simp add: tagged_division_of_def tagged_partial_division_of_def case_prod_beta) apply(metis i) apply blast apply blast by fastforce (*f is injective becuase interiors of different K's are disjoint and f is in interior*) have f_inj: "inj_on f p" - apply(simp add: inj_on_def) - proof- - {fix x y - assume "x \ p" "y \ p" - "f x = f y" - then have "x = y" - using f - tagged_division_ofD(5)[OF assms(2)] - (*sledgehammer*) - by (smt case_prodE disjoint_insert(2) mk_disjoint_insert)}note * = this - show "\x\p. \y\p. f x = f y \ x = y" using * by auto + unfolding inj_on_def + proof (intro strip) + fix x y + assume "x \ p" "y \ p" "f x = f y" + then show "x = y" + using f tagged_division_ofD(5)[OF assms(2)] + by (smt (verit, del_insts) IntI case_prodE empty_iff) qed let ?\' = "\x. if (\xK \ p. f xK = x) then (\ o fst o the_inv_into p f) x else \ x" have 2: "?\' fine ?p'" using assms(3) - apply(auto simp add: fine_def case_prod_beta the_inv_into_f_f[OF f_inj]) - by force + by (force simp add: fine_def case_prod_beta the_inv_into_f_f[OF f_inj]) have 3: "gauge ?\'" using assms(5) assms(3) f' - apply(auto simp add: fine_def gauge_def case_prod_beta the_inv_into_f_f[OF f_inj]) - by force + by (force simp add: fine_def gauge_def case_prod_beta the_inv_into_f_f[OF f_inj]) have "?p' tagged_division_of {a..b} \ ?\' fine ?p' \ (\(x, K)\?p'. x \ s) \ gauge ?\'" using 0 1 2 3 by auto - then show ?thesis by smt + then show ?thesis by meson qed lemma has_integral_bound_spike_finite: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" assumes "0 \ B" and "finite S" and f: "(f has_integral i) (cbox a b)" and leB: "\x. x \ cbox a b - S \ norm (f x) \ B" shows "norm i \ B * content (cbox a b)" proof - define g where "g \ (\x. if x \ S then 0 else f x)" then have "\x. x \ cbox a b - S \ norm (g x) \ B" using leB by simp moreover have "(g has_integral i) (cbox a b)" using has_integral_spike_finite [OF \finite S\ _ f] by (simp add: g_def) ultimately show ?thesis by (simp add: \0 \ B\ g_def has_integral_bound) qed lemma has_integral_bound_: fixes f :: "real \ 'a::real_normed_vector" assumes "a < b" and "0 \ B" and f: "(f has_integral i) (cbox a b)" and "finite s" and "\x\(cbox a b)-s. norm (f x) \ B" shows "norm i \ B * content (cbox a b)" using has_integral_bound_spike_finite assms by blast corollary has_integral_bound_real': fixes f :: "real \ 'b::real_normed_vector" assumes "0 \ B" and f: "(f has_integral i) (cbox a b)" and "finite s" and "\x\(cbox a b)-s. norm (f x) \ B" shows "norm i \ B * content {a..b}" - (*sledgehammer*) by (metis assms(1) assms(3) assms(4) box_real(2) f has_integral_bound_spike_finite) lemma integral_has_vector_derivative_continuous_at': fixes f :: "real \ 'a::banach" assumes "finite s" and f: "f integrable_on {a..b}" and x: "x \ {a..b} - s" and fx: "continuous (at x within ({a..b} - s)) f" shows "((\u. integral {a..u} f) has_vector_derivative f x) (at x within ({a..b} - s))" proof - let ?I = "\a b. integral {a..b} f" { fix e::real assume "e > 0" obtain d where "d>0" and d: "\x'. \x' \ {a..b} - s; \x' - x\ < d\ \ norm(f x' - f x) \ e" using \e>0\ fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le) have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \ e * \y - x\" if y: "y \ {a..b} - s" and yx: "\y - x\ < d" for y proof (cases "y < x") case False have "f integrable_on {a..y}" using f y by (simp add: integrable_subinterval_real) then have Idiff: "?I a y - ?I a x = ?I x y" using False x by (simp add: algebra_simps Henstock_Kurzweil_Integration.integral_combine) have fux_int: "((\u. f u - f x) has_integral integral {x..y} f - (y-x) *\<^sub>R f x) {x..y}" apply (rule has_integral_diff) using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]]) using has_integral_const_real [of "f x" x y] False apply simp done show ?thesis using False apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc) apply (rule has_integral_bound_real'[where f="(\u. f u - f x)"]) using yx False d x y \e>0\ apply (auto simp add: Idiff fux_int) proof- let ?M48= "mset_set s" show "\z. y - x < d \ (\x'. a \ x' \ x' \ b \ x' \ s \ \x' - x\ < d \ norm (f x' - f x) \ e) \ 0 < e \ z \# ?M48 \ a \ x \ x \ s \ y \ b \ y \ s \ x \ z \ z \ y \ norm (f z - f x) \ e" using assms by auto qed next case True have "f integrable_on {a..x}" using f x by (simp add: integrable_subinterval_real) then have Idiff: "?I a x - ?I a y = ?I y x" using True x y by (simp add: algebra_simps Henstock_Kurzweil_Integration.integral_combine) have fux_int: "((\u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}" apply (rule has_integral_diff) using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]]) using has_integral_const_real [of "f x" y x] True - apply simp - done + by simp have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \ e * \y - x\" using True apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc) apply (rule has_integral_bound_real'[where f="(\u. f u - f x)"]) using yx True d x y \e>0\ apply (auto simp add: Idiff fux_int) proof- let ?M44= "mset_set s" show " \xa. x - y < d \ y < x \ (\x'. a \ x' \ x' \ b \ x' \ s \ \x' - x\ < d \ norm (f x' - f x) \ e) \ 0 < e \ xa \# ?M44 \ x \ b \ x \ s \ a \ y \ y \ s \ y \ xa \ xa \ x \ norm (f xa - f x) \ e" using assms by auto qed then show ?thesis by (simp add: algebra_simps norm_minus_commute) qed then have "\d>0. \y\{a..b} - s. \y - x\ < d \ norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \ e * \y - x\" using \d>0\ by blast } then show ?thesis by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left) qed -lemma integral_has_vector_derivative': - fixes f :: "real \ 'a::banach" - assumes "finite s" - "f integrable_on {a..b}" - "x \ {a..b} - s" - "continuous (at x within {a..b} - s) f" - shows "((\u. integral {a .. u} f) has_vector_derivative f(x)) (at x within {a .. b} - s)" - apply (rule integral_has_vector_derivative_continuous_at') - using assms - apply (auto simp: continuous_on_eq_continuous_within) - done - -lemma fundamental_theorem_of_calculus_interior_stronger: - fixes f :: "real \ 'a::banach" - assumes "finite S" - and "a \ b" "\x. x \ {a <..< b} - S \ (f has_vector_derivative f'(x)) (at x)" - and "continuous_on {a .. b} f" - shows "(f' has_integral (f b - f a)) {a .. b}" - using assms -proof (induction arbitrary: a b) - case empty - then show ?case - using fundamental_theorem_of_calculus_interior by force -next - case (insert x S) - show ?case - proof (cases "x \ {a<..a < x\ \x < b\ insert.prems continuous_on_subset by force+ - moreover have "(f' has_integral f b - f x) {x..b}" - apply (rule insert) - using \x < b\ \a < x\ insert.prems continuous_on_subset by force+ - ultimately show ?thesis - by (meson finite_insert fundamental_theorem_of_calculus_interior_strong insert.hyps(1) insert.prems(1) insert.prems(2) insert.prems(3)) - qed -qed - lemma at_within_closed_interval_finite: fixes x::real assumes "a < x" "x < b" "x \ S" "finite S" shows "(at x within {a..b} - S) = at x" proof - have "interior ({a..b} - S) = {a<..finite S\ by (simp add: interior_diff finite_imp_closed) then show ?thesis using at_within_interior assms by fastforce qed -lemma at_within_cbox_finite: - assumes "x \ box a b" "x \ S" "finite S" - shows "(at x within cbox a b - S) = at x" -proof - - have "interior (cbox a b - S) = box a b - S" - using \finite S\ by (simp add: interior_diff finite_imp_closed) - then show ?thesis - using at_within_interior assms by fastforce -qed - lemma fundamental_theorem_of_calculus_interior_stronger': fixes f :: "real \ 'a::banach" assumes "finite S" and "a \ b" "\x. x \ {a <..< b} - S \ (f has_vector_derivative f'(x)) (at x within {a..b} - S)" and "continuous_on {a .. b} f" shows "(f' has_integral (f b - f a)) {a .. b}" using assms fundamental_theorem_of_calculus_interior_strong at_within_cbox_finite - (*sledgehammer*) by (metis DiffD1 DiffD2 interior_atLeastAtMost_real interior_cbox interval_cbox) lemma has_integral_substitution_general_: fixes f :: "real \ 'a::euclidean_space" and g :: "real \ real" assumes s: "finite s" and le: "a \ b" and subset: "g ` {a..b} \ {c..d}" and f: "f integrable_on {c..d}" "continuous_on ({c..d} - (g ` s)) f" - (*and f [continuous_intros]: "continuous_on {c..d} f"*) and g : "continuous_on {a..b} g" "inj_on g ({a..b} \ s)" and deriv [derivative_intros]: "\x. x \ {a..b} - s \ (g has_field_derivative g' x) (at x within {a..b})" shows "((\x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}" proof - let ?F = "\x. integral {c..g x} f" have cont_int: "continuous_on {a..b} ?F" by (rule continuous_on_compose2[OF _ g(1) subset] indefinite_integral_continuous_1 f)+ have deriv: "\x. x \ {a..b} - s \ (((\x. integral {c..x} f) \ g) has_vector_derivative g' x *\<^sub>R f (g x)) (at x within ({a..b} - s))" apply (rule has_vector_derivative_eq_rhs) apply (rule vector_diff_chain_within) apply (subst has_real_derivative_iff_has_vector_derivative [symmetric]) proof- fix x::real assume ass: "x \ {a..b} - s" let ?f'3 = "g' x" have i:"{a..b} - s \ {a..b}" by auto have ii: " (g has_vector_derivative g' x) (at x within {a..b})" using deriv[OF ass] by (simp only: has_real_derivative_iff_has_vector_derivative) show "(g has_real_derivative ?f'3) (at x within {a..b} - s)" using has_vector_derivative_within_subset[OF ii i] by (simp only: has_real_derivative_iff_has_vector_derivative) next let ?g'3 = "f o g" show "\x. x \ {a..b} - s \ ((\x. integral {c..x} f) has_vector_derivative ?g'3 x) (at (g x) within g ` ({a..b} - s))" proof- fix x::real assume ass: "x \ {a..b} - s" have "finite (g ` s)" using s by auto then have i: "((\x. integral {c..x} f) has_vector_derivative f(g x)) (at (g x) within ({c..d} - g ` s))" - apply (rule integral_has_vector_derivative') - proof- + proof (rule integral_has_vector_derivative_continuous_at') show " f integrable_on {c..d}" using f by auto show "g x \ {c..d} - g ` s" using ass subset - (*sledgehammer*) - by (smt Diff_iff Un_upper1 Un_upper2 g(2) imageE image_subset_iff inj_onD subsetCE) + by (smt (verit) Diff_iff g(2) inf_sup_ord(4) inj_on_image_mem_iff subsetD sup_ge1) show "continuous (at (g x) within {c..d} - g ` s) f" - (*sledgehammer*) using \g x \ {c..d} - g ` s\ continuous_on_eq_continuous_within f(2) by blast qed have ii: "g ` ({a..b} - s) \ ({c..d} - g ` s)" using subset g(2) - (*sledgehammer*) - by (smt Diff_subset Un_Diff Un_commute Un_upper2 inj_on_image_set_diff subset_trans sup.order_iff) + by (simp add: image_subset_iff inj_on_image_mem_iff) then show "((\x. integral {c..x} f) has_vector_derivative ?g'3 x) (at (g x) within g ` ({a..b} - s))" - (*sledgehammer*) - by (smt Diff_subset has_vector_derivative_weaken Un_upper1 Un_upper2 \finite (g ` s)\ ass comp_def continuous_on_eq_continuous_within f(1) f(2) g(2) image_diff_subset image_subset_iff inj_on_image_set_diff integral_has_vector_derivative_continuous_at' subset_trans) + using has_vector_derivative_within_subset i by fastforce qed show "\x. x \ {a..b} - s \ g' x *\<^sub>R ?g'3 x = g' x *\<^sub>R f (g x)" by auto qed have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x)) (at x within {a..b} - s)" if "x \ {a<..x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}" using cont_int using fundamental_theorem_of_calculus_interior_stronger'[OF s le deriv] by blast also from subset have "g x \ {c..d}" if "x \ {a..b}" for x using that by blast from this[of a] this[of b] le have cd: "c \ g a" "g b \ d" "c \ g b" "g a \ d" by auto have "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f" proof cases assume "g a \ g b" note le = le this from cd have "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f" by (meson Henstock_Kurzweil_Integration.integral_combine atLeastatMost_subset_iff f(1) integrable_on_subinterval le(2) order_refl) with le show ?thesis by (cases "g a = g b") (simp_all add: algebra_simps) next assume less: "\g a \ g b" - then have "g a \ g b" by simp - note le = le this + then have le: "g a \ g b" by simp from cd have "integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f" - by (meson Henstock_Kurzweil_Integration.integral_combine atLeastatMost_subset_iff f(1) integrable_on_subinterval le(2) order_refl) + by (meson Henstock_Kurzweil_Integration.integral_combine atLeastatMost_subset_iff f(1) integrable_on_subinterval le order_refl) with less show ?thesis by (simp_all add: algebra_simps) qed finally show ?thesis . qed lemma has_integral_substitution_general__: fixes f :: "real \ 'a::euclidean_space" and g :: "real \ real" assumes s: "finite s" and le: "a \ b" and s_subset: "s \ {a..b}" and subset: "g ` {a..b} \ {c..d}" and f: "f integrable_on {c..d}" "continuous_on ({c..d} - (g ` s)) f" - (*and f [continuous_intros]: "continuous_on {c..d} f"*) and g : "continuous_on {a..b} g" "inj_on g {a..b}" and deriv [derivative_intros]: "\x. x \ {a..b} - s \ (g has_field_derivative g' x) (at x within {a..b})" shows "((\x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}" using s_subset has_integral_substitution_general_[OF s le subset f g(1) _ deriv] by (simp add: g(2) sup_absorb1) lemma has_integral_substitution_general_': fixes f :: "real \ 'a::euclidean_space" and g :: "real \ real" assumes s: "finite s" and le: "a \ b" and s': "finite s'" and subset: "g ` {a..b} \ {c..d}" and f: "f integrable_on {c..d}" "continuous_on ({c..d} - s') f" and g : "continuous_on {a..b} g" "\x\s'. finite (g -` {x})" "surj_on s' g" "inj_on g ({a..b} \ ((s \ g -` s')))" and deriv [derivative_intros]: "\x. x \ {a..b} - s \ (g has_field_derivative g' x) (at x within {a..b})" shows "((\x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}" proof- have a: "g -` s' = \{t. \x. t = g -` {x} \ x \ s'}" using s s' by blast have "finite (\{t. \x. t = g -` {x} \ x \ s'})" using s' by (metis (no_types, lifting) \g -` s' = \{g -` {x} |x. x \ s'}\ finite_UN_I g(2) vimage_eq_UN) then have 0: "finite (s \ (g -` s'))" - using a s - by simp + using a s by simp have 1: "continuous_on ({c..d} - g ` (s \ g -` s')) f" using f(2) surj_on_image_vimage_eq by (metis Diff_mono Un_upper2 continuous_on_subset equalityE g(3) image_Un) have 2: " (\x. x \ {a..b} - (s \ g -` s') \ (g has_real_derivative g' x) (at x within {a..b}))" using deriv by auto show ?thesis using has_integral_substitution_general_[OF 0 assms(2) subset f(1) 1 g(1) g(4) 2] by auto qed end