Theory Integrals
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 ⨂⇩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⇧L (lborel ⨂⇩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)))"
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)))"
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)))"
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 ⨂⇩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⇧L (lborel ⨂⇩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 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)))"
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 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
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
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)"
using within_range
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
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))"
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)"
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
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)
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"
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
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)"
using within_range
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 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 *⇩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 *⇩R f (g x))"
proof -
have "continuous_on {a .. b} (λx. g' x *⇩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 *⇩R f (g x))
= integral {a .. b} (λx. g' x *⇩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<..<b} = {a,b}"
apply(simp add: frontier_def)
using assms
by auto
lemma ic_not_closed:
assumes "a < (b::real)"
shows "¬ 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} ∪ {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} ∪ {b<..c}))"
proof-
have "b ∉ ({a..<b} ∪ {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} ∪ {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} ∪ {b<..c})"
proof-
have "b ∉ ({a..<b} ∪ {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} ∪ {x<..b}" by auto
then have 0: "⋃S = {a..<x} ∪ {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:
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)]
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 (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
have f_inj: "inj_on f p"
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)
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'
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 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}"
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) *⇩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) *⇩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) *⇩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
by simp
have "norm (integral {a..x} f - integral {a..y} f - (x - y) *⇩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) *⇩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 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<..<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
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 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 *⇩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 *⇩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))"
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
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"
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)
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))"
using has_vector_derivative_within_subset i by fastforce
qed
show "⋀x. x ∈ {a..b} - s ⟹ g' x *⇩R ?g'3 x = g' x *⇩R f (g x)" by auto
qed
have deriv: "(?F has_vector_derivative g' x *⇩R f (g x))
(at x within {a..b} - s)" if "x ∈ {a<..<b} - (s)" for x
using deriv[of x] that by (simp add: at_within_Icc_at o_def)
have "((λx. g' x *⇩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 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 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 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 *⇩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 *⇩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
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