Quelle  Integrals.thy

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
    (*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)"
        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
    (*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)"
        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 *<sub>R</sub> 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</sub> f (g x))"
  proof -
    have "continuous_on {a .. b} (λx. g' x *<sub>R</sub> 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</sub> f (g x))
                      = integral {a .. b} (λx. g' x *<sub>R</sub> 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
  assumes "a < (b::real)"
  shows  frontier_ic: "frontier {a<..b} = {a,b}" 
     and frontier_ci:  "frontier {a<..<b} = {a,b}"
  using assms by(auto simp: frontier_def)

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 assms by force

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:(*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)]
  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
      (*f is injective becuase interiors of different K's are disjoint and f is in interior*)
  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 * measure lborel (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 * measure lborel (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 * measure lborel {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 *<sub>R</sub> 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