author paulson Thu, 03 Jun 2021 10:47:20 +0100 changeset 74052 8893e0ed263a parent 74049 26c0ccf17f31 child 74053 56f31baaa837
 src/HOL/Analysis/Convex_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Derivative.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Linear_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Path_Connected.thy file | annotate | diff | comparison | revisions src/HOL/Complex_Analysis/Complex_Singularities.thy file | annotate | diff | comparison | revisions src/HOL/Complex_Analysis/Contour_Integration.thy file | annotate | diff | comparison | revisions src/HOL/Deriv.thy file | annotate | diff | comparison | revisions src/HOL/Limits.thy file | annotate | diff | comparison | revisions
```--- 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```
```--- 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 @@
qed

-lemma piecewise_C1_differentiable_neg:
+lemma piecewise_C1_differentiable_const [derivative_intros]:
+  "(\<lambda>x. c) piecewise_C1_differentiable_on S"
+
+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)

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 @@
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"

+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	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"
@@ -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	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```
```--- 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)"```
```--- 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}"
@@ -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}"

lemma has_contour_integral:```
```--- 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>```
```--- 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>
+  fixes a::"'a::group_add" shows "range ((+) a) = UNIV"
+
+lemma range_diff [simp]:
+  fixes a::"'a::group_add" shows "range ((-) a) = UNIV"
+
+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```