Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: TemperatureSensor.vdmpp Sprache: Text

Original von: 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.58 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.