--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri May 25 23:11:06 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat May 26 08:36:19 2018 +0100
@@ -91,14 +91,14 @@
(infixr "piecewise'_differentiable'_on" 50)
where "f piecewise_differentiable_on i \<equiv>
continuous_on i f \<and>
- (\<exists>s. finite s \<and> (\<forall>x \<in> i - s. f differentiable (at x within i)))"
+ (\<exists>S. finite S \<and> (\<forall>x \<in> i - S. f differentiable (at x within i)))"
lemma piecewise_differentiable_on_imp_continuous_on:
- "f piecewise_differentiable_on s \<Longrightarrow> continuous_on s f"
+ "f piecewise_differentiable_on S \<Longrightarrow> continuous_on S f"
by (simp add: piecewise_differentiable_on_def)
lemma piecewise_differentiable_on_subset:
- "f piecewise_differentiable_on s \<Longrightarrow> t \<le> s \<Longrightarrow> f piecewise_differentiable_on t"
+ "f piecewise_differentiable_on S \<Longrightarrow> T \<le> S \<Longrightarrow> f piecewise_differentiable_on T"
using continuous_on_subset
unfolding piecewise_differentiable_on_def
apply safe
@@ -113,29 +113,29 @@
done
lemma differentiable_imp_piecewise_differentiable:
- "(\<And>x. x \<in> s \<Longrightarrow> f differentiable (at x within s))
- \<Longrightarrow> f piecewise_differentiable_on s"
+ "(\<And>x. x \<in> S \<Longrightarrow> f differentiable (at x within S))
+ \<Longrightarrow> f piecewise_differentiable_on S"
by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def
intro: differentiable_within_subset)
-lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on s"
+lemma piecewise_differentiable_const [iff]: "(\<lambda>x. z) piecewise_differentiable_on S"
by (simp add: differentiable_imp_piecewise_differentiable)
lemma piecewise_differentiable_compose:
- "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on (f ` s);
- \<And>x. finite (s \<inter> f-`{x})\<rbrakk>
- \<Longrightarrow> (g o f) piecewise_differentiable_on s"
+ "\<lbrakk>f piecewise_differentiable_on S; g piecewise_differentiable_on (f ` S);
+ \<And>x. finite (S \<inter> f-`{x})\<rbrakk>
+ \<Longrightarrow> (g o f) piecewise_differentiable_on S"
apply (simp add: piecewise_differentiable_on_def, safe)
apply (blast intro: continuous_on_compose2)
apply (rename_tac A B)
- apply (rule_tac x="A \<union> (\<Union>x\<in>B. s \<inter> f-`{x})" in exI)
+ apply (rule_tac x="A \<union> (\<Union>x\<in>B. S \<inter> f-`{x})" in exI)
apply (blast intro!: differentiable_chain_within)
done
lemma piecewise_differentiable_affine:
fixes m::real
- assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` s)"
- shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on s"
+ assumes "f piecewise_differentiable_on ((\<lambda>x. m *\<^sub>R x + c) ` S)"
+ shows "(f o (\<lambda>x. m *\<^sub>R x + c)) piecewise_differentiable_on S"
proof (cases "m = 0")
case True
then show ?thesis
@@ -156,13 +156,13 @@
"a \<le> c" "c \<le> b" "f c = g c"
shows "(\<lambda>x. if x \<le> c then f x else g x) piecewise_differentiable_on {a..b}"
proof -
- obtain s t where st: "finite s" "finite t"
- "\<forall>x\<in>{a..c} - s. f differentiable at x within {a..c}"
- "\<forall>x\<in>{c..b} - t. g differentiable at x within {c..b}"
+ obtain S T where st: "finite S" "finite T"
+ and fd: "\<And>x. x \<in> {a..c} - S \<Longrightarrow> f differentiable at x within {a..c}"
+ and gd: "\<And>x. x \<in> {c..b} - T \<Longrightarrow> g differentiable at x within {c..b}"
using assms
by (auto simp: piecewise_differentiable_on_def)
- have finabc: "finite ({a,b,c} \<union> (s \<union> t))"
- by (metis \<open>finite s\<close> \<open>finite t\<close> finite_Un finite_insert finite.emptyI)
+ have finabc: "finite ({a,b,c} \<union> (S \<union> T))"
+ by (metis \<open>finite S\<close> \<open>finite T\<close> finite_Un finite_insert finite.emptyI)
have "continuous_on {a..c} f" "continuous_on {c..b} g"
using assms piecewise_differentiable_on_def by auto
then have "continuous_on {a..b} (\<lambda>x. if x \<le> c then f x else g x)"
@@ -172,43 +172,35 @@
by (force simp: ivl_disj_un_two_touch)
moreover
{ fix x
- assume x: "x \<in> {a..b} - ({a,b,c} \<union> (s \<union> t))"
+ assume x: "x \<in> {a..b} - ({a,b,c} \<union> (S \<union> T))"
have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg")
proof (cases x c rule: le_cases)
case le show ?diff_fg
- proof (rule differentiable_transform_within [where d = "dist x c" and f = f])
- have "f differentiable at x within ({a<..<c} - s)"
- apply (rule differentiable_at_withinI)
- using x le st
- by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real le st(3) x)
- moreover have "open ({a<..<c} - s)"
- by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
- ultimately show "f differentiable at x within {a..b}"
- using x le by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
+ proof (rule differentiable_transform_within [where d = "dist x c"])
+ have "f differentiable at x"
+ using x le fd [of x] at_within_interior [of x "{a..c}"] by simp
+ then show "f differentiable at x within {a..b}"
+ by (simp add: differentiable_at_withinI)
qed (use x le st dist_real_def in auto)
next
case ge show ?diff_fg
- proof (rule differentiable_transform_within [where d = "dist x c" and f = g])
- have "g differentiable at x within ({c<..<b} - t)"
- apply (rule differentiable_at_withinI)
- using x ge st
- by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real)
- moreover have "open ({c<..<b} - t)"
- by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
- ultimately show "g differentiable at x within {a..b}"
- using x ge by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
+ proof (rule differentiable_transform_within [where d = "dist x c"])
+ have "g differentiable at x"
+ using x ge gd [of x] at_within_interior [of x "{c..b}"] by simp
+ then show "g differentiable at x within {a..b}"
+ by (simp add: differentiable_at_withinI)
qed (use x ge st dist_real_def in auto)
qed
}
- then have "\<exists>s. finite s \<and>
- (\<forall>x\<in>{a..b} - s. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})"
+ then have "\<exists>S. finite S \<and>
+ (\<forall>x\<in>{a..b} - S. (\<lambda>x. if x \<le> c then f x else g x) differentiable at x within {a..b})"
by (meson finabc)
ultimately show ?thesis
by (simp add: piecewise_differentiable_on_def)
qed
lemma piecewise_differentiable_neg:
- "f piecewise_differentiable_on s \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on s"
+ "f piecewise_differentiable_on S \<Longrightarrow> (\<lambda>x. -(f x)) piecewise_differentiable_on S"
by (auto simp: piecewise_differentiable_on_def continuous_on_minus)
lemma piecewise_differentiable_add:
@@ -216,11 +208,11 @@
"g piecewise_differentiable_on i"
shows "(\<lambda>x. f x + g x) piecewise_differentiable_on i"
proof -
- obtain s t where st: "finite s" "finite t"
- "\<forall>x\<in>i - s. f differentiable at x within i"
- "\<forall>x\<in>i - t. g differentiable at x within i"
+ obtain S T where st: "finite S" "finite T"
+ "\<forall>x\<in>i - S. f differentiable at x within i"
+ "\<forall>x\<in>i - T. g differentiable at x within i"
using assms by (auto simp: piecewise_differentiable_on_def)
- then have "finite (s \<union> t) \<and> (\<forall>x\<in>i - (s \<union> t). (\<lambda>x. f x + g x) differentiable at x within i)"
+ then have "finite (S \<union> T) \<and> (\<forall>x\<in>i - (S \<union> T). (\<lambda>x. f x + g x) differentiable at x within i)"
by auto
moreover have "continuous_on i f" "continuous_on i g"
using assms piecewise_differentiable_on_def by auto
@@ -229,8 +221,8 @@
qed
lemma piecewise_differentiable_diff:
- "\<lbrakk>f piecewise_differentiable_on s; g piecewise_differentiable_on s\<rbrakk>
- \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on s"
+ "\<lbrakk>f piecewise_differentiable_on S; g piecewise_differentiable_on S\<rbrakk>
+ \<Longrightarrow> (\<lambda>x. f x - g x) piecewise_differentiable_on S"
unfolding diff_conv_add_uminus
by (metis piecewise_differentiable_add piecewise_differentiable_neg)
@@ -249,33 +241,63 @@
done
lemma piecewise_differentiable_D1:
- "(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}"
- apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D1)
- apply (rule_tac x="insert 1 ((( * )2)`s)" in exI)
- apply simp
- apply (intro ballI)
- apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (( * )(inverse 2))"
- in differentiable_transform_within)
- apply (auto simp: dist_real_def joinpaths_def)
- apply (rule differentiable_chain_within derivative_intros | simp)+
- apply (rule differentiable_subset)
- apply (force simp:)+
- done
+ assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}"
+ shows "g1 piecewise_differentiable_on {0..1}"
+proof -
+ obtain S where cont: "continuous_on {0..1} g1" and "finite S"
+ and S: "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g1 +++ g2 differentiable at x within {0..1}"
+ using assms unfolding piecewise_differentiable_on_def
+ by (blast dest!: continuous_on_joinpaths_D1)
+ show ?thesis
+ unfolding piecewise_differentiable_on_def
+ proof (intro exI conjI ballI cont)
+ show "finite (insert 1 ((( * )2) ` S))"
+ by (simp add: \<open>finite S\<close>)
+ show "g1 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 1 (( * ) 2 ` S)" for x
+ proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within)
+ have "g1 +++ g2 differentiable at (x / 2) within {0..1 / 2}"
+ by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
+ then show "g1 +++ g2 \<circ> ( * ) (inverse 2) differentiable at x within {0..1}"
+ by (auto intro: differentiable_chain_within)
+ qed (use that in \<open>auto simp: joinpaths_def\<close>)
+ qed
+qed
lemma piecewise_differentiable_D2:
- "\<lbrakk>(g1 +++ g2) piecewise_differentiable_on {0..1}; pathfinish g1 = pathstart g2\<rbrakk>
- \<Longrightarrow> g2 piecewise_differentiable_on {0..1}"
- apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D2)
- apply (rule_tac x="insert 0 ((\<lambda>x. 2*x-1)`s)" in exI)
- apply simp
- apply (intro ballI)
- apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)"
- in differentiable_transform_within)
- apply (auto simp: dist_real_def joinpaths_def abs_if field_simps split: if_split_asm)
- apply (rule differentiable_chain_within derivative_intros | simp)+
- apply (rule differentiable_subset)
- apply (force simp: divide_simps)+
- done
+ assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" and eq: "pathfinish g1 = pathstart g2"
+ shows "g2 piecewise_differentiable_on {0..1}"
+proof -
+ have [simp]: "g1 1 = g2 0"
+ using eq by (simp add: pathfinish_def pathstart_def)
+ obtain S where cont: "continuous_on {0..1} g2" and "finite S"
+ and S: "\<And>x. x \<in> {0..1} - S \<Longrightarrow> g1 +++ g2 differentiable at x within {0..1}"
+ using assms unfolding piecewise_differentiable_on_def
+ by (blast dest!: continuous_on_joinpaths_D2)
+ show ?thesis
+ unfolding piecewise_differentiable_on_def
+ proof (intro exI conjI ballI cont)
+ show "finite (insert 0 ((\<lambda>x. 2*x-1)`S))"
+ by (simp add: \<open>finite S\<close>)
+ show "g2 differentiable at x within {0..1}" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1)`S)" for x
+ proof (rule_tac d="dist ((x+1)/2) (1/2)" in differentiable_transform_within)
+ have x2: "(x + 1) / 2 \<notin> S"
+ using that
+ apply (clarsimp simp: image_iff)
+ by (metis add.commute add_diff_cancel_left' mult_2 real_sum_of_halves)
+ have "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
+ by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+
+ then show "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
+ by (auto intro: differentiable_chain_within)
+ show "(g1 +++ g2 \<circ> (\<lambda>x. (x + 1) / 2)) x' = g2 x'" if "x' \<in> {0..1}" "dist x' x < dist ((x + 1) / 2) (1 / 2)" for x'
+ proof -
+ have [simp]: "(2*x'+2)/2 = x'+1"
+ by (simp add: divide_simps)
+ show ?thesis
+ using that by (auto simp: joinpaths_def)
+ qed
+ qed (use that in \<open>auto simp: joinpaths_def\<close>)
+ qed
+qed
subsubsection\<open>The concept of continuously differentiable\<close>
@@ -590,7 +612,7 @@
apply (simp_all add: dist_real_def joinpaths_def)
apply (auto simp: dist_real_def joinpaths_def field_simps)
apply (rule differentiable_chain_at derivative_intros | force)+
- apply (drule_tac x= "(x + 1) / 2" in bspec, force simp: divide_simps)
+ apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps)
apply assumption
done
have [simp]: "vector_derivative (g2 \<circ> (\<lambda>x. 2*x-1)) (at ((x+1)/2)) = 2 *\<^sub>R vector_derivative g2 (at x)"
@@ -604,7 +626,7 @@
apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric]
intro!: g2D differentiable_chain_at)
done
- have [simp]: "((\<lambda>x. (x + 1) / 2) ` ({0..1} - insert 0 ((\<lambda>x. 2 * x - 1) ` s))) = ({1/2..1} - insert (1/2) s)"
+ have [simp]: "((\<lambda>x. (x+1) / 2) ` ({0..1} - insert 0 ((\<lambda>x. 2 * x - 1) ` s))) = ({1/2..1} - insert (1/2) s)"
apply (simp add: image_set_diff inj_on_def image_image)
apply (auto simp: image_affinity_atLeastAtMost_div add_divide_distrib)
done
--- a/src/HOL/Analysis/Complex_Transcendental.thy Fri May 25 23:11:06 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sat May 26 08:36:19 2018 +0100
@@ -1796,8 +1796,7 @@
lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
apply (simp add: powr_def)
- using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
- by auto
+ using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def by auto
lemma powr_complexpow [simp]:
fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
@@ -1817,10 +1816,14 @@
qed simp
lemma powr_real_real:
- "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
- apply (simp add: powr_def)
- by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
- exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
+ assumes "w \<in> \<real>" "z \<in> \<real>" "0 < Re w"
+ shows "w powr z = exp(Re z * ln(Re w))"
+proof -
+ have "w \<noteq> 0"
+ using assms by auto
+ with assms show ?thesis
+ by (simp add: powr_def Ln_Reals_eq of_real_exp)
+qed
lemma powr_of_real:
fixes x::real and y::real
@@ -1874,13 +1877,14 @@
shows "((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
proof (cases "z=0")
case False
- with assms show ?thesis
- apply (simp add: powr_def)
- apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
- apply (auto simp: dist_complex_def)
- apply (intro derivative_eq_intros | simp)+
- apply (simp add: field_simps exp_diff)
- done
+ show ?thesis
+ unfolding powr_def
+ proof (rule DERIV_transform_at)
+ show "((\<lambda>z. exp (s * Ln z)) has_field_derivative s * (if z = 0 then 0 else exp ((s - 1) * Ln z)))
+ (at z)"
+ apply (intro derivative_eq_intros | simp add: assms)+
+ by (simp add: False divide_complex_def exp_diff left_diff_distrib')
+ qed (use False in auto)
qed (use assms in auto)
declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
@@ -1908,12 +1912,12 @@
\<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within s)"
by simp
also have "... \<longleftrightarrow> ((\<lambda>z. g z ^ nat n) has_field_derivative dd') (at z within s)"
- apply (rule has_field_derivative_cong_eventually)
- subgoal unfolding eventually_at
+ proof (rule has_field_derivative_cong_eventually)
+ show "\<forall>\<^sub>F x in at z within s. g x powr of_int n = g x ^ nat n"
+ unfolding eventually_at
apply (rule exI[where x=e])
using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute)
- subgoal using powr_of_int \<open>g z\<noteq>0\<close> that by simp
- done
+ qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
also have "..." unfolding dd'_def using gderiv that
by (auto intro!: derivative_eq_intros)
finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within s)" .
@@ -1933,17 +1937,20 @@
\<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within s)"
by simp
also have "... \<longleftrightarrow> ((\<lambda>z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within s)"
- apply (rule has_field_derivative_cong_eventually)
- subgoal unfolding eventually_at
+ proof (rule has_field_derivative_cong_eventually)
+ show "\<forall>\<^sub>F x in at z within s. g x powr of_int n = inverse (g x ^ nat (- n))"
+ unfolding eventually_at
apply (rule exI[where x=e])
using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute)
- subgoal using powr_of_int \<open>g z\<noteq>0\<close> that by simp
- done
- also have "..." unfolding dd'_def using gderiv that \<open>g z\<noteq>0\<close>
- apply (auto intro!: derivative_eq_intros)
- apply (simp add:divide_simps power_add[symmetric])
- apply (subgoal_tac "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)")
- by auto
+ qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
+ also have "..."
+ proof -
+ have "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)"
+ by auto
+ then show ?thesis
+ unfolding dd'_def using gderiv that \<open>g z\<noteq>0\<close>
+ by (auto intro!: derivative_eq_intros simp add:divide_simps power_add[symmetric])
+ qed
finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within s)" .
then show ?thesis unfolding dd_def by simp
qed
@@ -1990,15 +1997,11 @@
assumes "f holomorphic_on s"
shows "(\<lambda>z. w powr (f z)) holomorphic_on s"
proof (cases "w = 0")
- case True
- then show ?thesis
- by simp
-next
case False
with assms show ?thesis
unfolding holomorphic_on_def field_differentiable_def
by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
-qed
+qed simp
lemma holomorphic_on_divide_gen [holomorphic_intros]:
assumes f: "f holomorphic_on s" and g: "g holomorphic_on s" and 0: "\<And>z z'. \<lbrakk>z \<in> s; z' \<in> s\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0"
@@ -2019,14 +2022,7 @@
lemma norm_powr_real_powr:
"w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
- by (cases "w = 0")
- (auto simp add: norm_powr_real powr_def Im_Ln_eq_0
- complex_is_Real_iff in_Reals_norm complex_eq_iff)
-
-lemma tendsto_ln_complex [tendsto_intros]:
- assumes "(f \<longlongrightarrow> a) F" "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
- shows "((\<lambda>z. ln (f z :: complex)) \<longlongrightarrow> ln a) F"
- using tendsto_compose[OF continuous_at_Ln[of a, unfolded isCont_def] assms(1)] assms(2) by simp
+ by (metis dual_order.order_iff_strict norm_powr_real norm_zero of_real_0 of_real_Re powr_def)
lemma tendsto_powr_complex:
fixes f g :: "_ \<Rightarrow> complex"
@@ -2095,16 +2091,9 @@
lemma tendsto_powr_complex' [tendsto_intros]:
fixes f g :: "_ \<Rightarrow> complex"
- assumes fz: "a \<notin> \<real>\<^sub>\<le>\<^sub>0 \<or> (a = 0 \<and> Re b > 0)"
- assumes fg: "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
+ assumes "a \<notin> \<real>\<^sub>\<le>\<^sub>0 \<or> (a = 0 \<and> Re b > 0)" and "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
shows "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
-proof (cases "a = 0")
- case True
- with assms show ?thesis by (auto intro!: tendsto_powr_complex_0)
-next
- case False
- with assms show ?thesis by (auto intro!: tendsto_powr_complex elim!: nonpos_Reals_cases)
-qed
+ using assms tendsto_powr_complex tendsto_powr_complex_0 by fastforce
lemma tendsto_neg_powr_complex_of_real:
assumes "filterlim f at_top F" and "Re s < 0"
@@ -2185,12 +2174,13 @@
using e assms by simp
with x have "x > 0"
by linarith
- then show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
- using e assms x
- apply (auto simp: field_simps)
- apply (rule_tac y = "e * (x\<^sup>2 * (Re s)\<^sup>2)" in le_less_trans)
- apply (auto simp: power2_eq_square field_simps add_pos_pos)
- done
+ then have "x * 2 \<le> e * (x\<^sup>2 * (Re s)\<^sup>2)"
+ using e assms x by (auto simp: power2_eq_square field_simps)
+ also have "... < e * (2 + (x * (Re s * 2) + x\<^sup>2 * (Re s)\<^sup>2))"
+ using e assms \<open>x > 0\<close>
+ by (auto simp: power2_eq_square field_simps add_pos_pos)
+ finally show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
+ by (auto simp: algebra_simps)
qed
then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < 1 + (Re s * x) + (1/2) * (Re s * x)^2"
using e by (simp add: field_simps)
@@ -2217,8 +2207,7 @@
shows "((\<lambda>n. ln n / (n powr s)) \<longlongrightarrow> 0) sequentially"
using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms
apply (subst filterlim_sequentially_Suc [symmetric])
- apply (simp add: lim_sequentially dist_norm
- Ln_Reals_eq norm_powr_real_powr norm_divide)
+ apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide)
done
lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
@@ -2414,14 +2403,15 @@
"continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
case True
- then have "Im z = 0" "Re z < 0 \<or> z = 0"
- using cnj.code complex_cnj_zero_iff by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
- then show ?thesis
+ have *: "\<And>e. \<lbrakk>0 < e\<rbrakk>
+ \<Longrightarrow> \<forall>x'\<in>\<real> \<inter> {w. 0 \<le> Re w}. cmod x' < e^2 \<longrightarrow> cmod (csqrt x') < e"
+ by (auto simp: Reals_def real_less_lsqrt)
+ have "Im z = 0" "Re z < 0 \<or> z = 0"
+ using True cnj.code complex_cnj_zero_iff by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
+ with * show ?thesis
apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
- apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
- apply (rule_tac x="e^2" in exI)
- apply (auto simp: Reals_def)
- by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
+ apply (auto simp: continuous_within_eps_delta)
+ using zero_less_power by blast
next
case False
then show ?thesis by (blast intro: continuous_within_csqrt)
@@ -2514,8 +2504,8 @@
proof -
have nz0: "1 + \<i>*z \<noteq> 0"
using assms
- by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add imaginary_unit.simps
- less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
+ by (metis abs_one add_diff_cancel_left' complex_i_mult_minus diff_0 i_squared imaginary_unit.simps
+ less_asym neg_equal_iff_equal)
have "z \<noteq> -\<i>" using assms
by auto
then have zz: "1 + z * z \<noteq> 0"
@@ -2543,11 +2533,10 @@
done
show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
unfolding Arctan_def scaleR_conv_of_real
- apply (rule DERIV_cong)
apply (intro derivative_eq_intros | simp add: nz0 *)+
using nz0 nz1 zz
- apply (simp add: divide_simps power2_eq_square)
- apply (auto simp: algebra_simps)
+ apply (simp add: algebra_simps divide_simps power2_eq_square)
+ apply algebra
done
qed
@@ -2594,8 +2583,8 @@
proof
fix n
have "ereal (norm (h u n) / norm (h u (Suc n))) =
- ereal (inverse (norm u)^2) * ereal ((of_nat (2*Suc n+1) / of_nat (Suc n)) /
- (of_nat (2*Suc n-1) / of_nat (Suc n)))"
+ ereal (inverse (norm u)^2) * ereal (((2*Suc n+1) / (Suc n)) /
+ ((2*Suc n-1) / (Suc n)))"
by (simp add: h_def norm_mult norm_power norm_divide divide_simps
power2_eq_square eval_nat_numeral del: of_nat_add of_nat_Suc)
also have "of_nat (2*Suc n+1) / of_nat (Suc n) = (2::real) + inverse (real (Suc n))"
@@ -2641,10 +2630,10 @@
finally have "(G has_field_derivative inverse (1 + u\<^sup>2)) (at u)" .
from DERIV_diff[OF has_field_derivative_Arctan this] Im_u u
show "((\<lambda>u. Arctan u - G u) has_field_derivative 0) (at u within ball 0 1)"
- by (simp_all add: dist_0_norm at_within_open[OF _ open_ball])
+ by (simp_all add: at_within_open[OF _ open_ball])
qed simp_all
- then obtain c where c: "\<And>u. norm u < 1 \<Longrightarrow> Arctan u - G u = c" by (auto simp: dist_0_norm)
- from this[of 0] have "c = 0" by (simp add: G_def g_def powser_zero)
+ then obtain c where c: "\<And>u. norm u < 1 \<Longrightarrow> Arctan u - G u = c" by auto
+ from this[of 0] have "c = 0" by (simp add: G_def g_def)
with c z have "Arctan z = G z" by simp
with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff)
thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
@@ -2690,14 +2679,19 @@
by simp
lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
- unfolding Arctan_def divide_complex_def
- apply (simp add: complex_eq_iff)
- apply (rule norm_exp_imaginary)
- apply (subst exp_Ln, auto)
- apply (simp_all add: cmod_def complex_eq_iff)
- apply (auto simp: divide_simps)
- apply (metis power_one sum_power2_eq_zero_iff zero_neq_one, algebra)
- done
+proof -
+ have ne: "1 + x\<^sup>2 \<noteq> 0"
+ by (metis power_one sum_power2_eq_zero_iff zero_neq_one)
+ have "Re (Ln ((1 - \<i> * x) * inverse (1 + \<i> * x))) = 0"
+ apply (rule norm_exp_imaginary)
+ apply (subst exp_Ln)
+ using ne apply (simp_all add: cmod_def complex_eq_iff)
+ apply (auto simp: divide_simps)
+ apply algebra
+ done
+ then show ?thesis
+ unfolding Arctan_def divide_complex_def by (simp add: complex_eq_iff)
+qed
lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))"
proof (rule arctan_unique)
@@ -2796,15 +2790,13 @@
lemma abs_arctan_le:
fixes x::real shows "\<bar>arctan x\<bar> \<le> \<bar>x\<bar>"
proof -
- { fix w::complex and z::complex
- assume *: "w \<in> \<real>" "z \<in> \<real>"
- have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)"
- apply (rule field_differentiable_bound [OF convex_Reals, of Arctan _ 1])
- apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
- apply (force simp add: Reals_def)
- apply (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
- using * by auto
- }
+ have 1: "\<And>x. x \<in> \<real> \<Longrightarrow> cmod (inverse (1 + x\<^sup>2)) \<le> 1"
+ by (simp add: norm_divide divide_simps in_Reals_norm complex_is_Real_iff power2_eq_square)
+ have "cmod (Arctan w - Arctan z) \<le> 1 * cmod (w-z)" if "w \<in> \<real>" "z \<in> \<real>" for w z
+ apply (rule field_differentiable_bound [OF convex_Reals, of Arctan _ 1])
+ apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan])
+ using 1 that apply (auto simp: Reals_def)
+ done
then have "cmod (Arctan (of_real x) - Arctan 0) \<le> 1 * cmod (of_real x -0)"
using Reals_0 Reals_of_real by blast
then show ?thesis
@@ -2826,15 +2818,14 @@
"arctan x \<le> (\<Sum>k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))"
proof -
have tendsto_zero: "?a \<longlonglongrightarrow> 0"
- using assms
- apply -
- apply (rule tendsto_eq_rhs[where x="0 * 0"])
- subgoal by (intro tendsto_mult real_tendsto_divide_at_top)
+ proof (rule tendsto_eq_rhs)
+ show "(\<lambda>k. 1 / real (k * 2 + 1) * x ^ (k * 2 + 1)) \<longlonglongrightarrow> 0 * 0"
+ using assms
+ by (intro tendsto_mult real_tendsto_divide_at_top)
(auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real
intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially
- tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top)
- subgoal by simp
- done
+ tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top)
+ qed simp
have nonneg: "0 \<le> ?a n" for n
by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms)
have le: "?a (Suc n) \<le> ?a n" for n
@@ -2849,8 +2840,7 @@
subsection \<open>Bounds on pi using real arctangent\<close>
lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)"
- using machin
- by simp
+ using machin by simp
lemma pi_approx: "3.141592653588 \<le> pi" "pi \<le> 3.1415926535899"
unfolding pi_machin
@@ -2885,10 +2875,10 @@
lemma one_minus_z2_notin_nonpos_Reals:
assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
shows "1 - z\<^sup>2 \<notin> \<real>\<^sub>\<le>\<^sub>0"
- using assms
- apply (auto simp: complex_nonpos_Reals_iff Re_power2 Im_power2)
- using power2_less_0 [of "Im z"] apply force
- using abs_square_less_1 not_le by blast
+ using assms
+ apply (auto simp: complex_nonpos_Reals_iff Re_power2 Im_power2)
+ using power2_less_0 [of "Im z"] apply force
+ using abs_square_less_1 not_le by blast
lemma isCont_Arcsin_lemma:
assumes le0: "Re (\<i> * z + csqrt (1 - z\<^sup>2)) \<le> 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
@@ -2899,6 +2889,8 @@
using assms by (fastforce simp: cmod_def abs_square_less_1 [symmetric])
next
case False
+ have leim: "(cmod (1 - z\<^sup>2) + (1 - Re (z\<^sup>2))) / 2 \<le> (Im z)\<^sup>2"
+ using le0 sqrt_le_D by fastforce
have neq: "(cmod z)\<^sup>2 \<noteq> 1 + cmod (1 - z\<^sup>2)"
proof (clarsimp simp add: cmod_def)
assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 = 1 + sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
@@ -2908,12 +2900,8 @@
by (simp add: power2_eq_square algebra_simps)
qed
moreover have 2: "(Im z)\<^sup>2 = (1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2"
- using le0
- apply simp
- apply (drule sqrt_le_D)
- using cmod_power2 [of z] norm_triangle_ineq2 [of "z^2" 1]
- apply (simp add: norm_power Re_power2 norm_minus_commute [of 1])
- done
+ using leim cmod_power2 [of z] norm_triangle_ineq2 [of "z^2" 1]
+ by (simp add: norm_power Re_power2 norm_minus_commute [of 1])
ultimately show False
by (simp add: Re_power2 Im_power2 cmod_power2)
qed
@@ -2922,15 +2910,12 @@
assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
shows "isCont Arcsin z"
proof -
- have *: "\<i> * z + csqrt (1 - z\<^sup>2) \<notin> \<real>\<^sub>\<le>\<^sub>0"
+ have 1: "\<i> * z + csqrt (1 - z\<^sup>2) \<notin> \<real>\<^sub>\<le>\<^sub>0"
by (metis isCont_Arcsin_lemma assms complex_nonpos_Reals_iff)
+ have 2: "1 - z\<^sup>2 \<notin> \<real>\<^sub>\<le>\<^sub>0"
+ by (simp add: one_minus_z2_notin_nonpos_Reals assms)
show ?thesis
- using assms
- apply (simp add: Arcsin_def)
- apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
- apply (simp add: one_minus_z2_notin_nonpos_Reals assms)
- apply (rule *)
- done
+ using assms unfolding Arcsin_def by (intro isCont_Ln' isCont_csqrt' continuous_intros 1 2)
qed
lemma isCont_Arcsin' [simp]:
@@ -2982,10 +2967,7 @@
also have "... = - (\<i> * Ln (exp (\<i>*z)))"
by (simp add: field_simps power2_eq_square)
also have "... = z"
- apply (subst Complex_Transcendental.Ln_exp)
- using assms
- apply (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: if_split_asm)
- done
+ using assms by (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: if_split_asm)
finally show ?thesis .
qed
@@ -3003,21 +2985,15 @@
by (metis Arcsin_1 Arcsin_sin Im_complex_of_real Re_complex_of_real abs_of_nonneg of_real_minus pi_half_ge_zero power2_minus real_sqrt_abs sin_Arcsin sin_minus)
lemma has_field_derivative_Arcsin:
- assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+ assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
shows "(Arcsin has_field_derivative inverse(cos(Arcsin z))) (at z)"
-proof -
+proof -
have "(sin (Arcsin z))\<^sup>2 \<noteq> 1"
- using assms
- apply atomize
- apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
- apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
- by (metis abs_minus_cancel abs_one abs_power2 one_neq_neg_one)
+ using assms one_minus_z2_notin_nonpos_Reals by force
then have "cos (Arcsin z) \<noteq> 0"
by (metis diff_0_right power_zero_numeral sin_squared_eq)
then show ?thesis
- apply (rule has_field_derivative_inverse_basic [OF DERIV_sin _ _ open_ball [of z 1]])
- apply (auto intro: isCont_Arcsin assms)
- done
+ by (rule has_field_derivative_inverse_basic [OF DERIV_sin _ _ open_ball [of z 1]]) (auto intro: isCont_Arcsin assms)
qed
declare has_field_derivative_Arcsin [derivative_intros]
@@ -3049,13 +3025,11 @@
"Arccos \<equiv> \<lambda>z. -\<i> * Ln(z + \<i> * csqrt(1 - z\<^sup>2))"
lemma Arccos_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Im(z + \<i> * csqrt(1 - z\<^sup>2))"
- using Arcsin_range_lemma [of "-z"]
- by simp
+ using Arcsin_range_lemma [of "-z"] by simp
lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0"
using Arcsin_body_lemma [of z]
- by (metis complex_i_mult_minus diff_add_cancel minus_diff_eq minus_unique mult.assoc mult.left_commute
- power2_csqrt power2_eq_square zero_neq_one)
+ by (metis Arcsin_body_lemma complex_i_mult_minus diff_minus_eq_add power2_minus right_minus_eq)
lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))"
by (simp add: Arccos_def)
@@ -3158,7 +3132,7 @@
using Arccos_cos by blast
lemma Arccos_0 [simp]: "Arccos 0 = pi/2"
- by (rule Arccos_unique) (auto simp: of_real_numeral)
+ by (rule Arccos_unique) auto
lemma Arccos_1 [simp]: "Arccos 1 = 0"
by (rule Arccos_unique) auto
@@ -3170,19 +3144,15 @@
assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
shows "(Arccos has_field_derivative - inverse(sin(Arccos z))) (at z)"
proof -
- have "(cos (Arccos z))\<^sup>2 \<noteq> 1"
- using assms
- apply atomize
- apply (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
- apply (metis abs_minus_cancel abs_one abs_power2 numeral_One numeral_neq_neg_one)
- apply (metis left_minus less_irrefl power_one sum_power2_gt_zero_iff zero_neq_neg_one)
- done
+ have "x\<^sup>2 \<noteq> -1" for x::real
+ by (sos "((R<1 + (([~1] * A=0) + (R<1 * (R<1 * [x__]^2)))))")
+ with assms have "(cos (Arccos z))\<^sup>2 \<noteq> 1"
+ by (auto simp: complex_eq_iff Re_power2 Im_power2 abs_square_eq_1)
then have "- sin (Arccos z) \<noteq> 0"
by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square)
then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)"
- apply (rule has_field_derivative_inverse_basic [OF DERIV_cos _ _ open_ball [of z 1]])
- apply (auto intro: isCont_Arccos assms)
- done
+ by (rule has_field_derivative_inverse_basic [OF DERIV_cos _ _ open_ball [of z 1]])
+ (auto intro: isCont_Arccos assms)
then show ?thesis
by simp
qed