--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Jun 02 12:45:27 2021 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Jun 03 10:58:15 2021 +0100
@@ -1658,6 +1658,31 @@
unfolding islimpt_def by blast
qed
+lemma islimpt_Ioc [simp]:
+ fixes a :: real
+ assumes "a<b"
+ shows "x islimpt {a<..b} \<longleftrightarrow> x \<in> {a..b}" (is "?lhs = ?rhs")
+proof
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (metis assms closed_atLeastAtMost closed_limpt closure_greaterThanAtMost closure_subset islimpt_subset)
+next
+ assume ?rhs
+ then have "x \<in> closure {a<..<b}"
+ using assms closure_greaterThanLessThan by blast
+ then show ?lhs
+ by (metis (no_types) Diff_empty Diff_insert0 interior_lessThanAtMost interior_limit_point interior_subset islimpt_in_closure islimpt_subset)
+qed
+
+lemma islimpt_Ico [simp]:
+ fixes a :: real
+ assumes "a<b" shows "x islimpt {a..<b} \<longleftrightarrow> x \<in> {a..b}"
+ by (metis assms closure_atLeastLessThan closure_greaterThanAtMost islimpt_Ioc limpt_of_closure)
+
+lemma islimpt_Icc [simp]:
+ fixes a :: real
+ assumes "a<b" shows "x islimpt {a..b} \<longleftrightarrow> x \<in> {a..b}"
+ by (metis assms closure_atLeastLessThan islimpt_Ico limpt_of_closure)
+
lemma connected_imp_perfect_aff_dim:
"\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
using aff_dim_sing connected_imp_perfect by blast
--- a/src/HOL/Analysis/Derivative.thy Wed Jun 02 12:45:27 2021 +0000
+++ b/src/HOL/Analysis/Derivative.thy Thu Jun 03 10:58:15 2021 +0100
@@ -3281,6 +3281,10 @@
unfolding C1_differentiable_on_eq
by (rule continuous_intros | simp add: continuous_at_imp_continuous_on differentiable_imp_continuous_within)+
+lemma C1_differentiable_on_of_real [derivative_intros]: "of_real C1_differentiable_on S"
+ unfolding C1_differentiable_on_def
+ by (smt (verit, del_insts) DERIV_ident UNIV_I continuous_on_const has_vector_derivative_of_real has_vector_derivative_transform)
+
definition\<^marker>\<open>tag important\<close> piecewise_C1_differentiable_on
(infixr "piecewise'_C1'_differentiable'_on" 50)
@@ -3298,7 +3302,7 @@
C1_differentiable_on_def differentiable_def has_vector_derivative_def
intro: has_derivative_at_withinI)
-lemma piecewise_C1_differentiable_compose:
+lemma piecewise_C1_differentiable_compose [derivative_intros]:
assumes fg: "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on (f ` S)" and fin: "\<And>x. finite (S \<inter> f-`{x})"
shows "(g \<circ> f) piecewise_C1_differentiable_on S"
proof -
@@ -3334,7 +3338,7 @@
unfolding C1_differentiable_on_eq continuous_on_eq_continuous_within
using differentiable_at_withinI differentiable_imp_continuous_within by blast
-lemma C1_differentiable_on_empty [iff]: "f C1_differentiable_on {}"
+lemma C1_differentiable_on_empty [iff,derivative_intros]: "f C1_differentiable_on {}"
unfolding C1_differentiable_on_def
by auto
@@ -3356,7 +3360,7 @@
done
qed
-lemma piecewise_C1_differentiable_cases:
+lemma piecewise_C1_differentiable_cases [derivative_intros]:
fixes c::real
assumes "f piecewise_C1_differentiable_on {a..c}"
"g piecewise_C1_differentiable_on {c..b}"
@@ -3444,12 +3448,21 @@
by (simp add: piecewise_C1_differentiable_on_def)
qed
-lemma piecewise_C1_differentiable_neg:
+lemma piecewise_C1_differentiable_const [derivative_intros]:
+ "(\<lambda>x. c) piecewise_C1_differentiable_on S"
+ by (simp add: C1_differentiable_imp_piecewise)
+
+lemma piecewise_C1_differentiable_scaleR [derivative_intros]:
+ "\<lbrakk>f piecewise_C1_differentiable_on S\<rbrakk>
+ \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) piecewise_C1_differentiable_on S"
+ by (force simp add: piecewise_C1_differentiable_on_def continuous_on_scaleR)
+
+lemma piecewise_C1_differentiable_neg [derivative_intros]:
"f piecewise_C1_differentiable_on S \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_C1_differentiable_on S"
unfolding piecewise_C1_differentiable_on_def
by (auto intro!: continuous_on_minus C1_differentiable_on_minus)
-lemma piecewise_C1_differentiable_add:
+lemma piecewise_C1_differentiable_add [derivative_intros]:
assumes "f piecewise_C1_differentiable_on i"
"g piecewise_C1_differentiable_on i"
shows "(\<lambda>x. f x + g x) piecewise_C1_differentiable_on i"
@@ -3466,10 +3479,26 @@
by (auto simp: piecewise_C1_differentiable_on_def continuous_on_add)
qed
-lemma piecewise_C1_differentiable_diff:
+lemma piecewise_C1_differentiable_diff [derivative_intros]:
"\<lbrakk>f piecewise_C1_differentiable_on S; g piecewise_C1_differentiable_on S\<rbrakk>
\<Longrightarrow> (\<lambda>x. f x - g x) piecewise_C1_differentiable_on S"
unfolding diff_conv_add_uminus
by (metis piecewise_C1_differentiable_add piecewise_C1_differentiable_neg)
+lemma piecewise_C1_differentiable_cmult_right [derivative_intros]:
+ fixes c::complex
+ shows "f piecewise_C1_differentiable_on S
+ \<Longrightarrow> (\<lambda>x. f x * c) piecewise_C1_differentiable_on S"
+ by (force simp: piecewise_C1_differentiable_on_def continuous_on_mult_right)
+
+lemma piecewise_C1_differentiable_cmult_left [derivative_intros]:
+ fixes c::complex
+ shows "f piecewise_C1_differentiable_on S
+ \<Longrightarrow> (\<lambda>x. c * f x) piecewise_C1_differentiable_on S"
+ using piecewise_C1_differentiable_cmult_right [of f S c] by (simp add: mult.commute)
+
+lemma piecewise_C1_differentiable_on_of_real [derivative_intros]:
+ "of_real piecewise_C1_differentiable_on S"
+ by (simp add: C1_differentiable_imp_piecewise C1_differentiable_on_of_real)
+
end
--- a/src/HOL/Analysis/Linear_Algebra.thy Wed Jun 02 12:45:27 2021 +0000
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Jun 03 10:58:15 2021 +0100
@@ -688,6 +688,9 @@
shows "linear f \<Longrightarrow> f differentiable net"
by (metis linear_imp_has_derivative differentiable_def)
+lemma of_real_differentiable [simp,derivative_intros]: "of_real differentiable F"
+ by (simp add: bounded_linear_imp_differentiable bounded_linear_of_real)
+
subsection\<^marker>\<open>tag unimportant\<close> \<open>We continue\<close>
@@ -1056,7 +1059,7 @@
lemma norm_le_infnorm:
fixes x :: "'a::euclidean_space"
shows "norm x \<le> sqrt DIM('a) * infnorm x"
- unfolding norm_eq_sqrt_inner id_def
+ unfolding norm_eq_sqrt_inner id_def
proof (rule real_le_lsqrt[OF inner_ge_zero])
show "sqrt DIM('a) * infnorm x \<ge> 0"
by (simp add: zero_le_mult_iff infnorm_pos_le)
@@ -1085,7 +1088,7 @@
(is "?lhs \<longleftrightarrow> ?rhs")
proof (cases "x=0")
case True
- then show ?thesis
+ then show ?thesis
by auto
next
case False
@@ -1095,9 +1098,9 @@
norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) = 0)"
using False unfolding inner_simps
by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
- also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)"
+ also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)"
using False by (simp add: field_simps inner_commute)
- also have "\<dots> \<longleftrightarrow> ?lhs"
+ also have "\<dots> \<longleftrightarrow> ?lhs"
using False by auto
finally show ?thesis by metis
qed
@@ -1125,7 +1128,7 @@
shows "norm (x + y) = norm x + norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
proof (cases "x = 0 \<or> y = 0")
case True
- then show ?thesis
+ then show ?thesis
by force
next
case False
@@ -1206,7 +1209,7 @@
by (auto simp: insert_commute)
next
case False
- show ?thesis
+ show ?thesis
proof
assume h: "?lhs"
then obtain u where u: "\<forall> x\<in> {0,x,y}. \<forall>y\<in> {0,x,y}. \<exists>c. x - y = c *\<^sub>R u"
@@ -1250,7 +1253,7 @@
proof
assume "\<bar>x \<bullet> y\<bar> = norm x * norm y"
then show "collinear {0, x, y}"
- unfolding norm_cauchy_schwarz_abs_eq collinear_lemma
+ unfolding norm_cauchy_schwarz_abs_eq collinear_lemma
by (meson eq_vector_fraction_iff nnz)
next
assume "collinear {0, x, y}"
--- a/src/HOL/Analysis/Path_Connected.thy Wed Jun 02 12:45:27 2021 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy Thu Jun 03 10:58:15 2021 +0100
@@ -207,6 +207,9 @@
unfolding pathstart_def reversepath_def pathfinish_def
by auto
+lemma reversepath_o: "reversepath g = g \<circ> (-)1"
+ by (auto simp: reversepath_def)
+
lemma pathstart_join[simp]: "pathstart (g1 +++ g2) = pathstart g1"
unfolding pathstart_def joinpaths_def pathfinish_def
by auto
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Wed Jun 02 12:45:27 2021 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Jun 03 10:58:15 2021 +0100
@@ -18,6 +18,11 @@
shows "is_pole g b"
using is_pole_cong assms by auto
+lemma is_pole_shift_iff:
+ fixes f :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector)"
+ shows "is_pole (f \<circ> (+) d) a = is_pole f (a + d)"
+ by (metis add_diff_cancel_right' filterlim_shift_iff is_pole_def)
+
lemma is_pole_tendsto:
fixes f::"('a::topological_space \<Rightarrow> 'b::real_normed_div_algebra)"
shows "is_pole f x \<Longrightarrow> ((inverse o f) \<longlongrightarrow> 0) (at x)"
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy Wed Jun 02 12:45:27 2021 +0000
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Thu Jun 03 10:58:15 2021 +0100
@@ -68,8 +68,8 @@
text\<open>Show that we can forget about the localized derivative.\<close>
lemma has_integral_localized_vector_derivative:
- "((\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow>
- ((\<lambda>x. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}"
+ "((\<lambda>x. f (g x) * vector_derivative p (at x within {a..b})) has_integral i) {a..b} \<longleftrightarrow>
+ ((\<lambda>x. f (g x) * vector_derivative p (at x)) has_integral i) {a..b}"
proof -
have *: "{a..b} - {a,b} = interior {a..b}"
by (simp add: atLeastAtMost_diff_ends)
@@ -78,8 +78,8 @@
qed
lemma integrable_on_localized_vector_derivative:
- "(\<lambda>x. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} \<longleftrightarrow>
- (\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}"
+ "(\<lambda>x. f (g x) * vector_derivative p (at x within {a..b})) integrable_on {a..b} \<longleftrightarrow>
+ (\<lambda>x. f (g x) * vector_derivative p (at x)) integrable_on {a..b}"
by (simp add: integrable_on_def has_integral_localized_vector_derivative)
lemma has_contour_integral:
--- a/src/HOL/Deriv.thy Wed Jun 02 12:45:27 2021 +0000
+++ b/src/HOL/Deriv.thy Thu Jun 03 10:58:15 2021 +0100
@@ -708,6 +708,23 @@
(\<lambda>x. f x * g x) differentiable (at x within s)"
unfolding differentiable_def by (blast intro: has_derivative_mult)
+lemma differentiable_cmult_left_iff [simp]:
+ fixes c::"'a::real_normed_field"
+ shows "(\<lambda>t. c * q t) differentiable at t \<longleftrightarrow> c = 0 \<or> (\<lambda>t. q t) differentiable at t" (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ {assume "c \<noteq> 0"
+ then have "q differentiable at t"
+ using differentiable_mult [OF differentiable_const L, of concl: "1/c"] by auto
+ } then show ?rhs
+ by auto
+qed auto
+
+lemma differentiable_cmult_right_iff [simp]:
+ fixes c::"'a::real_normed_field"
+ shows "(\<lambda>t. q t * c) differentiable at t \<longleftrightarrow> c = 0 \<or> (\<lambda>t. q t) differentiable at t" (is "?lhs = ?rhs")
+ by (simp add: mult.commute flip: differentiable_cmult_left_iff)
+
lemma differentiable_inverse [simp, derivative_intros]:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
--- a/src/HOL/Limits.thy Wed Jun 02 12:45:27 2021 +0000
+++ b/src/HOL/Limits.thy Thu Jun 03 10:58:15 2021 +0100
@@ -11,6 +11,20 @@
imports Real_Vector_Spaces
begin
+text \<open>Lemmas related to shifting/scaling\<close>
+lemma range_add [simp]:
+ fixes a::"'a::group_add" shows "range ((+) a) = UNIV"
+ by (metis add_minus_cancel surjI)
+
+lemma range_diff [simp]:
+ fixes a::"'a::group_add" shows "range ((-) a) = UNIV"
+ by (metis (full_types) add_minus_cancel diff_minus_eq_add surj_def)
+
+lemma range_mult [simp]:
+ fixes a::"real" shows "range ((*) a) = (if a=0 then {0} else UNIV)"
+ by (simp add: surj_def) (meson dvdE dvd_field_iff)
+
+
subsection \<open>Filter going to infinity norm\<close>
definition at_infinity :: "'a::real_normed_vector filter"
@@ -1461,6 +1475,28 @@
for a d :: "real"
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
+lemma filterlim_shift:
+ fixes d :: "'a::real_normed_vector"
+ assumes "filterlim f F (at a)"
+ shows "filterlim (f \<circ> (+) d) F (at (a - d))"
+ unfolding filterlim_iff
+proof (intro strip)
+ fix P
+ assume "eventually P F"
+ then have "\<forall>\<^sub>F x in filtermap (\<lambda>y. y - d) (at a). P (f (d + x))"
+ using assms by (force simp add: filterlim_iff eventually_filtermap)
+ then show "(\<forall>\<^sub>F x in at (a - d). P ((f \<circ> (+) d) x))"
+ by (force simp add: filtermap_at_shift)
+qed
+
+lemma filterlim_shift_iff:
+ fixes d :: "'a::real_normed_vector"
+ shows "filterlim (f \<circ> (+) d) F (at (a - d)) = filterlim f F (at a)" (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs show ?rhs
+ using filterlim_shift [OF L, of "-d"] by (simp add: filterlim_iff)
+qed (metis filterlim_shift)
+
lemma at_right_to_0: "at_right a = filtermap (\<lambda>x. x + a) (at_right 0)"
for a :: real
using filtermap_at_right_shift[of "-a" 0] by simp