# HG changeset patch # User paulson # Date 1502193389 -7200 # Node ID 5eb0faf4477abbee676a50dabefb0ff7744b5f2a # Parent 92b4f0073eea1e0fb4387b0f7d812b791811dffb partly unravelled fundamental_theorem_of_calculus_interior diff -r 92b4f0073eea -r 5eb0faf4477a src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Aug 08 12:37:01 2017 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Aug 08 13:56:29 2017 +0200 @@ -3639,8 +3639,8 @@ have "continuous (at a within {a..b}) f" using contf continuous_on_eq_continuous_within by force with eba8 obtain k where "0 < k" - and k: "\x. \x \ {a..b}; 0 < norm (x-a); norm (x-a) < k\ - \ norm (f x - f a) < e * (b - a) / 8" + and k: "\x. \x \ {a..b}; 0 < norm (x-a); norm (x-a) < k\ + \ norm (f x - f a) < e * (b - a) / 8" unfolding continuous_within Lim_within dist_norm by metis obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \ e * (b - a) / 8" proof (cases "f' a = 0") @@ -3757,15 +3757,9 @@ note * = additive_tagged_division_1[OF assms(1) as(1), symmetric] have **: "\n1 s1 n2 s2::real. n2 \ s2 / 2 \ n1 - s1 \ s2 / 2 \ n1 + n2 \ s1 + s2" by arith - show "norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b}" - unfolding content_real[OF assms(1)] and *[of "\x. x"] *[of f] sum_subtractf[symmetric] split_minus - unfolding sum_distrib_left - apply (subst(2) pA) - apply (subst pA) - unfolding sum.union_disjoint[OF pA(2-)] - proof (rule norm_triangle_le, rule **, goal_cases) - case 1 - show ?case + have 1: "norm (\(x, k)\p - ?A. + content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) + \ (\n\p - ?A. e * (case n of (x, k) \ Sup k - Inf k)) / 2" apply (rule order_trans) apply (rule sum_norm_le) defer @@ -3818,11 +3812,11 @@ done then show False by auto qed - next - have *: "\x s1 s2::real. 0 \ s1 \ x \ (s1 + s2) / 2 \ x - s1 \ s2 / 2" - by auto - case 2 - have ge0: "0 \ e * (Sup k - Inf k)" if xkp: "(x, k) \ p \ {t. fst t \ {a, b}}" for x k + have 2: "norm (\(x, k)\p \ ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) - + (\n\p \ ?A. e * (case n of (x, k) \ Sup k - Inf k)) + \ (\n\p - ?A. e * (case n of (x, k) \ Sup k - Inf k)) / 2" + proof - + have ge0: "0 \ e * (Sup k - Inf k)" if xkp: "(x, k) \ p \ ?A" for x k proof - obtain u v where uv: "k = cbox u v" by (meson Int_iff xkp p(4)) @@ -4062,7 +4056,9 @@ qed (insert p(1) ab e, auto simp add: field_simps) qed auto qed - show ?case + have *: "\x s1 s2::real. 0 \ s1 \ x \ (s1 + s2) / 2 \ x - s1 \ s2 / 2" + by auto + show ?thesis apply (rule * [OF sum_nonneg]) using ge0 apply force unfolding sum.union_disjoint[OF pA(2-),symmetric] pA(1)[symmetric] @@ -4072,6 +4068,14 @@ apply (rule **) done qed + show "norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b}" + unfolding content_real[OF assms(1)] and *[of "\x. x"] *[of f] sum_subtractf[symmetric] split_minus + unfolding sum_distrib_left + apply (subst(2) pA) + apply (subst pA) + unfolding sum.union_disjoint[OF pA(2-)] + using ** norm_triangle_le 1 2 + by blast qed qed