# HG changeset patch # User paulson # Date 1502229289 -7200 # Node ID cc66710c9d48156a8c542bfeb0385ca15998319d # Parent 5eb0faf4477abbee676a50dabefb0ff7744b5f2a more cleanup of fundamental_theorem_of_calculus_interior diff -r 5eb0faf4477a -r cc66710c9d48 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Aug 08 13:56:29 2017 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Aug 08 23:54:49 2017 +0200 @@ -9,6 +9,12 @@ Lebesgue_Measure Tagged_Division begin +lemma norm_triangle_le_sub: "norm x + norm y \ e \ norm (x - y) \ e" + apply (subst(asm)(2) norm_minus_cancel[symmetric]) + apply (drule norm_triangle_le) + apply (auto simp add: algebra_simps) + done + lemma eps_leI: assumes "(\e::'a::linordered_idom. 0 < e \ x < y + e)" shows "x \ y" by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl) @@ -18,7 +24,7 @@ (* try instead structured proofs below *) lemma norm_diff2: "\y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \ e1; norm(y2 - x2) \ e2\ - \ norm(y - x) \ e" + \ norm(y-x) \ e" using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"] by (simp add: add_diff_add) @@ -2669,11 +2675,11 @@ then have "\x. \d>0. x \ {a..b} \ (\y\{a..b}. - norm (y - x) < d \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e * norm (y - x))" + norm (y-x) < d \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e * norm (y-x))" using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast then obtain d where d: "\x. 0 < d x" - "\x y. \x \ {a..b}; y \ {a..b}; norm (y - x) < d x\ - \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e * norm (y - x)" + "\x y. \x \ {a..b}; y \ {a..b}; norm (y-x) < d x\ + \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e * norm (y-x)" by metis show "\d. gauge d \ (\p. p tagged_division_of (cbox a b) \ d fine p \ @@ -2954,16 +2960,16 @@ unfolding euclidean_eq_iff[where 'a='a] using i by auto have *: "Basis = insert i (Basis - {i})" using i by auto - have "norm (y - x) < e + sum (\i. 0) Basis" + have "norm (y-x) < e + sum (\i. 0) Basis" apply (rule le_less_trans[OF norm_le_l1]) apply (subst *) apply (subst sum.insert) prefer 3 apply (rule add_less_le_mono) proof - - show "\(y - x) \ i\ < e" + show "\(y-x) \ i\ < e" using di as(2) y_def i xi by (auto simp: inner_simps) - show "(\i\Basis - {i}. \(y - x) \ i\) \ (\i\Basis. 0)" + show "(\i\Basis - {i}. \(y-x) \ i\) \ (\i\Basis. 0)" unfolding y_def by (auto simp: inner_simps) qed auto then show "dist y x < e" @@ -3145,7 +3151,7 @@ assume "e > 0" obtain d where "d>0" and d: "\x'. \x' \ {a..b}; \x' - x\ < d\ \ norm(f x' - f x) \ e" using \e>0\ fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le) - have "norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \ e * \y - x\" + have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \ e * \y - x\" if y: "y \ {a..b}" and yx: "\y - x\ < d" for y proof (cases "y < x") case False @@ -3153,7 +3159,7 @@ using f y by (simp add: integrable_subinterval_real) then have Idiff: "?I a y - ?I a x = ?I x y" using False x by (simp add: algebra_simps integral_combine) - have fux_int: "((\u. f u - f x) has_integral integral {x..y} f - (y - x) *\<^sub>R f x) {x..y}" + have fux_int: "((\u. f u - f x) has_integral integral {x..y} f - (y-x) *\<^sub>R f x) {x..y}" apply (rule has_integral_diff) using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]]) using has_integral_const_real [of "f x" x y] False @@ -3186,7 +3192,7 @@ then show ?thesis by (simp add: algebra_simps norm_minus_commute) qed - then have "\d>0. \y\{a..b}. \y - x\ < d \ norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \ e * \y - x\" + then have "\d>0. \y\{a..b}. \y - x\ < d \ norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \ e * \y - x\" using \d>0\ by blast } then show ?thesis @@ -3583,12 +3589,6 @@ lemma split_minus[simp]: "(\(x, k). f x k) x - (\(x, k). g x k) x = (\(x, k). f x k - g x k) x" by (simp add: split_def) -lemma norm_triangle_le_sub: "norm x + norm y \ e \ norm (x - y) \ e" - apply (subst(asm)(2) norm_minus_cancel[symmetric]) - apply (drule norm_triangle_le) - apply (auto simp add: algebra_simps) - done - theorem fundamental_theorem_of_calculus_interior: fixes f :: "real \ 'a::real_normed_vector" assumes "a \ b" @@ -3613,7 +3613,7 @@ note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt] have bounded: "\x. x \ {a<.. bounded_linear (\u. u *\<^sub>R f' x)" using derf_exp by simp - have "\x \ box a b. \d>0. \y. norm (y - x) < d \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e/2 * norm (y - x)" + have "\x \ box a b. \d>0. \y. norm (y-x) < d \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e/2 * norm (y-x)" (is "\x \ box a b. ?Q x") proof fix x assume x: "x \ box a b" @@ -3623,8 +3623,8 @@ qed from this [unfolded bgauge_existence_lemma] obtain d where d: "\x. 0 < d x" - "\x y. \x \ box a b; norm (y - x) < d x\ - \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ e / 2 * norm (y - x)" + "\x y. \x \ box a b; norm (y-x) < d x\ + \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e / 2 * norm (y-x)" by metis have "bounded (f ` cbox a b)" apply (rule compact_imp_bounded compact_continuous_image)+ @@ -3757,61 +3757,47 @@ 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 - have 1: "norm (\(x, k)\p - ?A. + have XX: False if xk: "(x,k) \ p" + and less: "e * (Sup k - Inf k) / 2 < norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))" + and "x \ a" "x \ b" + for x k + proof - + obtain u v where k: "k = cbox u v" + using p(4) xk by blast + then have "u \ v" and uv: "{u, v} \ cbox u v" + using p(2)[OF xk] by auto + then have result: "e * (v - u) / 2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))" + using less[unfolded k box_real interval_bounds_real content_real] by auto + then have "x \ box a b" + using p(2) p(3) \x \ a\ \x \ b\ xk by fastforce + with d have *: "\y. norm (y-x) < d x + \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e / 2 * norm (y-x)" + by metis + have xd: "norm (u - x) < d x" "norm (v - x) < d x" + using fineD[OF as(2) xk] \x \ a\ \x \ b\ uv + by (auto simp add: k subset_eq dist_commute dist_real_def) + have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) = + norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))" + by (rule arg_cong[where f=norm]) (auto simp: scaleR_left.diff) + also have "\ \ e / 2 * norm (u - x) + e / 2 * norm (v - x)" + by (metis norm_triangle_le_sub add_mono * xd) + also have "\ \ e / 2 * norm (v - u)" + using p(2)[OF xk] by (auto simp add: field_simps k) + also have "\ < norm ((v - u) *\<^sub>R f' x - (f v - f u))" + using result by (simp add: \u \ v\) + finally have "e * (v - u) / 2 < e * (v - u) / 2" + using uv by auto + then show False by auto + qed + have "norm (\(x, k)\p - ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) + \ (\(x, k)\p - ?A. norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))))" + by (auto intro: sum_norm_le) + also have "... \ (\n\p - ?A. e * (case n of (x, k) \ Sup k - Inf k) / 2)" + using XX by (force intro: sum_mono) + finally 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 - apply (subst sum_divide_distrib) - apply (rule order_refl) - apply safe - apply (unfold not_le o_def split_conv fst_conv) - proof (rule ccontr) - fix x k - assume xk: "(x, k) \ p" - "e * (Sup k - Inf k) / 2 < - norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))" - obtain u v where k: "k = cbox u v" - using p(4) xk(1) by blast - then have "u \ v" and uv: "{u, v} \ cbox u v" - using p(2)[OF xk(1)] by auto - then have result: "e * (v - u) / 2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))" - using xk(2)[unfolded k box_real interval_bounds_real content_real] by auto - assume as': "x \ a" "x \ b" - then have "x \ box a b" - using p(2-3)[OF xk(1)] by (auto simp: mem_box) - note * = d(2)[OF this] - have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) = - norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))" - apply (rule arg_cong[of _ _ norm]) - unfolding scaleR_left.diff - apply auto - done - also have "\ \ e / 2 * norm (u - x) + e / 2 * norm (v - x)" - apply (rule norm_triangle_le_sub) - apply (rule add_mono) - apply (rule_tac[!] *) - using fineD[OF as(2) xk(1)] as' - unfolding k subset_eq - apply - - apply (erule_tac x=u in ballE) - apply (erule_tac[3] x=v in ballE) - using uv - apply (auto simp:dist_real_def) - done - also have "\ \ e / 2 * norm (v - u)" - using p(2)[OF xk(1)] - unfolding k - by (auto simp add: field_simps) - finally have "e * (v - u) / 2 < e * (v - u) / 2" - apply - - apply (rule less_le_trans[OF result]) - using uv - apply auto - done - then show False by auto - qed + by (simp add: sum_divide_distrib) 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" @@ -3839,16 +3825,14 @@ proof goal_cases fix x k assume "(x, k) \ p \ {t. fst t \ {a, b}} - p \ {t. fst t \ {a, b} \ content (snd t) \ 0}" - then have xk: "(x, k) \ p" "content k = 0" + then have xk: "(x, k) \ p" and k0: "content k = 0" by auto then obtain u v where uv: "k = cbox u v" using p(4) by blast have "k \ {}" - using p(2)[OF xk(1)] by auto + using p(2)[OF xk] by auto then have *: "u = v" - using xk - unfolding uv content_eq_0 box_eq_empty - by auto + using xk k0 by (auto simp: uv content_eq_0 box_eq_empty) then show "content k *\<^sub>R (f' (x)) - (f ((Sup k)) - f ((Inf k))) = 0" using xk unfolding uv by auto next