--- 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 \<le> e \<Longrightarrow> norm (x - y) \<le> 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 "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> 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: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
- \<Longrightarrow> norm(y - x) \<le> e"
+ \<Longrightarrow> norm(y-x) \<le> e"
using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
by (simp add: add_diff_add)
@@ -2669,11 +2675,11 @@
then have "\<forall>x. \<exists>d>0.
x \<in> {a..b} \<longrightarrow>
(\<forall>y\<in>{a..b}.
- norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e * norm (y - x))"
+ norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x))"
using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast
then obtain d where d: "\<And>x. 0 < d x"
- "\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; norm (y - x) < d x\<rbrakk>
- \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e * norm (y - x)"
+ "\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; norm (y-x) < d x\<rbrakk>
+ \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x)"
by metis
show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
@@ -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 (\<lambda>i. 0) Basis"
+ have "norm (y-x) < e + sum (\<lambda>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 "\<bar>(y - x) \<bullet> i\<bar> < e"
+ show "\<bar>(y-x) \<bullet> i\<bar> < e"
using di as(2) y_def i xi by (auto simp: inner_simps)
- show "(\<Sum>i\<in>Basis - {i}. \<bar>(y - x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>Basis. 0)"
+ show "(\<Sum>i\<in>Basis - {i}. \<bar>(y-x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>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: "\<And>x'. \<lbrakk>x' \<in> {a..b}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
using \<open>e>0\<close> 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) \<le> e * \<bar>y - x\<bar>"
+ have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < 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: "((\<lambda>u. f u - f x) has_integral integral {x..y} f - (y - x) *\<^sub>R f x) {x..y}"
+ have fux_int: "((\<lambda>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 "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y - x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+ then have "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
using \<open>d>0\<close> by blast
}
then show ?thesis
@@ -3583,12 +3589,6 @@
lemma split_minus[simp]: "(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
by (simp add: split_def)
-lemma norm_triangle_le_sub: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> 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 \<Rightarrow> 'a::real_normed_vector"
assumes "a \<le> b"
@@ -3613,7 +3613,7 @@
note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
using derf_exp by simp
- have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
+ have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
(is "\<forall>x \<in> box a b. ?Q x")
proof
fix x assume x: "x \<in> box a b"
@@ -3623,8 +3623,8 @@
qed
from this [unfolded bgauge_existence_lemma]
obtain d where d: "\<And>x. 0 < d x"
- "\<And>x y. \<lbrakk>x \<in> box a b; norm (y - x) < d x\<rbrakk>
- \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e / 2 * norm (y - x)"
+ "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk>
+ \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> 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 **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
by arith
- have 1: "norm (\<Sum>(x, k)\<in>p - ?A.
+ have XX: False if xk: "(x,k) \<in> p"
+ and less: "e * (Sup k - Inf k) / 2 < norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))"
+ and "x \<noteq> a" "x \<noteq> b"
+ for x k
+ proof -
+ obtain u v where k: "k = cbox u v"
+ using p(4) xk by blast
+ then have "u \<le> v" and uv: "{u, v} \<subseteq> 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 \<in> box a b"
+ using p(2) p(3) \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> xk by fastforce
+ with d have *: "\<And>y. norm (y-x) < d x
+ \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> 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] \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> 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 "\<dots> \<le> e / 2 * norm (u - x) + e / 2 * norm (v - x)"
+ by (metis norm_triangle_le_sub add_mono * xd)
+ also have "\<dots> \<le> e / 2 * norm (v - u)"
+ using p(2)[OF xk] by (auto simp add: field_simps k)
+ also have "\<dots> < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
+ using result by (simp add: \<open>u \<le> v\<close>)
+ finally have "e * (v - u) / 2 < e * (v - u) / 2"
+ using uv by auto
+ then show False by auto
+ qed
+ have "norm (\<Sum>(x, k)\<in>p - ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
+ \<le> (\<Sum>(x, k)\<in>p - ?A. norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))))"
+ by (auto intro: sum_norm_le)
+ also have "... \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k) / 2)"
+ using XX by (force intro: sum_mono)
+ finally have 1: "norm (\<Sum>(x, k)\<in>p - ?A.
content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
\<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> 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) \<in> 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 \<le> v" and uv: "{u, v} \<subseteq> 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 \<noteq> a" "x \<noteq> b"
- then have "x \<in> 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 "\<dots> \<le> 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 "\<dots> \<le> 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 (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) -
(\<Sum>n\<in>p \<inter> ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))
\<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
@@ -3839,16 +3825,14 @@
proof goal_cases
fix x k
assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> {t. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
- then have xk: "(x, k) \<in> p" "content k = 0"
+ then have xk: "(x, k) \<in> 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 \<noteq> {}"
- 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