Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lifting_Code_Dt_Test.thy Sprache: Isabelle

Untersuchung Isabelle^©

(*  Author:     John Harrison
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)
                Huge cleanup by LCP
*)

section \<open>Henstock-Kurzweil Gauge Integration in Many Dimensions\<close>

theory Henstock_Kurzweil_Integration
imports
  Lebesgue_Measure Tagged_Division
begin

lemma norm_diff2: "\y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \ e1; norm(y2 - x2) \ e2\
  \<Longrightarrow> norm(y-x) \<le> e"
  using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
  by (simp add: add_diff_add)

lemma setcomp_dot1: "{z. P (z \ (i,0))} = {(x,y). P(x \ i)}"
  by auto

lemma setcomp_dot2: "{z. P (z \ (0,i))} = {(x,y). P(y \ i)}"
  by auto

lemma Sigma_Int_Paircomp1: "(Sigma A B) \ {(x, y). P x} = Sigma (A \ {x. P x}) B"
  by blast

lemma Sigma_Int_Paircomp2: "(Sigma A B) \ {(x, y). P y} = Sigma A (\z. B z \ {y. P y})"
  by blast
(* END MOVE *)

subsection \<open>Content (length, area, volume...) of an interval\<close>

abbreviation content :: "'a::euclidean_space set \ real"
  where "content s \ measure lborel s"

lemma content_cbox_cases:
  "content (cbox a b) = (if \i\Basis. a\i \ b\i then prod (\i. b\i - a\i) Basis else 0)"
  by (simp add: measure_lborel_cbox_eq inner_diff)

lemma content_cbox: "\i\Basis. a\i \ b\i \ content (cbox a b) = (\i\Basis. b\i - a\i)"
  unfolding content_cbox_cases by simp

lemma content_cbox': "cbox a b \ {} \ content (cbox a b) = (\i\Basis. b\i - a\i)"
  by (simp add: box_ne_empty inner_diff)

lemma content_cbox_if: "content (cbox a b) = (if cbox a b = {} then 0 else \i\Basis. b\i - a\i)"
  by (simp add: content_cbox')

lemma content_cbox_cart:
   "cbox a b \ {} \ content(cbox a b) = prod (\i. b$i - a$i) UNIV"
  by (simp add: content_cbox_if Basis_vec_def cart_eq_inner_axis axis_eq_axis prod.UNION_disjoint)

lemma content_cbox_if_cart:
   "content(cbox a b) = (if cbox a b = {} then 0 else prod (\i. b$i - a$i) UNIV)"
  by (simp add: content_cbox_cart)

lemma content_division_of:
  assumes "K \ \" "\ division_of S"
  shows "content K = (\i \ Basis. interval_upperbound K \ i - interval_lowerbound K \ i)"
proof -
  obtain a b where "K = cbox a b"
    using cbox_division_memE assms by metis
  then show ?thesis
    using assms by (force simp: division_of_def content_cbox')
qed

lemma content_real: "a \ b \ content {a..b} = b - a"
  by simp

lemma abs_eq_content: "\y - x\ = (if x\y then content {x..y} else content {y..x})"
  by (auto simp: content_real)

lemma content_singleton: "content {a} = 0"
  by simp

lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
  by simp

lemma content_pos_le [iff]: "0 \ content X"
  by simp

corollary\<^marker>\<open>tag unimportant\<close> content_nonneg [simp]: "\<not> content (cbox a b) < 0"
  using not_le by blast

lemma content_pos_lt: "\i\Basis. a\i < b\i \ 0 < content (cbox a b)"
  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: prod_pos)

lemma content_eq_0: "content (cbox a b) = 0 \ (\i\Basis. b\i \ a\i)"
  by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)

lemma content_eq_0_interior: "content (cbox a b) = 0 \ interior(cbox a b) = {}"
  unfolding content_eq_0 interior_cbox box_eq_empty by auto

lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \ (\i\Basis. a\i < b\i)"
  by (auto simp add: content_cbox_cases less_le prod_nonneg)

lemma content_empty [simp]: "content {} = 0"
  by simp

lemma content_real_if [simp]: "content {a..b} = (if a \ b then b - a else 0)"
  by (simp add: content_real)

lemma content_subset: "cbox a b \ cbox c d \ content (cbox a b) \ content (cbox c d)"
  unfolding measure_def
  by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq)

lemma content_lt_nz: "0 < content (cbox a b) \ content (cbox a b) \ 0"
  unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce

lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
  unfolding measure_lborel_cbox_eq Basis_prod_def
  apply (subst prod.union_disjoint)
  apply (auto simp: bex_Un ball_Un)
  apply (subst (1 2) prod.reindex_nontrivial)
  apply auto
  done

lemma content_cbox_pair_eq0_D:
   "content (cbox (a,c) (b,d)) = 0 \ content (cbox a b) = 0 \ content (cbox c d) = 0"
  by (simp add: content_Pair)

lemma content_cbox_plus:
  fixes x :: "'a::euclidean_space"
  shows "content(cbox x (x + h *\<^sub>R One)) = (if h \ 0 then h ^ DIM('a) else 0)"
  by (simp add: algebra_simps content_cbox_if box_eq_empty)

lemma content_0_subset: "content(cbox a b) = 0 \ s \ cbox a b \ content s = 0"
  using emeasure_mono[of s "cbox a b" lborel]
  by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)

lemma content_ball_pos:
  assumes "r > 0"
  shows   "content (ball c r) > 0"
proof -
  from rational_boxes[OF assms, of c] obtain a b where ab: "c \ box a b" "box a b \ ball c r"
    by auto
  from ab have "0 < content (box a b)"
    by (subst measure_lborel_box_eq) (auto intro!: prod_pos simp: algebra_simps box_def)
  have "emeasure lborel (box a b) \ emeasure lborel (ball c r)"
    using ab by (intro emeasure_mono) auto
  also have "emeasure lborel (box a b) = ennreal (content (box a b))"
    using emeasure_lborel_box_finite[of a b] by (intro emeasure_eq_ennreal_measure) auto
  also have "emeasure lborel (ball c r) = ennreal (content (ball c r))"
    using emeasure_lborel_ball_finite[of c r] by (intro emeasure_eq_ennreal_measure) auto
  finally show ?thesis
    using \<open>content (box a b) > 0\<close> by simp
qed

lemma content_cball_pos:
  assumes "r > 0"
  shows   "content (cball c r) > 0"
proof -
  from rational_boxes[OF assms, of c] obtain a b where ab: "c \ box a b" "box a b \ ball c r"
    by auto
  from ab have "0 < content (box a b)"
    by (subst measure_lborel_box_eq) (auto intro!: prod_pos simp: algebra_simps box_def)
  have "emeasure lborel (box a b) \ emeasure lborel (ball c r)"
    using ab by (intro emeasure_mono) auto
  also have "\ \ emeasure lborel (cball c r)"
    by (intro emeasure_mono) auto
  also have "emeasure lborel (box a b) = ennreal (content (box a b))"
    using emeasure_lborel_box_finite[of a b] by (intro emeasure_eq_ennreal_measure) auto
  also have "emeasure lborel (cball c r) = ennreal (content (cball c r))"
    using emeasure_lborel_cball_finite[of c r] by (intro emeasure_eq_ennreal_measure) auto
  finally show ?thesis
    using \<open>content (box a b) > 0\<close> by simp
qed

lemma content_split:
  fixes a :: "'a::euclidean_space"
  assumes "k \ Basis"
  shows "content (cbox a b) = content(cbox a b \ {x. x\k \ c}) + content(cbox a b \ {x. x\k \ c})"
  \<comment> \<open>Prove using measure theory\<close>
proof (cases "\i\Basis. a \ i \ b \ i")
  case True
  have 1: "\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\Basis-{k}. Z i (Y i))"
    by (simp add: if_distrib prod.delta_remove assms)
  note simps = interval_split[OF assms] content_cbox_cases
  have 2: "(\i\Basis. b\i - a\i) = (\i\Basis-{k}. b\i - a\i) * (b\k - a\k)"
    by (metis (no_types, lifting) assms finite_Basis mult.commute prod.remove)
  have "\x. min (b \ k) c = max (a \ k) c \
    x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
    by  (auto simp add: field_simps)
  moreover
  have **: "(\i\Basis. ((\i\Basis. (if i = k then min (b \ k) c else b \ i) *\<^sub>R i) \ i - a \ i)) =
      (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
    "(\i\Basis. b \ i - ((\i\Basis. (if i = k then max (a \ k) c else a \ i) *\<^sub>R i) \ i)) =
      (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
    by (auto intro!: prod.cong)
  have "\ a \ k \ c \ \ c \ b \ k \ False"
    unfolding not_le using True assms by auto
  ultimately show ?thesis
    using assms unfolding simps ** 1[of "\i x. b\i - x"] 1[of "\i x. x - a\i"] 2
    by auto
next
  case False
  then have "cbox a b = {}"
    unfolding box_eq_empty by (auto simp: not_le)
  then show ?thesis
    by (auto simp: not_le)
qed

lemma division_of_content_0:
  assumes "content (cbox a b) = 0" "d division_of (cbox a b)" "K \ d"
  shows "content K = 0"
  unfolding forall_in_division[OF assms(2)]
  by (meson assms content_0_subset division_of_def)

lemma sum_content_null:
  assumes "content (cbox a b) = 0"
    and "p tagged_division_of (cbox a b)"
  shows "(\(x,K)\p. content K *\<^sub>R f x) = (0::'a::real_normed_vector)"
proof (rule sum.neutral, rule)
  fix y
  assume y: "y \ p"
  obtain x K where xk: "y = (x, K)"
    using surj_pair[of y] by blast
  then obtain c d where k: "K = cbox c d" "K \ cbox a b"
    by (metis assms(2) tagged_division_ofD(3) tagged_division_ofD(4) y)
  have "(\(x',K'). content K' *\<^sub>R f x') y = content K *\<^sub>R f x"
    unfolding xk by auto
  also have "\ = 0"
    using assms(1) content_0_subset k(2) by auto
  finally show "(\(x, k). content k *\<^sub>R f x) y = 0" .
qed

global_interpretation sum_content: operative plus 0 content
  rewrites "comm_monoid_set.F plus 0 = sum"
proof -
  interpret operative plus 0 content
    by standard (auto simp add: content_split [symmetric] content_eq_0_interior)
  show "operative plus 0 content"
    by standard
  show "comm_monoid_set.F plus 0 = sum"
    by (simp add: sum_def)
qed

lemma additive_content_division: "d division_of (cbox a b) \ sum content d = content (cbox a b)"
  by (fact sum_content.division)

lemma additive_content_tagged_division:
  "d tagged_division_of (cbox a b) \ sum (\(x,l). content l) d = content (cbox a b)"
  by (fact sum_content.tagged_division)

lemma subadditive_content_division:
  assumes "\ division_of S" "S \ cbox a b"
  shows "sum content \ \ content(cbox a b)"
proof -
  have "\ division_of \\" "\\ \ cbox a b"
    using assms by auto
  then obtain \<D>' where "\<D> \<subseteq> \<D>'" "\<D>' division_of cbox a b"
    using partial_division_extend_interval by metis
  then have "sum content \ \ sum content \'"
    using sum_mono2 by blast
  also have "... \ content(cbox a b)"
    by (simp add: \<open>\<D>' division_of cbox a b\<close> additive_content_division less_eq_real_def)
  finally show ?thesis .
qed

lemma content_real_eq_0: "content {a..b::real} = 0 \ a \ b"
  by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)

lemma property_empty_interval: "\a b. content (cbox a b) = 0 \ P (cbox a b) \ P {}"
  using content_empty unfolding empty_as_interval by auto

lemma interval_bounds_nz_content [simp]:
  assumes "content (cbox a b) \ 0"
  shows "interval_upperbound (cbox a b) = b"
    and "interval_lowerbound (cbox a b) = a"
  by (metis assms content_empty interval_bounds')+

subsection \<open>Gauge integral\<close>

text \<open>Case distinction to define it first on compact intervals first, then use a limit. This is only
much later unified. In Fremlin: Measure Theory, Volume 4I this is generalized using residual sets.\<close>

definition has_integral :: "('n::euclidean_space \ 'b::real_normed_vector) \ 'b \ 'n set \ bool"
  (infixr "has'_integral" 46)
  where "(f has_integral I) s \
    (if \<exists>a b. s = cbox a b
      then ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R f x) \<longlongrightarrow> I) (division_filter s)
      else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
        (\<exists>z. ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R (if x \<in> s then f x else 0)) \<longlongrightarrow> z) (division_filter (cbox a b)) \<and>
          norm (z - I) < e)))"

lemma has_integral_cbox:
  "(f has_integral I) (cbox a b) \ ((\p. \(x,k)\p. content k *\<^sub>R f x) \ I) (division_filter (cbox a b))"
  by (auto simp add: has_integral_def)

lemma has_integral:
  "(f has_integral y) (cbox a b) \
    (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
      (\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) \<D> - y) < e))"
  by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff)

lemma has_integral_real:
  "(f has_integral y) {a..b::real} \
    (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
      (\<forall>\<D>. \<D> tagged_division_of {a..b} \<and> \<gamma> fine \<D> \<longrightarrow>
        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) \<D> - y) < e))"
  unfolding box_real[symmetric] by (rule has_integral)

lemma has_integralD[dest]:
  assumes "(f has_integral y) (cbox a b)"
    and "e > 0"
  obtains \<gamma>
    where "gauge \"
      and "\\. \ tagged_division_of (cbox a b) \ \ fine \ \
        norm ((\<Sum>(x,k)\<in>\<D>. content k *\<^sub>R f x) - y) < e"
  using assms unfolding has_integral by auto

lemma has_integral_alt:
  "(f has_integral y) i \
    (if \<exists>a b. i = cbox a b
     then (f has_integral y) i
     else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
      (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e)))"
  by (subst has_integral_def) (auto simp add: has_integral_cbox)

lemma has_integral_altD:
  assumes "(f has_integral y) i"
    and "\ (\a b. i = cbox a b)"
    and "e>0"
  obtains B where "B > 0"
    and "\a b. ball 0 B \ cbox a b \
      (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - y) < e)"
  using assms has_integral_alt[of f y i] by auto

definition integrable_on (infixr "integrable'_on" 46)
  where "f integrable_on i \ (\y. (f has_integral y) i)"

definition "integral i f = (SOME y. (f has_integral y) i \ \ f integrable_on i \ y=0)"

lemma integrable_integral[intro]: "f integrable_on i \ (f has_integral (integral i f)) i"
  unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)

lemma not_integrable_integral: "\ f integrable_on i \ integral i f = 0"
  unfolding integrable_on_def integral_def by blast

lemma has_integral_integrable[dest]: "(f has_integral i) s \ f integrable_on s"
  unfolding integrable_on_def by auto

lemma has_integral_integral: "f integrable_on s \ (f has_integral (integral s f)) s"
  by auto

subsection \<open>Basic theorems about integrals\<close>

lemma has_integral_eq_rhs: "(f has_integral j) S \ i = j \ (f has_integral i) S"
  by (rule forw_subst)

lemma has_integral_unique_cbox:
  fixes f :: "'n::euclidean_space \ 'a::real_normed_vector"
  shows "(f has_integral k1) (cbox a b) \ (f has_integral k2) (cbox a b) \ k1 = k2"
    by (auto simp: has_integral_cbox intro: tendsto_unique[OF division_filter_not_empty])

lemma has_integral_unique:
  fixes f :: "'n::euclidean_space \ 'a::real_normed_vector"
  assumes "(f has_integral k1) i" "(f has_integral k2) i"
  shows "k1 = k2"
proof (rule ccontr)
  let ?e = "norm (k1 - k2)/2"
  let ?F = "(\x. if x \ i then f x else 0)"
  assume "k1 \ k2"
  then have e: "?e > 0"
    by auto
  have nonbox: "\ (\a b. i = cbox a b)"
    using \<open>k1 \<noteq> k2\<close> assms has_integral_unique_cbox by blast
  obtain B1 where B1:
      "0 < B1"
      "\a b. ball 0 B1 \ cbox a b \
        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k1) < norm (k1 - k2)/2"
    by (rule has_integral_altD[OF assms(1) nonbox,OF e]) blast
  obtain B2 where B2:
      "0 < B2"
      "\a b. ball 0 B2 \ cbox a b \
        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2)/2"
    by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
  obtain a b :: 'n where ab: "ball 0 B1 \ cbox a b" "ball 0 B2 \ cbox a b"
    by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox_symmetric)
  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2)/2"
    using B1(2)[OF ab(1)] by blast
  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2)/2"
    using B2(2)[OF ab(2)] by blast
  have "z = w"
    using has_integral_unique_cbox[OF w(1) z(1)] by auto
  then have "norm (k1 - k2) \ norm (z - k2) + norm (w - k1)"
    using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
    by (auto simp add: norm_minus_commute)
  also have "\ < norm (k1 - k2)/2 + norm (k1 - k2)/2"
    by (metis add_strict_mono z(2) w(2))
  finally show False by auto
qed

lemma integral_unique [intro]: "(f has_integral y) k \ integral k f = y"
  unfolding integral_def
  by (rule some_equality) (auto intro: has_integral_unique)

lemma has_integral_iff: "(f has_integral i) S \ (f integrable_on S \ integral S f = i)"
  by blast

lemma eq_integralD: "integral k f = y \ (f has_integral y) k \ \ f integrable_on k \ y=0"
  unfolding integral_def integrable_on_def
  apply (erule subst)
  apply (rule someI_ex)
  by blast

lemma has_integral_const [intro]:
  fixes a b :: "'a::euclidean_space"
  shows "((\x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)"
  using eventually_division_filter_tagged_division[of "cbox a b"]
     additive_content_tagged_division[of _ a b]
  by (auto simp: has_integral_cbox split_beta' scaleR_sum_left[symmetric]
           elim!: eventually_mono intro!: tendsto_cong[THEN iffD1, OF _ tendsto_const])

lemma has_integral_const_real [intro]:
  fixes a b :: real
  shows "((\x. c) has_integral (content {a..b} *\<^sub>R c)) {a..b}"
  by (metis box_real(2) has_integral_const)

lemma has_integral_integrable_integral: "(f has_integral i) s \ f integrable_on s \ integral s f = i"
  by blast

lemma integral_const [simp]:
  fixes a b :: "'a::euclidean_space"
  shows "integral (cbox a b) (\x. c) = content (cbox a b) *\<^sub>R c"
  by (rule integral_unique) (rule has_integral_const)

lemma integral_const_real [simp]:
  fixes a b :: real
  shows "integral {a..b} (\x. c) = content {a..b} *\<^sub>R c"
  by (metis box_real(2) integral_const)

lemma has_integral_is_0_cbox:
  fixes f :: "'n::euclidean_space \ 'a::real_normed_vector"
  assumes "\x. x \ cbox a b \ f x = 0"
  shows "(f has_integral 0) (cbox a b)"
    unfolding has_integral_cbox
    using eventually_division_filter_tagged_division[of "cbox a b"] assms
    by (subst tendsto_cong[where g="\_. 0"])
       (auto elim!: eventually_mono intro!: sum.neutral simp: tag_in_interval)

lemma has_integral_is_0:
  fixes f :: "'n::euclidean_space \ 'a::real_normed_vector"
  assumes "\x. x \ S \ f x = 0"
  shows "(f has_integral 0) S"
proof (cases "(\a b. S = cbox a b)")
  case True with assms has_integral_is_0_cbox show ?thesis
    by blast
next
  case False
  have *: "(\x. if x \ S then f x else 0) = (\x. 0)"
    by (auto simp add: assms)
  show ?thesis
    using has_integral_is_0_cbox False
    by (subst has_integral_alt) (force simp add: *)
qed

lemma has_integral_0[simp]: "((\x::'n::euclidean_space. 0) has_integral 0) S"
  by (rule has_integral_is_0) auto

lemma has_integral_0_eq[simp]: "((\x. 0) has_integral i) S \ i = 0"
  using has_integral_unique[OF has_integral_0] by auto

lemma has_integral_linear_cbox:
  fixes f :: "'n::euclidean_space \ 'a::real_normed_vector"
  assumes f: "(f has_integral y) (cbox a b)"
    and h: "bounded_linear h"
  shows "((h \ f) has_integral (h y)) (cbox a b)"
proof -
  interpret bounded_linear h using h .
  show ?thesis
    unfolding has_integral_cbox using tendsto [OF f [unfolded has_integral_cbox]]
    by (simp add: sum scaleR split_beta')
qed

lemma has_integral_linear:
  fixes f :: "'n::euclidean_space \ 'a::real_normed_vector"
  assumes f: "(f has_integral y) S"
    and h: "bounded_linear h"
  shows "((h \ f) has_integral (h y)) S"
proof (cases "(\a b. S = cbox a b)")
  case True with f h has_integral_linear_cbox show ?thesis
    by blast
next
  case False
  interpret bounded_linear h using h .
  from pos_bounded obtain B where B: "0 < B" "\x. norm (h x) \ norm x * B"
    by blast
  let ?S = "\f x. if x \ S then f x else 0"
  show ?thesis
  proof (subst has_integral_alt, clarsimp simp: False)
    fix e :: real
    assume e: "e > 0"
    have *: "0 < e/B" using e B(1) by simp
    obtain M where M:
      "M > 0"
      "\a b. ball 0 M \ cbox a b \
        \<exists>z. (?S f has_integral z) (cbox a b) \<and> norm (z - y) < e/B"
      using has_integral_altD[OF f False *] by blast
    show "\B>0. \a b. ball 0 B \ cbox a b \
      (\<exists>z. (?S(h \<circ> f) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
    proof (rule exI, intro allI conjI impI)
      show "M > 0" using M by metis
    next
      fix a b::'n
      assume sb: "ball 0 M \ cbox a b"
      obtain z where z: "(?S f has_integral z) (cbox a b)" "norm (z - y) < e/B"
        using M(2)[OF sb] by blast
      have *: "?S(h \ f) = h \ ?S f"
        using zero by auto
      show "\z. (?S(h \ f) has_integral z) (cbox a b) \ norm (z - h y) < e"
      proof (intro exI conjI)
        show "(?S(h \ f) has_integral h z) (cbox a b)"
          by (simp add: * has_integral_linear_cbox[OF z(1) h])
        show "norm (h z - h y) < e"
          by (metis B diff le_less_trans pos_less_divide_eq z(2))
      qed
    qed
  qed
qed

lemma has_integral_scaleR_left:
  "(f has_integral y) S \ ((\x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) S"
  using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)

lemma integrable_on_scaleR_left:
  assumes "f integrable_on A"
  shows "(\x. f x *\<^sub>R y) integrable_on A"
  using assms has_integral_scaleR_left unfolding integrable_on_def by blast

lemma has_integral_mult_left:
  fixes c :: "_ :: real_normed_algebra"
  shows "(f has_integral y) S \ ((\x. f x * c) has_integral (y * c)) S"
  using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)

lemma has_integral_divide:
  fixes c :: "_ :: real_normed_div_algebra"
  shows "(f has_integral y) S \ ((\x. f x / c) has_integral (y / c)) S"
  unfolding divide_inverse by (simp add: has_integral_mult_left)

text\<open>The case analysis eliminates the condition \<^term>\<open>f integrable_on S\<close> at the cost
     of the type class constraint \<open>division_ring\<close>\<close>
corollary integral_mult_left [simp]:
  fixes c:: "'a::{real_normed_algebra,division_ring}"
  shows "integral S (\x. f x * c) = integral S f * c"
proof (cases "f integrable_on S \ c = 0")
  case True then show ?thesis
    by (force intro: has_integral_mult_left)
next
  case False then have "\ (\x. f x * c) integrable_on S"
    using has_integral_mult_left [of "(\x. f x * c)" _ S "inverse c"]
    by (auto simp add: mult.assoc)
  with False show ?thesis by (simp add: not_integrable_integral)
qed

corollary integral_mult_right [simp]:
  fixes c:: "'a::{real_normed_field}"
  shows "integral S (\x. c * f x) = c * integral S f"
by (simp add: mult.commute [of c])

corollary integral_divide [simp]:
  fixes z :: "'a::real_normed_field"
  shows "integral S (\x. f x / z) = integral S (\x. f x) / z"
using integral_mult_left [of S f "inverse z"]
  by (simp add: divide_inverse_commute)

lemma has_integral_mult_right:
  fixes c :: "'a :: real_normed_algebra"
  shows "(f has_integral y) i \ ((\x. c * f x) has_integral (c * y)) i"
  using has_integral_linear[OF _ bounded_linear_mult_right] by (simp add: comp_def)

lemma has_integral_cmul: "(f has_integral k) S \ ((\x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) S"
  unfolding o_def[symmetric]
  by (metis has_integral_linear bounded_linear_scaleR_right)

lemma has_integral_cmult_real:
  fixes c :: real
  assumes "c \ 0 \ (f has_integral x) A"
  shows "((\x. c * f x) has_integral c * x) A"
proof (cases "c = 0")
  case True
  then show ?thesis by simp
next
  case False
  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
    unfolding real_scaleR_def .
qed

lemma has_integral_neg: "(f has_integral k) S \ ((\x. -(f x)) has_integral -k) S"
  by (drule_tac c="-1" in has_integral_cmul) auto

lemma has_integral_neg_iff: "((\x. - f x) has_integral k) S \ (f has_integral - k) S"
  using has_integral_neg[of f "- k"] has_integral_neg[of "\x. - f x" k] by auto

lemma has_integral_add_cbox:
  fixes f :: "'n::euclidean_space \ 'a::real_normed_vector"
  assumes "(f has_integral k) (cbox a b)" "(g has_integral l) (cbox a b)"
  shows "((\x. f x + g x) has_integral (k + l)) (cbox a b)"
  using assms
    unfolding has_integral_cbox
    by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add)

lemma has_integral_add:
  fixes f :: "'n::euclidean_space \ 'a::real_normed_vector"
  assumes f: "(f has_integral k) S" and g: "(g has_integral l) S"
  shows "((\x. f x + g x) has_integral (k + l)) S"
proof (cases "\a b. S = cbox a b")
  case True with has_integral_add_cbox assms show ?thesis
    by blast
next
  let ?S = "\f x. if x \ S then f x else 0"
  case False
  then show ?thesis
  proof (subst has_integral_alt, clarsimp, goal_cases)
    case (1 e)
    then have e2: "e/2 > 0"
      by auto
    obtain Bf where "0 < Bf"
      and Bf: "\a b. ball 0 Bf \ cbox a b \
                     \<exists>z. (?S f has_integral z) (cbox a b) \<and> norm (z - k) < e/2"
      using has_integral_altD[OF f False e2] by blast
    obtain Bg where "0 < Bg"
      and Bg: "\a b. ball 0 Bg \ (cbox a b) \
                     \<exists>z. (?S g has_integral z) (cbox a b) \<and> norm (z - l) < e/2"
      using has_integral_altD[OF g False e2] by blast
    show ?case
    proof (rule_tac x="max Bf Bg" in exI, clarsimp simp add: max.strict_coboundedI1 \<open>0 < Bf\<close>)
      fix a b
      assume "ball 0 (max Bf Bg) \ cbox a (b::'n)"
      then have fs: "ball 0 Bf \ cbox a (b::'n)" and gs: "ball 0 Bg \ cbox a (b::'n)"
        by auto
      obtain w where w: "(?S f has_integral w) (cbox a b)" "norm (w - k) < e/2"
        using Bf[OF fs] by blast
      obtain z where z: "(?S g has_integral z) (cbox a b)" "norm (z - l) < e/2"
        using Bg[OF gs] by blast
      have *: "\x. (if x \ S then f x + g x else 0) = (?S f x) + (?S g x)"
        by auto
      show "\z. (?S(\x. f x + g x) has_integral z) (cbox a b) \ norm (z - (k + l)) < e"
      proof (intro exI conjI)
        show "(?S(\x. f x + g x) has_integral (w + z)) (cbox a b)"
          by (simp add: has_integral_add_cbox[OF w(1) z(1), unfolded *[symmetric]])
        show "norm (w + z - (k + l)) < e"
          by (metis dist_norm dist_triangle_add_half w(2) z(2))
      qed
    qed
  qed
qed

lemma has_integral_diff:
  "(f has_integral k) S \ (g has_integral l) S \
    ((\<lambda>x. f x - g x) has_integral (k - l)) S"
  using has_integral_add[OF _ has_integral_neg, of f k S g l]
  by (auto simp: algebra_simps)

lemma integral_0 [simp]:
  "integral S (\x::'n::euclidean_space. 0::'m::real_normed_vector) = 0"
  by (rule integral_unique has_integral_0)+

lemma integral_add: "f integrable_on S \ g integrable_on S \
    integral S (\<lambda>x. f x + g x) = integral S f + integral S g"
  by (rule integral_unique) (metis integrable_integral has_integral_add)

lemma integral_cmul [simp]: "integral S (\x. c *\<^sub>R f x) = c *\<^sub>R integral S f"
proof (cases "f integrable_on S \ c = 0")
  case True with has_integral_cmul integrable_integral show ?thesis
    by fastforce
next
  case False then have "\ (\x. c *\<^sub>R f x) integrable_on S"
    using has_integral_cmul [of "(\x. c *\<^sub>R f x)" _ S "inverse c"] by auto
  with False show ?thesis by (simp add: not_integrable_integral)
qed

lemma integral_mult:
  fixes K::real
  shows "f integrable_on X \ K * integral X f = integral X (\x. K * f x)"
  unfolding real_scaleR_def[symmetric] integral_cmul ..

lemma integral_neg [simp]: "integral S (\x. - f x) = - integral S f"
proof (cases "f integrable_on S")
  case True then show ?thesis
    by (simp add: has_integral_neg integrable_integral integral_unique)
next
  case False then have "\ (\x. - f x) integrable_on S"
    using has_integral_neg [of "(\x. - f x)" _ S ] by auto
  with False show ?thesis by (simp add: not_integrable_integral)
qed

lemma integral_diff: "f integrable_on S \ g integrable_on S \
    integral S (\<lambda>x. f x - g x) = integral S f - integral S g"
  by (rule integral_unique) (metis integrable_integral has_integral_diff)

lemma integrable_0: "(\x. 0) integrable_on S"
  unfolding integrable_on_def using has_integral_0 by auto

lemma integrable_add: "f integrable_on S \ g integrable_on S \ (\x. f x + g x) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_add)

lemma integrable_cmul: "f integrable_on S \ (\x. c *\<^sub>R f(x)) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_cmul)

lemma integrable_on_scaleR_iff [simp]:
  fixes c :: real
  assumes "c \ 0"
  shows "(\x. c *\<^sub>R f x) integrable_on S \ f integrable_on S"
  using integrable_cmul[of "\x. c *\<^sub>R f x" S "1 / c"] integrable_cmul[of f S c] \c \ 0\
  by auto

lemma integrable_on_cmult_iff [simp]:
  fixes c :: real
  assumes "c \ 0"
  shows "(\x. c * f x) integrable_on S \ f integrable_on S"
  using integrable_on_scaleR_iff [of c f] assms by simp

lemma integrable_on_cmult_left:
  assumes "f integrable_on S"
  shows "(\x. of_real c * f x) integrable_on S"
    using integrable_cmul[of f S "of_real c"] assms
    by (simp add: scaleR_conv_of_real)

lemma integrable_neg: "f integrable_on S \ (\x. -f(x)) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_neg)

lemma integrable_neg_iff: "(\x. -f(x)) integrable_on S \ f integrable_on S"
  using integrable_neg by fastforce

lemma integrable_diff:
  "f integrable_on S \ g integrable_on S \ (\x. f x - g x) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_diff)

lemma integrable_linear:
  "f integrable_on S \ bounded_linear h \ (h \ f) integrable_on S"
  unfolding integrable_on_def by(auto intro: has_integral_linear)

lemma integral_linear:
  "f integrable_on S \ bounded_linear h \ integral S (h \ f) = h (integral S f)"
  by (meson has_integral_iff has_integral_linear)

lemma integrable_on_cnj_iff:
  "(\x. cnj (f x)) integrable_on A \ f integrable_on A"
  using integrable_linear[OF _ bounded_linear_cnj, of f A]
        integrable_linear[OF _ bounded_linear_cnj, of "cnj \ f" A]
  by (auto simp: o_def)

lemma integral_cnj: "cnj (integral A f) = integral A (\x. cnj (f x))"
  by (cases "f integrable_on A")
     (simp_all add: integral_linear[OF _ bounded_linear_cnj, symmetric]
                    o_def integrable_on_cnj_iff not_integrable_integral)

lemma integral_component_eq[simp]:
  fixes f :: "'n::euclidean_space \ 'm::euclidean_space"
  assumes "f integrable_on S"
  shows "integral S (\x. f x \ k) = integral S f \ k"
  unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] ..

lemma has_integral_sum:
  assumes "finite T"
    and "\a. a \ T \ ((f a) has_integral (i a)) S"
  shows "((\x. sum (\a. f a x) T) has_integral (sum i T)) S"
  using assms(1) subset_refl[of T]
proof (induct rule: finite_subset_induct)
  case empty
  then show ?case by auto
next
  case (insert x F)
  with assms show ?case
    by (simp add: has_integral_add)
qed

lemma integral_sum:
  "\finite I; \a. a \ I \ f a integrable_on S\ \
   integral S (\<lambda>x. \<Sum>a\<in>I. f a x) = (\<Sum>a\<in>I. integral S (f a))"
  by (simp add: has_integral_sum integrable_integral integral_unique)

lemma integrable_sum:
  "\finite I; \a. a \ I \ f a integrable_on S\ \ (\x. \a\I. f a x) integrable_on S"
  unfolding integrable_on_def using has_integral_sum[of I] by metis

lemma has_integral_eq:
  assumes "\x. x \ s \ f x = g x"
    and "(f has_integral k) s"
  shows "(g has_integral k) s"
  using has_integral_diff[OF assms(2), of "\x. f x - g x" 0]
  using has_integral_is_0[of s "\x. f x - g x"]
  using assms(1)
  by auto

lemma integrable_eq: "\f integrable_on s; \x. x \ s \ f x = g x\ \ g integrable_on s"
  unfolding integrable_on_def
  using has_integral_eq[of s f g] has_integral_eq by blast

lemma has_integral_cong:
  assumes "\x. x \ s \ f x = g x"
  shows "(f has_integral i) s = (g has_integral i) s"
  using has_integral_eq[of s f g] has_integral_eq[of s g f] assms
  by auto

lemma integral_cong:
  assumes "\x. x \ s \ f x = g x"
  shows "integral s f = integral s g"
  unfolding integral_def
by (metis (full_types, hide_lams) assms has_integral_cong integrable_eq)

lemma integrable_on_cmult_left_iff [simp]:
  assumes "c \ 0"
  shows "(\x. of_real c * f x) integrable_on s \ f integrable_on s"
        (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "(\x. of_real (1 / c) * (of_real c * f x)) integrable_on s"
    using integrable_cmul[of "\x. of_real c * f x" s "1 / of_real c"]
    by (simp add: scaleR_conv_of_real)
  then have "(\x. (of_real (1 / c) * of_real c * f x)) integrable_on s"
    by (simp add: algebra_simps)
  with \<open>c \<noteq> 0\<close> show ?rhs
    by (metis (no_types, lifting) integrable_eq mult.left_neutral nonzero_divide_eq_eq of_real_1 of_real_mult)
qed (blast intro: integrable_on_cmult_left)

lemma integrable_on_cmult_right:
  fixes f :: "_ \ 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
  assumes "f integrable_on s"
  shows "(\x. f x * of_real c) integrable_on s"
using integrable_on_cmult_left [OF assms] by (simp add: mult.commute)

lemma integrable_on_cmult_right_iff [simp]:
  fixes f :: "_ \ 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
  assumes "c \ 0"
  shows "(\x. f x * of_real c) integrable_on s \ f integrable_on s"
using integrable_on_cmult_left_iff [OF assms] by (simp add: mult.commute)

lemma integrable_on_cdivide:
  fixes f :: "_ \ 'b :: real_normed_field"
  assumes "f integrable_on s"
  shows "(\x. f x / of_real c) integrable_on s"
by (simp add: integrable_on_cmult_right divide_inverse assms flip: of_real_inverse)

lemma integrable_on_cdivide_iff [simp]:
  fixes f :: "_ \ 'b :: real_normed_field"
  assumes "c \ 0"
  shows "(\x. f x / of_real c) integrable_on s \ f integrable_on s"
by (simp add: divide_inverse assms flip: of_real_inverse)

lemma has_integral_null [intro]: "content(cbox a b) = 0 \ (f has_integral 0) (cbox a b)"
  unfolding has_integral_cbox
  using eventually_division_filter_tagged_division[of "cbox a b"]
  by (subst tendsto_cong[where g="\_. 0"]) (auto elim: eventually_mono intro: sum_content_null)

lemma has_integral_null_real [intro]: "content {a..b::real} = 0 \ (f has_integral 0) {a..b}"
  by (metis box_real(2) has_integral_null)

lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \ (f has_integral i) (cbox a b) \ i = 0"
  by (auto simp add: has_integral_null dest!: integral_unique)

lemma integral_null [simp]: "content (cbox a b) = 0 \ integral (cbox a b) f = 0"
  by (metis has_integral_null integral_unique)

lemma integrable_on_null [intro]: "content (cbox a b) = 0 \ f integrable_on (cbox a b)"
  by (simp add: has_integral_integrable)

lemma has_integral_empty[intro]: "(f has_integral 0) {}"
  by (meson ex_in_conv has_integral_is_0)

lemma has_integral_empty_eq[simp]: "(f has_integral i) {} \ i = 0"
  by (auto simp add: has_integral_empty has_integral_unique)

lemma integrable_on_empty[intro]: "f integrable_on {}"
  unfolding integrable_on_def by auto

lemma integral_empty[simp]: "integral {} f = 0"
  by (rule integral_unique) (rule has_integral_empty)

lemma has_integral_refl[intro]:
  fixes a :: "'a::euclidean_space"
  shows "(f has_integral 0) (cbox a a)"
    and "(f has_integral 0) {a}"
proof -
  show "(f has_integral 0) (cbox a a)"
     by (rule has_integral_null) simp
  then show "(f has_integral 0) {a}"
    by simp
qed

lemma integrable_on_refl[intro]: "f integrable_on cbox a a"
  unfolding integrable_on_def by auto

lemma integral_refl [simp]: "integral (cbox a a) f = 0"
  by (rule integral_unique) auto

lemma integral_singleton [simp]: "integral {a} f = 0"
  by auto

lemma integral_blinfun_apply:
  assumes "f integrable_on s"
  shows "integral s (\x. blinfun_apply h (f x)) = blinfun_apply h (integral s f)"
  by (subst integral_linear[symmetric, OF assms blinfun.bounded_linear_right]) (simp add: o_def)

lemma blinfun_apply_integral:
  assumes "f integrable_on s"
  shows "blinfun_apply (integral s f) x = integral s (\y. blinfun_apply (f y) x)"
  by (metis (no_types, lifting) assms blinfun.prod_left.rep_eq integral_blinfun_apply integral_cong)

lemma has_integral_componentwise_iff:
  fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space"
  shows "(f has_integral y) A \ (\b\Basis. ((\x. f x \ b) has_integral (y \ b)) A)"
proof safe
  fix b :: 'b assume "(f has_integral y) A"
  from has_integral_linear[OF this(1) bounded_linear_inner_left, of b]
    show "((\x. f x \ b) has_integral (y \ b)) A" by (simp add: o_def)
next
  assume "(\b\Basis. ((\x. f x \ b) has_integral (y \ b)) A)"
  hence "\b\Basis. (((\x. x *\<^sub>R b) \ (\x. f x \ b)) has_integral ((y \ b) *\<^sub>R b)) A"
    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
  hence "((\x. \b\Basis. (f x \ b) *\<^sub>R b) has_integral (\b\Basis. (y \ b) *\<^sub>R b)) A"
    by (intro has_integral_sum) (simp_all add: o_def)
  thus "(f has_integral y) A" by (simp add: euclidean_representation)
qed

lemma has_integral_componentwise:
  fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space"
  shows "(\b. b \ Basis \ ((\x. f x \ b) has_integral (y \ b)) A) \ (f has_integral y) A"
  by (subst has_integral_componentwise_iff) blast

lemma integrable_componentwise_iff:
  fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space"
  shows "f integrable_on A \ (\b\Basis. (\x. f x \ b) integrable_on A)"
proof
  assume "f integrable_on A"
  then obtain y where "(f has_integral y) A" by (auto simp: integrable_on_def)
  hence "(\b\Basis. ((\x. f x \ b) has_integral (y \ b)) A)"
    by (subst (asm) has_integral_componentwise_iff)
  thus "(\b\Basis. (\x. f x \ b) integrable_on A)" by (auto simp: integrable_on_def)
next
  assume "(\b\Basis. (\x. f x \ b) integrable_on A)"
  then obtain y where "\b\Basis. ((\x. f x \ b) has_integral y b) A"
    unfolding integrable_on_def by (subst (asm) bchoice_iff) blast
  hence "\b\Basis. (((\x. x *\<^sub>R b) \ (\x. f x \ b)) has_integral (y b *\<^sub>R b)) A"
    by (intro ballI has_integral_linear) (simp_all add: bounded_linear_scaleR_left)
  hence "((\x. \b\Basis. (f x \ b) *\<^sub>R b) has_integral (\b\Basis. y b *\<^sub>R b)) A"
    by (intro has_integral_sum) (simp_all add: o_def)
  thus "f integrable_on A" by (auto simp: integrable_on_def o_def euclidean_representation)
qed

lemma integrable_componentwise:
  fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space"
  shows "(\b. b \ Basis \ (\x. f x \ b) integrable_on A) \ f integrable_on A"
  by (subst integrable_componentwise_iff) blast

lemma integral_componentwise:
  fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space"
  assumes "f integrable_on A"
  shows "integral A f = (\b\Basis. integral A (\x. (f x \ b) *\<^sub>R b))"
proof -
  from assms have integrable: "\b\Basis. (\x. x *\<^sub>R b) \ (\x. (f x \ b)) integrable_on A"
    by (subst (asm) integrable_componentwise_iff, intro integrable_linear ballI)
       (simp_all add: bounded_linear_scaleR_left)
  have "integral A f = integral A (\x. \b\Basis. (f x \ b) *\<^sub>R b)"
    by (simp add: euclidean_representation)
  also from integrable have "\ = (\a\Basis. integral A (\x. (f x \ a) *\<^sub>R a))"
    by (subst integral_sum) (simp_all add: o_def)
  finally show ?thesis .
qed

lemma integrable_component:
  "f integrable_on A \ (\x. f x \ (y :: 'b :: euclidean_space)) integrable_on A"
  by (drule integrable_linear[OF _ bounded_linear_inner_left[of y]]) (simp add: o_def)

subsection \<open>Cauchy-type criterion for integrability\<close>

proposition integrable_Cauchy:
  fixes f :: "'n::euclidean_space \ 'a::{real_normed_vector,complete_space}"
  shows "f integrable_on cbox a b \
        (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
          (\<forall>\<D>1 \<D>2. \<D>1 tagged_division_of (cbox a b) \<and> \<gamma> fine \<D>1 \<and>
            \<D>2 tagged_division_of (cbox a b) \<and> \<gamma> fine \<D>2 \<longrightarrow>
            norm ((\<Sum>(x,K)\<in>\<D>1. content K *\<^sub>R f x) - (\<Sum>(x,K)\<in>\<D>2. content K *\<^sub>R f x)) < e))"
  (is "?l = (\e>0. \\. ?P e \)")
proof (intro iffI allI impI)
  assume ?l
  then obtain y
    where y: "\e. e > 0 \
        \<exists>\<gamma>. gauge \<gamma> \<and>
            (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
                 norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - y) < e)"
    by (auto simp: integrable_on_def has_integral)
  show "\\. ?P e \" if "e > 0" for e
  proof -
    have "e/2 > 0" using that by auto
    with y obtain \<gamma> where "gauge \<gamma>"
      and \<gamma>: "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<Longrightarrow>
                  norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f x) - y) < e/2"
      by meson
    show ?thesis
    apply (rule_tac x=\<gamma> in exI, clarsimp simp: \<open>gauge \<gamma>\<close>)
        by (blast intro!: \<gamma> dist_triangle_half_l[where y=y,unfolded dist_norm])
    qed
next
  assume "\e>0. \\. ?P e \"
  then have "\n::nat. \\. ?P (1 / (n + 1)) \"
    by auto
  then obtain \<gamma> :: "nat \<Rightarrow> 'n \<Rightarrow> 'n set" where \<gamma>:
    "\m. gauge (\ m)"
    "\m \1 \2. \\1 tagged_division_of cbox a b;
              \<gamma> m fine \<D>1; \<D>2 tagged_division_of cbox a b; \<gamma> m fine \<D>2\<rbrakk>
              \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>1. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> \<D>2. content K *\<^sub>R f x))
                  < 1 / (m + 1)"
    by metis
  have "gauge (\x. \{\ i x |i. i \ {0..n}})" for n
    using \<gamma> by (intro gauge_Inter) auto
  then have "\n. \p. p tagged_division_of (cbox a b) \ (\x. \{\ i x |i. i \ {0..n}}) fine p"
    by (meson fine_division_exists)
  then obtain p where p: "\z. p z tagged_division_of cbox a b"
                         "\z. (\x. \{\ i x |i. i \ {0..z}}) fine p z"
    by meson
  have dp: "\i n. i\n \ \ i fine p n"
    using p unfolding fine_Inter
    using atLeastAtMost_iff by blast
  have "Cauchy (\n. sum (\(x,K). content K *\<^sub>R (f x)) (p n))"
  proof (rule CauchyI)
    fix e::real
    assume "0 < e"
    then obtain N where "N \ 0" and N: "inverse (real N) < e"
      using real_arch_inverse[of e] by blast
    show "\M. \m\M. \n\M. norm ((\(x,K) \ p m. content K *\<^sub>R f x) - (\(x,K) \ p n. content K *\<^sub>R f x)) < e"
    proof (intro exI allI impI)
      fix m n
      assume mn: "N \ m" "N \ n"
      have "norm ((\(x,K) \ p m. content K *\<^sub>R f x) - (\(x,K) \ p n. content K *\<^sub>R f x)) < 1 / (real N + 1)"
        by (simp add: p(1) dp mn \<gamma>)
      also have "... < e"
        using  N \<open>N \<noteq> 0\<close> \<open>0 < e\<close> by (auto simp: field_simps)
      finally show "norm ((\(x,K) \ p m. content K *\<^sub>R f x) - (\(x,K) \ p n. content K *\<^sub>R f x)) < e" .
    qed
  qed
  then obtain y where y: "\no. \n\no. norm ((\(x,K) \ p n. content K *\<^sub>R f x) - y) < r" if "r > 0" for r
    by (auto simp: convergent_eq_Cauchy[symmetric] dest: LIMSEQ_D)
  show ?l
    unfolding integrable_on_def has_integral
  proof (rule_tac x=y in exI, clarify)
    fix e :: real
    assume "e>0"
    then have e2: "e/2 > 0" by auto
    then obtain N1::nat where N1: "N1 \ 0" "inverse (real N1) < e/2"
      using real_arch_inverse by blast
    obtain N2::nat where N2: "\n. n \ N2 \ norm ((\(x,K) \ p n. content K *\<^sub>R f x) - y) < e/2"
      using y[OF e2] by metis
    show "\\. gauge \ \
              (\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
                norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - y) < e)"
    proof (intro exI conjI allI impI)
      show "gauge (\ (N1+N2))"
        using \<gamma> by auto
      show "norm ((\(x,K) \ q. content K *\<^sub>R f x) - y) < e"
           if "q tagged_division_of cbox a b \ \ (N1+N2) fine q" for q
      proof (rule norm_triangle_half_r)
        have "norm ((\(x,K) \ p (N1+N2). content K *\<^sub>R f x) - (\(x,K) \ q. content K *\<^sub>R f x))
               < 1 / (real (N1+N2) + 1)"
          by (rule \<gamma>; simp add: dp p that)
        also have "... < e/2"
          using N1 \<open>0 < e\<close> by (auto simp: field_simps intro: less_le_trans)
        finally show "norm ((\(x,K) \ p (N1+N2). content K *\<^sub>R f x) - (\(x,K) \ q. content K *\<^sub>R f x)) < e/2" .
        show "norm ((\(x,K) \ p (N1+N2). content K *\<^sub>R f x) - y) < e/2"
          using N2 le_add_same_cancel2 by blast
      qed
    qed
  qed
qed

subsection \<open>Additivity of integral on abutting intervals\<close>

lemma tagged_division_split_left_inj_content:
  assumes \<D>: "\<D> tagged_division_of S"
    and "(x1, K1) \ \" "(x2, K2) \ \" "K1 \ K2" "K1 \ {x. x\k \ c} = K2 \ {x. x\k \ c}" "k \ Basis"
  shows "content (K1 \ {x. x\k \ c}) = 0"
proof -
  from tagged_division_ofD(4)[OF \<D> \<open>(x1, K1) \<in> \<D>\<close>] obtain a b where K1: "K1 = cbox a b"
    by auto
  then have "interior (K1 \ {x. x \ k \ c}) = {}"
    by (metis tagged_division_split_left_inj assms)
  then show ?thesis
    unfolding K1 interval_split[OF \<open>k \<in> Basis\<close>] by (auto simp: content_eq_0_interior)
qed

lemma tagged_division_split_right_inj_content:
  assumes \<D>: "\<D> tagged_division_of S"
    and "(x1, K1) \ \" "(x2, K2) \ \" "K1 \ K2" "K1 \ {x. x\k \ c} = K2 \ {x. x\k \ c}" "k \ Basis"
  shows "content (K1 \ {x. x\k \ c}) = 0"
proof -
  from tagged_division_ofD(4)[OF \<D> \<open>(x1, K1) \<in> \<D>\<close>] obtain a b where K1: "K1 = cbox a b"
    by auto
  then have "interior (K1 \ {x. c \ x \ k}) = {}"
    by (metis tagged_division_split_right_inj assms)
  then show ?thesis
    unfolding K1 interval_split[OF \<open>k \<in> Basis\<close>]
    by (auto simp: content_eq_0_interior)
qed

proposition has_integral_split:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  assumes fi: "(f has_integral i) (cbox a b \ {x. x\k \ c})"
      and fj: "(f has_integral j) (cbox a b \ {x. x\k \ c})"
      and k: "k \ Basis"
shows "(f has_integral (i + j)) (cbox a b)"
  unfolding has_integral
proof clarify
  fix e::real
  assume "0 < e"
  then have e: "e/2 > 0"
    by auto
    obtain \<gamma>1 where \<gamma>1: "gauge \<gamma>1"
      and \<gamma>1norm:
        "\\. \\ tagged_division_of cbox a b \ {x. x \ k \ c}; \1 fine \\
             \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - i) < e/2"
       apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
       apply (simp add: interval_split[symmetric] k)
      done
    obtain \<gamma>2 where \<gamma>2: "gauge \<gamma>2"
      and \<gamma>2norm:
        "\\. \\ tagged_division_of cbox a b \ {x. c \ x \ k}; \2 fine \\
             \<Longrightarrow> norm ((\<Sum>(x, k) \<in> \<D>. content k *\<^sub>R f x) - j) < e/2"
       apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
       apply (simp add: interval_split[symmetric] k)
       done
  let ?\<gamma> = "\<lambda>x. if x\<bullet>k = c then (\<gamma>1 x \<inter> \<gamma>2 x) else ball x \<bar>x\<bullet>k - c\<bar> \<inter> \<gamma>1 x \<inter> \<gamma>2 x"
  have "gauge ?\"
    using \<gamma>1 \<gamma>2 unfolding gauge_def by auto
  then show "\\. gauge \ \
                 (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
                      norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) - (i + j)) < e)"
  proof (rule_tac x="?\" in exI, safe)
    fix p
    assume p: "p tagged_division_of (cbox a b)" and "?\ fine p"
    have ab_eqp: "cbox a b = \{K. \x. (x, K) \ p}"
      using p by blast
    have xk_le_c: "x\k \ c" if as: "(x,K) \ p" and K: "K \ {x. x\k \ c} \ {}" for x K
    proof (rule ccontr)
      assume **: "\ x \ k \ c"
      then have "K \ ball x \x \ k - c\"
        using \<open>?\<gamma> fine p\<close> as by (fastforce simp: not_le algebra_simps)
      with K obtain y where y: "y \ ball x \x \ k - c\" "y\k \ c"
        by blast
      then have "\x \ k - y \ k\ < \x \ k - c\"
        using Basis_le_norm[OF k, of "x - y"]
        by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
      with y show False
        using ** by (auto simp add: field_simps)
    qed
    have xk_ge_c: "x\k \ c" if as: "(x,K) \ p" and K: "K \ {x. x\k \ c} \ {}" for x K
    proof (rule ccontr)
      assume **: "\ x \ k \ c"
      then have "K \ ball x \x \ k - c\"
        using \<open>?\<gamma> fine p\<close> as by (fastforce simp: not_le algebra_simps)
      with K obtain y where y: "y \ ball x \x \ k - c\" "y\k \ c"
        by blast
      then have "\x \ k - y \ k\ < \x \ k - c\"
        using Basis_le_norm[OF k, of "x - y"]
        by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
      with y show False
        using ** by (auto simp add: field_simps)
    qed
    have fin_finite: "finite {(x,f K) | x K. (x,K) \ s \ P x K}"
      if "finite s" for s and f :: "'a set \ 'a set" and P :: "'a \ 'a set \ bool"
    proof -
      from that have "finite ((\(x,K). (x, f K)) ` s)"
        by auto
      then show ?thesis
        by (rule rev_finite_subset) auto
    qed
    { fix \<G> :: "'a set \<Rightarrow> 'a set"
      fix i :: "'a \ 'a set"
      assume "i \ (\(x, k). (x, \ k)) ` p - {(x, \ k) |x k. (x, k) \ p \ \ k \ {}}"
      then obtain x K where xk: "i = (x, \ K)" "(x,K) \ p"
                                 "(x, \ K) \ {(x, \ K) |x K. (x,K) \ p \ \ K \ {}}"
        by auto
      have "content (\ K) = 0"
        using xk using content_empty by auto
      then have "(\(x,K). content K *\<^sub>R f x) i = 0"
        unfolding xk split_conv by auto
    } note [simp] = this
    have "finite p"
      using p by blast
    let ?M1 = "{(x, K \ {x. x\k \ c}) |x K. (x,K) \ p \ K \ {x. x\k \ c} \ {}}"
    have \<gamma>1_fine: "\<gamma>1 fine ?M1"
      using \<open>?\<gamma> fine p\<close> by (fastforce simp: fine_def split: if_split_asm)
    have "norm ((\(x, k)\?M1. content k *\<^sub>R f x) - i) < e/2"
    proof (rule \<gamma>1norm [OF tagged_division_ofI \<gamma>1_fine])
      show "finite ?M1"
        by (rule fin_finite) (use p in blast)
      show "\{k. \x. (x, k) \ ?M1} = cbox a b \ {x. x\k \ c}"
        by (auto simp: ab_eqp)

      fix x L
      assume xL: "(x, L) \ ?M1"
      then obtain x' L' where xL': "x = x'" "L = L' \ {x. x \ k \ c}"
                                   "(x', L') \ p" "L' \ {x. x \ k \ c} \ {}"
        by blast
      then obtain a' b' where ab': "L' = cbox a' b'"
        using p by blast
      show "x \ L" "L \ cbox a b \ {x. x \ k \ c}"
        using p xk_le_c xL' by auto
      show "\a b. L = cbox a b"
        using p xL' ab' by (auto simp add: interval_split[OF k,where c=c])

      fix y R
      assume yR: "(y, R) \ ?M1"
      then obtain y' R' where yR': "y = y'" "R = R' \ {x. x \ k \ c}"
                                   "(y', R') \ p" "R' \ {x. x \ k \ c} \ {}"
        by blast
      assume as: "(x, L) \ (y, R)"
      show "interior L \ interior R = {}"
      proof (cases "L' = R' \ x' = y'")
        case False
        have "interior R' = {}"
          by (metis (no_types) False Pair_inject inf.idem tagged_division_ofD(5) [OF p] xL'(3) yR'(3))
        then show ?thesis
          using yR' by simp
      next
        case True
        then have "L' \ R'"
          using as unfolding xL' yR' by auto
        have "interior L' \ interior R' = {}"
          by (metis (no_types) Pair_inject \<open>L' \<noteq> R'\<close> p tagged_division_ofD(5) xL'(3) yR'(3))
        then show ?thesis
          using xL'(2) yR'(2) by auto
      qed
    qed
    moreover
    let ?M2 = "{(x,K \ {x. x\k \ c}) |x K. (x,K) \ p \ K \ {x. x\k \ c} \ {}}"
    have \<gamma>2_fine: "\<gamma>2 fine ?M2"
      using \<open>?\<gamma> fine p\<close> by (fastforce simp: fine_def split: if_split_asm)
    have "norm ((\(x, k)\?M2. content k *\<^sub>R f x) - j) < e/2"
    proof (rule \<gamma>2norm [OF tagged_division_ofI \<gamma>2_fine])
      show "finite ?M2"
        by (rule fin_finite) (use p in blast)
      show "\{k. \x. (x, k) \ ?M2} = cbox a b \ {x. x\k \ c}"
        by (auto simp: ab_eqp)

      fix x L
      assume xL: "(x, L) \ ?M2"
      then obtain x' L' where xL': "x = x'" "L = L' \ {x. x \ k \ c}"
                                   "(x', L') \ p" "L' \ {x. x \ k \ c} \ {}"
        by blast
      then obtain a' b' where ab': "L' = cbox a' b'"
        using p by blast
      show "x \ L" "L \ cbox a b \ {x. x \ k \ c}"
        using p xk_ge_c xL' by auto
      show "\a b. L = cbox a b"
        using p xL' ab' by (auto simp add: interval_split[OF k,where c=c])

      fix y R
      assume yR: "(y, R) \ ?M2"
      then obtain y' R' where yR': "y = y'" "R = R' \ {x. x \ k \ c}"
                                   "(y', R') \ p" "R' \ {x. x \ k \ c} \ {}"
        by blast
      assume as: "(x, L) \ (y, R)"
      show "interior L \ interior R = {}"
      proof (cases "L' = R' \ x' = y'")
        case False
        have "interior R' = {}"
          by (metis (no_types) False Pair_inject inf.idem tagged_division_ofD(5) [OF p] xL'(3) yR'(3))
        then show ?thesis
          using yR' by simp
      next
        case True
        then have "L' \ R'"
          using as unfolding xL' yR' by auto
        have "interior L' \ interior R' = {}"
          by (metis (no_types) Pair_inject \<open>L' \<noteq> R'\<close> p tagged_division_ofD(5) xL'(3) yR'(3))
        then show ?thesis
          using xL'(2) yR'(2) by auto
      qed
    qed
    ultimately
    have "norm (((\(x,K) \ ?M1. content K *\<^sub>R f x) - i) + ((\(x,K) \ ?M2. content K *\<^sub>R f x) - j)) < e/2 + e/2"
      using norm_add_less by blast
    moreover have "((\(x,K) \ ?M1. content K *\<^sub>R f x) - i) +
                   ((\<Sum>(x,K) \<in> ?M2. content K *\<^sub>R f x) - j) =
                   (\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f x) - (i + j)"
    proof -
      have eq0: "\x y. x = (0::real) \ x *\<^sub>R (y::'b) = 0"
         by auto
      have cont_eq: "\g. (\(x,l). content l *\<^sub>R f x) \ (\(x,l). (x,g l)) = (\(x,l). content (g l) *\<^sub>R f x)"
        by auto
      have *: "\\ :: 'a set \ 'a set.
                  (\<Sum>(x,K)\<in>{(x, \<G> K) |x K. (x,K) \<in> p \<and> \<G> K \<noteq> {}}. content K *\<^sub>R f x) =
                  (\<Sum>(x,K)\<in>(\<lambda>(x,K). (x, \<G> K)) ` p. content K *\<^sub>R f x)"
        by (rule sum.mono_neutral_left) (auto simp: \<open>finite p\<close>)
      have "((\(x, k)\?M1. content k *\<^sub>R f x) - i) + ((\(x, k)\?M2. content k *\<^sub>R f x) - j) =
        (\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)"
        by auto
      moreover have "\ = (\(x,K) \ p. content (K \ {x. x \ k \ c}) *\<^sub>R f x) +
        (\<Sum>(x,K) \<in> p. content (K \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)"
        unfolding *
        apply (subst (1 2) sum.reindex_nontrivial)
           apply (auto intro!: k p eq0 tagged_division_split_left_inj_content tagged_division_split_right_inj_content
                       simp: cont_eq \<open>finite p\<close>)
        done
      moreover have "\x. x \ p \ (\(a,B). content (B \ {a. a \ k \ c}) *\<^sub>R f a) x +
                                (\<lambda>(a,B). content (B \<inter> {a. c \<le> a \<bullet> k}) *\<^sub>R f a) x =
                                (\<lambda>(a,B). content B *\<^sub>R f a) x"
      proof clarify
        fix a B
        assume "(a, B) \ p"
        with p obtain u v where uv: "B = cbox u v" by blast
        then show "content (B \ {x. x \ k \ c}) *\<^sub>R f a + content (B \ {x. c \ x \ k}) *\<^sub>R f a = content B *\<^sub>R f a"
          by (auto simp: scaleR_left_distrib uv content_split[OF k,of u v c])
      qed
      ultimately show ?thesis
        by (auto simp: sum.distrib[symmetric])
      qed
    ultimately show "norm ((\(x, k)\p. content k *\<^sub>R f x) - (i + j)) < e"
      by auto
  qed
qed

subsection \<open>A sort of converse, integrability on subintervals\<close>

lemma has_integral_separate_sides:
  fixes f :: "'a::euclidean_space \ 'b::real_normed_vector"
  assumes f: "(f has_integral i) (cbox a b)"
    and "e > 0"
    and k: "k \ Basis"
  obtains d where "gauge d"
    "\p1 p2. p1 tagged_division_of (cbox a b \ {x. x\k \ c}) \ d fine p1 \
        p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow>
        norm ((sum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + sum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e"
proof -
  obtain \<gamma> where d: "gauge \<gamma>"
      "\p. \p tagged_division_of cbox a b; \ fine p\
            \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < e"
    using has_integralD[OF f \<open>e > 0\<close>] by metis
  { fix p1 p2
    assume tdiv1: "p1 tagged_division_of (cbox a b) \ {x. x \ k \ c}" and "\ fine p1"
    note p1=tagged_division_ofD[OF this(1)]
    assume tdiv2: "p2 tagged_division_of (cbox a b) \ {x. c \ x \ k}" and "\ fine p2"
    note p2=tagged_division_ofD[OF this(1)]
    note tagged_division_Un_interval[OF tdiv1 tdiv2]
    note p12 = tagged_division_ofD[OF this] this
    { fix a b
      assume ab: "(a, b) \ p1 \ p2"
      have "(a, b) \ p1"
        using ab by auto
      obtain u v where uv: "b = cbox u v"
        using \<open>(a, b) \<in> p1\<close> p1(4) by moura
      have "b \ {x. x\k = c}"
        using ab p1(3)[of a b] p2(3)[of a b] by fastforce
      moreover
      have "interior {x::'a. x \ k = c} = {}"
      proof (rule ccontr)
        assume "\ ?thesis"
        then obtain x where x: "x \ interior {x::'a. x\k = c}"
          by auto
        then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> {x. x \<bullet> k = c}"
          using mem_interior by metis
        have x: "x\k = c"
          using x interior_subset by fastforce
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.43 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lifting_Code_Dt_Test.thy Sprache: Isabelle

Untersuchung Isabelle^©

¤ Dauer der Verarbeitung: 0.43 Sekunden (vorverarbeitet) ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Lifting_Code_Dt_Test.thy Sprache: Isabelle

Untersuchung Isabelle©

¤ Dauer der Verarbeitung: 0.43 Sekunden (vorverarbeitet) ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

^© Kompilation durch diese Firma

Untersuchung Isabelle^©