--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Apr 30 08:49:37 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Apr 30 22:13:21 2018 +0100
@@ -2470,8 +2470,8 @@
proof
show "convex hull (s \<times> t) \<subseteq> (convex hull s) \<times> (convex hull t)"
by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull)
- have "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)"
- proof (intro hull_induct)
+ have "(x, y) \<in> convex hull (s \<times> t)" if x: "x \<in> convex hull s" and y: "y \<in> convex hull t" for x y
+ proof (rule hull_induct [OF x], rule hull_induct [OF y])
fix x y assume "x \<in> s" and "y \<in> t"
then show "(x, y) \<in> convex hull (s \<times> t)"
by (simp add: hull_inc)
@@ -2484,8 +2484,8 @@
by (auto simp: image_def Bex_def)
finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
next
- show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
- proof (unfold Collect_ball_eq, rule convex_INT [rule_format])
+ show "convex {x. (x, y) \<in> convex hull s \<times> t}"
+ proof -
fix y let ?S = "((\<lambda>x. (x, 0)) -` (\<lambda>p. (0, - y) + p) ` (convex hull s \<times> t))"
have "convex ?S"
by (intro convex_linear_vimage convex_translation convex_convex_hull,
@@ -2496,7 +2496,7 @@
qed
qed
then show "(convex hull s) \<times> (convex hull t) \<subseteq> convex hull (s \<times> t)"
- unfolding subset_eq split_paired_Ball_Sigma .
+ unfolding subset_eq split_paired_Ball_Sigma by blast
qed
@@ -2512,16 +2512,13 @@
fixes S :: "'a::real_vector set"
assumes "S \<noteq> {}"
shows "convex hull (insert a S) =
- {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull S) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}"
+ {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull S) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}"
(is "_ = ?hull")
- apply (rule, rule hull_minimal, rule)
+proof (intro equalityI hull_minimal subsetI)
+ fix x
+ assume "x \<in> insert a S"
+ then have "\<exists>u\<ge>0. \<exists>v\<ge>0. u + v = 1 \<and> (\<exists>b. b \<in> convex hull S \<and> x = u *\<^sub>R a + v *\<^sub>R b)"
unfolding insert_iff
- prefer 3
- apply rule
-proof -
- fix x
- assume x: "x = a \<or> x \<in> S"
- then have "\<exists>u\<ge>0. \<exists>v\<ge>0. u + v = 1 \<and> (\<exists>b. b \<in> convex hull S \<and> x = u *\<^sub>R a + v *\<^sub>R b)"
proof
assume "x = a"
then show ?thesis
@@ -2619,7 +2616,7 @@
lemma convex_hull_insert_alt:
"convex hull (insert a S) =
- (if S = {} then {a}
+ (if S = {} then {a}
else {(1 - u) *\<^sub>R a + u *\<^sub>R x |x u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> convex hull S})"
apply (auto simp: convex_hull_insert)
using diff_eq_eq apply fastforce
@@ -4371,7 +4368,7 @@
finally have "y \<in> S"
apply (subst *)
apply (rule assms(1)[unfolded convex_alt,rule_format])
- apply (rule d[unfolded subset_eq,rule_format])
+ apply (rule d[THEN subsetD])
unfolding mem_ball
using assms(3-5) **
apply auto
@@ -4751,22 +4748,17 @@
lemma affine_hull_linear_image:
assumes "bounded_linear f"
shows "f ` (affine hull s) = affine hull f ` s"
- apply rule
- unfolding subset_eq ball_simps
- apply (rule_tac[!] hull_induct, rule hull_inc)
- prefer 3
- apply (erule imageE)
- apply (rule_tac x=xa in image_eqI, assumption)
- apply (rule hull_subset[unfolded subset_eq, rule_format], assumption)
proof -
interpret f: bounded_linear f by fact
- show "affine {x. f x \<in> affine hull f ` s}"
+ have "affine {x. f x \<in> affine hull f ` s}"
unfolding affine_def
by (auto simp: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format])
- show "affine {x. x \<in> f ` (affine hull s)}"
+ moreover have "affine {x. x \<in> f ` (affine hull s)}"
using affine_affine_hull[unfolded affine_def, of s]
unfolding affine_def by (auto simp: f.scaleR [symmetric] f.add [symmetric])
-qed auto
+ ultimately show ?thesis
+ by (auto simp: hull_inc elim!: hull_induct)
+qed
lemma rel_interior_injective_on_span_linear_image:
@@ -6484,8 +6476,8 @@
show "convex (cbox x y)"
by (rule convex_box)
next
- fix s assume "{x, y} \<subseteq> s" and "convex s"
- then show "cbox x y \<subseteq> s"
+ fix S assume "{x, y} \<subseteq> S" and "convex S"
+ then show "cbox x y \<subseteq> S"
unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def
by - (clarify, simp (no_asm_use), fast)
qed
@@ -6516,66 +6508,53 @@
text \<open>And this is a finite set of vertices.\<close>
lemma unit_cube_convex_hull:
- obtains s :: "'a::euclidean_space set"
- where "finite s" and "cbox 0 (\<Sum>Basis) = convex hull s"
- apply (rule that[of "{x::'a. \<forall>i\<in>Basis. x\<bullet>i=0 \<or> x\<bullet>i=1}"])
- apply (rule finite_subset[of _ "(\<lambda>s. (\<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i)::'a) ` Pow Basis"])
- prefer 3
- apply (rule unit_interval_convex_hull, rule)
- unfolding mem_Collect_eq
-proof -
- fix x :: 'a
- assume as: "\<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1"
- show "x \<in> (\<lambda>s. \<Sum>i\<in>Basis. (if i\<in>s then 1 else 0) *\<^sub>R i) ` Pow Basis"
- apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
- using as
- apply (subst euclidean_eq_iff, auto)
- done
-qed auto
+ obtains S :: "'a::euclidean_space set"
+ where "finite S" and "cbox 0 (\<Sum>Basis) = convex hull S"
+proof
+ show "finite {x::'a. \<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1}"
+ proof (rule finite_subset, clarify)
+ show "finite ((\<lambda>S. \<Sum>i\<in>Basis. (if i \<in> S then 1 else 0) *\<^sub>R i) ` Pow Basis)"
+ using finite_Basis by blast
+ fix x :: 'a
+ assume as: "\<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1"
+ show "x \<in> (\<lambda>S. \<Sum>i\<in>Basis. (if i\<in>S then 1 else 0) *\<^sub>R i) ` Pow Basis"
+ apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
+ using as
+ apply (subst euclidean_eq_iff, auto)
+ done
+ qed
+ show "cbox 0 One = convex hull {x. \<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1}"
+ using unit_interval_convex_hull by blast
+qed
text \<open>Hence any cube (could do any nonempty interval).\<close>
lemma cube_convex_hull:
assumes "d > 0"
- obtains s :: "'a::euclidean_space set" where
- "finite s" and "cbox (x - (\<Sum>i\<in>Basis. d*\<^sub>Ri)) (x + (\<Sum>i\<in>Basis. d*\<^sub>Ri)) = convex hull s"
+ obtains S :: "'a::euclidean_space set" where
+ "finite S" and "cbox (x - (\<Sum>i\<in>Basis. d*\<^sub>Ri)) (x + (\<Sum>i\<in>Basis. d*\<^sub>Ri)) = convex hull S"
proof -
- let ?d = "(\<Sum>i\<in>Basis. d*\<^sub>Ri)::'a"
+ let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
have *: "cbox (x - ?d) (x + ?d) = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 (\<Sum>Basis)"
- apply (rule set_eqI, rule)
- unfolding image_iff
- defer
- apply (erule bexE)
- proof -
+ proof (intro set_eqI iffI)
fix y
- assume as: "y\<in>cbox (x - ?d) (x + ?d)"
+ assume "y \<in> cbox (x - ?d) (x + ?d)"
then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
using assms by (simp add: mem_box field_simps inner_simps)
- with \<open>0 < d\<close> show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
- by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
+ with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum (( *\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
+ by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"])
next
- fix y z
- assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
- have "\<And>i. i\<in>Basis \<Longrightarrow> 0 \<le> d * (z \<bullet> i) \<and> d * (z \<bullet> i) \<le> d"
- using assms as(1)[unfolded mem_box]
+ fix y
+ assume "y \<in> (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 One"
+ then obtain z where z: "z \<in> cbox 0 One" "y = x - ?d + (2*d) *\<^sub>R z"
by auto
then show "y \<in> cbox (x - ?d) (x + ?d)"
- unfolding as(2) mem_box
- apply -
- apply rule
- using as(1)[unfolded mem_box]
- apply (erule_tac x=i in ballE)
- using assms
- apply (auto simp: inner_simps)
- done
+ using z assms by (auto simp: mem_box inner_simps)
qed
- obtain s where "finite s" "cbox 0 (\<Sum>Basis::'a) = convex hull s"
+ obtain S where "finite S" "cbox 0 (\<Sum>Basis::'a) = convex hull S"
using unit_cube_convex_hull by auto
then show ?thesis
- apply (rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"])
- unfolding * and convex_hull_affinity
- apply auto
- done
+ by (rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` S"]) (auto simp: convex_hull_affinity *)
qed
subsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
@@ -6635,18 +6614,18 @@
lemma closed_interval_as_convex_hull:
fixes a :: "'a::euclidean_space"
- obtains s where "finite s" "cbox a b = convex hull s"
+ obtains S where "finite S" "cbox a b = convex hull S"
proof (cases "cbox a b = {}")
case True with convex_hull_empty that show ?thesis
by blast
next
case False
- obtain s::"'a set" where "finite s" and eq: "cbox 0 One = convex hull s"
+ obtain S::"'a set" where "finite S" and eq: "cbox 0 One = convex hull S"
by (blast intro: unit_cube_convex_hull)
have lin: "linear (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k)"
by (rule linear_compose_sum) (auto simp: algebra_simps linearI)
- have "finite ((+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` s)"
- by (rule finite_imageI \<open>finite s\<close>)+
+ have "finite ((+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` S)"
+ by (rule finite_imageI \<open>finite S\<close>)+
then show ?thesis
apply (rule that)
apply (simp add: convex_hull_translation convex_hull_linear_image [OF lin, symmetric])
@@ -6658,31 +6637,23 @@
subsection%unimportant \<open>Bounded convex function on open set is continuous\<close>
lemma convex_on_bounded_continuous:
- fixes s :: "('a::real_normed_vector) set"
- assumes "open s"
- and "convex_on s f"
- and "\<forall>x\<in>s. \<bar>f x\<bar> \<le> b"
- shows "continuous_on s f"
+ fixes S :: "('a::real_normed_vector) set"
+ assumes "open S"
+ and "convex_on S f"
+ and "\<forall>x\<in>S. \<bar>f x\<bar> \<le> b"
+ shows "continuous_on S f"
apply (rule continuous_at_imp_continuous_on)
unfolding continuous_at_real_range
proof (rule,rule,rule)
fix x and e :: real
- assume "x \<in> s" "e > 0"
+ assume "x \<in> S" "e > 0"
define B where "B = \<bar>b\<bar> + 1"
- have B: "0 < B" "\<And>x. x\<in>s \<Longrightarrow> \<bar>f x\<bar> \<le> B"
- unfolding B_def
- defer
- apply (drule assms(3)[rule_format])
- apply auto
- done
- obtain k where "k > 0" and k: "cball x k \<subseteq> s"
- using assms(1)[unfolded open_contains_cball, THEN bspec[where x=x]]
- using \<open>x\<in>s\<close> by auto
+ then have B: "0 < B""\<And>x. x\<in>S \<Longrightarrow> \<bar>f x\<bar> \<le> B"
+ using assms(3) by auto
+ obtain k where "k > 0" and k: "cball x k \<subseteq> S"
+ using \<open>x \<in> S\<close> assms(1) open_contains_cball_eq by blast
show "\<exists>d>0. \<forall>x'. norm (x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e"
- apply (rule_tac x="min (k / 2) (e / (2 * B) * k)" in exI)
- apply rule
- defer
- proof (rule, rule)
+ proof (intro exI conjI allI impI)
fix y
assume as: "norm (y - x) < min (k / 2) (e / (2 * B) * k)"
show "\<bar>f y - f x\<bar> < e"
@@ -6692,22 +6663,16 @@
have "2 < t" "0<t"
unfolding t_def using as False and \<open>k>0\<close>
by (auto simp:field_simps)
- have "y \<in> s"
- apply (rule k[unfolded subset_eq,rule_format])
+ have "y \<in> S"
+ apply (rule k[THEN subsetD])
unfolding mem_cball dist_norm
apply (rule order_trans[of _ "2 * norm (x - y)"])
using as
by (auto simp: field_simps norm_minus_commute)
{
define w where "w = x + t *\<^sub>R (y - x)"
- have "w \<in> s"
- unfolding w_def
- apply (rule k[unfolded subset_eq,rule_format])
- unfolding mem_cball dist_norm
- unfolding t_def
- using \<open>k>0\<close>
- apply auto
- done
+ have "w \<in> S"
+ using \<open>k>0\<close> by (auto simp: dist_norm t_def w_def k[THEN subsetD])
have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x"
by (auto simp: algebra_simps)
also have "\<dots> = 0"
@@ -6720,23 +6685,17 @@
by (auto simp:field_simps)
have "f y - f x \<le> (f w - f x) / t"
using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w]
- using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> s\<close> \<open>w \<in> s\<close>
+ using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> S\<close> \<open>w \<in> S\<close>
by (auto simp:field_simps)
also have "... < e"
- using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>x\<in>s\<close>] 2 \<open>t > 0\<close> by (auto simp: field_simps)
+ using B(2)[OF \<open>w\<in>S\<close>] and B(2)[OF \<open>x\<in>S\<close>] 2 \<open>t > 0\<close> by (auto simp: field_simps)
finally have th1: "f y - f x < e" .
}
moreover
{
define w where "w = x - t *\<^sub>R (y - x)"
- have "w \<in> s"
- unfolding w_def
- apply (rule k[unfolded subset_eq,rule_format])
- unfolding mem_cball dist_norm
- unfolding t_def
- using \<open>k > 0\<close>
- apply auto
- done
+ have "w \<in> S"
+ using \<open>k > 0\<close> by (auto simp: dist_norm t_def w_def k[THEN subsetD])
have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x"
by (auto simp: algebra_simps)
also have "\<dots> = x"
@@ -6749,12 +6708,12 @@
using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
by (auto simp:field_simps)
then have *: "(f w - f y) / t < e"
- using B(2)[OF \<open>w\<in>s\<close>] and B(2)[OF \<open>y\<in>s\<close>]
+ using B(2)[OF \<open>w\<in>S\<close>] and B(2)[OF \<open>y\<in>S\<close>]
using \<open>t > 0\<close>
by (auto simp:field_simps)
have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
- using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> s\<close> \<open>w \<in> s\<close>
+ using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> S\<close> \<open>w \<in> S\<close>
by (auto simp:field_simps)
also have "\<dots> = (f w + t * f y) / (1 + t)"
using \<open>t > 0\<close> by (auto simp: divide_simps)
@@ -6843,11 +6802,7 @@
by (simp add: dist_norm abs_le_iff algebra_simps)
show "cball x d \<subseteq> convex hull c"
unfolding 2
- apply clarsimp
- apply (simp only: dist_norm)
- apply (subst inner_diff_left [symmetric], simp)
- apply (erule (1) order_trans [OF Basis_le_norm])
- done
+ by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le)
have e': "e = (\<Sum>(i::'a)\<in>Basis. d)"
by (simp add: d_def DIM_positive)
show "convex hull c \<subseteq> cball x e"
--- a/src/HOL/Analysis/Derivative.thy Mon Apr 30 08:49:37 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy Mon Apr 30 22:13:21 2018 +0100
@@ -373,77 +373,76 @@
lemma frechet_derivative_unique_within:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
- assumes "(f has_derivative f') (at x within s)"
- and "(f has_derivative f'') (at x within s)"
- and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> s"
+ assumes "(f has_derivative f') (at x within S)"
+ and "(f has_derivative f'') (at x within S)"
+ and "\<forall>i\<in>Basis. \<forall>e>0. \<exists>d. 0 < \<bar>d\<bar> \<and> \<bar>d\<bar> < e \<and> (x + d *\<^sub>R i) \<in> S"
shows "f' = f''"
proof -
note as = assms(1,2)[unfolded has_derivative_def]
then interpret f': bounded_linear f' by auto
from as interpret f'': bounded_linear f'' by auto
- have "x islimpt s" unfolding islimpt_approachable
+ have "x islimpt S" unfolding islimpt_approachable
proof (rule, rule)
fix e :: real
assume "e > 0"
- obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> s"
+ obtain d where "0 < \<bar>d\<bar>" and "\<bar>d\<bar> < e" and "x + d *\<^sub>R (SOME i. i \<in> Basis) \<in> S"
using assms(3) SOME_Basis \<open>e>0\<close> by blast
- then show "\<exists>x'\<in>s. x' \<noteq> x \<and> dist x' x < e"
+ then show "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
apply (rule_tac x="x + d *\<^sub>R (SOME i. i \<in> Basis)" in bexI)
unfolding dist_norm
apply (auto simp: SOME_Basis nonzero_Basis)
done
qed
- then have *: "netlimit (at x within s) = x"
+ then have *: "netlimit (at x within S) = x"
apply (auto intro!: netlimit_within)
by (metis trivial_limit_within)
show ?thesis
- apply (rule linear_eq_stdbasis)
- unfolding linear_conv_bounded_linear
- apply (rule as(1,2)[THEN conjunct1])+
- proof (rule, rule ccontr)
+ proof (rule linear_eq_stdbasis)
+ show "linear f'" "linear f''"
+ unfolding linear_conv_bounded_linear using as by auto
+ next
fix i :: 'a
assume i: "i \<in> Basis"
define e where "e = norm (f' i - f'' i)"
- assume "f' i \<noteq> f'' i"
- then have "e > 0"
- unfolding e_def by auto
- obtain d where d:
- "0 < d"
- "(\<And>xa. xa\<in>s \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow>
- dist ((f xa - f x - f' (xa - x)) /\<^sub>R norm (xa - x) -
- (f xa - f x - f'' (xa - x)) /\<^sub>R norm (xa - x)) (0 - 0) < e)"
- using tendsto_diff [OF as(1,2)[THEN conjunct2]]
- unfolding * Lim_within
- using \<open>e>0\<close> by blast
- obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> s"
- using assms(3) i d(1) by blast
- have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
+ show "f' i = f'' i"
+ proof (rule ccontr)
+ assume "f' i \<noteq> f'' i"
+ then have "e > 0"
+ unfolding e_def by auto
+ obtain d where d:
+ "0 < d"
+ "(\<And>y. y\<in>S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow>
+ dist ((f y - f x - f' (y - x)) /\<^sub>R norm (y - x) -
+ (f y - f x - f'' (y - x)) /\<^sub>R norm (y - x)) (0 - 0) < e)"
+ using tendsto_diff [OF as(1,2)[THEN conjunct2]]
+ unfolding * Lim_within
+ using \<open>e>0\<close> by blast
+ obtain c where c: "0 < \<bar>c\<bar>" "\<bar>c\<bar> < d \<and> x + c *\<^sub>R i \<in> S"
+ using assms(3) i d(1) by blast
+ have *: "norm (- ((1 / \<bar>c\<bar>) *\<^sub>R f' (c *\<^sub>R i)) + (1 / \<bar>c\<bar>) *\<^sub>R f'' (c *\<^sub>R i)) =
norm ((1 / \<bar>c\<bar>) *\<^sub>R (- (f' (c *\<^sub>R i)) + f'' (c *\<^sub>R i)))"
- unfolding scaleR_right_distrib by auto
- also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
- unfolding f'.scaleR f''.scaleR
- unfolding scaleR_right_distrib scaleR_minus_right
- by auto
- also have "\<dots> = e"
- unfolding e_def
- using c(1)
- using norm_minus_cancel[of "f' i - f'' i"]
- by auto
- finally show False
- using c
- using d(2)[of "x + c *\<^sub>R i"]
- unfolding dist_norm
- unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
- scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
- using i
- by (auto simp: inverse_eq_divide)
+ unfolding scaleR_right_distrib by auto
+ also have "\<dots> = norm ((1 / \<bar>c\<bar>) *\<^sub>R (c *\<^sub>R (- (f' i) + f'' i)))"
+ unfolding f'.scaleR f''.scaleR
+ unfolding scaleR_right_distrib scaleR_minus_right
+ by auto
+ also have "\<dots> = e"
+ unfolding e_def
+ using c(1)
+ using norm_minus_cancel[of "f' i - f'' i"]
+ by auto
+ finally show False
+ using c
+ using d(2)[of "x + c *\<^sub>R i"]
+ unfolding dist_norm
+ unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff
+ scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib
+ using i
+ by (auto simp: inverse_eq_divide)
+ qed
qed
qed
-lemma frechet_derivative_unique_at:
- "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
- by (rule has_derivative_unique)
-
lemma frechet_derivative_unique_within_closed_interval:
fixes f::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
@@ -506,12 +505,12 @@
from assms(1) have *: "at x within box a b = at x"
by (metis at_within_interior interior_open open_box)
from assms(2,3) [unfolded *] show "f' = f''"
- by (rule frechet_derivative_unique_at)
+ by (rule has_derivative_unique)
qed
lemma frechet_derivative_at:
"(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
- apply (rule frechet_derivative_unique_at[of f])
+ apply (rule has_derivative_unique[of f])
apply assumption
unfolding frechet_derivative_works[symmetric]
using differentiable_def
--- a/src/HOL/Analysis/Linear_Algebra.thy Mon Apr 30 08:49:37 2018 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Mon Apr 30 22:13:21 2018 +0100
@@ -72,7 +72,7 @@
lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
unfolding hull_def by auto
-lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
+lemma hull_induct: "\<lbrakk>a \<in> Q hull S; \<And>x. x\<in> S \<Longrightarrow> P x; Q {x. P x}\<rbrakk> \<Longrightarrow> P a"
using hull_minimal[of S "{x. P x}" Q]
by (auto simp add: subset_eq)
@@ -339,20 +339,12 @@
unfolding dependent_def by auto
lemma (in real_vector) independent_mono: "independent A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> independent B"
- apply (clarsimp simp add: dependent_def span_mono)
- apply (subgoal_tac "span (B - {a}) \<le> span (A - {a})")
- apply force
- apply (rule span_mono)
- apply auto
- done
+ unfolding dependent_def span_mono
+ by (metis insert_Diff local.span_mono subsetCE subset_insert_iff)
lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow> subspace B \<Longrightarrow> span A = B"
by (metis order_antisym span_def hull_minimal)
-lemma (in real_vector) span_induct':
- "\<forall>x \<in> S. P x \<Longrightarrow> subspace {x. P x} \<Longrightarrow> \<forall>x \<in> span S. P x"
- unfolding span_def by (rule hull_induct) auto
-
inductive_set (in real_vector) span_induct_alt_help for S :: "'a set"
where
span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
@@ -1063,19 +1055,19 @@
done
lemma linear_eq_0_span:
- assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
- shows "\<forall>x \<in> span B. f x = 0"
- using f0 subspace_kernel[OF lf]
- by (rule span_induct')
-
-lemma linear_eq_0: "linear f \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = 0 \<Longrightarrow> \<forall>x\<in>S. f x = 0"
- using linear_eq_0_span[of f B] by auto
-
-lemma linear_eq_span: "linear f \<Longrightarrow> linear g \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x \<in> span B. f x = g x"
- using linear_eq_0_span[of "\<lambda>x. f x - g x" B] by (auto simp: linear_compose_sub)
-
-lemma linear_eq: "linear f \<Longrightarrow> linear g \<Longrightarrow> S \<subseteq> span B \<Longrightarrow> \<forall>x\<in>B. f x = g x \<Longrightarrow> \<forall>x\<in>S. f x = g x"
- using linear_eq_span[of f g B] by auto
+ assumes x: "x \<in> span B" and lf: "linear f" and f0: "\<And>x. x\<in>B \<Longrightarrow> f x = 0"
+ shows "f x = 0"
+ using x f0 subspace_kernel[OF lf] span_induct
+ by blast
+
+lemma linear_eq_0: "\<lbrakk>x \<in> S; linear f; S \<subseteq> span B; \<And>x. x\<in>B \<Longrightarrow> f x = 0\<rbrakk> \<Longrightarrow> f x = 0"
+ using linear_eq_0_span[of x B f] by auto
+
+lemma linear_eq_span: "\<lbrakk>x \<in> span B; linear f; linear g; \<And>x. x\<in>B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> f x = g x"
+ using linear_eq_0_span[of x B "\<lambda>x. f x - g x"] by (auto simp: linear_compose_sub)
+
+lemma linear_eq: "\<lbrakk>x \<in> S; linear f; linear g; S \<subseteq> span B; \<And>x. x\<in>B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> f x = g x"
+ using linear_eq_span[of _ B f g] by auto
text \<open>The degenerate case of the Exchange Lemma.\<close>
@@ -1174,13 +1166,13 @@
have fB: "inj_on f B"
using fi by (auto simp: \<open>span S = span B\<close> intro: subset_inj_on span_superset)
- have "\<forall>x\<in>span B. g (f x) = x"
- proof (intro linear_eq_span)
+ have "g (f x) = x" if "x \<in> span B" for x
+ proof (rule linear_eq_span)
show "linear (\<lambda>x. x)" "linear (\<lambda>x. g (f x))"
using linear_id linear_compose[OF \<open>linear f\<close> \<open>linear g\<close>] by (auto simp: id_def comp_def)
- show "\<forall>x \<in> B. g (f x) = x"
- using g fi \<open>span S = span B\<close> by (auto simp: fB)
- qed
+ show "g (f x) = x" if "x \<in> B" for x
+ using g fi \<open>span S = span B\<close> by (simp add: fB that)
+ qed (rule that)
moreover
have "inv_into B f ` f ` B \<subseteq> B"
by (auto simp: fB)
@@ -1210,8 +1202,7 @@
ultimately have "\<forall>x\<in>B. f (g x) = x"
by auto
then have "\<forall>x\<in>span B. f (g x) = x"
- using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>]
- by (intro linear_eq_span) (auto simp: id_def comp_def)
+ using linear_id linear_compose[OF \<open>linear g\<close> \<open>linear f\<close>] linear_eq_span by fastforce
moreover have "inv_into (span S) f ` B \<subseteq> span S"
using \<open>B \<subseteq> T\<close> \<open>span T \<subseteq> f`span S\<close> by (auto intro: inv_into_into span_superset)
then have "range g \<subseteq> span S"
@@ -2457,8 +2448,8 @@
done
with a have a0:"?a \<noteq> 0"
by auto
- have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
- proof (rule span_induct')
+ have "?a \<bullet> x = 0" if "x\<in>span B" for x
+ proof (rule span_induct [OF that])
show "subspace {x. ?a \<bullet> x = 0}"
by (auto simp add: subspace_def inner_add)
next
@@ -2481,9 +2472,9 @@
intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])
done
}
- then show "\<forall>x \<in> B. ?a \<bullet> x = 0"
- by blast
- qed
+ then show "?a \<bullet> x = 0" if "x \<in> B" for x
+ using that by blast
+ qed
with a0 show ?thesis
unfolding sSB by (auto intro: exI[where x="?a"])
qed
@@ -2635,9 +2626,9 @@
fixes f :: "'a::euclidean_space \<Rightarrow> _"
assumes lf: "linear f"
and lg: "linear g"
- and fg: "\<forall>b\<in>Basis. f b = g b"
+ and fg: "\<And>b. b \<in> Basis \<Longrightarrow> f b = g b"
shows "f = g"
- using linear_eq[OF lf lg, of _ Basis] fg by auto
+ using linear_eq[OF _ lf lg, of _ _ Basis] fg by auto
text \<open>Similar results for bilinear functions.\<close>
@@ -2646,8 +2637,9 @@
and bg: "bilinear g"
and SB: "S \<subseteq> span B"
and TC: "T \<subseteq> span C"
- and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
- shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
+ and "x\<in>S" "y\<in>T"
+ and fg: "\<And>x y. \<lbrakk>x \<in> B; y\<in> C\<rbrakk> \<Longrightarrow> f x y = g x y"
+ shows "f x y = g x y"
proof -
let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
from bf bg have sp: "subspace ?P"
@@ -2655,27 +2647,30 @@
by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
intro: bilinear_ladd[OF bf])
- have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
- apply (rule span_induct' [OF _ sp])
- apply (rule ballI)
- apply (rule span_induct')
- apply (simp add: fg)
+ have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
apply (auto simp add: subspace_def)
using bf bg unfolding bilinear_def linear_iff
- apply (auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def
+ apply (auto simp add: bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add
intro: bilinear_ladd[OF bf])
done
+ have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
+ apply (rule span_induct [OF that sp])
+ apply (rule ballI)
+ apply (erule span_induct)
+ apply (simp_all add: sfg fg)
+ done
then show ?thesis
- using SB TC by auto
+ using SB TC assms by auto
qed
lemma bilinear_eq_stdbasis:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> _"
assumes bf: "bilinear f"
and bg: "bilinear g"
- and fg: "\<forall>i\<in>Basis. \<forall>j\<in>Basis. f i j = g i j"
+ and fg: "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> f i j = g i j"
shows "f = g"
- using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis] fg] by blast
+ using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg
+ by blast
text \<open>An injective map @{typ "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"} is also surjective.\<close>
@@ -2695,13 +2690,7 @@
apply (rule card_ge_dim_independent)
apply blast
apply (rule independent_injective_image[OF B(2) lf fi])
- apply (rule order_eq_refl)
- apply (rule sym)
- unfolding d
- apply (rule card_image)
- apply (rule subset_inj_on[OF fi])
- apply blast
- done
+ by (metis card_image d fi inj_on_subset order_refl top_greatest)
from th show ?thesis
unfolding span_linear_image[OF lf] surj_def
using B(3) by blast