author paulson Mon, 28 Jun 2021 15:05:46 +0100 changeset 74145 26171a89466a parent 74144 0a12ca4f3e8d child 74147 9b981f5612d0
A few useful lemmas about derivatives, colinearity and other topics
 src/HOL/Analysis/Complex_Analysis_Basics.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Complex_Transcendental.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Derivative.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Elementary_Metric_Spaces.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Linear_Algebra.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/Complex_Analysis_Basics.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Jun 28 15:05:46 2021 +0100
@@ -148,6 +148,16 @@
"f holomorphic_on s \<Longrightarrow> continuous_on s f"
by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)

+lemma holomorphic_closedin_preimage_constant:
+  assumes "f holomorphic_on D"
+  shows "closedin (top_of_set D) {z\<in>D. f z = a}"
+  by (simp add: assms continuous_closedin_preimage_constant holomorphic_on_imp_continuous_on)
+
+lemma holomorphic_closed_preimage_constant:
+  assumes "f holomorphic_on UNIV"
+  shows "closed {z. f z = a}"
+  using holomorphic_closedin_preimage_constant [OF assms] by simp
+
lemma holomorphic_on_subset [elim]:
"f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
unfolding holomorphic_on_def```
```--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jun 28 15:05:46 2021 +0100
@@ -1778,7 +1778,24 @@

subsection\<open>The Argument of a Complex Number\<close>

-text\<open>Finally: it's is defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
+text\<open>Unlike in HOL Light, it's defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>
+
+lemma Arg_eq_Im_Ln:
+  assumes "z \<noteq> 0" shows "arg z = Im (Ln z)"
+proof (rule arg_unique)
+  show "sgn z = cis (Im (Ln z))"
+    by (metis assms exp_Ln exp_eq_polar nonzero_mult_div_cancel_left norm_eq_zero
+              norm_exp_eq_Re of_real_eq_0_iff sgn_eq)
+  show "- pi < Im (Ln z)"
+    by (simp add: assms mpi_less_Im_Ln)
+  show "Im (Ln z) \<le> pi"
+    by (simp add: Im_Ln_le_pi assms)
+qed
+
+text \<open>The 1990s definition of argument coincides with the more recent one\<close>
+lemma Arg_definition_equivalence:
+  shows "arg z = (if z = 0 then 0 else Im (Ln z))"
+  by (simp add: Arg_eq_Im_Ln arg_zero)

definition\<^marker>\<open>tag important\<close> Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
```
```--- a/src/HOL/Analysis/Derivative.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Mon Jun 28 15:05:46 2021 +0100
@@ -1870,7 +1870,7 @@
\<Longrightarrow> vector_derivative (\<lambda>x. f x + g x) (at a) = vector_derivative f (at a) + vector_derivative g (at a)"

-lemma vector_derivative_diff_at [simp]:
+lemma vector_derivative_diff_at [simp,derivative_intros]:
"\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
\<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])```
```--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Jun 28 15:05:46 2021 +0100
@@ -1465,6 +1465,12 @@
using bounded_closed_imp_seq_compact compact_eq_seq_compact_metric compact_imp_bounded compact_imp_closed
by auto

+lemma bounded_infinite_imp_islimpt:
+  fixes S :: "'a::heine_borel set"
+  assumes "T \<subseteq> S" "bounded S" "infinite T"
+  obtains x where "x islimpt S"
+  by (meson assms closed_limpt compact_eq_Bolzano_Weierstrass compact_eq_bounded_closed islimpt_subset)
+
lemma compact_Inter:
fixes \<F> :: "'a :: heine_borel set set"
assumes com: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" and "\<F> \<noteq> {}"```
```--- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Jun 28 15:05:46 2021 +0100
@@ -1240,6 +1240,22 @@
qed
qed

+lemma collinear_iff_Reals: "collinear {0::complex,w,z} \<longleftrightarrow> z/w \<in> \<real>"
+proof
+  show "z/w \<in> \<real> \<Longrightarrow> collinear {0,w,z}"
+    by (metis Reals_cases collinear_lemma nonzero_divide_eq_eq scaleR_conv_of_real)
+qed (auto simp: collinear_lemma scaleR_conv_of_real)
+
+lemma collinear_scaleR_iff: "collinear {0, \<alpha> *\<^sub>R w, \<beta> *\<^sub>R z} \<longleftrightarrow> collinear {0,w,z} \<or> \<alpha>=0 \<or> \<beta>=0"
+  (is "?lhs = ?rhs")
+proof (cases "\<alpha>=0 \<or> \<beta>=0")
+  case False
+  then have "(\<exists>c. \<beta> *\<^sub>R z = (c * \<alpha>) *\<^sub>R w) = (\<exists>c. z = c *\<^sub>R w)"
+    by (metis mult.commute scaleR_scaleR vector_fraction_eq_iff)
+  then show ?thesis
+    by (auto simp add: collinear_lemma)
+qed (auto simp: collinear_lemma)
+
lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
proof (cases "x=0")
case True
@@ -1262,6 +1278,16 @@
qed
qed

+lemma norm_triangle_eq_imp_collinear:
+  fixes x y :: "'a::real_inner"
+  assumes "norm (x + y) = norm x + norm y"
+  shows "collinear{0,x,y}"
+proof (cases "x = 0 \<or> y = 0")
+  case False
+  with assms show ?thesis
+    by (meson norm_cauchy_schwarz_abs_eq norm_cauchy_schwarz_equal norm_triangle_eq)
+qed (use collinear_lemma in blast)
+

subsection\<open>Properties of special hyperplanes\<close>
```
```--- a/src/HOL/Deriv.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Deriv.thy	Mon Jun 28 15:05:46 2021 +0100
@@ -813,6 +813,38 @@
lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..

+lemma field_derivative_lim_unique:
+  assumes f: "(f has_field_derivative df) (at z)"
+      and s: "s \<longlonglongrightarrow> 0"  "\<And>n. s n \<noteq> 0"
+      and a: "(\<lambda>n. (f (z + s n) - f z) / s n) \<longlonglongrightarrow> a"
+    shows "df = a"
+proof (rule ccontr)
+  assume "df \<noteq> a"
+  obtain q where qpos: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> q \<epsilon> > 0"
+             and q: "\<And>\<epsilon> y. \<lbrakk>\<epsilon> > 0; y \<noteq> z; dist y z < q \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f y - f z) / (y - z)) df < \<epsilon>"
+    using f unfolding LIM_def has_field_derivative_iff by metis
+  obtain NA where NA: "\<And>\<epsilon> n. \<lbrakk>\<epsilon> > 0; n \<ge> NA \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f (z + s n) - f z) / s n) a < \<epsilon>"
+    using a unfolding LIMSEQ_def by metis
+  obtain NB where NB: "\<And>\<epsilon> n. \<lbrakk>\<epsilon> > 0; n \<ge> NB \<epsilon>\<rbrakk> \<Longrightarrow> norm (s n) < \<epsilon>"
+    using s unfolding LIMSEQ_def by (metis norm_conv_dist)
+  have df: "\<And>\<epsilon> n. \<epsilon> > 0 \<Longrightarrow> \<lbrakk>0 < \<epsilon>; norm (s n) < q \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f (z + s n) - f z) / s n) df < \<epsilon>"
+  define \<delta> where "\<delta> \<equiv> dist df a / 2"
+  with \<open>df \<noteq> a\<close> have "\<delta> > 0" and \<delta>: "\<delta>+\<delta> \<le> dist df a"
+    by auto
+  define N where "N \<equiv> max (NA \<delta>) (NB (q \<delta>))"
+  then have "norm (s N) < q \<delta>"
+    by (simp add: NB \<open>\<delta> > 0\<close> qpos)
+  then have "dist ((f (z + s N) - f z) / s N) df < \<delta>"
+    by (simp add: \<open>0 < \<delta>\<close> df)
+  moreover have "dist ((f (z + s N) - f z) / s N) a < \<delta>"
+    using NA N_def \<open>0 < \<delta>\<close> by force
+  ultimately have "dist df a < dist df a"
+    by (smt (verit, ccfv_SIG) \<delta> dist_commute dist_triangle)
+  then show False ..
+qed
+
lemma mult_commute_abs: "(\<lambda>x. x * c) = (*) c"
for c :: "'a::ab_semigroup_mult"
@@ -1194,14 +1226,40 @@
DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
by (rule has_field_derivative_cong_ev) simp_all

+lemma DERIV_mirror: "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x)) x :> - y)"
+  for f :: "real \<Rightarrow> real" and x y :: real
+  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
+      tendsto_minus_cancel_left field_simps conj_commute)
+
lemma DERIV_shift:
"(f has_field_derivative y) (at (x + z)) = ((\<lambda>x. f (x + z)) has_field_derivative y) (at x)"

-lemma DERIV_mirror: "(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x)) x :> - y)"
-  for f :: "real \<Rightarrow> real" and x y :: real
-  by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
-      tendsto_minus_cancel_left field_simps conj_commute)
+lemma DERIV_at_within_shift_lemma:
+  assumes "(f has_field_derivative y) (at (z+x) within (+) z ` S)"
+  shows "(f \<circ> (+)z has_field_derivative y) (at x within S)"
+proof -
+  have "((+)z has_field_derivative 1) (at x within S)"
+    by (rule derivative_eq_intros | simp)+
+  with assms DERIV_image_chain show ?thesis
+    by (metis mult.right_neutral)
+qed
+
+lemma DERIV_at_within_shift:
+  "(f has_field_derivative y) (at (z+x) within (+) z ` S) \<longleftrightarrow>
+   ((\<lambda>x. f (z+x)) has_field_derivative y) (at x within S)"   (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using DERIV_at_within_shift_lemma unfolding o_def by blast
+next
+  have [simp]: "(\<lambda>x. x - z) ` (+) z ` S = S"
+    by force
+  assume R: ?rhs
+  have "(f \<circ> (+) z \<circ> (+) (- z) has_field_derivative y) (at (z + x) within (+) z ` S)"
+    by (rule DERIV_at_within_shift_lemma) (use R in \<open>simp add: o_def\<close>)
+  then show ?lhs
+qed

lemma floor_has_real_derivative:
fixes f :: "real \<Rightarrow> 'a::{floor_ceiling,order_topology}"```
```--- a/src/HOL/Limits.thy	Sat Jun 26 20:55:43 2021 +0200
+++ b/src/HOL/Limits.thy	Mon Jun 28 15:05:46 2021 +0100
@@ -1777,7 +1777,15 @@
qed

lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
- by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
+  by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
+
+lemma filterlim_inverse_at_top_iff:
+  "eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> (LIM x F. inverse (f x) :> at_top) \<longleftrightarrow> (f \<longlongrightarrow> (0 :: real)) F"
+  by (auto dest: tendsto_inverse_0_at_top filterlim_inverse_at_top)
+
+lemma filterlim_at_top_iff_inverse_0:
+  "eventually (\<lambda>x. 0 < f x) F \<Longrightarrow> (LIM x F. f x :> at_top) \<longleftrightarrow> ((inverse \<circ> f) \<longlongrightarrow> (0 :: real)) F"
+  using filterlim_inverse_at_top_iff [of "inverse \<circ> f"] by auto

lemma real_tendsto_divide_at_top:
fixes c::"real"```