# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1622713640 -3600
# Node ID 8893e0ed263a4cfc5392b146413ebc3518e697c6
# Parent  26c0ccf17f318614a645ec9136edea1e845989e2
new lemmas mostly about paths

diff -r 26c0ccf17f31 -r 8893e0ed263a src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Jun 03 10:47:20 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
diff -r 26c0ccf17f31 -r 8893e0ed263a src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Analysis/Derivative.thy	Thu Jun 03 10:47:20 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
diff -r 26c0ccf17f31 -r 8893e0ed263a src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Jun 03 10:47:20 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}"
diff -r 26c0ccf17f31 -r 8893e0ed263a src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Jun 03 10:47:20 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
diff -r 26c0ccf17f31 -r 8893e0ed263a src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Thu Jun 03 10:47:20 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)"
diff -r 26c0ccf17f31 -r 8893e0ed263a src/HOL/Complex_Analysis/Contour_Integration.thy
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy	Thu Jun 03 10:47:20 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:
diff -r 26c0ccf17f31 -r 8893e0ed263a src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Deriv.thy	Thu Jun 03 10:47:20 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>
diff -r 26c0ccf17f31 -r 8893e0ed263a src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 31 20:27:45 2021 +0000
+++ b/src/HOL/Limits.thy	Thu Jun 03 10:47:20 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