--- a/src/HOL/Analysis/Borel_Space.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Borel_Space.thy Thu Feb 22 18:01:08 2018 +0100
@@ -242,6 +242,11 @@
shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
+lemma closed_subset_contains_Sup:
+ fixes A C :: "real set"
+ shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
+ by (metis closure_contains_Sup closure_minimal subset_eq)
+
lemma deriv_nonneg_imp_mono:
assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Feb 22 18:01:08 2018 +0100
@@ -8,8 +8,35 @@
imports
Topology_Euclidean_Space
Operator_Norm
+ Uniform_Limit
begin
+lemma onorm_componentwise:
+ assumes "bounded_linear f"
+ shows "onorm f \<le> (\<Sum>i\<in>Basis. norm (f i))"
+proof -
+ {
+ fix i::'a
+ assume "i \<in> Basis"
+ hence "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> onorm (\<lambda>x. (x \<bullet> i)) * norm (f i)"
+ by (auto intro!: onorm_scaleR_left_lemma bounded_linear_inner_left)
+ also have "\<dots> \<le> norm i * norm (f i)"
+ by (rule mult_right_mono)
+ (auto simp: ac_simps Cauchy_Schwarz_ineq2 intro!: onorm_le)
+ finally have "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> norm (f i)" using \<open>i \<in> Basis\<close>
+ by simp
+ } hence "onorm (\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<le> (\<Sum>i\<in>Basis. norm (f i))"
+ by (auto intro!: order_trans[OF onorm_sum_le] bounded_linear_scaleR_const
+ sum_mono bounded_linear_inner_left)
+ also have "(\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) = (\<lambda>x. f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i))"
+ by (simp add: linear_sum bounded_linear.linear assms linear_simps)
+ also have "\<dots> = f"
+ by (simp add: euclidean_representation)
+ finally show ?thesis .
+qed
+
+lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]
+
subsection \<open>Intro rules for @{term bounded_linear}\<close>
named_theorems bounded_linear_intros
@@ -447,6 +474,15 @@
shows "continuous F f"
using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
+lemma
+ continuous_on_blinfun_componentwise:
+ fixes f:: "'d::t2_space \<Rightarrow> 'e::euclidean_space \<Rightarrow>\<^sub>L 'f::real_normed_vector"
+ assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on s (\<lambda>x. f x i)"
+ shows "continuous_on s f"
+ using assms
+ by (auto intro!: continuous_at_imp_continuous_on intro!: tendsto_componentwise1
+ simp: continuous_on_eq_continuous_within continuous_def)
+
lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
by (auto intro!: bounded_linearI' bounded_linear_intros)
@@ -692,4 +728,9 @@
lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
+lemmas bounded_linear_function_uniform_limit_intros[uniform_limit_intros] =
+ bounded_linear.uniform_limit[OF bounded_linear_apply_blinfun]
+ bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
+ bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
+
end
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Feb 22 18:01:08 2018 +0100
@@ -1,7 +1,7 @@
section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
theory Cartesian_Euclidean_Space
-imports Finite_Cartesian_Product Derivative
+imports Finite_Cartesian_Product Derivative
begin
lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
@@ -1471,4 +1471,9 @@
unfolding vec_lambda_beta
by auto
+lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] =
+ bounded_linear.uniform_limit[OF blinfun.bounded_linear_right]
+ bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
+ bounded_linear.uniform_limit[OF bounded_linear_component_cart]
+
end
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Feb 22 18:01:08 2018 +0100
@@ -1199,7 +1199,7 @@
lemma vector_derivative_linepath_within:
"x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b - a"
- apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified])
+ apply (rule vector_derivative_within_cbox [of 0 "1::real", simplified])
apply (auto simp: has_vector_derivative_linepath_within)
done
@@ -2695,7 +2695,7 @@
then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \<midarrow>x\<rightarrow> 0"
by (simp add: Lim_at dist_norm inverse_eq_divide)
show ?thesis
- apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
+ apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
apply (rule Lim_transform [OF * Lim_eventually])
apply (simp add: inverse_eq_divide [symmetric] eventually_at)
using \<open>open s\<close> x
@@ -3573,7 +3573,7 @@
if "x \<in> {0..1} - S" for x
proof -
have "vector_derivative (uminus \<circ> \<gamma>) (at x within cbox 0 1) = - vector_derivative \<gamma> (at x within cbox 0 1)"
- apply (rule vector_derivative_within_closed_interval)
+ apply (rule vector_derivative_within_cbox)
using that
apply (auto simp: o_def)
apply (rule has_vector_derivative_minus)
--- a/src/HOL/Analysis/Connected.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Connected.thy Thu Feb 22 18:01:08 2018 +0100
@@ -1095,6 +1095,43 @@
qed
qed
+text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
+
+lemma distance_attains_sup:
+ assumes "compact s" "s \<noteq> {}"
+ shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
+proof (rule continuous_attains_sup [OF assms])
+ {
+ fix x
+ assume "x\<in>s"
+ have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
+ by (intro tendsto_dist tendsto_const tendsto_ident_at)
+ }
+ then show "continuous_on s (dist a)"
+ unfolding continuous_on ..
+qed
+
+text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
+
+lemma distance_attains_inf:
+ fixes a :: "'a::heine_borel"
+ assumes "closed s" and "s \<noteq> {}"
+ obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
+proof -
+ from assms obtain b where "b \<in> s" by auto
+ let ?B = "s \<inter> cball a (dist b a)"
+ have "?B \<noteq> {}" using \<open>b \<in> s\<close>
+ by (auto simp: dist_commute)
+ moreover have "continuous_on ?B (dist a)"
+ by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
+ moreover have "compact ?B"
+ by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
+ ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
+ by (metis continuous_attains_inf)
+ with that show ?thesis by fastforce
+qed
+
+
subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
lemma summable_imp_bounded:
@@ -1353,6 +1390,24 @@
shows "infdist x S > 0"
using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
+lemma
+ infdist_attains_inf:
+ fixes X::"'a::heine_borel set"
+ assumes "closed X"
+ assumes "X \<noteq> {}"
+ obtains x where "x \<in> X" "infdist y X = dist y x"
+proof -
+ have "bdd_below (dist y ` X)"
+ by auto
+ from distance_attains_inf[OF assms, of y]
+ obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
+ have "infdist y X = dist y x"
+ by (auto simp: infdist_def assms
+ intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
+ with \<open>x \<in> X\<close> show ?thesis ..
+qed
+
+
text \<open>Every metric space is a T4 space:\<close>
instance metric_space \<subseteq> t4_space
@@ -1423,6 +1478,36 @@
shows "continuous F (\<lambda>x. infdist (f x) A)"
using assms unfolding continuous_def by (rule tendsto_infdist)
+lemma compact_infdist_le:
+ fixes A::"'a::heine_borel set"
+ assumes "A \<noteq> {}"
+ assumes "compact A"
+ assumes "e > 0"
+ shows "compact {x. infdist x A \<le> e}"
+proof -
+ from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
+ continuous_infdist[OF continuous_ident, of _ UNIV A]
+ have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
+ moreover
+ from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
+ by (auto simp: compact_eq_bounded_closed bounded_def)
+ {
+ fix y
+ assume le: "infdist y A \<le> e"
+ from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
+ obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
+ have "dist x0 y \<le> dist y z + dist x0 z"
+ by (metis dist_commute dist_triangle)
+ also have "dist y z \<le> e" using le z by simp
+ also have "dist x0 z \<le> b" using b z by simp
+ finally have "dist x0 y \<le> b + e" by arith
+ } then
+ have "bounded {x. infdist x A \<le> e}"
+ by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
+ ultimately show "compact {x. infdist x A \<le> e}"
+ by (simp add: compact_eq_bounded_closed)
+qed
+
subsection \<open>Equality of continuous functions on closure and related results.\<close>
lemma continuous_closedin_preimage_constant:
@@ -2209,6 +2294,13 @@
by (metis assms continuous_open_vimage vimage_def)
qed
+lemma open_neg_translation:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "open s"
+ shows "open((\<lambda>x. a - x) ` s)"
+ using open_translation[OF open_negations[OF assms], of a]
+ by (auto simp: image_image)
+
lemma open_affinity:
fixes S :: "'a::real_normed_vector set"
assumes "open S" "c \<noteq> 0"
@@ -2392,42 +2484,6 @@
(\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e))"
unfolding continuous_on_iff dist_norm by simp
-text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
-
-lemma distance_attains_sup:
- assumes "compact s" "s \<noteq> {}"
- shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
-proof (rule continuous_attains_sup [OF assms])
- {
- fix x
- assume "x\<in>s"
- have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
- by (intro tendsto_dist tendsto_const tendsto_ident_at)
- }
- then show "continuous_on s (dist a)"
- unfolding continuous_on ..
-qed
-
-text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
-
-lemma distance_attains_inf:
- fixes a :: "'a::heine_borel"
- assumes "closed s" and "s \<noteq> {}"
- obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
-proof -
- from assms obtain b where "b \<in> s" by auto
- let ?B = "s \<inter> cball a (dist b a)"
- have "?B \<noteq> {}" using \<open>b \<in> s\<close>
- by (auto simp: dist_commute)
- moreover have "continuous_on ?B (dist a)"
- by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
- moreover have "compact ?B"
- by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
- ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
- by (metis continuous_attains_inf)
- with that show ?thesis by fastforce
-qed
-
subsection \<open>Cartesian products\<close>
@@ -2911,6 +2967,38 @@
using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
qed
+lemma compact_in_open_separated:
+ fixes A::"'a::heine_borel set"
+ assumes "A \<noteq> {}"
+ assumes "compact A"
+ assumes "open B"
+ assumes "A \<subseteq> B"
+ obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
+proof atomize_elim
+ have "closed (- B)" "compact A" "- B \<inter> A = {}"
+ using assms by (auto simp: open_Diff compact_eq_bounded_closed)
+ from separate_closed_compact[OF this]
+ obtain d'::real where d': "d'>0" "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d' \<le> dist x y"
+ by auto
+ define d where "d = d' / 2"
+ hence "d>0" "d < d'" using d' by auto
+ with d' have d: "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d < dist x y"
+ by force
+ show "\<exists>e>0. {x. infdist x A \<le> e} \<subseteq> B"
+ proof (rule ccontr)
+ assume "\<nexists>e. 0 < e \<and> {x. infdist x A \<le> e} \<subseteq> B"
+ with \<open>d > 0\<close> obtain x where x: "infdist x A \<le> d" "x \<notin> B"
+ by auto
+ from assms have "closed A" "A \<noteq> {}" by (auto simp: compact_eq_bounded_closed)
+ from infdist_attains_inf[OF this]
+ obtain y where y: "y \<in> A" "infdist x A = dist x y"
+ by auto
+ have "dist x y \<le> d" using x y by simp
+ also have "\<dots> < dist x y" using y d x by auto
+ finally show False by simp
+ qed
+qed
+
subsection \<open>Compact sets and the closure operation.\<close>
@@ -4221,6 +4309,14 @@
using \<open>x\<in>s\<close> by blast
qed
+lemma banach_fix_type:
+ fixes f::"'a::complete_space\<Rightarrow>'a"
+ assumes c:"0 \<le> c" "c < 1"
+ and lipschitz:"\<forall>x. \<forall>y. dist (f x) (f y) \<le> c * dist x y"
+ shows "\<exists>!x. (f x = x)"
+ using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
+ by auto
+
subsection \<open>Edelstein fixed point theorem\<close>
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Feb 22 18:01:08 2018 +0100
@@ -6659,9 +6659,13 @@
subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
-lemma is_interval_1:
- "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
- unfolding is_interval_def by auto
+lemma mem_is_interval_1_I:
+ fixes a b c::real
+ assumes "is_interval S"
+ assumes "a \<in> S" "c \<in> S"
+ assumes "a \<le> b" "b \<le> c"
+ shows "b \<in> S"
+ using assms is_interval_1 by blast
lemma is_interval_connected_1:
fixes s :: "real set"
@@ -6708,6 +6712,9 @@
shows "is_interval s \<longleftrightarrow> convex s"
by (metis is_interval_convex convex_connected is_interval_connected_1)
+lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
+ by (metis connected_ball is_interval_connected_1)
+
lemma connected_compact_interval_1:
"connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
@@ -6731,6 +6738,10 @@
by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
qed
+lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
+ by (auto simp: is_interval_convex_1 convex_cball)
+
+
subsection \<open>Another intermediate value theorem formulation\<close>
lemma ivt_increasing_component_on_1:
--- a/src/HOL/Analysis/Derivative.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Derivative.thy Thu Feb 22 18:01:08 2018 +0100
@@ -48,18 +48,6 @@
shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
-text \<open>These are the only cases we'll care about, probably.\<close>
-
-lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
- bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
- unfolding has_derivative_def Lim
- by (auto simp add: netlimit_within field_simps)
-
-lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
- bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
- using has_derivative_within [of f f' x UNIV]
- by simp
-
text \<open>More explicit epsilon-delta forms.\<close>
lemma has_derivative_within':
@@ -131,27 +119,6 @@
by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
qed
-subsubsection \<open>Limit transformation for derivatives\<close>
-
-lemma has_derivative_transform_within:
- assumes "(f has_derivative f') (at x within s)"
- and "0 < d"
- and "x \<in> s"
- and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
- shows "(g has_derivative f') (at x within s)"
- using assms
- unfolding has_derivative_within
- by (force simp add: intro: Lim_transform_within)
-
-lemma has_derivative_transform_within_open:
- assumes "(f has_derivative f') (at x)"
- and "open s"
- and "x \<in> s"
- and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
- shows "(g has_derivative f') (at x)"
- using assms unfolding has_derivative_at
- by (force simp add: intro: Lim_transform_within_open)
-
subsection \<open>Differentiability\<close>
definition
@@ -304,6 +271,10 @@
unfolding differentiable_on_def
by auto
+lemma has_derivative_continuous_on:
+ "(\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
+ by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def)
+
text \<open>Results about neighborhoods filter.\<close>
lemma eventually_nhds_metric_le:
@@ -1143,6 +1114,20 @@
by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
qed
+lemma vector_differentiable_bound_linearization:
+ fixes f::"real \<Rightarrow> 'b::real_normed_vector"
+ assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
+ assumes "closed_segment a b \<subseteq> S"
+ assumes B: "\<forall>x\<in>S. norm (f' x - f' x0) \<le> B"
+ assumes "x0 \<in> S"
+ shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
+ using assms
+ by (intro differentiable_bound_linearization[of a b S f "\<lambda>x h. h *\<^sub>R f' x" x0 B])
+ (force simp: closed_segment_real_eq has_vector_derivative_def
+ scaleR_diff_right[symmetric] mult.commute[of B]
+ intro!: onorm_le mult_left_mono)+
+
+
text \<open>In particular.\<close>
lemma has_derivative_zero_constant:
@@ -1169,6 +1154,14 @@
using assms(2)[of x] by (simp add: has_field_derivative_def A)
qed fact
+lemma
+ has_vector_derivative_zero_constant:
+ assumes "convex s"
+ assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_vector_derivative 0) (at x within s)"
+ obtains c where "\<And>x. x \<in> s \<Longrightarrow> f x = c"
+ using has_derivative_zero_constant[of s f] assms
+ by (auto simp: has_vector_derivative_def)
+
lemma has_derivative_zero_unique:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "convex s"
@@ -2510,7 +2503,7 @@
apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
done
-lemma vector_derivative_within_closed_interval:
+lemma vector_derivative_within_cbox:
assumes ab: "a < b" "x \<in> cbox a b"
assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
shows "vector_derivative f (at x within cbox a b) = f'"
@@ -2518,6 +2511,14 @@
vector_derivative_works[THEN iffD1] differentiableI_vector)
fact
+lemma vector_derivative_within_closed_interval:
+ fixes f::"real \<Rightarrow> 'a::euclidean_space"
+ assumes "a < b" and "x \<in> {a .. b}"
+ assumes "(f has_vector_derivative f') (at x within {a .. b})"
+ shows "vector_derivative f (at x within {a .. b}) = f'"
+ using assms vector_derivative_within_cbox
+ by fastforce
+
lemma has_vector_derivative_within_subset:
"(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
@@ -2561,6 +2562,14 @@
unfolding has_vector_derivative_def
by (rule has_derivative_transform_within_open)
+lemma has_vector_derivative_transform:
+ assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+ assumes f': "(f has_vector_derivative f') (at x within s)"
+ shows "(g has_vector_derivative f') (at x within s)"
+ using assms
+ unfolding has_vector_derivative_def
+ by (rule has_derivative_transform)
+
lemma vector_diff_chain_at:
assumes "(f has_vector_derivative f') (at x)"
and "(g has_vector_derivative g') (at (f x))"
@@ -2589,7 +2598,7 @@
lemma vector_derivative_at_within_ivl:
"(f has_vector_derivative f') (at x) \<Longrightarrow>
a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
-using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
+ using has_vector_derivative_at_within vector_derivative_within_cbox by fastforce
lemma vector_derivative_chain_at:
assumes "f differentiable at x" "(g differentiable at (f x))"
@@ -2917,21 +2926,19 @@
qed
lemma has_derivative_partialsI:
- assumes fx: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>x. f x y) has_derivative blinfun_apply (fx x y)) (at x within X)"
+ fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
+ assumes fx: "((\<lambda>x. f x y) has_derivative fx) (at x within X)"
assumes fy: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)"
- assumes fx_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fx x y)"
- assumes fy_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fy x y)"
- assumes "x \<in> X" "y \<in> Y"
- assumes "convex X" "convex Y"
- shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx x y tx + fy x y ty)) (at (x, y) within X \<times> Y)"
+ assumes fy_cont[unfolded continuous_within]: "continuous (at (x, y) within X \<times> Y) (\<lambda>(x, y). fy x y)"
+ assumes "y \<in> Y" "convex Y"
+ shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx tx + fy x y ty)) (at (x, y) within X \<times> Y)"
proof (safe intro!: has_derivativeI tendstoI, goal_cases)
case (2 e')
+ interpret fx: bounded_linear "fx" using fx by (rule has_derivative_bounded_linear)
define e where "e = e' / 9"
have "e > 0" using \<open>e' > 0\<close> by (simp add: e_def)
- have "(x, y) \<in> X \<times> Y" using assms by auto
- from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF this,
- unfolded continuous_within, THEN tendstoD, OF \<open>e > 0\<close>]
+ from fy_cont[THEN tendstoD, OF \<open>e > 0\<close>]
have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. dist (fy x' y') (fy x y) < e"
by (auto simp: split_beta')
from this[unfolded eventually_at] obtain d' where
@@ -2971,12 +2978,12 @@
} note onorm = this
have ev_mem: "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. (x', y') \<in> X \<times> Y"
- using \<open>x \<in> X\<close> \<open>y \<in> Y\<close>
+ using \<open>y \<in> Y\<close>
by (auto simp: eventually_at intro!: zero_less_one)
moreover
have ev_dist: "\<forall>\<^sub>F xy in at (x, y) within X \<times> Y. dist xy (x, y) < d" if "d > 0" for d
using eventually_at_ball[OF that]
- by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True)
+ by (rule eventually_elim2) (auto simp: dist_commute mem_ball intro!: eventually_True)
note ev_dist[OF \<open>0 < d\<close>]
ultimately
have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
@@ -2997,32 +3004,31 @@
have "\<dots> \<subseteq> ball y d \<inter> Y"
using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
- (auto simp: dist_commute)
+ (auto simp: dist_commute mem_ball)
finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
} note seg = this
have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
- by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
+ by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: mem_ball dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
by (rule differentiable_bound_linearization[where S="?S"])
(auto intro!: \<open>0 < d\<close> \<open>y \<in> Y\<close>)
qed
moreover
- let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx x y) (x' - x)) \<le> norm (x' - x) * e"
- from fx[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
+ let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
+ from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
have "\<forall>\<^sub>F x' in at x within X. ?le x'"
by eventually_elim
- (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
+ (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps fx.zero split: if_split_asm)
then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
by (rule eventually_at_Pair_within_TimesI1)
- (simp add: blinfun.bilinear_simps)
+ (simp add: blinfun.bilinear_simps fx.zero)
moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
unfolding norm_eq_zero right_minus_eq
by (auto simp: eventually_at intro!: zero_less_one)
moreover
- from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF SigmaI[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>],
- unfolded continuous_within, THEN tendstoD, OF \<open>0 < e\<close>]
+ from fy_cont[THEN tendstoD, OF \<open>0 < e\<close>]
have "\<forall>\<^sub>F x' in at x within X. norm (fy x' y - fy x y) < e"
unfolding eventually_at
using \<open>y \<in> Y\<close>
@@ -3032,22 +3038,22 @@
(simp add: blinfun.bilinear_simps \<open>0 < e\<close>)
ultimately
have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
- norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R
+ norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R
norm ((x', y') - (x, y)))
< e'"
apply eventually_elim
proof safe
fix x' y'
- have "norm (f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) \<le>
+ have "norm (f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) \<le>
norm (f x' y' - f x' y - fy x' y (y' - y)) +
norm (fy x y (y' - y) - fy x' y (y' - y)) +
- norm (f x' y - f x y - fx x y (x' - x))"
+ norm (f x' y - f x y - fx (x' - x))"
by norm
also
assume nz: "norm ((x', y') - (x, y)) \<noteq> 0"
and nfy: "norm (fy x' y - fy x y) < e"
assume "norm (f x' y' - f x' y - blinfun_apply (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
- also assume "norm (f x' y - f x y - blinfun_apply (fx x y) (x' - x)) \<le> norm (x' - x) * e"
+ also assume "norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
also
have "norm ((fy x y) (y' - y) - (fy x' y) (y' - y)) \<le> norm ((fy x y) - (fy x' y)) * norm (y' - y)"
by (auto simp: blinfun.bilinear_simps[symmetric] intro!: norm_blinfun)
@@ -3070,11 +3076,80 @@
also have "\<dots> < norm ((x', y') - (x, y)) * e'"
using \<open>0 < e'\<close> nz
by (auto simp: e_def)
- finally show "norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
+ finally show "norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
by (auto simp: divide_simps dist_norm mult.commute)
qed
then show ?case
by eventually_elim (auto simp: dist_norm field_simps)
-qed (auto intro!: bounded_linear_intros simp: split_beta')
+next
+ from has_derivative_bounded_linear[OF fx]
+ obtain fxb where "fx = blinfun_apply fxb"
+ by (metis bounded_linear_Blinfun_apply)
+ then show "bounded_linear (\<lambda>(tx, ty). fx tx + blinfun_apply (fy x y) ty)"
+ by (auto intro!: bounded_linear_intros simp: split_beta')
+qed
+
+
+subsection \<open>Differentiable case distinction\<close>
+
+lemma has_derivative_within_If_eq:
+ "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
+ (bounded_linear f' \<and>
+ ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)
+ else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
+ \<longlongrightarrow> 0) (at x within s))"
+ (is "_ = (_ \<and> (?if \<longlongrightarrow> 0) _)")
+proof -
+ have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
+ ((if P y then f y else g y) -
+ ((if P x then f x else g x) + f' (y - x)))) = ?if"
+ by (auto simp: inverse_eq_divide)
+ thus ?thesis by (auto simp: has_derivative_within)
+qed
+
+lemma has_derivative_If_within_closures:
+ assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
+ assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
+ assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
+ assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
+ assumes x_in: "x \<in> s \<union> t"
+ shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative
+ (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
+proof -
+ from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)"
+ by (auto simp add: has_derivative_within)
+ from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)"
+ by (auto simp add: has_derivative_within)
+ have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
+ using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in
+ by (unfold_locales; force)
+ show ?thesis
+ using f' g' closure_subset[of t] closure_subset[of s]
+ unfolding has_derivative_within_If_eq
+ by (intro conjI bl tendsto_If_within_closures x_in)
+ (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
+qed
+
+lemma has_vector_derivative_If_within_closures:
+ assumes x_in: "x \<in> s \<union> t"
+ assumes "u = s \<union> t"
+ assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
+ assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
+ assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
+ assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
+ shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative
+ (if x \<in> s then f' x else g' x)) (at x within u)"
+ unfolding has_vector_derivative_def assms
+ using x_in
+ apply (intro has_derivative_If_within_closures[where
+ ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
+ THEN has_derivative_eq_rhs])
+ subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
+ subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
+ by (auto simp: assms)
end
--- a/src/HOL/Analysis/Euclidean_Space.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Euclidean_Space.thy Thu Feb 22 18:01:08 2018 +0100
@@ -84,6 +84,10 @@
lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
unfolding euclidean_representation_sum by simp
+lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (inner x b) * (inner y b))"
+ by (subst (1 2) euclidean_representation [symmetric])
+ (simp add: inner_sum_right inner_Basis ac_simps)
+
lemma (in euclidean_space) choice_Basis_iff:
fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Feb 22 18:01:08 2018 +0100
@@ -20,9 +20,19 @@
declare vec_lambda_inject [simplified, simp]
+bundle vec_syntax begin
notation
vec_nth (infixl "$" 90) and
vec_lambda (binder "\<chi>" 10)
+end
+
+bundle no_vec_syntax begin
+no_notation
+ vec_nth (infixl "$" 90) and
+ vec_lambda (binder "\<chi>" 10)
+end
+
+unbundle vec_syntax
(*
Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Feb 22 18:01:08 2018 +0100
@@ -621,6 +621,11 @@
with False show ?thesis by (simp add: not_integrable_integral)
qed
+lemma integral_mult:
+ fixes K::real
+ shows "f integrable_on X \<Longrightarrow> K * integral X f = integral X (\<lambda>x. K * f x)"
+ unfolding real_scaleR_def[symmetric] integral_cmul ..
+
lemma integral_neg [simp]: "integral S (\<lambda>x. - f x) = - integral S f"
proof (cases "f integrable_on S")
case True then show ?thesis
@@ -2549,6 +2554,13 @@
lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real]
+lemma integrable_continuous_closed_segment:
+ fixes f :: "real \<Rightarrow> 'a::banach"
+ assumes "continuous_on (closed_segment a b) f"
+ shows "f integrable_on (closed_segment a b)"
+ using assms
+ by (auto intro!: integrable_continuous_interval simp: closed_segment_eq_real_ivl)
+
subsection \<open>Specialization of additivity to one dimension.\<close>
@@ -2722,6 +2734,32 @@
subsection \<open>Taylor series expansion\<close>
+lemma mvt_integral:
+ fixes f::"'a::real_normed_vector\<Rightarrow>'b::banach"
+ assumes f'[derivative_intros]:
+ "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
+ assumes line_in: "\<And>t. t \<in> {0..1} \<Longrightarrow> x + t *\<^sub>R y \<in> S"
+ shows "f (x + y) - f x = integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) y)" (is ?th1)
+proof -
+ from assms have subset: "(\<lambda>xa. x + xa *\<^sub>R y) ` {0..1} \<subseteq> S" by auto
+ note [derivative_intros] =
+ has_derivative_subset[OF _ subset]
+ has_derivative_in_compose[where f="(\<lambda>xa. x + xa *\<^sub>R y)" and g = f]
+ note [continuous_intros] =
+ continuous_on_compose2[where f="(\<lambda>xa. x + xa *\<^sub>R y)"]
+ continuous_on_subset[OF _ subset]
+ have "\<And>t. t \<in> {0..1} \<Longrightarrow>
+ ((\<lambda>t. f (x + t *\<^sub>R y)) has_vector_derivative f' (x + t *\<^sub>R y) y)
+ (at t within {0..1})"
+ using assms
+ by (auto simp: has_vector_derivative_def
+ linear_cmul[OF has_derivative_linear[OF f'], symmetric]
+ intro!: derivative_eq_intros)
+ from fundamental_theorem_of_calculus[rule_format, OF _ this]
+ show ?th1
+ by (auto intro!: integral_unique[symmetric])
+qed
+
lemma (in bounded_bilinear) sum_prod_derivatives_has_vector_derivative:
assumes "p>0"
and f0: "Df 0 = f"
@@ -2835,7 +2873,6 @@
qed
-
subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
proposition division_of_nontrivial:
@@ -3024,6 +3061,21 @@
unfolding integrable_on_def
by (auto intro!: has_integral_combine)
+lemma integral_minus_sets:
+ fixes f::"real \<Rightarrow> 'a::banach"
+ shows "c \<le> a \<Longrightarrow> c \<le> b \<Longrightarrow> f integrable_on {c .. max a b} \<Longrightarrow>
+ integral {c .. a} f - integral {c .. b} f =
+ (if a \<le> b then - integral {a .. b} f else integral {b .. a} f)"
+ using integral_combine[of c a b f] integral_combine[of c b a f]
+ by (auto simp: algebra_simps max_def)
+
+lemma integral_minus_sets':
+ fixes f::"real \<Rightarrow> 'a::banach"
+ shows "c \<ge> a \<Longrightarrow> c \<ge> b \<Longrightarrow> f integrable_on {min a b .. c} \<Longrightarrow>
+ integral {a .. c} f - integral {b .. c} f =
+ (if a \<le> b then integral {a .. b} f else - integral {b .. a} f)"
+ using integral_combine[of b a c f] integral_combine[of a b c f]
+ by (auto simp: algebra_simps min_def)
subsection \<open>Reduce integrability to "local" integrability.\<close>
@@ -3129,13 +3181,19 @@
using assms integral_has_vector_derivative_continuous_at [OF integrable_continuous_real]
by (fastforce simp: continuous_on_eq_continuous_within)
+lemma integral_has_real_derivative:
+ assumes "continuous_on {a..b} g"
+ assumes "t \<in> {a..b}"
+ shows "((\<lambda>x. integral {a..x} g) has_real_derivative g t) (at t within {a..b})"
+ using integral_has_vector_derivative[of a b g t] assms
+ by (auto simp: has_field_derivative_iff_has_vector_derivative)
+
lemma antiderivative_continuous:
fixes q b :: real
assumes "continuous_on {a..b} f"
obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
using integral_has_vector_derivative[OF assms] by auto
-
subsection \<open>Combined fundamental theorem of calculus.\<close>
lemma antiderivative_integral_continuous:
@@ -3149,7 +3207,8 @@
have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
proof -
have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
- by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
+ by (metis atLeastAtMost_iff atLeastatMost_subset_iff box_real(2) g
+ has_vector_derivative_within_subset subsetCE that(1,2))
then show ?thesis
by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
qed
@@ -4125,6 +4184,28 @@
by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous_1 assms)
qed
+theorem integral_has_vector_derivative':
+ fixes f :: "real \<Rightarrow> 'b::banach"
+ assumes "continuous_on {a..b} f"
+ and "x \<in> {a..b}"
+ shows "((\<lambda>u. integral {u..b} f) has_vector_derivative - f x) (at x within {a..b})"
+proof -
+ have *: "integral {x..b} f = integral {a .. b} f - integral {a .. x} f" if "a \<le> x" "x \<le> b" for x
+ using integral_combine[of a x b for x, OF that integrable_continuous_real[OF assms(1)]]
+ by (simp add: algebra_simps)
+ show ?thesis
+ using \<open>x \<in> _\<close> *
+ by (rule has_vector_derivative_transform)
+ (auto intro!: derivative_eq_intros assms integral_has_vector_derivative)
+qed
+
+lemma integral_has_real_derivative':
+ assumes "continuous_on {a..b} g"
+ assumes "t \<in> {a..b}"
+ shows "((\<lambda>x. integral {x..b} g) has_real_derivative -g t) (at t within {a..b})"
+ using integral_has_vector_derivative'[OF assms]
+ by (auto simp: has_field_derivative_iff_has_vector_derivative)
+
subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
@@ -4661,6 +4742,10 @@
shows "f integrable_on S \<longleftrightarrow> f integrable_on T"
by (blast intro: integrable_spike_set assms negligible_subset)
+lemma integrable_on_insert_iff: "f integrable_on (insert x X) \<longleftrightarrow> f integrable_on X"
+ for f::"_ \<Rightarrow> 'a::banach"
+ by (rule integrable_spike_set_eq) (auto simp: insert_Diff_if)
+
lemma has_integral_interior:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
@@ -6049,6 +6134,26 @@
qed
qed
+lemma continuous_on_imp_absolutely_integrable_on:
+ fixes f::"real \<Rightarrow> 'a::banach"
+ shows "continuous_on {a..b} f \<Longrightarrow>
+ norm (integral {a..b} f) \<le> integral {a..b} (\<lambda>x. norm (f x))"
+ by (intro integral_norm_bound_integral integrable_continuous_real continuous_on_norm) auto
+
+lemma integral_bound:
+ fixes f::"real \<Rightarrow> 'a::banach"
+ assumes "a \<le> b"
+ assumes "continuous_on {a .. b} f"
+ assumes "\<And>t. t \<in> {a .. b} \<Longrightarrow> norm (f t) \<le> B"
+ shows "norm (integral {a .. b} f) \<le> B * (b - a)"
+proof -
+ note continuous_on_imp_absolutely_integrable_on[OF assms(2)]
+ also have "integral {a..b} (\<lambda>x. norm (f x)) \<le> integral {a..b} (\<lambda>_. B)"
+ by (rule integral_le)
+ (auto intro!: integrable_continuous_real continuous_intros assms)
+ also have "\<dots> = B * (b - a)" using assms by simp
+ finally show ?thesis .
+qed
lemma integral_norm_bound_integral_component:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
--- a/src/HOL/Analysis/L2_Norm.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/L2_Norm.thy Thu Feb 22 18:01:08 2018 +0100
@@ -98,13 +98,6 @@
qed
qed
-lemma sqrt_sum_squares_le_sum:
- "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
- apply (rule power2_le_imp_le)
- apply (simp add: power2_sum)
- apply simp
- done
-
lemma L2_set_le_sum [rule_format]:
"(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
apply (cases "finite A")
--- a/src/HOL/Analysis/Linear_Algebra.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Feb 22 18:01:08 2018 +0100
@@ -2987,10 +2987,6 @@
lemma infnorm_le_norm: "infnorm x \<le> norm x"
by (simp add: Basis_le_norm infnorm_Max)
-lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
- by (subst (1 2) euclidean_representation [symmetric])
- (simp add: inner_sum_right inner_Basis ac_simps)
-
lemma norm_le_infnorm:
fixes x :: "'a::euclidean_space"
shows "norm x \<le> sqrt DIM('a) * infnorm x"
--- a/src/HOL/Analysis/Operator_Norm.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Operator_Norm.thy Thu Feb 22 18:01:08 2018 +0100
@@ -235,4 +235,13 @@
shows "onorm (\<lambda>x. f x + g x) < e"
using assms by (rule onorm_triangle [THEN order_le_less_trans])
+lemma onorm_sum:
+ assumes "finite S"
+ assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
+ shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
+ using assms
+ by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
+
+lemmas onorm_sum_le = onorm_sum[THEN order_trans]
+
end
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Feb 22 18:01:08 2018 +0100
@@ -214,9 +214,20 @@
using image_smult_cbox[of m a b]
by (simp add: cbox_interval)
-lemma is_interval_closed_interval [simp]:
- "is_interval {a .. (b::'a::ordered_euclidean_space)}"
- by (metis cbox_interval is_interval_cbox)
+lemma [simp]:
+ fixes a b::"'a::ordered_euclidean_space" and r s::real
+ shows is_interval_io: "is_interval {..<r}"
+ and is_interval_ic: "is_interval {..a}"
+ and is_interval_oi: "is_interval {r<..}"
+ and is_interval_ci: "is_interval {a..}"
+ and is_interval_oo: "is_interval {r<..<s}"
+ and is_interval_oc: "is_interval {r<..s}"
+ and is_interval_co: "is_interval {r..<s}"
+ and is_interval_cc: "is_interval {b..a}"
+ by (force simp: is_interval_def eucl_le[where 'a='a])+
+
+lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
+ by (auto simp: real_atLeastGreaterThan_eq)
lemma compact_interval [simp]:
fixes a b::"'a::ordered_euclidean_space"
--- a/src/HOL/Analysis/Product_Vector.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Product_Vector.thy Thu Feb 22 18:01:08 2018 +0100
@@ -306,6 +306,11 @@
by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
qed simp
+lemma differentiable_Pair [simp, derivative_intros]:
+ "f differentiable at x within s \<Longrightarrow> g differentiable at x within s \<Longrightarrow>
+ (\<lambda>x. (f x, g x)) differentiable at x within s"
+ unfolding differentiable_def by (blast intro: has_derivative_Pair)
+
lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
@@ -313,6 +318,17 @@
"((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
unfolding split_beta' .
+
+subsubsection \<open>Vector derivatives involving pairs\<close>
+
+lemma has_vector_derivative_Pair[derivative_intros]:
+ assumes "(f has_vector_derivative f') (at x within s)"
+ "(g has_vector_derivative g') (at x within s)"
+ shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
+ using assms
+ by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
+
+
subsection \<open>Product is an inner product space\<close>
instantiation prod :: (real_inner, real_inner) real_inner
@@ -368,4 +384,9 @@
lemma norm_snd_le: "norm y \<le> norm (x,y)"
by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
+lemma norm_Pair_le:
+ shows "norm (x, y) \<le> norm x + norm y"
+ unfolding norm_Pair
+ by (metis norm_ge_zero sqrt_sum_squares_le_sum)
+
end
--- a/src/HOL/Analysis/Riemann_Mapping.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Thu Feb 22 18:01:08 2018 +0100
@@ -489,7 +489,7 @@
let ?g = "\<lambda>z. (SOME g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = a \<and> pathfinish g = z)"
show "((\<lambda>z. contour_integral (?g z) f) has_field_derivative f x)
(at x)"
- proof (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right, rule Lim_transform)
+ proof (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right, rule Lim_transform)
show "(\<lambda>y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \<midarrow>x\<rightarrow> 0"
proof (clarsimp simp add: Lim_at)
fix e::real assume "e > 0"
--- a/src/HOL/Analysis/Starlike.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy Thu Feb 22 18:01:08 2018 +0100
@@ -13,9 +13,87 @@
begin
+subsection \<open>Midpoint\<close>
+
definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
+lemma midpoint_idem [simp]: "midpoint x x = x"
+ unfolding midpoint_def
+ unfolding scaleR_right_distrib
+ unfolding scaleR_left_distrib[symmetric]
+ by auto
+
+lemma midpoint_sym: "midpoint a b = midpoint b a"
+ unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
+
+lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
+proof -
+ have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
+ by simp
+ then show ?thesis
+ unfolding midpoint_def scaleR_2 [symmetric] by simp
+qed
+
+lemma
+ fixes a::real
+ assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
+ and le_midpoint_1: "midpoint a b \<le> b"
+ by (simp_all add: midpoint_def assms)
+
+lemma dist_midpoint:
+ fixes a b :: "'a::real_normed_vector" shows
+ "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
+ "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
+ "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
+ "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
+proof -
+ have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
+ unfolding equation_minus_iff by auto
+ have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2"
+ by auto
+ note scaleR_right_distrib [simp]
+ show ?t1
+ unfolding midpoint_def dist_norm
+ apply (rule **)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t2
+ unfolding midpoint_def dist_norm
+ apply (rule *)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t3
+ unfolding midpoint_def dist_norm
+ apply (rule *)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+ show ?t4
+ unfolding midpoint_def dist_norm
+ apply (rule **)
+ apply (simp add: scaleR_right_diff_distrib)
+ apply (simp add: scaleR_2)
+ done
+qed
+
+lemma midpoint_eq_endpoint [simp]:
+ "midpoint a b = a \<longleftrightarrow> a = b"
+ "midpoint a b = b \<longleftrightarrow> a = b"
+ unfolding midpoint_eq_iff by auto
+
+lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
+ using midpoint_eq_iff by metis
+
+lemma midpoint_linear_image:
+ "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
+by (simp add: linear_iff midpoint_def)
+
+
+subsection \<open>Line segments\<close>
+
definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
@@ -106,86 +184,6 @@
apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
using of_real_eq_iff by fastforce
-lemma midpoint_idem [simp]: "midpoint x x = x"
- unfolding midpoint_def
- unfolding scaleR_right_distrib
- unfolding scaleR_left_distrib[symmetric]
- by auto
-
-lemma midpoint_sym: "midpoint a b = midpoint b a"
- unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
-
-lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
-proof -
- have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
- by simp
- then show ?thesis
- unfolding midpoint_def scaleR_2 [symmetric] by simp
-qed
-
-lemma
- fixes a::real
- assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
- and le_midpoint_1: "midpoint a b \<le> b"
- by (simp_all add: midpoint_def assms)
-
-lemma dist_midpoint:
- fixes a b :: "'a::real_normed_vector" shows
- "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
- "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
- "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
- "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
-proof -
- have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
- unfolding equation_minus_iff by auto
- have **: "\<And>x y::'a. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2"
- by auto
- note scaleR_right_distrib [simp]
- show ?t1
- unfolding midpoint_def dist_norm
- apply (rule **)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t2
- unfolding midpoint_def dist_norm
- apply (rule *)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t3
- unfolding midpoint_def dist_norm
- apply (rule *)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
- show ?t4
- unfolding midpoint_def dist_norm
- apply (rule **)
- apply (simp add: scaleR_right_diff_distrib)
- apply (simp add: scaleR_2)
- done
-qed
-
-lemma midpoint_eq_endpoint [simp]:
- "midpoint a b = a \<longleftrightarrow> a = b"
- "midpoint a b = b \<longleftrightarrow> a = b"
- unfolding midpoint_eq_iff by auto
-
-lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
- using midpoint_eq_iff by metis
-
-lemma midpoint_linear_image:
- "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
-by (simp add: linear_iff midpoint_def)
-
-subsection\<open>Starlike sets\<close>
-
-definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
-
-lemma starlike_UNIV [simp]: "starlike UNIV"
- by (simp add: starlike_def)
-
lemma convex_contains_segment:
"convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
unfolding convex_alt closed_segment_def by auto
@@ -197,10 +195,6 @@
"\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
using convex_contains_segment by blast
-lemma convex_imp_starlike:
- "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
- unfolding convex_contains_segment starlike_def by auto
-
lemma segment_convex_hull:
"closed_segment a b = convex hull {a,b}"
proof -
@@ -349,7 +343,7 @@
proof -
have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
using \<open>u \<le> 1\<close> by force
- then show ?thesis
+ then show ?thesis
by (simp add: dist_norm real_vector.scale_right_diff_distrib)
qed
also have "... \<le> dist a b"
@@ -581,7 +575,6 @@
by (metis image_comp convex_translation)
qed
-
lemmas convex_segment = convex_closed_segment convex_open_segment
lemma connected_segment [iff]:
@@ -589,6 +582,33 @@
shows "connected (closed_segment x y)"
by (simp add: convex_connected)
+lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
+ by (auto simp: is_interval_convex_1)
+
+lemma IVT'_closed_segment_real:
+ fixes f :: "real \<Rightarrow> real"
+ assumes "y \<in> closed_segment (f a) (f b)"
+ assumes "continuous_on (closed_segment a b) f"
+ shows "\<exists>x \<in> closed_segment a b. f x = y"
+ using IVT'[of f a y b]
+ IVT'[of "-f" a "-y" b]
+ IVT'[of f b y a]
+ IVT'[of "-f" b "-y" a] assms
+ by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
+
+
+subsection\<open>Starlike sets\<close>
+
+definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
+
+lemma starlike_UNIV [simp]: "starlike UNIV"
+ by (simp add: starlike_def)
+
+lemma convex_imp_starlike:
+ "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
+ unfolding convex_contains_segment starlike_def by auto
+
+
lemma affine_hull_closed_segment [simp]:
"affine hull (closed_segment a b) = affine hull {a,b}"
by (simp add: segment_convex_hull)
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Feb 22 18:01:08 2018 +0100
@@ -7,7 +7,7 @@
section \<open>Elementary topology in Euclidean space.\<close>
theory Topology_Euclidean_Space
-imports
+imports
"HOL-Library.Indicator_Function"
"HOL-Library.Countable_Set"
"HOL-Library.FuncSet"
@@ -1112,6 +1112,9 @@
lemma ball_subset_cball [simp, intro]: "ball x e \<subseteq> cball x e"
by (simp add: subset_eq)
+lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
+ by (auto simp: mem_ball mem_cball)
+
lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
by force
@@ -1124,6 +1127,22 @@
lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
by (simp add: subset_eq)
+lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
+ by (auto simp: mem_ball mem_cball)
+
+lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
+ by (auto simp: mem_ball mem_cball)
+
+lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
+ unfolding mem_cball
+proof -
+ have "dist z x \<le> dist z y + dist y x"
+ by (rule dist_triangle)
+ also assume "dist z y \<le> b"
+ also assume "dist y x \<le> a"
+ finally show "dist z x \<le> b + a" by arith
+qed
+
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
by (simp add: set_eq_iff) arith
@@ -1253,6 +1272,17 @@
unfolding dist_norm norm_eq_sqrt_inner L2_set_def
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
+lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
+proof -
+ have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
+ by simp
+ also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
+ by (intro sum_mono2) (auto simp: that)
+ finally show ?thesis
+ unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
+ by (auto intro!: real_le_rsqrt)
+qed
+
lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
by (rule eventually_nhds_in_open) simp_all
@@ -1262,6 +1292,20 @@
lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
+lemma at_within_ball: "e > 0 \<Longrightarrow> dist x y < e \<Longrightarrow> at y within ball x e = at y"
+ by (subst at_within_open) auto
+
+lemma atLeastAtMost_eq_cball:
+ fixes a b::real
+ shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
+ by (auto simp: dist_real_def field_simps mem_cball)
+
+lemma greaterThanLessThan_eq_ball:
+ fixes a b::real
+ shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
+ by (auto simp: dist_real_def field_simps mem_ball)
+
+
subsection \<open>Boxes\<close>
abbreviation One :: "'a::euclidean_space"
@@ -1834,6 +1878,14 @@
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
+lemma is_interval_1:
+ "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
+ unfolding is_interval_def by auto
+
+lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
+ unfolding is_interval_def
+ by blast
+
lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
@@ -1916,6 +1968,88 @@
by blast
qed
+lemma is_real_interval_union:
+ "is_interval (X \<union> Y)"
+ if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
+ for X Y::"real set"
+proof -
+ consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
+ then show ?thesis
+ proof cases
+ case 1
+ then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
+ by blast
+ then show ?thesis
+ using I 1 X Y unfolding is_interval_1
+ by (metis (full_types) Un_iff le_cases)
+ qed (use that in auto)
+qed
+
+lemma is_interval_translationI:
+ assumes "is_interval X"
+ shows "is_interval ((+) x ` X)"
+ unfolding is_interval_def
+proof safe
+ fix b d e
+ assume "b \<in> X" "d \<in> X"
+ "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
+ (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
+ hence "e - x \<in> X"
+ by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
+ (auto simp: algebra_simps)
+ thus "e \<in> (+) x ` X" by force
+qed
+
+lemma is_interval_uminusI:
+ assumes "is_interval X"
+ shows "is_interval (uminus ` X)"
+ unfolding is_interval_def
+proof safe
+ fix b d e
+ assume "b \<in> X" "d \<in> X"
+ "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
+ (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
+ hence "- e \<in> X"
+ by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
+ (auto simp: algebra_simps)
+ thus "e \<in> uminus ` X" by force
+qed
+
+lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
+ using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
+ by (auto simp: image_image)
+
+lemma is_interval_neg_translationI:
+ assumes "is_interval X"
+ shows "is_interval ((-) x ` X)"
+proof -
+ have "(-) x ` X = (+) x ` uminus ` X"
+ by (force simp: algebra_simps)
+ also have "is_interval \<dots>"
+ by (metis is_interval_uminusI is_interval_translationI assms)
+ finally show ?thesis .
+qed
+
+lemma is_interval_translation[simp]:
+ "is_interval ((+) x ` X) = is_interval X"
+ using is_interval_neg_translationI[of "(+) x ` X" x]
+ by (auto intro!: is_interval_translationI simp: image_image)
+
+lemma is_interval_minus_translation[simp]:
+ shows "is_interval ((-) x ` X) = is_interval X"
+proof -
+ have "(-) x ` X = (+) x ` uminus ` X"
+ by (force simp: algebra_simps)
+ also have "is_interval \<dots> = is_interval X"
+ by simp
+ finally show ?thesis .
+qed
+
+lemma is_interval_minus_translation'[simp]:
+ shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
+ using is_interval_translation[of "-c" X]
+ by (metis image_cong uminus_add_conv_diff)
+
subsection \<open>Limit points\<close>
@@ -2629,6 +2763,15 @@
lemma not_trivial_limit_within: "\<not> trivial_limit (at x within S) = (x \<in> closure (S - {x}))"
using islimpt_in_closure by (metis trivial_limit_within)
+lemma not_in_closure_trivial_limitI:
+ "x \<notin> closure s \<Longrightarrow> trivial_limit (at x within s)"
+ using not_trivial_limit_within[of x s]
+ by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)
+
+lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
+ if "x \<in> closure s \<Longrightarrow> filterlim f l (at x within s)"
+ by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)
+
lemma at_within_eq_bot_iff: "at c within A = bot \<longleftrightarrow> c \<notin> closure (A - {c})"
using not_trivial_limit_within[of c A] by blast
@@ -3229,6 +3372,28 @@
qed
qed
+lemma tendsto_If_within_closures:
+ assumes f: "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (f \<longlongrightarrow> l x) (at x within s \<union> (closure s \<inter> closure t))"
+ assumes g: "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+ (g \<longlongrightarrow> l x) (at x within t \<union> (closure s \<inter> closure t))"
+ assumes "x \<in> s \<union> t"
+ shows "((\<lambda>x. if x \<in> s then f x else g x) \<longlongrightarrow> l x) (at x within s \<union> t)"
+proof -
+ have *: "(s \<union> t) \<inter> {x. x \<in> s} = s" "(s \<union> t) \<inter> {x. x \<notin> s} = t - s"
+ by auto
+ have "(f \<longlongrightarrow> l x) (at x within s)"
+ by (rule filterlim_at_within_closure_implies_filterlim)
+ (use \<open>x \<in> _\<close> in \<open>auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\<close>)
+ moreover
+ have "(g \<longlongrightarrow> l x) (at x within t - s)"
+ by (rule filterlim_at_within_closure_implies_filterlim)
+ (use \<open>x \<in> _\<close> in
+ \<open>auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\<close>)
+ ultimately show ?thesis
+ by (intro filterlim_at_within_If) (simp_all only: *)
+qed
+
subsection \<open>Boundedness\<close>
--- a/src/HOL/Analysis/Uniform_Limit.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy Thu Feb 22 18:01:08 2018 +0100
@@ -438,6 +438,7 @@
bounded_linear.uniform_limit[OF bounded_linear_mult_right]
bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
+
lemmas uniform_limit_uminus[uniform_limit_intros] =
bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
@@ -728,5 +729,7 @@
apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
using sm sums_unique by fastforce
+lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
+
end
--- a/src/HOL/Deriv.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Deriv.thy Thu Feb 22 18:01:08 2018 +0100
@@ -26,6 +26,13 @@
most cases @{term s} is either a variable or @{term UNIV}.
\<close>
+text \<open>These are the only cases we'll care about, probably.\<close>
+
+lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
+ bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
+ unfolding has_derivative_def tendsto_iff
+ by (subst eventually_Lim_ident_at) (auto simp add: field_simps)
+
lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
by simp
@@ -189,6 +196,52 @@
lemmas has_derivative_within_subset = has_derivative_subset
+lemma has_derivative_within_singleton_iff:
+ "(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g"
+ by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear)
+
+
+subsubsection \<open>Limit transformation for derivatives\<close>
+
+lemma has_derivative_transform_within:
+ assumes "(f has_derivative f') (at x within s)"
+ and "0 < d"
+ and "x \<in> s"
+ and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
+ shows "(g has_derivative f') (at x within s)"
+ using assms
+ unfolding has_derivative_within
+ by (force simp add: intro: Lim_transform_within)
+
+lemma has_derivative_transform_within_open:
+ assumes "(f has_derivative f') (at x within t)"
+ and "open s"
+ and "x \<in> s"
+ and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
+ shows "(g has_derivative f') (at x within t)"
+ using assms unfolding has_derivative_within
+ by (force simp add: intro: Lim_transform_within_open)
+
+lemma has_derivative_transform:
+ assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+ assumes "(f has_derivative f') (at x within s)"
+ shows "(g has_derivative f') (at x within s)"
+ using assms
+ by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto
+
+lemma has_derivative_transform_eventually:
+ assumes "(f has_derivative f') (at x within s)"
+ "(\<forall>\<^sub>F x' in at x within s. f x' = g x')"
+ assumes "f x = g x" "x \<in> s"
+ shows "(g has_derivative f') (at x within s)"
+ using assms
+proof -
+ from assms(2,3) obtain d where "d > 0" "\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'"
+ by (force simp: eventually_at)
+ from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)]
+ show ?thesis .
+qed
+
subsection \<open>Continuity\<close>
@@ -295,6 +348,14 @@
((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
by (blast intro: has_derivative_in_compose has_derivative_subset)
+lemma has_derivative_in_compose2:
+ assumes "\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)"
+ assumes "f ` s \<subseteq> t" "x \<in> s"
+ assumes "(f has_derivative f') (at x within s)"
+ shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)"
+ using assms
+ by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g])
+
lemma (in bounded_bilinear) FDERIV:
assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)"
@@ -467,6 +528,10 @@
all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>.
\<close>
+lemma has_derivative_at2: "(f has_derivative f') (at x) \<longleftrightarrow>
+ bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
+ using has_derivative_within [of f f' x UNIV]
+ by simp
lemma has_derivative_zero_unique:
assumes "((\<lambda>x. 0) has_derivative F) (at x)"
shows "F = (\<lambda>h. 0)"
@@ -542,10 +607,19 @@
(\<lambda>x. f (g x)) differentiable (at x within s)"
by (blast intro: differentiable_in_compose differentiable_subset)
-lemma differentiable_sum [simp, derivative_intros]:
+lemma differentiable_add [simp, derivative_intros]:
"f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_add)
+lemma differentiable_sum[simp, derivative_intros]:
+ assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
+ shows "(\<lambda>x. sum (\<lambda>a. f a x) s) differentiable net"
+proof -
+ from bchoice[OF assms(2)[unfolded differentiable_def]]
+ show ?thesis
+ by (auto intro!: has_derivative_sum simp: differentiable_def)
+qed
+
lemma differentiable_minus [simp, derivative_intros]:
"f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
unfolding differentiable_def by (blast intro: has_derivative_minus)
@@ -651,6 +725,14 @@
for c :: "'a::ab_semigroup_mult"
by (simp add: fun_eq_iff mult.commute)
+lemma DERIV_compose_FDERIV:
+ fixes f::"real\<Rightarrow>real"
+ assumes "DERIV f (g x) :> f'"
+ assumes "(g has_derivative g') (at x within s)"
+ shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
+ using assms has_derivative_compose[of g g' x s f "( * ) f'"]
+ by (auto simp: has_field_derivative_def ac_simps)
+
subsection \<open>Vector derivative\<close>
@@ -998,6 +1080,8 @@
by eventually_elim auto
qed
+lemmas has_derivative_floor[derivative_intros] =
+ floor_has_real_derivative[THEN DERIV_compose_FDERIV]
text \<open>Caratheodory formulation of derivative at a point\<close>
--- a/src/HOL/Library/Extended_Real.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Library/Extended_Real.thy Thu Feb 22 18:01:08 2018 +0100
@@ -1800,8 +1800,176 @@
lemma max_MInf2 [simp]: "max x (-\<infinity>::ereal) = x"
by (metis max_bot2 bot_ereal_def)
-
-subsubsection "Topological space"
+subsection \<open>Extended real intervals\<close>
+
+lemma real_greaterThanLessThan_infinity_eq:
+ "real_of_ereal ` {N::ereal<..<\<infinity>} =
+ (if N = \<infinity> then {} else if N = -\<infinity> then UNIV else {real_of_ereal N<..})"
+proof -
+ {
+ fix x::real
+ have "x \<in> real_of_ereal ` {- \<infinity><..<\<infinity>::ereal}"
+ by (auto intro!: image_eqI[where x="ereal x"])
+ } moreover {
+ fix x::ereal
+ assume "N \<noteq> - \<infinity>" "N < x" "x \<noteq> \<infinity>"
+ then have "real_of_ereal N < real_of_ereal x"
+ by (cases N; cases x; simp)
+ } moreover {
+ fix x::real
+ assume "N \<noteq> \<infinity>" "real_of_ereal N < x"
+ then have "x \<in> real_of_ereal ` {N<..<\<infinity>}"
+ by (cases N) (auto intro!: image_eqI[where x="ereal x"])
+ } ultimately show ?thesis by auto
+qed
+
+lemma real_greaterThanLessThan_minus_infinity_eq:
+ "real_of_ereal ` {-\<infinity><..<N::ereal} =
+ (if N = \<infinity> then UNIV else if N = -\<infinity> then {} else {..<real_of_ereal N})"
+proof -
+ have "real_of_ereal ` {-\<infinity><..<N::ereal} = uminus ` real_of_ereal ` {-N<..<\<infinity>}"
+ by (auto simp: ereal_uminus_less_reorder intro!: image_eqI[where x="-x" for x])
+ also note real_greaterThanLessThan_infinity_eq
+ finally show ?thesis by (auto intro!: image_eqI[where x="-x" for x])
+qed
+
+lemma real_greaterThanLessThan_inter:
+ "real_of_ereal ` {N<..<M::ereal} = real_of_ereal ` {-\<infinity><..<M} \<inter> real_of_ereal ` {N<..<\<infinity>}"
+ apply safe
+ subgoal by force
+ subgoal by force
+ subgoal for x y z
+ by (cases y; cases z) (auto intro!: image_eqI[where x=z] simp: )
+ done
+
+lemma real_atLeastGreaterThan_eq: "real_of_ereal ` {N<..<M::ereal} =
+ (if N = \<infinity> then {} else
+ if N = -\<infinity> then
+ (if M = \<infinity> then UNIV
+ else if M = -\<infinity> then {}
+ else {..< real_of_ereal M})
+ else if M = - \<infinity> then {}
+ else if M = \<infinity> then {real_of_ereal N<..}
+ else {real_of_ereal N <..< real_of_ereal M})"
+ apply (subst real_greaterThanLessThan_inter)
+ apply (subst real_greaterThanLessThan_minus_infinity_eq)
+ apply (subst real_greaterThanLessThan_infinity_eq)
+ apply auto
+ done
+
+lemma real_image_ereal_ivl:
+ fixes a b::ereal
+ shows
+ "real_of_ereal ` {a<..<b} =
+ (if a < b then (if a = - \<infinity> then if b = \<infinity> then UNIV else {..<real_of_ereal b}
+ else if b = \<infinity> then {real_of_ereal a<..} else {real_of_ereal a <..< real_of_ereal b}) else {})"
+ by (cases a; cases b; simp add: real_atLeastGreaterThan_eq not_less)
+
+lemma fixes a b c::ereal
+ shows not_inftyI: "a < b \<Longrightarrow> b < c \<Longrightarrow> abs b \<noteq> \<infinity>"
+ by force
+
+lemma
+ interval_neqs:
+ fixes r s t::real
+ shows "{r<..<s} \<noteq> {t<..}"
+ and "{r<..<s} \<noteq> {..<t}"
+ and "{r<..<ra} \<noteq> UNIV"
+ and "{r<..} \<noteq> {..<s}"
+ and "{r<..} \<noteq> UNIV"
+ and "{..<r} \<noteq> UNIV"
+ and "{} \<noteq> {r<..}"
+ and "{} \<noteq> {..<r}"
+ subgoal
+ by (metis dual_order.strict_trans greaterThanLessThan_iff greaterThan_iff gt_ex not_le order_refl)
+ subgoal
+ by (metis (no_types, hide_lams) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
+ lessThan_iff minus_minus neg_less_iff_less not_less order_less_irrefl)
+ subgoal by force
+ subgoal
+ by (metis greaterThanLessThan_empty_iff greaterThanLessThan_eq greaterThan_iff inf.idem
+ lessThan_iff lessThan_non_empty less_irrefl not_le)
+ subgoal by force
+ subgoal by force
+ subgoal using greaterThan_non_empty by blast
+ subgoal using lessThan_non_empty by blast
+ done
+
+lemma greaterThanLessThan_eq_iff:
+ fixes r s t u::real
+ shows "({r<..<s} = {t<..<u}) = (r \<ge> s \<and> u \<le> t \<or> r = t \<and> s = u)"
+ by (metis cInf_greaterThanLessThan cSup_greaterThanLessThan greaterThanLessThan_empty_iff not_le)
+
+lemma real_of_ereal_image_greaterThanLessThan_iff:
+ "real_of_ereal ` {a <..< b} = real_of_ereal ` {c <..< d} \<longleftrightarrow> (a \<ge> b \<and> c \<ge> d \<or> a = c \<and> b = d)"
+ unfolding real_atLeastGreaterThan_eq
+ by (cases a; cases b; cases c; cases d;
+ simp add: greaterThanLessThan_eq_iff interval_neqs interval_neqs[symmetric])
+
+lemma uminus_image_real_of_ereal_image_greaterThanLessThan:
+ "uminus ` real_of_ereal ` {l <..< u} = real_of_ereal ` {-u <..< -l}"
+ by (force simp: algebra_simps ereal_less_uminus_reorder
+ ereal_uminus_less_reorder intro: image_eqI[where x="-x" for x])
+
+lemma add_image_real_of_ereal_image_greaterThanLessThan:
+ "(+) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c + l <..< c + u}"
+ apply safe
+ subgoal for x
+ using ereal_less_add[of c]
+ by (force simp: real_of_ereal_add add.commute)
+ subgoal for _ x
+ by (force simp: add.commute real_of_ereal_minus ereal_minus_less ereal_less_minus
+ intro: image_eqI[where x="x - c"])
+ done
+
+lemma add2_image_real_of_ereal_image_greaterThanLessThan:
+ "(\<lambda>x. x + c) ` real_of_ereal ` {l <..< u} = real_of_ereal ` {l + c <..< u + c}"
+ using add_image_real_of_ereal_image_greaterThanLessThan[of c l u]
+ by (metis add.commute image_cong)
+
+lemma minus_image_real_of_ereal_image_greaterThanLessThan:
+ "(-) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c - u <..< c - l}"
+ (is "?l = ?r")
+proof -
+ have "?l = (+) c ` uminus ` real_of_ereal ` {l <..< u}" by auto
+ also note uminus_image_real_of_ereal_image_greaterThanLessThan
+ also note add_image_real_of_ereal_image_greaterThanLessThan
+ finally show ?thesis by (simp add: minus_ereal_def)
+qed
+
+lemma real_ereal_bound_lemma_up:
+ assumes "s \<in> real_of_ereal ` {a<..<b}"
+ assumes "t \<notin> real_of_ereal ` {a<..<b}"
+ assumes "s \<le> t"
+ shows "b \<noteq> \<infinity>"
+ using assms
+ apply (cases b)
+ subgoal by force
+ subgoal by (metis PInfty_neq_ereal(2) assms dual_order.strict_trans1 ereal_infty_less(1)
+ ereal_less_ereal_Ex greaterThanLessThan_empty_iff greaterThanLessThan_iff greaterThan_iff
+ image_eqI less_imp_le linordered_field_no_ub not_less order_trans
+ real_greaterThanLessThan_infinity_eq real_image_ereal_ivl real_of_ereal.simps(1))
+ subgoal by force
+ done
+
+lemma real_ereal_bound_lemma_down:
+ assumes "s \<in> real_of_ereal ` {a<..<b}"
+ assumes "t \<notin> real_of_ereal ` {a<..<b}"
+ assumes "t \<le> s"
+ shows "a \<noteq> - \<infinity>"
+ using assms
+ apply (cases b)
+ subgoal
+ apply safe
+ using assms(1)
+ apply (auto simp: real_greaterThanLessThan_minus_infinity_eq)
+ done
+ subgoal by (auto simp: real_greaterThanLessThan_minus_infinity_eq)
+ subgoal by auto
+ done
+
+
+subsection "Topological space"
instantiation ereal :: linear_continuum_topology
begin
@@ -2469,6 +2637,21 @@
by auto
qed (auto simp add: image_Union image_Int)
+lemma open_image_real_of_ereal:
+ fixes X::"ereal set"
+ assumes "open X"
+ assumes "\<infinity> \<notin> X"
+ assumes "-\<infinity> \<notin> X"
+ shows "open (real_of_ereal ` X)"
+proof -
+ have "real_of_ereal ` X = ereal -` X"
+ apply safe
+ subgoal by (metis assms(2) assms(3) real_of_ereal.elims vimageI)
+ subgoal using image_iff by fastforce
+ done
+ thus ?thesis
+ by (auto intro!: open_ereal_vimage assms)
+qed
lemma eventually_finite:
fixes x :: ereal
--- a/src/HOL/Limits.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Limits.thy Thu Feb 22 18:01:08 2018 +0100
@@ -52,6 +52,9 @@
for f :: "_ \<Rightarrow> real"
by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
+lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially"
+ by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially)
+
lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially"
by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
@@ -1256,6 +1259,20 @@
for a :: real
unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
+lemma at_to_0: "at a = filtermap (\<lambda>x. x + a) (at 0)"
+ for a :: "'a::real_normed_vector"
+ using filtermap_at_shift[of "-a" 0] by simp
+
+lemma filterlim_at_to_0:
+ "filterlim f F (at a) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at 0)"
+ for a :: "'a::real_normed_vector"
+ unfolding filterlim_def filtermap_filtermap at_to_0[of a] ..
+
+lemma eventually_at_to_0:
+ "eventually P (at a) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at 0)"
+ for a :: "'a::real_normed_vector"
+ unfolding at_to_0[of a] by (simp add: eventually_filtermap)
+
lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a)"
for a :: "'a::real_normed_vector"
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
@@ -1268,6 +1285,7 @@
for a :: real
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
+
lemma filterlim_at_left_to_right:
"filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
for a :: real
@@ -1486,6 +1504,36 @@
for c :: nat
by (rule filterlim_subseq) (auto simp: strict_mono_def)
+lemma filterlim_times_pos:
+ "LIM x F1. c * f x :> at_right l"
+ if "filterlim f (at_right p) F1" "0 < c" "l = c * p"
+ for c::"'a::{linordered_field, linorder_topology}"
+ unfolding filterlim_iff
+proof safe
+ fix P
+ assume "\<forall>\<^sub>F x in at_right l. P x"
+ then obtain d where "c * p < d" "\<And>y. y > c * p \<Longrightarrow> y < d \<Longrightarrow> P y"
+ unfolding \<open>l = _ \<close> eventually_at_right_field
+ by auto
+ then have "\<forall>\<^sub>F a in at_right p. P (c * a)"
+ by (auto simp: eventually_at_right_field \<open>0 < c\<close> field_simps intro!: exI[where x="d/c"])
+ from that(1)[unfolded filterlim_iff, rule_format, OF this]
+ show "\<forall>\<^sub>F x in F1. P (c * f x)" .
+qed
+
+lemma filtermap_nhds_times: "c \<noteq> 0 \<Longrightarrow> filtermap (times c) (nhds a) = nhds (c * a)"
+ for a c :: "'a::real_normed_field"
+ by (rule filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+ (auto intro!: tendsto_eq_intros filterlim_ident)
+
+lemma filtermap_times_pos_at_right:
+ fixes c::"'a::{linordered_field, linorder_topology}"
+ assumes "c > 0"
+ shows "filtermap (times c) (at_right p) = at_right (c * p)"
+ using assms
+ by (intro filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+ (auto intro!: filterlim_ident filterlim_times_pos)
+
lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
proof (rule antisym)
have "(inverse \<longlongrightarrow> (0::'a)) at_infinity"
@@ -1936,6 +1984,10 @@
lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
using lim_1_over_n by (simp add: inverse_eq_divide)
+lemma lim_inverse_n': "((\<lambda>n. 1 / n) \<longlongrightarrow> 0) sequentially"
+ using lim_inverse_n
+ by (simp add: inverse_eq_divide)
+
lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
--- a/src/HOL/NthRoot.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/NthRoot.thy Thu Feb 22 18:01:08 2018 +0100
@@ -480,6 +480,9 @@
lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
by (meson not_le real_less_rsqrt)
+lemma sqrt_ge_absD: "\<bar>x\<bar> \<le> sqrt y \<Longrightarrow> x\<^sup>2 \<le> y"
+ using real_sqrt_le_iff[of "x\<^sup>2"] by simp
+
lemma sqrt_even_pow2:
assumes n: "even n"
shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
@@ -538,6 +541,8 @@
DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
+lemmas has_derivative_real_sqrt[derivative_intros] = DERIV_real_sqrt[THEN DERIV_compose_FDERIV]
+
lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0"
for x :: real
apply auto
@@ -658,6 +663,13 @@
lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
by (simp add: power2_eq_square [symmetric])
+lemma sqrt_sum_squares_le_sum:
+ "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
+ apply (rule power2_le_imp_le)
+ apply (simp add: power2_sum)
+ apply simp
+ done
+
lemma real_sqrt_sum_squares_triangle_ineq:
"sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
apply (rule power2_le_imp_le)
--- a/src/HOL/Set_Interval.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Set_Interval.thy Thu Feb 22 18:01:08 2018 +0100
@@ -222,6 +222,10 @@
"{a..<b} = {a..b} - {b}"
by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
+lemma (in order) greaterThanAtMost_eq_atLeastAtMost_diff:
+ "{a<..b} = {a..b} - {a}"
+ by (auto simp add: greaterThanAtMost_def atLeastAtMost_def)
+
end
subsubsection\<open>Emptyness, singletons, subset\<close>
@@ -869,6 +873,19 @@
context linordered_semidom
begin
+lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}"
+proof -
+ have "n = k + (n - k)" if "i + k \<le> n" for n
+ proof -
+ have "n = (n - (k + i)) + (k + i)" using that
+ by (metis add_commute le_add_diff_inverse)
+ then show "n = k + (n - k)"
+ by (metis local.add_diff_cancel_left' add_assoc add_commute)
+ qed
+ then show ?thesis
+ by (fastforce simp: add_le_imp_le_diff add.commute)
+qed
+
lemma image_add_atLeastAtMost [simp]:
"plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
proof
@@ -911,112 +928,11 @@
"(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
by (simp add: add.commute [of _ k])
+lemma image_add_greaterThanAtMost[simp]: "(+) c ` {a<..b} = {c + a<..c + b}"
+ by (simp add: image_set_diff greaterThanAtMost_eq_atLeastAtMost_diff ac_simps)
+
end
-lemma image_Suc_atLeastAtMost [simp]:
- "Suc ` {i..j} = {Suc i..Suc j}"
- using image_add_atLeastAtMost [of 1 i j]
- by (simp only: plus_1_eq_Suc) simp
-
-lemma image_Suc_atLeastLessThan [simp]:
- "Suc ` {i..<j} = {Suc i..<Suc j}"
- using image_add_atLeastLessThan [of 1 i j]
- by (simp only: plus_1_eq_Suc) simp
-
-corollary image_Suc_atMost:
- "Suc ` {..n} = {1..Suc n}"
- by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-
-corollary image_Suc_lessThan:
- "Suc ` {..<n} = {1..n}"
- by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-
-lemma image_diff_atLeastAtMost [simp]:
- fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
- apply auto
- apply (rule_tac x="d-x" in rev_image_eqI, auto)
- done
-
-lemma image_mult_atLeastAtMost [simp]:
- fixes d::"'a::linordered_field"
- assumes "d>0" shows "(( * ) d ` {a..b}) = {d*a..d*b}"
- using assms
- by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
-
-lemma image_affinity_atLeastAtMost:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {m*a + c .. m *b + c}
- else {m*b + c .. m*a + c})"
- apply (case_tac "m=0", auto simp: mult_le_cancel_left)
- apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
- apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
- done
-
-lemma image_affinity_atLeastAtMost_diff:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {m*a - c .. m*b - c}
- else {m*b - c .. m*a - c})"
- using image_affinity_atLeastAtMost [of m "-c" a b]
- by simp
-
-lemma image_affinity_atLeastAtMost_div:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {a/m + c .. b/m + c}
- else {b/m + c .. a/m + c})"
- using image_affinity_atLeastAtMost [of "inverse m" c a b]
- by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma image_affinity_atLeastAtMost_div_diff:
- fixes c :: "'a::linordered_field"
- shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
- else if 0 \<le> m then {a/m - c .. b/m - c}
- else {b/m - c .. a/m - c})"
- using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
- by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma atLeast1_lessThan_eq_remove0:
- "{Suc 0..<n} = {..<n} - {0}"
- by auto
-
-lemma atLeast1_atMost_eq_remove0:
- "{Suc 0..n} = {..n} - {0}"
- by auto
-
-lemma image_add_int_atLeastLessThan:
- "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
- apply (auto simp add: image_def)
- apply (rule_tac x = "x - l" in bexI)
- apply auto
- done
-
-lemma image_minus_const_atLeastLessThan_nat:
- fixes c :: nat
- shows "(\<lambda>i. i - c) ` {x ..< y} =
- (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
- (is "_ = ?right")
-proof safe
- fix a assume a: "a \<in> ?right"
- show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
- proof cases
- assume "c < y" with a show ?thesis
- by (auto intro!: image_eqI[of _ _ "a + c"])
- next
- assume "\<not> c < y" with a show ?thesis
- by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
- qed
-qed auto
-
-lemma image_int_atLeastLessThan:
- "int ` {a..<b} = {int a..<int b}"
- by (auto intro!: image_eqI [where x = "nat x" for x])
-
-lemma image_int_atLeastAtMost:
- "int ` {a..b} = {int a..int b}"
- by (auto intro!: image_eqI [where x = "nat x" for x])
-
context ordered_ab_group_add
begin
@@ -1057,8 +973,184 @@
and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
+
+lemma image_add_atMost[simp]: "(+) c ` {..a} = {..c + a}"
+ by (auto intro!: image_eqI[where x="x - c" for x] simp: algebra_simps)
+
end
+lemma image_Suc_atLeastAtMost [simp]:
+ "Suc ` {i..j} = {Suc i..Suc j}"
+ using image_add_atLeastAtMost [of 1 i j]
+ by (simp only: plus_1_eq_Suc) simp
+
+lemma image_Suc_atLeastLessThan [simp]:
+ "Suc ` {i..<j} = {Suc i..<Suc j}"
+ using image_add_atLeastLessThan [of 1 i j]
+ by (simp only: plus_1_eq_Suc) simp
+
+corollary image_Suc_atMost:
+ "Suc ` {..n} = {1..Suc n}"
+ by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+corollary image_Suc_lessThan:
+ "Suc ` {..<n} = {1..n}"
+ by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+lemma image_diff_atLeastAtMost [simp]:
+ fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
+ apply auto
+ apply (rule_tac x="d-x" in rev_image_eqI, auto)
+ done
+
+lemma image_diff_atLeastLessThan [simp]:
+ fixes a b c::"'a::linordered_idom"
+ shows "(-) c ` {a..<b} = {c - b<..c - a}"
+proof -
+ have "(-) c ` {a..<b} = (+) c ` uminus ` {a ..<b}"
+ unfolding image_image by simp
+ also have "\<dots> = {c - b<..c - a}" by simp
+ finally show ?thesis by simp
+qed
+
+lemma image_minus_const_greaterThanAtMost_real[simp]:
+ fixes a b c::"'a::linordered_idom"
+ shows "(-) c ` {a<..b} = {c - b..<c - a}"
+proof -
+ have "(-) c ` {a<..b} = (+) c ` uminus ` {a<..b}"
+ unfolding image_image by simp
+ also have "\<dots> = {c - b..<c - a}" by simp
+ finally show ?thesis by simp
+qed
+
+lemma image_minus_const_atLeast_real[simp]:
+ fixes a c::"'a::linordered_idom"
+ shows "(-) c ` {a..} = {..c - a}"
+proof -
+ have "(-) c ` {a..} = (+) c ` uminus ` {a ..}"
+ unfolding image_image by simp
+ also have "\<dots> = {..c - a}" by simp
+ finally show ?thesis by simp
+qed
+
+lemma image_minus_const_AtMost_real[simp]:
+ fixes b c::"'a::linordered_idom"
+ shows "(-) c ` {..b} = {c - b..}"
+proof -
+ have "(-) c ` {..b} = (+) c ` uminus ` {..b}"
+ unfolding image_image by simp
+ also have "\<dots> = {c - b..}" by simp
+ finally show ?thesis by simp
+qed
+
+context linordered_field begin
+
+lemma image_mult_atLeastAtMost [simp]:
+ "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
+ using that
+ by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
+
+lemma image_mult_atLeastAtMost_if:
+ "( * ) c ` {x .. y} =
+ (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
+proof -
+ consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
+ using local.antisym_conv3 local.leI by blast
+ then show ?thesis
+ proof cases
+ case 1
+ have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
+ by (simp add: image_image)
+ also have "\<dots> = {c * y .. c * x}"
+ using \<open>c < 0\<close>
+ by simp
+ finally show ?thesis
+ using \<open>c < 0\<close> by auto
+ qed (auto simp: not_le local.mult_less_cancel_left_pos)
+qed
+
+lemma image_mult_atLeastAtMost_if':
+ "(\<lambda>x. x * c) ` {x..y} =
+ (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
+ by (subst mult.commute)
+ (simp add: image_mult_atLeastAtMost_if mult.commute mult_le_cancel_left_pos)
+
+lemma image_affinity_atLeastAtMost:
+ "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {m*a + c .. m *b + c}
+ else {m*b + c .. m*a + c})"
+proof -
+ have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
+ unfolding image_comp[symmetric]
+ by (simp add: o_def)
+ then show ?thesis
+ by (auto simp add: image_comp[symmetric] image_mult_atLeastAtMost_if mult_le_cancel_left)
+qed
+
+lemma image_affinity_atLeastAtMost_diff:
+ "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {m*a - c .. m*b - c}
+ else {m*b - c .. m*a - c})"
+ using image_affinity_atLeastAtMost [of m "-c" a b]
+ by simp
+
+lemma image_affinity_atLeastAtMost_div:
+ "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {a/m + c .. b/m + c}
+ else {b/m + c .. a/m + c})"
+ using image_affinity_atLeastAtMost [of "inverse m" c a b]
+ by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+lemma image_affinity_atLeastAtMost_div_diff:
+ "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
+ else if 0 \<le> m then {a/m - c .. b/m - c}
+ else {b/m - c .. a/m - c})"
+ using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
+ by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+end
+
+lemma atLeast1_lessThan_eq_remove0:
+ "{Suc 0..<n} = {..<n} - {0}"
+ by auto
+
+lemma atLeast1_atMost_eq_remove0:
+ "{Suc 0..n} = {..n} - {0}"
+ by auto
+
+lemma image_add_int_atLeastLessThan:
+ "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
+ apply (auto simp add: image_def)
+ apply (rule_tac x = "x - l" in bexI)
+ apply auto
+ done
+
+lemma image_minus_const_atLeastLessThan_nat:
+ fixes c :: nat
+ shows "(\<lambda>i. i - c) ` {x ..< y} =
+ (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
+ (is "_ = ?right")
+proof safe
+ fix a assume a: "a \<in> ?right"
+ show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
+ proof cases
+ assume "c < y" with a show ?thesis
+ by (auto intro!: image_eqI[of _ _ "a + c"])
+ next
+ assume "\<not> c < y" with a show ?thesis
+ by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
+ qed
+qed auto
+
+lemma image_int_atLeastLessThan:
+ "int ` {a..<b} = {int a..<int b}"
+ by (auto intro!: image_eqI [where x = "nat x" for x])
+
+lemma image_int_atLeastAtMost:
+ "int ` {a..b} = {int a..int b}"
+ by (auto intro!: image_eqI [where x = "nat x" for x])
+
+
subsubsection \<open>Finiteness\<close>
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
--- a/src/HOL/Topological_Spaces.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Topological_Spaces.thy Thu Feb 22 18:01:08 2018 +0100
@@ -609,7 +609,6 @@
and "filterlim g G (at x within {x. \<not>P x})"
shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
using assms by (intro filterlim_at_within_If) simp_all
-
lemma (in linorder_topology) at_within_order:
assumes "UNIV \<noteq> {x}"
shows "at x within s =
@@ -692,7 +691,18 @@
(\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal
eventually_filtercomap_nhds eventually_principal by blast
-
+
+lemma eventually_at_right_field:
+ "eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
+ for x :: "'a::{linordered_field, linorder_topology}"
+ using linordered_field_no_ub[rule_format, of x]
+ by (auto simp: eventually_at_right)
+
+lemma eventually_at_left_field:
+ "eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)"
+ for x :: "'a::{linordered_field, linorder_topology}"
+ using linordered_field_no_lb[rule_format, of x]
+ by (auto simp: eventually_at_left)
subsubsection \<open>Tendsto\<close>
@@ -762,9 +772,11 @@
end
-lemma tendsto_within_subset:
- "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
- by (blast intro: tendsto_mono at_le)
+lemma (in topological_space) filterlim_within_subset:
+ "filterlim f l (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> filterlim f l (at x within T)"
+ by (blast intro: filterlim_mono at_le)
+
+lemmas tendsto_within_subset = filterlim_within_subset
lemma (in order_topology) order_tendsto_iff:
"(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
@@ -963,6 +975,11 @@
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
+lemma eventually_Lim_ident_at:
+ "(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
+ (\<forall>\<^sub>F y in at x within X. P x y)" for x::"'a::t2_space"
+ by (cases "at x within X = bot") (auto simp: Lim_ident_at)
+
lemma filterlim_at_bot_at_right:
fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
@@ -2612,6 +2629,37 @@
by (metis less_le)
qed
+lemma (in linorder_topology) not_in_connected_cases:
+ assumes conn: "connected S"
+ assumes nbdd: "x \<notin> S"
+ assumes ne: "S \<noteq> {}"
+ obtains "bdd_above S" "\<And>y. y \<in> S \<Longrightarrow> x \<ge> y" | "bdd_below S" "\<And>y. y \<in> S \<Longrightarrow> x \<le> y"
+proof -
+ obtain s where "s \<in> S" using ne by blast
+ {
+ assume "s \<le> x"
+ have "False" if "x \<le> y" "y \<in> S" for y
+ using connectedD_interval[OF conn \<open>s \<in> S\<close> \<open>y \<in> S\<close> \<open>s \<le> x\<close> \<open>x \<le> y\<close>] \<open>x \<notin> S\<close>
+ by simp
+ then have wit: "y \<in> S \<Longrightarrow> x \<ge> y" for y
+ using le_cases by blast
+ then have "bdd_above S"
+ by (rule local.bdd_aboveI)
+ note this wit
+ } moreover {
+ assume "x \<le> s"
+ have "False" if "x \<ge> y" "y \<in> S" for y
+ using connectedD_interval[OF conn \<open>y \<in> S\<close> \<open>s \<in> S\<close> \<open>x \<ge> y\<close> \<open>s \<ge> x\<close> ] \<open>x \<notin> S\<close>
+ by simp
+ then have wit: "y \<in> S \<Longrightarrow> x \<le> y" for y
+ using le_cases by blast
+ then have "bdd_below S"
+ by (rule bdd_belowI)
+ note this wit
+ } ultimately show ?thesis
+ by (meson le_cases that)
+qed
+
lemma connected_continuous_image:
assumes *: "continuous_on s f"
and "connected s"
@@ -3454,6 +3502,15 @@
lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
by (fact continuous_Pair)
+lemma continuous_on_compose_Pair:
+ assumes f: "continuous_on (Sigma A B) (\<lambda>(a, b). f a b)"
+ assumes g: "continuous_on C g"
+ assumes h: "continuous_on C h"
+ assumes subset: "\<And>c. c \<in> C \<Longrightarrow> g c \<in> A" "\<And>c. c \<in> C \<Longrightarrow> h c \<in> B (g c)"
+ shows "continuous_on C (\<lambda>c. f (g c) (h c))"
+ using continuous_on_compose2[OF f continuous_on_Pair[OF g h]] subset
+ by auto
+
subsubsection \<open>Connectedness of products\<close>
--- a/src/HOL/Transcendental.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Transcendental.thy Thu Feb 22 18:01:08 2018 +0100
@@ -1389,6 +1389,8 @@
declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
and DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV]
+
lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
proof -
from summable_norm[OF summable_norm_exp, of x]
@@ -1883,6 +1885,8 @@
declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
and DERIV_ln_divide[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_ln[derivative_intros] = DERIV_ln[THEN DERIV_compose_FDERIV]
+
lemma ln_series:
assumes "0 < x" and "x < 2"
shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
@@ -3094,24 +3098,33 @@
shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
using tendsto_powr'[of f a F g b] assms by auto
+lemma has_derivative_powr[derivative_intros]:
+ assumes g[derivative_intros]: "(g has_derivative g') (at x within X)"
+ and f[derivative_intros]:"(f has_derivative f') (at x within X)"
+ assumes pos: "0 < g x" and "x \<in> X"
+ shows "((\<lambda>x. g x powr f x::real) has_derivative (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
+proof -
+ have "\<forall>\<^sub>F x in at x within X. g x > 0"
+ by (rule order_tendstoD[OF _ pos])
+ (rule has_derivative_continuous[OF g, unfolded continuous_within])
+ then obtain d where "d > 0" and pos': "\<And>x'. x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> 0 < g x'"
+ using pos unfolding eventually_at by force
+ have "((\<lambda>x. exp (f x * ln (g x))) has_derivative
+ (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
+ using pos
+ by (auto intro!: derivative_eq_intros simp: divide_simps powr_def)
+ then show ?thesis
+ by (rule has_derivative_transform_within[OF _ \<open>d > 0\<close> \<open>x \<in> X\<close>]) (auto simp: powr_def dest: pos')
+qed
+
lemma DERIV_powr:
fixes r :: real
assumes g: "DERIV g x :> m"
and pos: "g x > 0"
and f: "DERIV f x :> r"
shows "DERIV (\<lambda>x. g x powr f x) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
-proof -
- have "DERIV (\<lambda>x. exp (f x * ln (g x))) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
- using pos
- by (auto intro!: derivative_eq_intros g pos f simp: powr_def field_simps exp_diff)
- then show ?thesis
- proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated])
- from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
- unfolding isCont_def by (rule order_tendstoD(1))
- with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
- by (auto simp: eventually_at_filter powr_def elim: eventually_mono)
- qed
-qed
+ using assms
+ by (auto intro!: derivative_eq_intros ext simp: has_field_derivative_def algebra_simps)
lemma DERIV_fun_powr:
fixes r :: real
@@ -3344,6 +3357,8 @@
declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
and DERIV_sin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_sin[derivative_intros] = DERIV_sin[THEN DERIV_compose_FDERIV]
+
lemma DERIV_cos [simp]: "DERIV cos x :> - sin x"
for x :: "'a::{real_normed_field,banach}"
unfolding sin_def cos_def scaleR_conv_of_real
@@ -3359,6 +3374,8 @@
declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
and DERIV_cos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_cos[derivative_intros] = DERIV_cos[THEN DERIV_compose_FDERIV]
+
lemma isCont_sin: "isCont sin x"
for x :: "'a::{real_normed_field,banach}"
by (rule DERIV_sin [THEN DERIV_isCont])
@@ -4598,6 +4615,8 @@
unfolding tan_def
by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
+lemmas has_derivative_tan[derivative_intros] = DERIV_tan[THEN DERIV_compose_FDERIV]
+
lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
for x :: "'a::{real_normed_field,banach}"
by (rule DERIV_tan [THEN DERIV_isCont])
@@ -5265,6 +5284,10 @@
DERIV_arctan[THEN DERIV_chain2, derivative_intros]
DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
+lemmas has_derivative_arctan[derivative_intros] = DERIV_arctan[THEN DERIV_compose_FDERIV]
+ and has_derivative_arccos[derivative_intros] = DERIV_arccos[THEN DERIV_compose_FDERIV]
+ and has_derivative_arcsin[derivative_intros] = DERIV_arcsin[THEN DERIV_compose_FDERIV]
+
lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- (pi/2)))"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
(auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1