--- a/CONTRIBUTORS Thu Jan 07 16:50:52 2016 +0100
+++ b/CONTRIBUTORS Fri Jan 08 15:49:01 2016 +0100
@@ -16,6 +16,10 @@
The Generalised Binomial Theorem.
The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
most important properties.
+
+* Autumn 2015: Manuel Eberl, TUM
+ Proper definition of division (with remainder) for formal power series;
+ Euclidean Ring and GCD instance for formal power series.
* Autumn 2015: Florian Haftmann, TUM
Rewrite definitions for global interpretations and sublocale declarations.
--- a/NEWS Thu Jan 07 16:50:52 2016 +0100
+++ b/NEWS Fri Jan 08 15:49:01 2016 +0100
@@ -651,6 +651,9 @@
* Library/Periodic_Fun: a locale that provides convenient lemmas for
periodic functions.
+* Library/Formal_Power_Series: proper definition of division (with remainder)
+for formal power series; instances for Euclidean Ring and GCD.
+
* HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
* HOL-Statespace: command 'statespace' uses mandatory qualifier for
--- a/src/HOL/Library/Countable.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Library/Countable.thy Fri Jan 08 15:49:01 2016 +0100
@@ -7,7 +7,7 @@
section \<open>Encoding (almost) everything into natural numbers\<close>
theory Countable
-imports Old_Datatype Rat Nat_Bijection
+imports Old_Datatype "~~/src/HOL/Rat" Nat_Bijection
begin
subsection \<open>The class of countable types\<close>
--- a/src/HOL/Library/Countable_Set_Type.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Fri Jan 08 15:49:01 2016 +0100
@@ -72,7 +72,7 @@
interpretation lifting_syntax .
-lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp
+lift_definition bot_cset :: "'a cset" is "{}" parametric empty_transfer by simp
lift_definition less_eq_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> bool"
is subset_eq parametric subset_transfer .
@@ -81,7 +81,7 @@
where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a cset)"
lemma less_cset_transfer[transfer_rule]:
- assumes [transfer_rule]: "bi_unique A"
+ assumes [transfer_rule]: "bi_unique A"
shows "((pcr_cset A) ===> (pcr_cset A) ===> op =) op \<subset> op <"
unfolding less_cset_def[abs_def] psubset_eq[abs_def] by transfer_prover
@@ -201,7 +201,7 @@
lemmas csingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred]
lemmas csingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred]
lemmas csubset_csingletonD = subset_singletonD[Transfer.transferred]
-lemmas cDiff_single_cinsert = diff_single_insert[Transfer.transferred]
+lemmas cDiff_single_cinsert = Diff_single_insert[Transfer.transferred]
lemmas cdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred]
lemmas cUn_csingleton_iff = Un_singleton_iff[Transfer.transferred]
lemmas csingleton_cUn_iff = singleton_Un_iff[Transfer.transferred]
@@ -389,14 +389,14 @@
subsubsection \<open>\<open>cimage\<close>\<close>
lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> B = cimage f AA)"
-by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE)
+by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE)
subsubsection \<open>bounded quantification\<close>
lemma cBex_simps [simp, no_atp]:
- "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)"
+ "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)"
"\<And>A P Q. cBex A (\<lambda>x. P \<and> Q x) = (P \<and> cBex A Q)"
- "\<And>P. cBex cempty P = False"
+ "\<And>P. cBex cempty P = False"
"\<And>a B P. cBex (cinsert a B) P = (P a \<or> cBex B P)"
"\<And>A P f. cBex (cimage f A) P = cBex A (\<lambda>x. P (f x))"
"\<And>A P. (\<not> cBex A P) = cBall A (\<lambda>x. \<not> P x)"
@@ -498,7 +498,7 @@
lemma cInt_parametric [transfer_rule]:
"bi_unique A \<Longrightarrow> (rel_cset A ===> rel_cset A ===> rel_cset A) cInt cInt"
-unfolding rel_fun_def
+unfolding rel_fun_def
using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred]
by blast
--- a/src/HOL/Library/FSet.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Library/FSet.thy Fri Jan 08 15:49:01 2016 +0100
@@ -286,7 +286,7 @@
lemmas fsingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred]
lemmas fsingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred]
lemmas fsubset_fsingletonD = subset_singletonD[Transfer.transferred]
-lemmas fminus_single_finsert = diff_single_insert[Transfer.transferred]
+lemmas fminus_single_finsert = Diff_single_insert[Transfer.transferred]
lemmas fdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred]
lemmas funion_fsingleton_iff = Un_singleton_iff[Transfer.transferred]
lemmas fsingleton_funion_iff = singleton_Un_iff[Transfer.transferred]
--- a/src/HOL/Limits.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Limits.thy Fri Jan 08 15:49:01 2016 +0100
@@ -137,7 +137,7 @@
by (auto elim!: allE[of _ n])
qed
-lemma Bseq_bdd_above':
+lemma Bseq_bdd_above':
"Bseq (X::nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))"
proof (elim BseqE, intro bdd_aboveI2)
fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "norm (X n) \<le> K"
@@ -152,7 +152,7 @@
lemma Bseq_eventually_mono:
assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g"
- shows "Bseq f"
+ shows "Bseq f"
proof -
from assms(1) obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> norm (g n)"
by (auto simp: eventually_at_top_linorder)
@@ -162,7 +162,7 @@
apply (rule max.coboundedI2, rule Max.coboundedI, auto) []
apply (rule max.coboundedI1, force intro: order.trans[OF N K])
done
- thus ?thesis by (blast intro: BseqI')
+ thus ?thesis by (blast intro: BseqI')
qed
lemma lemma_NBseq_def:
@@ -243,7 +243,7 @@
lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
by (simp add: Bseq_def)
-lemma Bseq_add:
+lemma Bseq_add:
assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
shows "Bseq (\<lambda>x. f x + c)"
proof -
@@ -260,12 +260,12 @@
lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto
-lemma Bseq_mult:
+lemma Bseq_mult:
assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_field)"
assumes "Bseq (g :: nat \<Rightarrow> 'a :: real_normed_field)"
shows "Bseq (\<lambda>x. f x * g x)"
proof -
- from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0"
+ from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0"
unfolding Bseq_def by blast
hence "\<And>x. norm (f x * g x) \<le> K1 * K2" by (auto simp: norm_mult intro!: mult_mono)
thus ?thesis by (rule BseqI')
@@ -794,7 +794,7 @@
lemma tendsto_add_const_iff:
"((\<lambda>x. c + f x :: 'a :: real_normed_vector) \<longlongrightarrow> c + d) F \<longleftrightarrow> (f \<longlongrightarrow> d) F"
- using tendsto_add[OF tendsto_const[of c], of f d]
+ using tendsto_add[OF tendsto_const[of c], of f d]
tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
@@ -1001,11 +1001,11 @@
lemma not_tendsto_and_filterlim_at_infinity:
assumes "F \<noteq> bot"
- assumes "(f \<longlongrightarrow> (c :: 'a :: real_normed_vector)) F"
+ assumes "(f \<longlongrightarrow> (c :: 'a :: real_normed_vector)) F"
assumes "filterlim f at_infinity F"
shows False
proof -
- from tendstoD[OF assms(2), of "1/2"]
+ from tendstoD[OF assms(2), of "1/2"]
have "eventually (\<lambda>x. dist (f x) c < 1/2) F" by simp
moreover from filterlim_at_infinity[of "norm c" f F] assms(3)
have "eventually (\<lambda>x. norm (f x) \<ge> norm c + 1) F" by simp
@@ -1037,7 +1037,7 @@
thus ?thesis by eventually_elim auto
qed
-lemma tendsto_of_nat [tendsto_intros]:
+lemma tendsto_of_nat [tendsto_intros]:
"filterlim (of_nat :: nat \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity sequentially"
proof (subst filterlim_at_infinity[OF order.refl], intro allI impI)
fix r :: real assume r: "r > 0"
@@ -1164,7 +1164,7 @@
fix r :: real assume r: "r > 0"
from assms(1) have "((\<lambda>x. norm (f x)) \<longlongrightarrow> norm c) F" by (rule tendsto_norm)
hence "eventually (\<lambda>x. norm (f x) < norm c + 1) F" by (rule order_tendstoD) simp_all
- moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all
+ moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all
with assms(2) have "eventually (\<lambda>x. norm (g x) \<ge> r + norm c + 1) F"
unfolding filterlim_at_infinity[OF order_refl] by (elim allE[of _ "r + norm c + 1"]) simp_all
ultimately show "eventually (\<lambda>x. norm (f x + g x) \<ge> r) F"
@@ -1506,7 +1506,7 @@
lemma eventually_at2:
"eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
- unfolding eventually_at dist_nz by auto
+ unfolding eventually_at by auto
lemma Lim_transform:
fixes a b :: "'a::real_normed_vector"
@@ -1526,28 +1526,16 @@
done
lemma Lim_transform_within:
- assumes "0 < d"
- and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f \<longlongrightarrow> l) (at x within S)"
+ assumes "(f \<longlongrightarrow> l) (at x within S)"
+ and "0 < d"
+ and "\<And>x'. \<lbrakk>x'\<in>S; 0 < dist x' x; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
shows "(g \<longlongrightarrow> l) (at x within S)"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>x. f x = g x) (at x within S)"
- using assms(1,2) by (auto simp: dist_nz eventually_at)
+ using assms by (auto simp: eventually_at)
show "(f \<longlongrightarrow> l) (at x within S)" by fact
qed
-lemma Lim_transform_at:
- assumes "0 < d"
- and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f \<longlongrightarrow> l) (at x)"
- shows "(g \<longlongrightarrow> l) (at x)"
- using _ assms(3)
-proof (rule Lim_transform_eventually)
- show "eventually (\<lambda>x. f x = g x) (at x)"
- unfolding eventually_at2
- using assms(1,2) by auto
-qed
-
text\<open>Common case assuming being away from some crucial point like 0.\<close>
lemma Lim_transform_away_within:
@@ -1574,15 +1562,15 @@
text\<open>Alternatively, within an open set.\<close>
lemma Lim_transform_within_open:
- assumes "open S" and "a \<in> S"
- and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
- and "(f \<longlongrightarrow> l) (at a)"
- shows "(g \<longlongrightarrow> l) (at a)"
+ assumes "(f \<longlongrightarrow> l) (at a within T)"
+ and "open s" and "a \<in> s"
+ and "\<And>x. \<lbrakk>x\<in>s; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
+ shows "(g \<longlongrightarrow> l) (at a within T)"
proof (rule Lim_transform_eventually)
- show "eventually (\<lambda>x. f x = g x) (at a)"
+ show "eventually (\<lambda>x. f x = g x) (at a within T)"
unfolding eventually_at_topological
- using assms(1,2,3) by auto
- show "(f \<longlongrightarrow> l) (at a)" by fact
+ using assms by auto
+ show "(f \<longlongrightarrow> l) (at a within T)" by fact
qed
text\<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
@@ -1642,7 +1630,7 @@
fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
also note n
- finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
+ finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
qed
@@ -1660,9 +1648,9 @@
lemma LIMSEQ_n_over_Suc_n: "(\<lambda>n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
proof (rule Lim_transform_eventually)
- show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) =
+ show "eventually (\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a) =
of_nat n / of_nat (Suc n)) sequentially"
- using eventually_gt_at_top[of "0::nat"]
+ using eventually_gt_at_top[of "0::nat"]
by eventually_elim (simp add: field_simps del: of_nat_Suc)
have "(\<lambda>n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \<longlonglongrightarrow> inverse 1"
by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all
@@ -1738,11 +1726,11 @@
thus ?thesis by (auto simp: convergent_def)
qed
-lemma convergent_of_real:
+lemma convergent_of_real:
"convergent f \<Longrightarrow> convergent (\<lambda>n. of_real (f n) :: 'a :: real_normed_algebra_1)"
unfolding convergent_def by (blast intro!: tendsto_of_real)
-lemma convergent_add_const_iff:
+lemma convergent_add_const_iff:
"convergent (\<lambda>n. c + f n :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
proof
assume "convergent (\<lambda>n. c + f n)"
@@ -1752,11 +1740,11 @@
from convergent_add[OF convergent_const[of c] this] show "convergent (\<lambda>n. c + f n)" by simp
qed
-lemma convergent_add_const_right_iff:
+lemma convergent_add_const_right_iff:
"convergent (\<lambda>n. f n + c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
using convergent_add_const_iff[of c f] by (simp add: add_ac)
-lemma convergent_diff_const_right_iff:
+lemma convergent_diff_const_right_iff:
"convergent (\<lambda>n. f n - c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)
@@ -1772,7 +1760,7 @@
shows "convergent (\<lambda>n. c * f n :: 'a :: real_normed_field) \<longleftrightarrow> convergent f"
proof
assume "convergent (\<lambda>n. c * f n)"
- from assms convergent_mult[OF this convergent_const[of "inverse c"]]
+ from assms convergent_mult[OF this convergent_const[of "inverse c"]]
show "convergent f" by (simp add: field_simps)
next
assume "convergent f"
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Jan 08 15:49:01 2016 +0100
@@ -99,21 +99,21 @@
case le show ?diff_fg
apply (rule differentiable_transform_within [where d = "dist x c" and f = f])
using x le st
- apply (simp_all add: dist_real_def dist_nz [symmetric])
+ apply (simp_all add: dist_real_def)
apply (rule differentiable_at_withinI)
apply (rule differentiable_within_open [where s = "{a<..<c} - s", THEN iffD1], simp_all)
apply (blast intro: open_greaterThanLessThan finite_imp_closed)
- apply (force elim!: differentiable_subset)
+ apply (force elim!: differentiable_subset)+
done
next
case ge show ?diff_fg
apply (rule differentiable_transform_within [where d = "dist x c" and f = g])
using x ge st
- apply (simp_all add: dist_real_def dist_nz [symmetric])
+ apply (simp_all add: dist_real_def)
apply (rule differentiable_at_withinI)
apply (rule differentiable_within_open [where s = "{c<..<b} - t", THEN iffD1], simp_all)
apply (blast intro: open_greaterThanLessThan finite_imp_closed)
- apply (force elim!: differentiable_subset)
+ apply (force elim!: differentiable_subset)+
done
qed
}
@@ -351,11 +351,11 @@
have "(\<lambda>x. if x \<le> c then f x else g x) differentiable at x" (is "?diff_fg")
proof (cases x c rule: le_cases)
case le show ?diff_fg
- apply (rule differentiable_transform_at [of "dist x c" _ f])
+ apply (rule differentiable_transform_within [where f=f and d = "dist x c"])
using x dist_real_def le st by (auto simp: C1_differentiable_on_eq)
next
case ge show ?diff_fg
- apply (rule differentiable_transform_at [of "dist x c" _ g])
+ apply (rule differentiable_transform_within [where f=g and d = "dist x c"])
using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq)
qed
}
@@ -370,18 +370,20 @@
apply (rule continuous_on_eq [OF fcon])
apply (simp add:)
apply (rule vector_derivative_at [symmetric])
- apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_at)
+ apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within)
apply (simp_all add: dist_norm vector_derivative_works [symmetric])
- using f_diff
- by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(1))
+ apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff linorder_not_le order_less_irrefl st(1))
+ apply auto
+ done
moreover have "continuous_on ({c<..<b} - t) (\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
apply (rule continuous_on_eq [OF gcon])
apply (simp add:)
apply (rule vector_derivative_at [symmetric])
- apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_at)
+ apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within)
apply (simp_all add: dist_norm vector_derivative_works [symmetric])
- using g_diff
- by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_imp_le st(2))
+ apply (metis (full_types) C1_differentiable_on_eq Diff_iff Groups.add_ac(2) add_mono_thms_linordered_field(5) atLeastAtMost_iff less_irrefl not_le st(2))
+ apply auto
+ done
ultimately have "continuous_on ({a<..<b} - insert c (s \<union> t))
(\<lambda>x. vector_derivative (\<lambda>x. if x \<le> c then f x else g x) (at x))"
apply (rule continuous_on_subset [OF continuous_on_open_Un], auto)
@@ -435,7 +437,7 @@
and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
then have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x
- apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_at)
+ apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_within)
using that
apply (simp_all add: dist_real_def joinpaths_def)
apply (rule differentiable_chain_at derivative_intros | force)+
@@ -450,9 +452,10 @@
using co12 by (rule continuous_on_subset) force
then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 o op*2) (at x))"
apply (rule continuous_on_eq [OF _ vector_derivative_at])
- apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_at)
+ apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_within)
apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric])
apply (force intro: g1D differentiable_chain_at)
+ apply auto
done
have "continuous_on ({0..1} - insert 1 (op * 2 ` s))
((\<lambda>x. 1/2 * vector_derivative (g1 o op*2) (at x)) o op*(1/2))"
@@ -481,7 +484,7 @@
and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
then have g2D: "g2 differentiable at x" if "x \<in> {0..1} - insert 0 ((\<lambda>x. 2*x-1) ` s)" for x
- apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_at)
+ apply (rule_tac d="dist ((x+1)/2) (1/2)" and f = "(g1 +++ g2) o (\<lambda>x. (x+1)/2)" in differentiable_transform_within)
using that
apply (simp_all add: dist_real_def joinpaths_def)
apply (auto simp: dist_real_def joinpaths_def field_simps)
@@ -496,7 +499,7 @@
using co12 by (rule continuous_on_subset) force
then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) s) (\<lambda>x. vector_derivative (g2 o (\<lambda>x. 2*x-1)) (at x))"
apply (rule continuous_on_eq [OF _ vector_derivative_at])
- apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_at)
+ apply (rule_tac f="g2 o (\<lambda>x. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within)
apply (auto simp: dist_real_def field_simps joinpaths_def vector_derivative_works [symmetric]
intro!: g2D differentiable_chain_at)
done
@@ -755,7 +758,7 @@
have g1: "\<lbrakk>0 \<le> z; z*2 < 1; z*2 \<notin> s1\<rbrakk> \<Longrightarrow>
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
2 *\<^sub>R vector_derivative g1 (at (z*2))" for z
- apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g1(2*x))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>z - 1/2\<bar>"]])
apply (simp_all add: dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x" 2 _ g1, simplified o_def])
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
@@ -765,7 +768,7 @@
have g2: "\<lbrakk>1 < z*2; z \<le> 1; z*2 - 1 \<notin> s2\<rbrakk> \<Longrightarrow>
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
2 *\<^sub>R vector_derivative g2 (at (z*2 - 1))" for z
- apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z - 1/2\<bar>" _ "(\<lambda>x. g2 (2*x - 1))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2 (2*x - 1))" and d = "\<bar>z - 1/2\<bar>"]])
apply (simp_all add: dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. 2*x - 1" 2 _ g2, simplified o_def])
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
@@ -816,7 +819,7 @@
have g1: "\<lbrakk>0 < z; z < 1; z \<notin> s1\<rbrakk> \<Longrightarrow>
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) =
2 *\<^sub>R vector_derivative g1 (at z)" for z
- apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>(z-1)/2\<bar>" _ "(\<lambda>x. g1(2*x))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g1(2*x))" and d = "\<bar>(z-1)/2\<bar>"]])
apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x*2" 2 _ g1, simplified o_def])
using s1
@@ -850,7 +853,7 @@
have g2: "\<lbrakk>0 < z; z < 1; z \<notin> s2\<rbrakk> \<Longrightarrow>
vector_derivative (\<lambda>x. if x*2 \<le> 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
2 *\<^sub>R vector_derivative g2 (at z)" for z
- apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "\<bar>z/2\<bar>" _ "(\<lambda>x. g2(2*x-1))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g2(2*x-1))" and d = "\<bar>z/2\<bar>"]])
apply (simp_all add: field_simps dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x*2-1" 2 _ g2, simplified o_def])
using s2
@@ -916,7 +919,7 @@
have "0 \<le> x \<Longrightarrow> x + a < 1 \<Longrightarrow> x \<notin> (\<lambda>x. x - a) ` s \<Longrightarrow>
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))"
unfolding shiftpath_def
- apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist(1-a) x" _ "(\<lambda>x. g(a+x))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g(a+x))" and d = "dist(1-a) x"]])
apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x+a" 1 _ g, simplified o_def scaleR_one])
apply (intro derivative_eq_intros | simp)+
@@ -929,7 +932,7 @@
have "1 < x + a \<Longrightarrow> x \<le> 1 \<Longrightarrow> x \<notin> (\<lambda>x. x - a + 1) ` s \<Longrightarrow>
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))"
unfolding shiftpath_def
- apply (rule vector_derivative_at [OF has_vector_derivative_transform_at [of "dist (1-a) x" _ "(\<lambda>x. g(a+x-1))"]])
+ apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(\<lambda>x. g(a+x-1))" and d = "dist (1-a) x"]])
apply (auto simp: field_simps dist_real_def abs_if split: split_if_asm)
apply (rule vector_diff_chain_at [of "\<lambda>x. x+a-1" 1 _ g, simplified o_def scaleR_one])
apply (intro derivative_eq_intros | simp)+
@@ -986,12 +989,12 @@
vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
apply (rule vector_derivative_at_within_ivl
[OF has_vector_derivative_transform_within_open
- [of "{0<..<1}-s" _ "(shiftpath (1 - a) (shiftpath a g))"]])
+ [where f = "(shiftpath (1 - a) (shiftpath a g))" and s = "{0<..<1}-s"]])
using s g assms x
apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
vector_derivative_within_interior vector_derivative_works [symmetric])
- apply (rule Derivative.differentiable_transform_at [of "min x (1-x)", OF _ _ gx])
- apply (auto simp: dist_real_def shiftpath_shiftpath abs_if)
+ apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"])
+ apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: split_if_asm)
done
} note vd = this
have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))"
@@ -4041,14 +4044,16 @@
using pi_ge_two e
by (force simp: winding_number_valid_path p field_simps norm_divide norm_mult intro: less_le_trans)
} note cmod_wn_diff = this
- show ?thesis
- apply (rule continuous_transform_at [of "min d e / 2" _ "winding_number p"])
- apply (auto simp: \<open>d>0\<close> \<open>e>0\<close> dist_norm wnwn simp del: less_divide_eq_numeral1)
+ then have "isCont (winding_number p) z"
apply (simp add: continuous_at_eps_delta, clarify)
apply (rule_tac x="min (pe/4) (e/2*pe^2/L/4)" in exI)
using \<open>pe>0\<close> \<open>L>0\<close>
apply (simp add: dist_norm cmod_wn_diff)
done
+ then show ?thesis
+ apply (rule continuous_transform_within [where d = "min d e / 2"])
+ apply (auto simp: \<open>d>0\<close> \<open>e>0\<close> dist_norm wnwn)
+ done
qed
corollary continuous_on_winding_number:
@@ -4393,14 +4398,15 @@
done
next
case False
- then have dxz: "dist x z > 0" using dist_nz by blast
+ then have dxz: "dist x z > 0" by auto
have cf: "continuous (at x within s) f"
using conf continuous_on_eq_continuous_within that by blast
- show ?thesis
- apply (rule continuous_transform_within [OF dxz that, of "\<lambda>w::complex. (f w - f z)/(w - z)"])
+ have "continuous (at x within s) (\<lambda>w. (f w - f z) / (w - z))"
+ by (rule cf continuous_intros | simp add: False)+
+ then show ?thesis
+ apply (rule continuous_transform_within [OF _ dxz that, of "\<lambda>w::complex. (f w - f z)/(w - z)"])
apply (force simp: dist_commute)
- apply (rule cf continuous_intros)+
- using False by auto
+ done
qed
have fink': "finite (insert z k)" using \<open>finite k\<close> by blast
have *: "((\<lambda>w. if w = z then f' else (f w - f z) / (w - z)) has_contour_integral 0) \<gamma>"
@@ -5485,7 +5491,7 @@
done
show ?thes2
apply (simp add: DERIV_within_iff del: power_Suc)
- apply (rule Lim_transform_at [OF \<open>0 < d\<close> _ tendsto_mult_left [OF *]])
+ apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
apply (simp add: \<open>k \<noteq> 0\<close> **)
done
qed
@@ -5566,7 +5572,7 @@
by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset)
have holf_ball: "f holomorphic_on ball z r" using holf_cball
using ball_subset_cball holomorphic_on_subset by blast
- { fix w assume w: "w \<in> ball z r"
+ { fix w assume w: "w \<in> ball z r"
have intf: "(\<lambda>u. f u / (u - w)\<^sup>2) contour_integrable_on circlepath z r"
by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball])
have fder': "(f has_field_derivative 1 / (2 * of_real pi * \<i>) * contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2))
@@ -5595,7 +5601,7 @@
by (simp add: holomorphic_on_open [OF \<open>open s\<close>] *)
qed
-lemma holomorphic_deriv [holomorphic_intros]:
+lemma holomorphic_deriv [holomorphic_intros]:
"\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
by (metis DERIV_deriv_iff_complex_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
@@ -5608,10 +5614,10 @@
lemma analytic_higher_deriv: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
unfolding analytic_on_def using holomorphic_higher_deriv by blast
-lemma has_field_derivative_higher_deriv:
- "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
+lemma has_field_derivative_higher_deriv:
+ "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
\<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
-by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply
+by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply
funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
@@ -5627,7 +5633,7 @@
shows "f analytic_on s"
proof -
{ fix z assume "z \<in> s"
- with assms obtain e a where
+ with assms obtain e a where
"0 < e" and z: "z \<in> ball a e" and contf: "continuous_on (ball a e) f"
and 0: "\<And>b c. closed_segment b c \<subseteq> ball a e
\<Longrightarrow> contour_integral (linepath a b) f +
@@ -5661,14 +5667,14 @@
shows "f analytic_on s"
proof -
{ fix z assume "z \<in> s"
- with assms obtain t where
+ with assms obtain t where
"open t" and z: "z \<in> t" and contf: "continuous_on t f"
and 0: "\<And>a b c. convex hull {a,b,c} \<subseteq> t
\<Longrightarrow> contour_integral (linepath a b) f +
contour_integral (linepath b c) f +
contour_integral (linepath c a) f = 0"
by force
- then obtain e where "e>0" and e: "ball z e \<subseteq> t"
+ then obtain e where "e>0" and e: "ball z e \<subseteq> t"
using open_contains_ball by blast
have [simp]: "continuous_on (ball z e) f" using contf
using continuous_on_subset e by blast
@@ -5689,7 +5695,7 @@
qed
proposition Morera_triangle:
- "\<lbrakk>continuous_on s f; open s;
+ "\<lbrakk>continuous_on s f; open s;
\<And>a b c. convex hull {a,b,c} \<subseteq> s
\<longrightarrow> contour_integral (linepath a b) f +
contour_integral (linepath b c) f +
@@ -5701,7 +5707,7 @@
subsection\<open> Combining theorems for higher derivatives including Leibniz rule.\<close>
-lemma higher_deriv_linear [simp]:
+lemma higher_deriv_linear [simp]:
"(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
by (induction n) (auto simp: deriv_const deriv_linear)
@@ -5718,21 +5724,21 @@
"(deriv ^^ n) id z = (if n = 0 then z else if n = 1 then 1 else 0)"
by (simp add: id_def)
-lemma has_complex_derivative_funpow_1:
+lemma has_complex_derivative_funpow_1:
"\<lbrakk>(f has_field_derivative 1) (at z); f z = z\<rbrakk> \<Longrightarrow> (f^^n has_field_derivative 1) (at z)"
apply (induction n)
apply auto
apply (metis DERIV_ident DERIV_transform_at id_apply zero_less_one)
by (metis DERIV_chain comp_funpow comp_id funpow_swap1 mult.right_neutral)
-proposition higher_deriv_uminus:
+proposition higher_deriv_uminus:
assumes "f holomorphic_on s" "open s" and z: "z \<in> s"
shows "(deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
using z
proof (induction n arbitrary: z)
case 0 then show ?case by simp
next
- case (Suc n z)
+ case (Suc n z)
have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
using Suc.prems assms has_field_derivative_higher_deriv by auto
show ?case
@@ -5744,7 +5750,7 @@
done
qed
-proposition higher_deriv_add:
+proposition higher_deriv_add:
fixes z::complex
assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
@@ -5752,7 +5758,7 @@
proof (induction n arbitrary: z)
case 0 then show ?case by simp
next
- case (Suc n z)
+ case (Suc n z)
have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
"((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
using Suc.prems assms has_field_derivative_higher_deriv by auto
@@ -5765,7 +5771,7 @@
done
qed
-corollary higher_deriv_diff:
+corollary higher_deriv_diff:
fixes z::complex
assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
@@ -5781,13 +5787,13 @@
proposition higher_deriv_mult:
fixes z::complex
assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
- shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
+ shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
(\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
using z
proof (induction n arbitrary: z)
case 0 then show ?case by simp
next
- case (Suc n z)
+ case (Suc n z)
have *: "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
"\<And>n. ((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
using Suc.prems assms has_field_derivative_higher_deriv by auto
@@ -5801,7 +5807,7 @@
show ?case
apply (simp only: funpow.simps o_apply)
apply (rule DERIV_imp_deriv)
- apply (rule DERIV_transform_within_open
+ apply (rule DERIV_transform_within_open
[of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
apply (simp add: algebra_simps)
apply (rule DERIV_cong [OF DERIV_setsum])
@@ -5817,7 +5823,7 @@
and fg: "\<And>w. w \<in> s \<Longrightarrow> f w = g w"
shows "(deriv ^^ i) f z = (deriv ^^ i) g z"
using z
-by (induction i arbitrary: z)
+by (induction i arbitrary: z)
(auto simp: fg intro: complex_derivative_transform_within_open holomorphic_higher_deriv assms)
proposition higher_deriv_compose_linear:
@@ -5829,7 +5835,7 @@
proof (induction n arbitrary: z)
case 0 then show ?case by simp
next
- case (Suc n z)
+ case (Suc n z)
have holo0: "f holomorphic_on op * u ` s"
by (meson fg f holomorphic_on_subset image_subset_iff)
have holo1: "(\<lambda>w. f (u * w)) holomorphic_on s"
@@ -5867,7 +5873,7 @@
by simp
qed
-lemma higher_deriv_add_at:
+lemma higher_deriv_add_at:
assumes "f analytic_on {z}" "g analytic_on {z}"
shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
proof -
@@ -5877,7 +5883,7 @@
by (auto simp: analytic_at_two)
qed
-lemma higher_deriv_diff_at:
+lemma higher_deriv_diff_at:
assumes "f analytic_on {z}" "g analytic_on {z}"
shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
proof -
@@ -5887,14 +5893,14 @@
by (auto simp: analytic_at_two)
qed
-lemma higher_deriv_uminus_at:
+lemma higher_deriv_uminus_at:
"f analytic_on {z} \<Longrightarrow> (deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
using higher_deriv_uminus
by (auto simp: analytic_at)
-lemma higher_deriv_mult_at:
+lemma higher_deriv_mult_at:
assumes "f analytic_on {z}" "g analytic_on {z}"
- shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
+ shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
(\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
proof -
have "f analytic_on {z} \<and> g analytic_on {z}"
@@ -5911,17 +5917,17 @@
assumes f: "continuous_on s f" and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
shows "f holomorphic_on s"
proof -
- { fix z
+ { fix z
assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f complex_differentiable at x"
have "f complex_differentiable at z"
proof (cases "z \<in> k")
case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
next
case True
- with finite_set_avoid [OF k, of z]
+ with finite_set_avoid [OF k, of z]
obtain d where "d>0" and d: "\<And>x. \<lbrakk>x\<in>k; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
by blast
- obtain e where "e>0" and e: "ball z e \<subseteq> s"
+ obtain e where "e>0" and e: "ball z e \<subseteq> s"
using s \<open>z \<in> s\<close> by (force simp add: open_contains_ball)
have fde: "continuous_on (ball z (min d e)) f"
by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
@@ -5930,7 +5936,7 @@
apply (rule Cauchy_theorem_triangle_cofinite [OF _ k])
apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset)
apply (rule cdf)
- apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset
+ apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset
interior_mono interior_subset subset_hull)
done
then have "f holomorphic_on ball z (min d e)"
@@ -5952,8 +5958,8 @@
shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
apply (simp add: holomorphic_on_open [symmetric] complex_differentiable_def)
- using no_isolated_singularity [where s = "interior s"]
- apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset
+ using no_isolated_singularity [where s = "interior s"]
+ apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset
has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
using assms
apply auto
@@ -6021,7 +6027,7 @@
by simp
show ?thes1 using *
using contour_integrable_on_def by blast
- show ?thes2
+ show ?thes2
unfolding contour_integral_unique [OF *] by (simp add: divide_simps)
qed
@@ -6065,13 +6071,13 @@
done
obtain B where "0 < B" and B: "\<And>u. u \<in> cball z r \<Longrightarrow> norm(f u) \<le> B"
by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
- obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
+ obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k"
and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> norm(u - w)"
apply (rule_tac k = "r - dist z w" in that)
using w
apply (auto simp: dist_norm norm_minus_commute)
by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
- have *: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>path_image (circlepath z r).
+ have *: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>path_image (circlepath z r).
norm ((\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k)) - f x / (x - w)) < e"
if "0 < e" for e
proof -
@@ -6111,7 +6117,7 @@
also have "... < e * k"
using \<open>0 < B\<close> N by (simp add: divide_simps)
also have "... \<le> e * norm (u - w)"
- using r kle \<open>0 < e\<close> by (simp add: dist_commute dist_norm)
+ using r kle \<open>0 < e\<close> by (simp add: dist_commute dist_norm)
finally show ?thesis
by (simp add: divide_simps norm_divide del: power_Suc)
qed
@@ -6140,10 +6146,10 @@
then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
sums (2 * of_real pi * ii * f w)"
using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]])
- then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2)))
+ then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2)))
sums ((2 * of_real pi * ii * f w) / (\<i> * (complex_of_real pi * 2)))"
by (rule Series.sums_divide)
- then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2)))
+ then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2)))
sums f w"
by (simp add: field_simps)
then show ?thesis
@@ -6155,7 +6161,7 @@
text\<open> These weak Liouville versions don't even need the derivative formula.\<close>
-lemma Liouville_weak_0:
+lemma Liouville_weak_0:
assumes holf: "f holomorphic_on UNIV" and inf: "(f \<longlongrightarrow> 0) at_infinity"
shows "f z = 0"
proof (rule ccontr)
@@ -6181,14 +6187,14 @@
by (auto simp: norm_mult norm_divide divide_simps)
qed
-proposition Liouville_weak:
+proposition Liouville_weak:
assumes "f holomorphic_on UNIV" and "(f \<longlongrightarrow> l) at_infinity"
shows "f z = l"
using Liouville_weak_0 [of "\<lambda>z. f z - l"]
by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero)
-proposition Liouville_weak_inverse:
+proposition Liouville_weak_inverse:
assumes "f holomorphic_on UNIV" and unbounded: "\<And>B. eventually (\<lambda>x. norm (f x) \<ge> B) at_infinity"
obtains z where "f z = 0"
proof -
@@ -6210,7 +6216,7 @@
text\<open> In particular we get the Fundamental Theorem of Algebra.\<close>
-theorem fundamental_theorem_of_algebra:
+theorem fundamental_theorem_of_algebra:
fixes a :: "nat \<Rightarrow> complex"
assumes "a 0 = 0 \<or> (\<exists>i \<in> {1..n}. a i \<noteq> 0)"
obtains z where "(\<Sum>i\<le>n. a i * z^i) = 0"
@@ -6257,7 +6263,7 @@
if w: "w \<in> ball z r" for w
proof -
def d \<equiv> "(r - norm(w - z))"
- have "0 < d" "d \<le> r" using w by (auto simp: norm_minus_commute d_def dist_norm)
+ have "0 < d" "d \<le> r" using w by (auto simp: norm_minus_commute d_def dist_norm)
have dle: "\<And>u. cmod (z - u) = r \<Longrightarrow> d \<le> cmod (u - w)"
unfolding d_def by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
have ev_int: "\<forall>\<^sub>F n in F. (\<lambda>u. f n u / (u - w)) contour_integrable_on circlepath z r"
@@ -6308,17 +6314,17 @@
proposition has_complex_derivative_uniform_limit:
fixes z::complex
- assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and>
+ assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and>
(\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"
and lim: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> cball z r. norm(f n x - g x) < e) F"
and F: "~ trivial_limit F" and "0 < r"
obtains g' where
- "continuous_on (cball z r) g"
+ "continuous_on (cball z r) g"
"\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F"
proof -
let ?conint = "contour_integral (circlepath z r)"
have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r"
- by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F];
+ by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F];
auto simp: holomorphic_on_open complex_differentiable_def)+
then obtain g' where g': "\<And>x. x \<in> ball z r \<Longrightarrow> (g has_field_derivative g' x) (at x)"
using DERIV_deriv_iff_has_field_derivative
@@ -6327,8 +6333,8 @@
by (simp add: DERIV_imp_deriv)
have tends_f'n_g': "((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F" if w: "w \<in> ball z r" for w
proof -
- have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)"
- if cont_fn: "continuous_on (cball z r) (f n)"
+ have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)"
+ if cont_fn: "continuous_on (cball z r) (f n)"
and fnd: "\<And>w. w \<in> ball z r \<Longrightarrow> (f n has_field_derivative f' n w) (at w)" for n
proof -
have hol_fn: "f n holomorphic_on ball z r"
@@ -6336,7 +6342,7 @@
have "(f n has_field_derivative 1 / (2 * of_real pi * \<i>) * ?conint (\<lambda>u. f n u / (u - w)\<^sup>2)) (at w)"
by (rule Cauchy_derivative_integral_circlepath [OF cont_fn hol_fn w])
then have f': "f' n w = 1 / (2 * of_real pi * \<i>) * ?conint (\<lambda>u. f n u / (u - w)\<^sup>2)"
- using DERIV_unique [OF fnd] w by blast
+ using DERIV_unique [OF fnd] w by blast
show ?thesis
by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] divide_simps)
qed
@@ -6358,7 +6364,7 @@
apply (simp add: \<open>0 < d\<close>)
apply (force simp add: dist_norm dle intro: less_le_trans)
done
- have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2))
+ have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2))
\<longlongrightarrow> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \<open>0 < r\<close>])
then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) \<longlongrightarrow> 0) F"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri Jan 08 15:49:01 2016 +0100
@@ -907,7 +907,7 @@
from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
by (simp add: has_field_derivative_def s)
have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
- by (rule has_derivative_transform_within_open[OF \<open>open s\<close> x _ g'])
+ by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
(insert g, auto simp: sums_iff)
thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Fri Jan 08 15:49:01 2016 +0100
@@ -1345,9 +1345,9 @@
by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
then show ?thesis
apply (simp add: continuous_at)
- apply (rule Lim_transform_within_open [of "-{z. z \<in> \<real> & 0 \<le> Re z}" _ "\<lambda>z. Im(Ln(-z)) + pi"])
+ apply (rule Lim_transform_within_open [where s= "-{z. z \<in> \<real> & 0 \<le> Re z}" and f = "\<lambda>z. Im(Ln(-z)) + pi"])
+ apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0])
apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge)
- apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0])
done
qed
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 08 15:49:01 2016 +0100
@@ -1368,9 +1368,7 @@
have "x \<in> s" using assms(1,3) by auto
assume "\<not> ?thesis"
then obtain y where "y\<in>s" and y: "f x > f y" by auto
- then have xy: "0 < dist x y"
- by (auto simp add: dist_nz[symmetric])
-
+ then have xy: "0 < dist x y" by auto
then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
using real_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
@@ -3401,8 +3399,8 @@
also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
by (auto simp: continuous_on_closed_vimage)
hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
- finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto
-qed
+ finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto
+qed
lemma interior_real_semiline':
fixes a :: real
@@ -3434,7 +3432,7 @@
lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
proof-
have "{a..b} = {a..} \<inter> {..b}" by auto
- also have "interior ... = {a<..} \<inter> {..<b}"
+ also have "interior ... = {a<..} \<inter> {..<b}"
by (simp add: interior_real_semiline interior_real_semiline')
also have "... = {a<..<b}" by auto
finally show ?thesis .
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jan 08 15:49:01 2016 +0100
@@ -165,36 +165,23 @@
subsubsection \<open>Limit transformation for derivatives\<close>
lemma has_derivative_transform_within:
- assumes "0 < d"
+ assumes "(f has_derivative f') (at x within s)"
+ and "0 < d"
and "x \<in> s"
- and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f has_derivative f') (at x within s)"
+ and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
shows "(g has_derivative f') (at x within s)"
using assms
- unfolding has_derivative_within
- apply clarify
- apply (rule Lim_transform_within, auto)
- done
-
-lemma has_derivative_transform_at:
- assumes "0 < d"
- and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f has_derivative f') (at x)"
- shows "(g has_derivative f') (at x)"
- using has_derivative_transform_within [of d x UNIV f g f'] assms
- by simp
+ unfolding has_derivative_within
+ by (force simp add: intro: Lim_transform_within)
lemma has_derivative_transform_within_open:
- assumes "open s"
+ assumes "(f has_derivative f') (at x)"
+ and "open s"
and "x \<in> s"
- and "\<forall>y\<in>s. f y = g y"
- and "(f has_derivative f') (at x)"
+ and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
shows "(g has_derivative f') (at x)"
- using assms
- unfolding has_derivative_at
- apply clarify
- apply (rule Lim_transform_within_open[OF assms(1,2)], auto)
- done
+ using assms unfolding has_derivative_at
+ by (force simp add: intro: Lim_transform_within_open)
subsection \<open>Differentiability\<close>
@@ -234,24 +221,13 @@
by (metis at_within_interior interior_open)
lemma differentiable_transform_within:
- assumes "0 < d"
+ assumes "f differentiable (at x within s)"
+ and "0 < d"
and "x \<in> s"
- and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
- assumes "f differentiable (at x within s)"
+ and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
shows "g differentiable (at x within s)"
- using assms(4)
- unfolding differentiable_def
- by (auto intro!: has_derivative_transform_within[OF assms(1-3)])
-
-lemma differentiable_transform_at:
- assumes "0 < d"
- and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
- and "f differentiable at x"
- shows "g differentiable at x"
- using assms(3)
- unfolding differentiable_def
- using has_derivative_transform_at[OF assms(1-2)]
- by auto
+ using assms has_derivative_transform_within unfolding differentiable_def
+ by blast
subsection \<open>Frechet derivative and Jacobian matrix\<close>
@@ -2263,7 +2239,7 @@
from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
by (simp add: has_field_derivative_def s)
have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
- by (rule has_derivative_transform_within_open[OF \<open>open s\<close> x _ g'])
+ by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
(insert g, auto simp: sums_iff)
thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
by (auto simp: summable_def differentiable_def has_field_derivative_def)
@@ -2475,29 +2451,20 @@
qed
lemma has_vector_derivative_transform_within:
- assumes "0 < d"
+ assumes "(f has_vector_derivative f') (at x within s)"
+ and "0 < d"
and "x \<in> s"
- and "\<forall>x'\<in>s. dist x' x < d \<longrightarrow> f x' = g x'"
- assumes "(f has_vector_derivative f') (at x within s)"
- shows "(g has_vector_derivative f') (at x within s)"
+ and "\<And>x'. \<lbrakk>x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
+ shows "(g has_vector_derivative f') (at x within s)"
using assms
unfolding has_vector_derivative_def
by (rule has_derivative_transform_within)
-lemma has_vector_derivative_transform_at:
- assumes "0 < d"
- and "\<forall>x'. dist x' x < d \<longrightarrow> f x' = g x'"
- and "(f has_vector_derivative f') (at x)"
- shows "(g has_vector_derivative f') (at x)"
- using assms
- unfolding has_vector_derivative_def
- by (rule has_derivative_transform_at)
-
lemma has_vector_derivative_transform_within_open:
- assumes "open s"
+ assumes "(f has_vector_derivative f') (at x)"
+ and "open s"
and "x \<in> s"
- and "\<forall>y\<in>s. f y = g y"
- and "(f has_vector_derivative f') (at x)"
+ and "\<And>y. y\<in>s \<Longrightarrow> f y = g y"
shows "(g has_vector_derivative f') (at x)"
using assms
unfolding has_vector_derivative_def
--- a/src/HOL/Multivariate_Analysis/Gamma.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy Fri Jan 08 15:49:01 2016 +0100
@@ -288,7 +288,7 @@
continuous.
This will later allow us to lift holomorphicity and continuity from the log-Gamma
- function to the inverse Gamma function, and from that to the Gamma function itself.
+ function to the inverse of the Gamma function, and from that to the Gamma function itself.
\<close>
definition ln_Gamma_series :: "('a :: {banach,real_normed_field,ln}) \<Rightarrow> nat \<Rightarrow> 'a" where
@@ -824,9 +824,8 @@
proof -
have "-Digamma (3/2 :: real) = -Digamma (of_nat 1 + 1/2)" by simp
also have "\<dots> = 2 * ln 2 + euler_mascheroni - 2" by (subst Digamma_half_integer) simp
- also from euler_mascheroni_approx have "euler_mascheroni \<le> (0.58::real)"
- by (simp add: abs_real_def split: split_if_asm)
- also from ln_2_bounds have "ln 2 < (0.7 :: real)" by simp
+ also note euler_mascheroni_less_13_over_22
+ also note ln2_le_25_over_36
finally show ?thesis by simp
qed
@@ -911,7 +910,7 @@
text \<open>
- We define a type class that captures all the fundamental properties of the inverse Gamma function
+ We define a type class that captures all the fundamental properties of the inverse of the Gamma function
and defines the Gamma function upon that. This allows us to instantiate the type class both for
the reals and for the complex numbers with a minimal amount of proof duplication.
\<close>
@@ -2267,7 +2266,7 @@
subsection \<open>Limits and residues\<close>
text \<open>
- The inverse Gamma function has simple zeros:
+ The inverse of the Gamma function has simple zeros:
\<close>
lemma rGamma_zeros:
@@ -2285,7 +2284,7 @@
text \<open>
- The simple zeros of the inverse Gamma function correspond to simple poles of the Gamma function,
+ The simple zeros of the inverse of the Gamma function correspond to simple poles of the Gamma function,
and their residues can easily be computed from the limit we have just proven:
\<close>
@@ -2452,6 +2451,60 @@
finally show ?thesis by (simp add: Gamma_def)
qed
+subsubsection \<open>Binomial coefficient form\<close>
+
+lemma Gamma_binomial:
+ "(\<lambda>n. ((z + of_nat n) gchoose n) * exp (-z * of_real (ln (of_nat n)))) \<longlonglongrightarrow> rGamma (z+1)"
+proof (cases "z = 0")
+ case False
+ show ?thesis
+ proof (rule Lim_transform_eventually)
+ let ?powr = "\<lambda>a b. exp (b * of_real (ln (of_nat a)))"
+ show "eventually (\<lambda>n. rGamma_series z n / z =
+ ((z + of_nat n) gchoose n) * ?powr n (-z)) sequentially"
+ proof (intro always_eventually allI)
+ fix n :: nat
+ from False have "((z + of_nat n) gchoose n) = pochhammer z (Suc n) / z / fact n"
+ by (simp add: gbinomial_pochhammer' pochhammer_rec)
+ also have "pochhammer z (Suc n) / z / fact n * ?powr n (-z) = rGamma_series z n / z"
+ by (simp add: rGamma_series_def divide_simps exp_minus)
+ finally show "rGamma_series z n / z = ((z + of_nat n) gchoose n) * ?powr n (-z)" ..
+ qed
+
+ from False have "(\<lambda>n. rGamma_series z n / z) \<longlonglongrightarrow> rGamma z / z" by (intro tendsto_intros)
+ also from False have "rGamma z / z = rGamma (z + 1)" using rGamma_plus1[of z]
+ by (simp add: field_simps)
+ finally show "(\<lambda>n. rGamma_series z n / z) \<longlonglongrightarrow> rGamma (z+1)" .
+ qed
+qed (simp_all add: binomial_gbinomial [symmetric])
+
+lemma fact_binomial_limit:
+ "(\<lambda>n. of_nat ((k + n) choose n) / of_nat (n ^ k) :: 'a :: Gamma) \<longlonglongrightarrow> 1 / fact k"
+proof (rule Lim_transform_eventually)
+ have "(\<lambda>n. of_nat ((k + n) choose n) / of_real (exp (of_nat k * ln (real_of_nat n))))
+ \<longlonglongrightarrow> 1 / Gamma (of_nat (Suc k) :: 'a)" (is "?f \<longlonglongrightarrow> _")
+ using Gamma_binomial[of "of_nat k :: 'a"]
+ by (simp add: binomial_gbinomial add_ac Gamma_def divide_simps exp_of_real [symmetric] exp_minus)
+ also have "Gamma (of_nat (Suc k)) = fact k" by (rule Gamma_fact)
+ finally show "?f \<longlonglongrightarrow> 1 / fact k" .
+
+ show "eventually (\<lambda>n. ?f n = of_nat ((k + n) choose n) / of_nat (n ^ k)) sequentially"
+ using eventually_gt_at_top[of "0::nat"]
+ proof eventually_elim
+ fix n :: nat assume n: "n > 0"
+ from n have "exp (real_of_nat k * ln (real_of_nat n)) = real_of_nat (n^k)"
+ by (simp add: exp_of_nat_mult)
+ thus "?f n = of_nat ((k + n) choose n) / of_nat (n ^ k)" by simp
+ qed
+qed
+
+lemma binomial_asymptotic:
+ "(\<lambda>n. of_nat ((k + n) choose n) / (of_nat (n ^ k) / fact k) :: 'a :: Gamma) \<longlonglongrightarrow> 1"
+ using tendsto_mult[OF fact_binomial_limit[of k] tendsto_const[of "fact k :: 'a"]] by simp
+
+
+subsection \<open>The Weierstraß product formula for the sine\<close>
+
lemma sin_product_formula_complex:
fixes z :: complex
shows "(\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k^2)) \<longlonglongrightarrow> sin (of_real pi * z)"
@@ -2496,6 +2549,9 @@
using tendsto_divide[OF sin_product_formula_real[of x] tendsto_const[of "pi * x"]] assms
by simp
+
+subsection \<open>The Solution to the Basel problem\<close>
+
theorem inverse_squares_sums: "(\<lambda>n. 1 / (n + 1)\<^sup>2) sums (pi\<^sup>2 / 6)"
proof -
def P \<equiv> "\<lambda>x n. (\<Prod>k=1..n. 1 - x^2 / of_nat k^2 :: real)"
@@ -2589,56 +2645,4 @@
qed
-
-subsection \<open>Binomial coefficient form\<close>
-
-lemma Gamma_binomial:
- "(\<lambda>n. ((z + of_nat n) gchoose n) * exp (-z * of_real (ln (of_nat n)))) \<longlonglongrightarrow> rGamma (z+1)"
-proof (cases "z = 0")
- case False
- show ?thesis
- proof (rule Lim_transform_eventually)
- let ?powr = "\<lambda>a b. exp (b * of_real (ln (of_nat a)))"
- show "eventually (\<lambda>n. rGamma_series z n / z =
- ((z + of_nat n) gchoose n) * ?powr n (-z)) sequentially"
- proof (intro always_eventually allI)
- fix n :: nat
- from False have "((z + of_nat n) gchoose n) = pochhammer z (Suc n) / z / fact n"
- by (simp add: gbinomial_pochhammer' pochhammer_rec)
- also have "pochhammer z (Suc n) / z / fact n * ?powr n (-z) = rGamma_series z n / z"
- by (simp add: rGamma_series_def divide_simps exp_minus)
- finally show "rGamma_series z n / z = ((z + of_nat n) gchoose n) * ?powr n (-z)" ..
- qed
-
- from False have "(\<lambda>n. rGamma_series z n / z) \<longlonglongrightarrow> rGamma z / z" by (intro tendsto_intros)
- also from False have "rGamma z / z = rGamma (z + 1)" using rGamma_plus1[of z]
- by (simp add: field_simps)
- finally show "(\<lambda>n. rGamma_series z n / z) \<longlonglongrightarrow> rGamma (z+1)" .
- qed
-qed (simp_all add: binomial_gbinomial [symmetric])
-
-lemma fact_binomial_limit:
- "(\<lambda>n. of_nat ((k + n) choose n) / of_nat (n ^ k) :: 'a :: Gamma) \<longlonglongrightarrow> 1 / fact k"
-proof (rule Lim_transform_eventually)
- have "(\<lambda>n. of_nat ((k + n) choose n) / of_real (exp (of_nat k * ln (real_of_nat n))))
- \<longlonglongrightarrow> 1 / Gamma (of_nat (Suc k) :: 'a)" (is "?f \<longlonglongrightarrow> _")
- using Gamma_binomial[of "of_nat k :: 'a"]
- by (simp add: binomial_gbinomial add_ac Gamma_def divide_simps exp_of_real [symmetric] exp_minus)
- also have "Gamma (of_nat (Suc k)) = fact k" by (rule Gamma_fact)
- finally show "?f \<longlonglongrightarrow> 1 / fact k" .
-
- show "eventually (\<lambda>n. ?f n = of_nat ((k + n) choose n) / of_nat (n ^ k)) sequentially"
- using eventually_gt_at_top[of "0::nat"]
- proof eventually_elim
- fix n :: nat assume n: "n > 0"
- from n have "exp (real_of_nat k * ln (real_of_nat n)) = real_of_nat (n^k)"
- by (simp add: exp_of_nat_mult)
- thus "?f n = of_nat ((k + n) choose n) / of_nat (n ^ k)" by simp
- qed
-qed
-
-lemma binomial_asymptotic:
- "(\<lambda>n. of_nat ((k + n) choose n) / (of_nat (n ^ k) / fact k) :: 'a :: Gamma) \<longlonglongrightarrow> 1"
- using tendsto_mult[OF fact_binomial_limit[of k] tendsto_const[of "fact k :: 'a"]] by simp
-
end
--- a/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy Fri Jan 08 15:49:01 2016 +0100
@@ -28,35 +28,9 @@
lemma setsum_Suc_diff':
fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
assumes "m \<le> n"
- shows "(\<Sum>i = m..<n. f(Suc i) - f i) = f n - f m"
+ shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
using assms by (induct n) (auto simp: le_Suc_eq)
-lemma eval_fact:
- "fact 0 = 1"
- "fact (Suc 0) = 1"
- "fact (numeral n) = numeral n * fact (pred_numeral n)"
- by (simp, simp, simp_all only: numeral_eq_Suc fact_Suc,
- simp only: numeral_eq_Suc [symmetric] of_nat_numeral)
-
-lemma setsum_poly_horner_expand:
- "(\<Sum>k<(numeral n::nat). f k * x^k) = f 0 + (\<Sum>k<pred_numeral n. f (k+1) * x^k) * x"
- "(\<Sum>k<Suc 0. f k * x^k) = (f 0 :: 'a :: semiring_1)"
- "(\<Sum>k<(0::nat). f k * x^k) = 0"
-proof -
- {
- fix m :: nat
- have "(\<Sum>k<Suc m. f k * x^k) = f 0 + (\<Sum>k=Suc 0..<Suc m. f k * x^k)"
- by (subst atLeast0LessThan [symmetric], subst setsum_head_upt_Suc) simp_all
- also have "(\<Sum>k=Suc 0..<Suc m. f k * x^k) = (\<Sum>k<m. f (k+1) * x^k) * x"
- by (subst setsum_shift_bounds_Suc_ivl)
- (simp add: setsum_left_distrib algebra_simps atLeast0LessThan power_commutes)
- finally have "(\<Sum>k<Suc m. f k * x ^ k) = f 0 + (\<Sum>k<m. f (k + 1) * x ^ k) * x" .
- }
- from this[of "pred_numeral n"]
- show "(\<Sum>k<numeral n. f k * x^k) = f 0 + (\<Sum>k<pred_numeral n. f (k+1) * x^k) * x"
- by (simp add: numeral_eq_Suc)
-qed simp_all
-
subsection \<open>The Harmonic numbers\<close>
@@ -133,7 +107,7 @@
qed (simp_all add: harm_def)
-subsection \<open>The Euler–Mascheroni constant\<close>
+subsection \<open>The Euler--Mascheroni constant\<close>
text \<open>
The limit of the difference between the partial harmonic sum and the natural logarithm
@@ -269,10 +243,9 @@
qed
-subsection \<open>Approximation of the Euler--Mascheroni constant\<close>
+subsection \<open>Bounds on the Euler--Mascheroni constant\<close>
-(* FIXME: ugly *)
-(* TODO: Move ? *)
+(* TODO: Move? *)
lemma ln_inverse_approx_le:
assumes "(x::real) > 0" "a > 0"
shows "ln (x + a) - ln x \<le> a * (inverse x + inverse (x + a))/2" (is "_ \<le> ?A")
@@ -401,7 +374,7 @@
qed
also from sums have "\<dots> = -inv (n+2) / 2" by (simp add: sums_iff)
finally have "euler_mascheroni \<ge> (\<Sum>k\<le>n. D k) + 1 / (of_nat (2 * (n+2)))"
- by (simp add: inv_def field_simps of_nat_mult)
+ by (simp add: inv_def field_simps)
also have "(\<Sum>k\<le>n. D k) = harm (Suc n) - (\<Sum>k\<le>n. ln (real_of_nat (Suc k+1)) - ln (of_nat (k+1)))"
unfolding harm_altdef D_def by (subst lessThan_Suc_atMost) (simp add: setsum.distrib setsum_subtractf)
also have "(\<Sum>k\<le>n. ln (real_of_nat (Suc k+1)) - ln (of_nat (k+1))) = ln (of_nat (n+2))"
@@ -447,7 +420,10 @@
lemma euler_mascheroni_pos: "euler_mascheroni > (0::real)"
using euler_mascheroni_lower[of 0] ln_2_less_1 by (simp add: harm_def)
-lemma ln_approx_aux:
+context
+begin
+
+private lemma ln_approx_aux:
fixes n :: nat and x :: real
defines "y \<equiv> (x-1)/(x+1)"
assumes x: "x > 0" "x \<noteq> 1"
@@ -514,65 +490,13 @@
thus "abs (ln x - (approx + d)) \<le> d" by auto
qed
-context
-begin
-
-qualified lemma ln_approx_abs':
- assumes "x > (1::real)"
- assumes "(x-1)/(x+1) = y"
- assumes "y^2 = ysqr"
- assumes "(\<Sum>k<n. inverse (of_nat (2*k+1)) * ysqr^k) = approx"
- assumes "y*ysqr^n / (1 - ysqr) / of_nat (2*n+1) = d"
- assumes "d \<le> e"
- shows "abs (ln x - (2*y*approx + d)) \<le> e"
-proof -
- note ln_approx_abs[OF assms(1), of n]
- also note assms(2)
- also have "y^(2*n+1) = y*ysqr^n" by (simp add: assms(3)[symmetric] power_mult)
- also note assms(3)
- also note assms(5)
- also note assms(5)
- also note assms(6)
- also have "(\<Sum>k<n. 2*y^(2*k+1) / real_of_nat (2 * k + 1)) = (2*y) * approx"
- apply (subst assms(4)[symmetric], subst setsum_right_distrib)
- apply (simp add: assms(3)[symmetric] power_mult)
- apply (simp add: mult_ac divide_simps)?
- done
- finally show ?thesis .
-qed
-
-lemma ln_2_approx: "\<bar>ln 2 - 0.69314718055\<bar> < inverse (2 ^ 36 :: real)" (is ?thesis1)
- and ln_2_bounds: "ln (2::real) \<in> {0.693147180549..0.693147180561}" (is ?thesis2)
-proof -
- def approx \<equiv> "0.69314718055 :: real" and approx' \<equiv> "4465284211343447 / 6442043387911560 :: real"
- def d \<equiv> "inverse (195259926456::real)"
- have "dist (ln 2) approx \<le> dist (ln 2) approx' + dist approx' approx" by (rule dist_triangle)
- also have "\<bar>ln (2::real) - (2 * (1/3) * (651187280816108 / 626309773824735) +
- inverse 195259926456)\<bar> \<le> inverse 195259926456"
- proof (rule ln_approx_abs'[where n = 10])
- show "(1/3::real)^2 = 1/9" by (simp add: power2_eq_square)
- qed (simp_all add: eval_nat_numeral)
- hence A: "dist (ln 2) approx' \<le> d" by (simp add: dist_real_def approx'_def d_def)
- hence "dist (ln 2) approx' + dist approx' approx \<le> \<dots> + dist approx' approx"
- by (rule add_right_mono)
- also have "\<dots> < inverse (2 ^ 36)" by (simp add: dist_real_def approx'_def approx_def d_def)
- finally show ?thesis1 unfolding dist_real_def approx_def .
-
- from A have "ln 2 \<in> {approx' - d..approx' + d}"
- by (simp add: dist_real_def abs_real_def split: split_if_asm)
- also have "\<dots> \<subseteq> {0.693147180549..0.693147180561}"
- by (subst atLeastatMost_subset_iff, rule disjI2) (simp add: approx'_def d_def)
- finally show ?thesis2 .
-qed
-
end
-
lemma euler_mascheroni_bounds:
fixes n :: nat assumes "n \<ge> 1" defines "t \<equiv> harm n - ln (of_nat (Suc n)) :: real"
shows "euler_mascheroni \<in> {t + inverse (of_nat (2*(n+1)))..t + inverse (of_nat (2*n))}"
using assms euler_mascheroni_upper[of "n-1"] euler_mascheroni_lower[of "n-1"]
- unfolding t_def by (cases n) (simp_all add: harm_Suc t_def inverse_eq_divide of_nat_mult)
+ unfolding t_def by (cases n) (simp_all add: harm_Suc t_def inverse_eq_divide)
lemma euler_mascheroni_bounds':
fixes n :: nat assumes "n \<ge> 1" "ln (real_of_nat (Suc n)) \<in> {l<..<u}"
@@ -580,28 +504,29 @@
{harm n - u + inverse (of_nat (2*(n+1)))<..<harm n - l + inverse (of_nat (2*n))}"
using euler_mascheroni_bounds[OF assms(1)] assms(2) by auto
-lemma euler_mascheroni_approx:
- defines "approx \<equiv> 0.577257 :: real" and "e \<equiv> 0.000063 :: real"
- shows "abs (euler_mascheroni - approx :: real) < e"
- (is "abs (_ - ?approx) < ?e")
+
+text \<open>
+ Approximation of @{term "ln 2"}. The lower bound is accurate to about 0.03; the upper
+ bound is accurate to about 0.0015.
+\<close>
+lemma ln2_ge_two_thirds: "2/3 \<le> ln (2::real)"
+ and ln2_le_25_over_36: "ln (2::real) \<le> 25/36"
+ using ln_approx_bounds[of 2 1, simplified, simplified eval_nat_numeral, simplified] by simp_all
+
+
+text \<open>
+ Approximation of the Euler--Mascheroni constant. The lower bound is accurate to about 0.0015;
+ the upper bound is accurate to about 0.015.
+\<close>
+lemma euler_mascheroni_gt_19_over_33: "(euler_mascheroni :: real) > 19/33" (is ?th1)
+ and euler_mascheroni_less_13_over_22: "(euler_mascheroni :: real) < 13/22" (is ?th2)
proof -
- def l \<equiv> "47388813395531028639296492901910937/82101866951584879688289000000000000 :: real"
- def u \<equiv> "142196984054132045946501548559032969 / 246305600854754639064867000000000000 :: real"
- have impI: "P \<longrightarrow> Q" if Q for P Q using that by blast
- have hsum_63: "harm 63 = (310559566510213034489743057 / 65681493561267903750631200 ::real)"
- by (simp add: harm_expand)
- from harm_Suc[of 63] have hsum_64: "harm 64 =
- 623171679694215690971693339 / (131362987122535807501262400::real)"
- by (subst (asm) hsum_63) simp
- have "ln (64::real) = real (6::nat) * ln 2" by (subst ln_realpow[symmetric]) simp_all
- hence "ln (real_of_nat (Suc 63)) \<in> {4.158883083293<..<4.158883083367}" using ln_2_bounds by simp
- from euler_mascheroni_bounds'[OF _ this]
- have "(euler_mascheroni :: real) \<in> {l<..<u}"
- by (simp add: hsum_63 del: greaterThanLessThan_iff) (simp only: l_def u_def)
- also have "\<dots> \<subseteq> {approx - e<..<approx + e}"
- by (subst greaterThanLessThan_subseteq_greaterThanLessThan, rule impI)
- (simp add: approx_def e_def u_def l_def)
- finally show ?thesis by (simp add: abs_real_def)
+ have "ln (real (Suc 7)) = 3 * ln 2" by (simp add: ln_powr [symmetric] powr_numeral)
+ also from ln_approx_bounds[of 2 3] have "\<dots> \<in> {3*307/443<..<3*4615/6658}"
+ by (simp add: eval_nat_numeral)
+ finally have "ln (real (Suc 7)) \<in> \<dots>" .
+ from euler_mascheroni_bounds'[OF _ this] have "?th1 \<and> ?th2" by (simp_all add: harm_expand)
+ thus ?th1 ?th2 by blast+
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Jan 08 15:49:01 2016 +0100
@@ -843,7 +843,7 @@
apply (rule that [OF \<open>path h\<close>])
using assms h
apply auto
- apply (metis diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff)
+ apply (metis Diff_single_insert frontier_subset_eq insert_iff interior_subset subset_iff)
done
qed
--- a/src/HOL/Multivariate_Analysis/Summation.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Summation.thy Fri Jan 08 15:49:01 2016 +0100
@@ -2,7 +2,7 @@
Author: Manuel Eberl, TU München
*)
-section \<open>Rounded dual logarithm\<close>
+section \<open>Radius of Convergence and Summation Tests\<close>
theory Summation
imports
@@ -16,6 +16,8 @@
various summability tests, lemmas to compute the radius of convergence etc.
\<close>
+subsection \<open>Rounded dual logarithm\<close>
+
(* This is required for the Cauchy condensation criterion *)
definition "natlog2 n = (if n = 0 then 0 else nat \<lfloor>log 2 (real_of_nat n)\<rfloor>)"
@@ -206,7 +208,7 @@
qed
-subsection \<open>Cauchy's condensation test\<close>
+subsubsection \<open>Cauchy's condensation test\<close>
context
fixes f :: "nat \<Rightarrow> real"
@@ -319,7 +321,7 @@
end
-subsection \<open>Summability of powers\<close>
+subsubsection \<open>Summability of powers\<close>
lemma abs_summable_complex_powr_iff:
"summable (\<lambda>n. norm (exp (of_real (ln (of_nat n)) * s))) \<longleftrightarrow> Re s < -1"
@@ -389,7 +391,7 @@
qed
-subsection \<open>Kummer's test\<close>
+subsubsection \<open>Kummer's test\<close>
lemma kummers_test_convergence:
fixes f p :: "nat \<Rightarrow> real"
@@ -480,7 +482,7 @@
qed
-subsection \<open>Ratio test\<close>
+subsubsection \<open>Ratio test\<close>
lemma ratio_test_convergence:
fixes f :: "nat \<Rightarrow> real"
@@ -511,7 +513,7 @@
qed (simp_all add: summable_const_iff)
-subsection \<open>Raabe's test\<close>
+subsubsection \<open>Raabe's test\<close>
lemma raabes_test_convergence:
fixes f :: "nat \<Rightarrow> real"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 08 15:49:01 2016 +0100
@@ -13,7 +13,7 @@
"~~/src/HOL/Library/FuncSet"
Linear_Algebra
Norm_Arith
-
+
begin
lemma image_affinity_interval:
@@ -51,6 +51,11 @@
shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
by (fact tendsto_within_open)
+lemma Lim_within_open_NO_MATCH:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ shows "a \<in> S \<Longrightarrow> NO_MATCH UNIV S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)"
+using tendsto_within_open by blast
+
lemma continuous_on_union:
"closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
by (fact continuous_on_closed_Un)
@@ -1486,7 +1491,7 @@
case False
let ?d = "min d (dist a x)"
have dp: "?d > 0"
- using False d(1) using dist_nz by auto
+ using False d(1) by auto
from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
by auto
with dp False show ?thesis
@@ -1511,7 +1516,7 @@
by blast
let ?m = "min (e/2) (dist x y) "
from e2 y(2) have mp: "?m > 0"
- by (simp add: dist_nz[symmetric])
+ by simp
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
by blast
have th: "dist z y < e" using z y
@@ -2312,11 +2317,11 @@
lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_iff eventually_at_le dist_nz)
+ by (auto simp add: tendsto_iff eventually_at_le)
lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_iff eventually_at dist_nz)
+ by (auto simp add: tendsto_iff eventually_at)
lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
@@ -2665,9 +2670,9 @@
by (metis closure_contains_Inf closure_minimal subset_eq)
lemma atLeastAtMost_subset_contains_Inf:
- fixes A :: "real set" and a b :: real
+ fixes A :: "real set" and a b :: real
shows "A \<noteq> {} \<Longrightarrow> a \<le> b \<Longrightarrow> A \<subseteq> {a..b} \<Longrightarrow> Inf A \<in> {a..b}"
- by (rule closed_subset_contains_Inf)
+ by (rule closed_subset_contains_Inf)
(auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a])
lemma not_trivial_limit_within_ball:
@@ -2940,8 +2945,7 @@
by (auto simp add: norm_minus_commute)
also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
- unfolding distrib_right using \<open>x\<noteq>y\<close>[unfolded dist_nz, unfolded dist_norm]
- by auto
+ unfolding distrib_right using \<open>x\<noteq>y\<close> by auto
also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
by (auto simp add: dist_norm)
finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
@@ -3019,8 +3023,8 @@
apply (simp only: dist_norm [symmetric])
apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
apply (rule mult_strict_right_mono)
- apply (simp add: k_def zero_less_dist_iff \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
- apply (simp add: zero_less_dist_iff \<open>x \<noteq> y\<close>)
+ apply (simp add: k_def \<open>0 < r\<close> \<open>x \<noteq> y\<close>)
+ apply (simp add: \<open>x \<noteq> y\<close>)
done
then have "z \<in> ball x (dist x y)"
by simp
@@ -3055,14 +3059,14 @@
shows "interior (cball x e) = ball x e"
proof (cases "e \<ge> 0")
case False note cs = this
- from cs have "ball x e = {}"
+ from cs have null: "ball x e = {}"
using ball_empty[of e x] by auto
moreover
{
fix y
assume "y \<in> cball x e"
then have False
- unfolding mem_cball using dist_nz[of x y] cs by auto
+ by (metis ball_eq_empty null cs dist_eq_0_iff dist_le_zero_iff empty_subsetI mem_cball subset_antisym subset_ball)
}
then have "cball x e = {}" by auto
then have "interior (cball x e) = {}"
@@ -3088,9 +3092,7 @@
then have "y \<in> ball x e"
proof (cases "x = y")
case True
- then have "e > 0"
- using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball]
- by (auto simp add: dist_commute)
+ then have "e > 0" using cs order.order_iff_strict xa_cball xa_y by fastforce
then show "y \<in> ball x e"
using \<open>x = y \<close> by simp
next
@@ -5165,7 +5167,6 @@
assume "y \<in> f ` (ball x d \<inter> s)"
then have "y \<in> ball (f x) e"
using d(2)
- unfolding dist_nz[symmetric]
apply (auto simp add: dist_commute)
apply (erule_tac x=xa in ballE)
apply auto
@@ -5200,9 +5201,7 @@
apply (rule_tac x=d in exI)
apply auto
apply (erule_tac x=xa in allE)
- apply (auto simp add: dist_commute dist_nz)
- unfolding dist_nz[symmetric]
- apply auto
+ apply (auto simp add: dist_commute)
done
next
assume ?rhs
@@ -5214,7 +5213,7 @@
apply (rule_tac x=d in exI)
apply auto
apply (erule_tac x="f xa" in allE)
- apply (auto simp add: dist_commute dist_nz)
+ apply (auto simp add: dist_commute)
done
qed
@@ -5285,14 +5284,14 @@
fix T :: "'b set"
assume "open T" and "f a \<in> T"
with \<open>?lhs\<close> obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
- unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz)
+ unfolding continuous_within tendsto_def eventually_at by auto
have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
using x(2) \<open>d>0\<close> by simp
then have "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
proof eventually_elim
case (elim n)
then show ?case
- using d x(1) \<open>f a \<in> T\<close> unfolding dist_nz[symmetric] by auto
+ using d x(1) \<open>f a \<in> T\<close> by auto
qed
}
then show ?rhs
@@ -5414,30 +5413,15 @@
lemma continuous_transform_within:
fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
- assumes "0 < d"
+ assumes "continuous (at x within s) f"
+ and "0 < d"
and "x \<in> s"
- and "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
- and "continuous (at x within s) f"
+ and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
shows "continuous (at x within s) g"
+ using assms
unfolding continuous_within
-proof (rule Lim_transform_within)
- show "0 < d" by fact
- show "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
- using assms(3) by auto
- have "f x = g x"
- using assms(1,2,3) by auto
- then show "(f \<longlongrightarrow> g x) (at x within s)"
- using assms(4) unfolding continuous_within by simp
-qed
-
-lemma continuous_transform_at:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
- assumes "0 < d"
- and "\<forall>x'. dist x' x < d --> f x' = g x'"
- and "continuous (at x) f"
- shows "continuous (at x) g"
- using continuous_transform_within [of d x UNIV f g] assms by simp
-
+ by (force simp add: intro: Lim_transform_within)
+
subsubsection \<open>Structural rules for pointwise continuity\<close>
@@ -5762,7 +5746,7 @@
done
qed
-lemma isCont_indicator:
+lemma isCont_indicator:
fixes x :: "'a::t2_space"
shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
proof auto
@@ -6243,7 +6227,6 @@
shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'. norm(x' - x) < d --> \<bar>f x' - f x\<bar> < e)"
unfolding continuous_at
unfolding Lim_at
- unfolding dist_nz[symmetric]
unfolding dist_norm
apply auto
apply (erule_tac x=e in allE)
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy Fri Jan 08 15:49:01 2016 +0100
@@ -1,38 +1,497 @@
-section \<open>Binary Approximations to Constants\<close>
+section \<open>Numeric approximations to Constants\<close>
theory Approximations
-imports Complex_Transcendental
+imports "../Complex_Transcendental" "../Harmonic_Numbers"
+begin
+
+lemma eval_fact:
+ "fact 0 = 1"
+ "fact (Suc 0) = 1"
+ "fact (numeral n) = numeral n * fact (pred_numeral n)"
+ by (simp, simp, simp_all only: numeral_eq_Suc fact_Suc,
+ simp only: numeral_eq_Suc [symmetric] of_nat_numeral)
+
+lemma setsum_poly_horner_expand:
+ "(\<Sum>k<(numeral n::nat). f k * x^k) = f 0 + (\<Sum>k<pred_numeral n. f (k+1) * x^k) * x"
+ "(\<Sum>k<Suc 0. f k * x^k) = (f 0 :: 'a :: semiring_1)"
+ "(\<Sum>k<(0::nat). f k * x^k) = 0"
+proof -
+ {
+ fix m :: nat
+ have "(\<Sum>k<Suc m. f k * x^k) = f 0 + (\<Sum>k=Suc 0..<Suc m. f k * x^k)"
+ by (subst atLeast0LessThan [symmetric], subst setsum_head_upt_Suc) simp_all
+ also have "(\<Sum>k=Suc 0..<Suc m. f k * x^k) = (\<Sum>k<m. f (k+1) * x^k) * x"
+ by (subst setsum_shift_bounds_Suc_ivl)
+ (simp add: setsum_left_distrib algebra_simps atLeast0LessThan power_commutes)
+ finally have "(\<Sum>k<Suc m. f k * x ^ k) = f 0 + (\<Sum>k<m. f (k + 1) * x ^ k) * x" .
+ }
+ from this[of "pred_numeral n"]
+ show "(\<Sum>k<numeral n. f k * x^k) = f 0 + (\<Sum>k<pred_numeral n. f (k+1) * x^k) * x"
+ by (simp add: numeral_eq_Suc)
+qed simp_all
+
+lemma power_less_one:
+ assumes "n > 0" "x \<ge> 0" "x < 1"
+ shows "x ^ n < (1::'a::linordered_semidom)"
+proof -
+ from assms consider "x > 0" | "x = 0" by force
+ thus ?thesis
+ proof cases
+ assume "x > 0"
+ with assms show ?thesis
+ by (cases n) (simp, hypsubst, rule power_Suc_less_one)
+ qed (insert assms, cases n, simp_all)
+qed
+
+lemma combine_bounds:
+ "x \<in> {a1..b1} \<Longrightarrow> y \<in> {a2..b2} \<Longrightarrow> a3 = a1 + a2 \<Longrightarrow> b3 = b1 + b2 \<Longrightarrow> x + y \<in> {a3..(b3::real)}"
+ "x \<in> {a1..b1} \<Longrightarrow> y \<in> {a2..b2} \<Longrightarrow> a3 = a1 - b2 \<Longrightarrow> b3 = b1 - a2 \<Longrightarrow> x - y \<in> {a3..(b3::real)}"
+ "c \<ge> 0 \<Longrightarrow> x \<in> {a..b} \<Longrightarrow> c * x \<in> {c*a..c*b}"
+ by (auto simp: mult_left_mono)
+
+lemma approx_coarsen:
+ "\<bar>x - a1\<bar> \<le> eps1 \<Longrightarrow> \<bar>a1 - a2\<bar> \<le> eps2 - eps1 \<Longrightarrow> \<bar>x - a2\<bar> \<le> (eps2 :: real)"
+ by simp
+
+
+subsection \<open>Approximation of $\ln 2$\<close>
+
+context
begin
-declare of_real_numeral [simp]
-
-subsection\<open>Approximation to pi\<close>
+qualified lemma ln_approx_abs':
+ assumes "x > (1::real)"
+ assumes "(x-1)/(x+1) = y"
+ assumes "y^2 = ysqr"
+ assumes "(\<Sum>k<n. inverse (of_nat (2*k+1)) * ysqr^k) = approx"
+ assumes "y*ysqr^n / (1 - ysqr) / of_nat (2*n+1) = d"
+ assumes "d \<le> e"
+ shows "abs (ln x - (2*y*approx + d)) \<le> e"
+proof -
+ note ln_approx_abs[OF assms(1), of n]
+ also note assms(2)
+ also have "y^(2*n+1) = y*ysqr^n" by (simp add: assms(3)[symmetric] power_mult)
+ also note assms(3)
+ also note assms(5)
+ also note assms(5)
+ also note assms(6)
+ also have "(\<Sum>k<n. 2*y^(2*k+1) / real_of_nat (2 * k + 1)) = (2*y) * approx"
+ apply (subst assms(4)[symmetric], subst setsum_right_distrib)
+ apply (simp add: assms(3)[symmetric] power_mult)
+ apply (simp add: mult_ac divide_simps)?
+ done
+ finally show ?thesis .
+qed
-lemma sin_pi6_straddle:
- assumes "0 \<le> a" "a \<le> b" "b \<le> 4" "sin(a/6) \<le> 1/2" "1/2 \<le> sin(b/6)"
- shows "a \<le> pi \<and> pi \<le> b"
+lemma ln_2_approx: "\<bar>ln 2 - 0.69314718055\<bar> < inverse (2 ^ 36 :: real)" (is ?thesis1)
+ and ln_2_bounds: "ln (2::real) \<in> {0.693147180549..0.693147180561}" (is ?thesis2)
+proof -
+ def approx \<equiv> "0.69314718055 :: real" and approx' \<equiv> "4465284211343447 / 6442043387911560 :: real"
+ def d \<equiv> "inverse (195259926456::real)"
+ have "dist (ln 2) approx \<le> dist (ln 2) approx' + dist approx' approx" by (rule dist_triangle)
+ also have "\<bar>ln (2::real) - (2 * (1/3) * (651187280816108 / 626309773824735) +
+ inverse 195259926456)\<bar> \<le> inverse 195259926456"
+ proof (rule ln_approx_abs'[where n = 10])
+ show "(1/3::real)^2 = 1/9" by (simp add: power2_eq_square)
+ qed (simp_all add: eval_nat_numeral)
+ hence A: "dist (ln 2) approx' \<le> d" by (simp add: dist_real_def approx'_def d_def)
+ hence "dist (ln 2) approx' + dist approx' approx \<le> \<dots> + dist approx' approx"
+ by (rule add_right_mono)
+ also have "\<dots> < inverse (2 ^ 36)" by (simp add: dist_real_def approx'_def approx_def d_def)
+ finally show ?thesis1 unfolding dist_real_def approx_def .
+
+ from A have "ln 2 \<in> {approx' - d..approx' + d}"
+ by (simp add: dist_real_def abs_real_def split: split_if_asm)
+ also have "\<dots> \<subseteq> {0.693147180549..0.693147180561}"
+ by (subst atLeastatMost_subset_iff, rule disjI2) (simp add: approx'_def d_def)
+ finally show ?thesis2 .
+qed
+
+end
+
+
+subsection \<open>Approximation of the Euler--Mascheroni constant\<close>
+
+lemma euler_mascheroni_approx:
+ defines "approx \<equiv> 0.577257 :: real" and "e \<equiv> 0.000063 :: real"
+ shows "abs (euler_mascheroni - approx :: real) < e"
+ (is "abs (_ - ?approx) < ?e")
proof -
- have *: "\<And>x::real. 0 < x & x < 7/5 \<Longrightarrow> 0 < sin x"
- using pi_ge_two
- by (auto intro: sin_gt_zero)
- have ab: "(b \<le> pi * 3 \<Longrightarrow> pi \<le> b)" "(a \<le> pi * 3 \<Longrightarrow> a \<le> pi)"
- using sin_mono_le_eq [of "pi/6" "b/6"] sin_mono_le_eq [of "a/6" "pi/6"] assms
- by (simp_all add: sin_30 power.power_Suc norm_divide)
- show ?thesis
- using assms Taylor_sin [of "a/6" 0] pi_ge_two
- by (auto simp: sin_30 power.power_Suc norm_divide intro: ab)
+ def l \<equiv> "47388813395531028639296492901910937/82101866951584879688289000000000000 :: real"
+ def u \<equiv> "142196984054132045946501548559032969 / 246305600854754639064867000000000000 :: real"
+ have impI: "P \<longrightarrow> Q" if Q for P Q using that by blast
+ have hsum_63: "harm 63 = (310559566510213034489743057 / 65681493561267903750631200 ::real)"
+ by (simp add: harm_expand)
+ from harm_Suc[of 63] have hsum_64: "harm 64 =
+ 623171679694215690971693339 / (131362987122535807501262400::real)"
+ by (subst (asm) hsum_63) simp
+ have "ln (64::real) = real (6::nat) * ln 2" by (subst ln_realpow[symmetric]) simp_all
+ hence "ln (real_of_nat (Suc 63)) \<in> {4.158883083293<..<4.158883083367}" using ln_2_bounds by simp
+ from euler_mascheroni_bounds'[OF _ this]
+ have "(euler_mascheroni :: real) \<in> {l<..<u}"
+ by (simp add: hsum_63 del: greaterThanLessThan_iff) (simp only: l_def u_def)
+ also have "\<dots> \<subseteq> {approx - e<..<approx + e}"
+ by (subst greaterThanLessThan_subseteq_greaterThanLessThan, rule impI)
+ (simp add: approx_def e_def u_def l_def)
+ finally show ?thesis by (simp add: abs_real_def)
+qed
+
+
+subsection \<open>Approximation to pi\<close>
+
+
+subsubsection \<open>Approximating the arctangent\<close>
+
+definition arctan_approx where
+ "arctan_approx n x = x * (\<Sum>k<n. (-(x^2))^k / real (2*k+1))"
+
+lemma arctan_series':
+ assumes "\<bar>x\<bar> \<le> 1"
+ shows "(\<lambda>k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1))) sums arctan x"
+ using summable_arctan_series[OF assms] arctan_series[OF assms] by (simp add: sums_iff)
+
+lemma arctan_approx:
+ assumes x: "0 \<le> x" "x < 1" and n: "even n"
+ shows "arctan x - arctan_approx n x \<in> {0..x^(2*n+1) / (1-x^4)}"
+proof -
+ def c \<equiv> "\<lambda>k. 1 / (1+(4*real k + 2*real n)) - x\<^sup>2 / (3+(4*real k + 2*real n))"
+ from assms have "(\<lambda>k. (-1) ^ k * (1 / real (k * 2 + 1) * x^(k*2+1))) sums arctan x"
+ using arctan_series' by simp
+ also have "(\<lambda>k. (-1) ^ k * (1 / real (k * 2 + 1) * x^(k*2+1))) =
+ (\<lambda>k. x * ((- (x^2))^k / real (2*k+1)))"
+ by (simp add: power2_eq_square power_mult power_mult_distrib mult_ac power_minus')
+ finally have "(\<lambda>k. x * ((- x\<^sup>2) ^ k / real (2 * k + 1))) sums arctan x" .
+ from sums_split_initial_segment[OF this, of n]
+ have "(\<lambda>i. x * ((- x\<^sup>2) ^ (i + n) / real (2 * (i + n) + 1))) sums
+ (arctan x - arctan_approx n x)"
+ by (simp add: arctan_approx_def setsum_right_distrib)
+ from sums_group[OF this, of 2] assms
+ have sums: "(\<lambda>k. x * (x\<^sup>2)^n * (x^4)^k * c k) sums (arctan x - arctan_approx n x)"
+ by (simp add: algebra_simps power_add power_mult [symmetric] c_def)
+
+ from assms have "0 \<le> arctan x - arctan_approx n x"
+ by (intro sums_le[OF _ sums_zero sums] allI mult_nonneg_nonneg)
+ (auto intro!: frac_le power_le_one simp: c_def)
+ moreover {
+ from assms have "c k \<le> 1 - 0" for k unfolding c_def
+ by (intro diff_mono divide_nonneg_nonneg add_nonneg_nonneg) auto
+ with assms have "x * x\<^sup>2 ^ n * (x ^ 4) ^ k * c k \<le> x * x\<^sup>2 ^ n * (x ^ 4) ^ k * 1" for k
+ by (intro mult_left_mono mult_right_mono mult_nonneg_nonneg) simp_all
+ with assms have "arctan x - arctan_approx n x \<le> x * (x\<^sup>2)^n * (1 / (1 - x^4))"
+ by (intro sums_le[OF _ sums sums_mult[OF geometric_sums]] allI mult_left_mono)
+ (auto simp: power_less_one)
+ also have "x * (x^2)^n = x^(2*n+1)" by (simp add: power_mult power_add)
+ finally have "arctan x - arctan_approx n x \<le> x^(2*n+1) / (1 - x^4)" by simp
+ }
+ ultimately show ?thesis by simp
+qed
+
+lemma arctan_approx_def': "arctan_approx n (1/x) =
+ (\<Sum>k<n. inverse (real (2 * k + 1) * (- x\<^sup>2) ^ k)) / x"
+proof -
+ have "(-1)^k / b = 1 / ((-1)^k * b)" for k :: nat and b :: real
+ by (cases "even k") auto
+ thus ?thesis by (simp add: arctan_approx_def field_simps power_minus')
+qed
+
+lemma expand_arctan_approx:
+ "(\<Sum>k<(numeral n::nat). inverse (f k) * inverse (x ^ k)) =
+ inverse (f 0) + (\<Sum>k<pred_numeral n. inverse (f (k+1)) * inverse (x^k)) / x"
+ "(\<Sum>k<Suc 0. inverse (f k) * inverse (x^k)) = inverse (f 0 :: 'a :: field)"
+ "(\<Sum>k<(0::nat). inverse (f k) * inverse (x^k)) = 0"
+proof -
+ {
+ fix m :: nat
+ have "(\<Sum>k<Suc m. inverse (f k * x^k)) =
+ inverse (f 0) + (\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k))"
+ by (subst atLeast0LessThan [symmetric], subst setsum_head_upt_Suc) simp_all
+ also have "(\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k)) = (\<Sum>k<m. inverse (f (k+1) * x^k)) / x"
+ by (subst setsum_shift_bounds_Suc_ivl)
+ (simp add: setsum_right_distrib divide_inverse algebra_simps
+ atLeast0LessThan power_commutes)
+ finally have "(\<Sum>k<Suc m. inverse (f k) * inverse (x ^ k)) =
+ inverse (f 0) + (\<Sum>k<m. inverse (f (k + 1)) * inverse (x ^ k)) / x" by simp
+ }
+ from this[of "pred_numeral n"]
+ show "(\<Sum>k<numeral n. inverse (f k) * inverse (x^k)) =
+ inverse (f 0) + (\<Sum>k<pred_numeral n. inverse (f (k+1)) * inverse (x^k)) / x"
+ by (simp add: numeral_eq_Suc)
+qed simp_all
+
+lemma arctan_diff_small:
+ assumes "\<bar>x*y::real\<bar> < 1"
+ shows "arctan x - arctan y = arctan ((x - y) / (1 + x * y))"
+proof -
+ have "arctan x - arctan y = arctan x + arctan (-y)" by (simp add: arctan_minus)
+ also from assms have "\<dots> = arctan ((x - y) / (1 + x * y))" by (subst arctan_add_small) simp_all
+ finally show ?thesis .
qed
-(*32-bit approximation. SLOW simplification steps: big calculations with the rewriting engine*)
-lemma pi_approx_32: "\<bar>pi - 13493037705/4294967296\<bar> \<le> inverse(2 ^ 32)"
- apply (simp only: abs_diff_le_iff)
- apply (rule sin_pi6_straddle, simp_all)
- using Taylor_sin [of "1686629713/3221225472" 11]
- apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral power_divide)
- apply (simp only: pos_le_divide_eq [symmetric])
- using Taylor_sin [of "6746518853/12884901888" 11]
- apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral power_divide)
- apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric])
- done
+
+subsubsection \<open>Machin-like formulae for pi\<close>
+
+text \<open>
+ We first define a small proof method that can prove Machin-like formulae for @{term "pi"}
+ automatically. Unfortunately, this takes far too much time for larger formulae because
+ the numbers involved become too large.
+\<close>
+
+definition "MACHIN_TAG a b \<equiv> a * (b::real)"
+
+lemma numeral_horner_MACHIN_TAG:
+ "MACHIN_TAG Numeral1 x = x"
+ "MACHIN_TAG (numeral (Num.Bit0 (Num.Bit0 n))) x =
+ MACHIN_TAG 2 (MACHIN_TAG (numeral (Num.Bit0 n)) x)"
+ "MACHIN_TAG (numeral (Num.Bit0 (Num.Bit1 n))) x =
+ MACHIN_TAG 2 (MACHIN_TAG (numeral (Num.Bit1 n)) x)"
+ "MACHIN_TAG (numeral (Num.Bit1 n)) x =
+ MACHIN_TAG 2 (MACHIN_TAG (numeral n) x) + x"
+ unfolding numeral_Bit0 numeral_Bit1 ring_distribs one_add_one[symmetric] MACHIN_TAG_def
+ by (simp_all add: algebra_simps)
+
+lemma tag_machin: "a * arctan b = MACHIN_TAG a (arctan b)" by (simp add: MACHIN_TAG_def)
+
+lemma arctan_double': "\<bar>a::real\<bar> < 1 \<Longrightarrow> MACHIN_TAG 2 (arctan a) = arctan (2 * a / (1 - a*a))"
+ unfolding MACHIN_TAG_def by (simp add: arctan_double power2_eq_square)
+
+ML \<open>
+ fun machin_term_conv ctxt ct =
+ let
+ val ctxt' = ctxt addsimps @{thms arctan_double' arctan_add_small}
+ in
+ case Thm.term_of ct of
+ Const (@{const_name MACHIN_TAG}, _) $ _ $
+ (Const (@{const_name "Transcendental.arctan"}, _) $ _) =>
+ Simplifier.rewrite ctxt' ct
+ |
+ Const (@{const_name MACHIN_TAG}, _) $ _ $
+ (Const (@{const_name "Groups.plus"}, _) $
+ (Const (@{const_name "Transcendental.arctan"}, _) $ _) $
+ (Const (@{const_name "Transcendental.arctan"}, _) $ _)) =>
+ Simplifier.rewrite ctxt' ct
+ | _ => raise CTERM ("machin_conv", [ct])
+ end
+
+ fun machin_tac ctxt =
+ let val conv = Conv.top_conv (Conv.try_conv o machin_term_conv) ctxt
+ in
+ SELECT_GOAL (
+ Local_Defs.unfold_tac ctxt
+ @{thms tag_machin[THEN eq_reflection] numeral_horner_MACHIN_TAG[THEN eq_reflection]}
+ THEN REPEAT (CHANGED (HEADGOAL (CONVERSION conv))))
+ THEN' Simplifier.simp_tac (ctxt addsimps @{thms arctan_add_small arctan_diff_small})
+ end
+\<close>
+
+method_setup machin = \<open>Scan.succeed (SIMPLE_METHOD' o machin_tac)\<close>
+
+text \<open>
+ We can now prove the ``standard'' Machin formula, which was already proven manually
+ in Isabelle, automatically.
+}\<close>
+lemma "pi / 4 = (4::real) * arctan (1 / 5) - arctan (1 / 239)"
+ by machin
+
+text \<open>
+ We can also prove the following more complicated formula:
+\<close>
+lemma machin': "pi/4 = (12::real) * arctan (1/18) + 8 * arctan (1/57) - 5 * arctan (1/239)"
+ by machin
+
+
+
+subsubsection \<open>Simple approximation of pi\<close>
+
+text \<open>
+ We can use the simple Machin formula and the Taylor series expansion of the arctangent
+ to approximate pi. For a given even natural number $n$, we expand @{term "arctan (1/5)"}
+ to $3n$ summands and @{term "arctan (1/239)"} to $n$ summands. This gives us at least
+ $13n-2$ bits of precision.
+\<close>
+
+definition "pi_approx n = 16 * arctan_approx (3*n) (1/5) - 4 * arctan_approx n (1/239)"
+
+lemma pi_approx:
+ fixes n :: nat assumes n: "even n" and "n > 0"
+ shows "\<bar>pi - pi_approx n\<bar> \<le> inverse (2^(13*n - 2))"
+proof -
+ from n have n': "even (3*n)" by simp
+ -- \<open>We apply the Machin formula\<close>
+ from machin have "pi = 16 * arctan (1/5) - 4 * arctan (1/239::real)" by simp
+ -- \<open>Taylor series expansion of the arctangent\<close>
+ also from arctan_approx[OF _ _ n', of "1/5"] arctan_approx[OF _ _ n, of "1/239"]
+ have "\<dots> - pi_approx n \<in> {-4*((1/239)^(2*n+1) / (1-(1/239)^4))..16*(1/5)^(6*n+1) / (1-(1/5)^4)}"
+ by (simp add: pi_approx_def)
+ -- \<open>Coarsening the bounds to make them a bit nicer\<close>
+ also have "-4*((1/239::real)^(2*n+1) / (1-(1/239)^4)) = -((13651919 / 815702160) / 57121^n)"
+ by (simp add: power_mult power2_eq_square) (simp add: field_simps)
+ also have "16*(1/5)^(6*n+1) / (1-(1/5::real)^4) = (125/39) / 15625^n"
+ by (simp add: power_mult power2_eq_square) (simp add: field_simps)
+ also have "{-((13651919 / 815702160) / 57121^n) .. (125 / 39) / 15625^n} \<subseteq>
+ {- (4 / 2^(13*n)) .. 4 / (2^(13*n)::real)}"
+ by (subst atLeastatMost_subset_iff, intro disjI2 conjI le_imp_neg_le)
+ (rule frac_le; simp add: power_mult power_mono)+
+ finally have "abs (pi - pi_approx n) \<le> 4 / 2^(13*n)" by auto
+ also from \<open>n > 0\<close> have "4 / 2^(13*n) = 1 / (2^(13*n - 2) :: real)"
+ by (cases n) (simp_all add: power_add)
+ finally show ?thesis by (simp add: divide_inverse)
+qed
+
+lemma pi_approx':
+ fixes n :: nat assumes n: "even n" and "n > 0" and "k \<le> 13*n - 2"
+ shows "\<bar>pi - pi_approx n\<bar> \<le> inverse (2^k)"
+ using assms(3) by (intro order.trans[OF pi_approx[OF assms(1,2)]]) (simp_all add: field_simps)
+
+text \<open>We can now approximate pi to 22 decimals within a fraction of a second.\<close>
+lemma pi_approx_75: "abs (pi - 3.1415926535897932384626 :: real) \<le> inverse (10^22)"
+proof -
+ def a \<equiv> "8295936325956147794769600190539918304 / 2626685325478320010006427764892578125 :: real"
+ def b \<equiv> "8428294561696506782041394632 / 503593538783547230635598424135 :: real"
+ -- \<open>The introduction of this constant prevents the simplifier from applying solvers that
+ we don't want. We want it to simply evaluate the terms to rational constants.}\<close>
+ def eq \<equiv> "op = :: real \<Rightarrow> real \<Rightarrow> bool"
+
+ -- \<open>Splitting the computation into several steps has the advantage that simplification can
+ be done in parallel\<close>
+ have "abs (pi - pi_approx 6) \<le> inverse (2^76)" by (rule pi_approx') simp_all
+ also have "pi_approx 6 = 16 * arctan_approx (3 * 6) (1 / 5) - 4 * arctan_approx 6 (1 / 239)"
+ unfolding pi_approx_def by simp
+ also have [unfolded eq_def]: "eq (16 * arctan_approx (3 * 6) (1 / 5)) a"
+ by (simp add: arctan_approx_def' power2_eq_square,
+ simp add: expand_arctan_approx, unfold a_def eq_def, rule refl)
+ also have [unfolded eq_def]: "eq (4 * arctan_approx 6 (1 / 239::real)) b"
+ by (simp add: arctan_approx_def' power2_eq_square,
+ simp add: expand_arctan_approx, unfold b_def eq_def, rule refl)
+ also have [unfolded eq_def]:
+ "eq (a - b) (171331331860120333586637094112743033554946184594977368554649608 /
+ 54536456744112171868276045488779391002026386559009552001953125)"
+ by (unfold a_def b_def, simp, unfold eq_def, rule refl)
+ finally show ?thesis by (rule approx_coarsen) simp
+qed
+
+text \<open>
+ The previous estimate of pi in this file was based on approximating the root of the
+ $\sin(\pi/6)$ in the interval $[0;4]$ using the Taylor series expansion of the sine to
+ verify that it is between two given bounds.
+ This was much slower and much less precise. We can easily recover this coarser estimate from
+ the newer, precise estimate:
+\<close>
+lemma pi_approx_32: "\<bar>pi - 13493037705/4294967296 :: real\<bar> \<le> inverse(2 ^ 32)"
+ by (rule approx_coarsen[OF pi_approx_75]) simp
+
+
+subsection \<open>A more complicated approximation of pi\<close>
+
+text \<open>
+ There are more complicated Machin-like formulae that have more terms with larger
+ denominators. Although they have more terms, each term requires fewer summands of the
+ Taylor series for the same precision, since it is evaluated closer to $0$.
+
+ Using a good formula, one can therefore obtain the same precision with fewer operations.
+ The big formulae used for computations of pi in practice are too complicated for us to
+ prove here, but we can use the three-term Machin-like formula @{thm machin'}.
+\<close>
+
+definition "pi_approx2 n = 48 * arctan_approx (6*n) (1/18::real) +
+ 32 * arctan_approx (4*n) (1/57) - 20 * arctan_approx (3*n) (1/239)"
+
+lemma pi_approx2:
+ fixes n :: nat assumes n: "even n" and "n > 0"
+ shows "\<bar>pi - pi_approx2 n\<bar> \<le> inverse (2^(46*n - 1))"
+proof -
+ from n have n': "even (6*n)" "even (4*n)" "even (3*n)" by simp_all
+ from machin' have "pi = 48 * arctan (1/18) + 32 * arctan (1/57) - 20 * arctan (1/239::real)"
+ by simp
+ hence "pi - pi_approx2 n = 48 * (arctan (1/18) - arctan_approx (6*n) (1/18)) +
+ 32 * (arctan (1/57) - arctan_approx (4*n) (1/57)) -
+ 20 * (arctan (1/239) - arctan_approx (3*n) (1/239))"
+ by (simp add: pi_approx2_def)
+ also have "\<dots> \<in> {-((20/239/(1-(1/239)^4)) * (1/239)^(6*n))..
+ (48/18 / (1-(1/18)^4))*(1/18)^(12*n) + (32/57/(1-(1/57)^4)) * (1/57)^(8*n)}"
+ (is "_ \<in> {-?l..?u1 + ?u2}")
+ apply ((rule combine_bounds(1,2))+; (rule combine_bounds(3); (rule arctan_approx)?)?)
+ apply (simp_all add: n)
+ apply (simp_all add: divide_simps)?
+ done
+ also {
+ have "?l \<le> (1/8) * (1/2)^(46*n)"
+ unfolding power_mult by (intro mult_mono power_mono) (simp_all add: divide_simps)
+ also have "\<dots> \<le> (1/2) ^ (46 * n - 1)"
+ by (cases n; simp_all add: power_add divide_simps)
+ finally have "?l \<le> (1/2) ^ (46 * n - 1)" .
+ moreover {
+ have "?u1 + ?u2 \<le> 4 * (1/2)^(48*n) + 1 * (1/2)^(46*n)"
+ unfolding power_mult by (intro add_mono mult_mono power_mono) (simp_all add: divide_simps)
+ also from \<open>n > 0\<close> have "4 * (1/2::real)^(48*n) \<le> (1/2)^(46*n)"
+ by (cases n) (simp_all add: field_simps power_add)
+ also from \<open>n > 0\<close> have "(1/2::real) ^ (46 * n) + 1 * (1 / 2) ^ (46 * n) = (1/2) ^ (46 * n - 1)"
+ by (cases n; simp_all add: power_add power_divide)
+ finally have "?u1 + ?u2 \<le> (1/2) ^ (46 * n - 1)" by - simp
+ }
+ ultimately have "{-?l..?u1 + ?u2} \<subseteq> {-((1/2)^(46*n-1))..(1/2)^(46*n-1)}"
+ by (subst atLeastatMost_subset_iff) simp_all
+ }
+ finally have "\<bar>pi - pi_approx2 n\<bar> \<le> ((1/2) ^ (46 * n - 1))" by auto
+ thus ?thesis by (simp add: divide_simps)
+qed
+
+lemma pi_approx2':
+ fixes n :: nat assumes n: "even n" and "n > 0" and "k \<le> 46*n - 1"
+ shows "\<bar>pi - pi_approx2 n\<bar> \<le> inverse (2^k)"
+ using assms(3) by (intro order.trans[OF pi_approx2[OF assms(1,2)]]) (simp_all add: field_simps)
+
+text \<open>
+ We can now approximate pi to 54 decimals using this formula. The computations are much
+ slower now; this is mostly because we use arbitrary-precision rational numbers, whose
+ numerators and demoninators get very large. Using dyadic floating point numbers would be
+ much more economical.
+\<close>
+lemma pi_approx_54_decimals:
+ "abs (pi - 3.141592653589793238462643383279502884197169399375105821 :: real) \<le> inverse (10^54)"
+ (is "abs (pi - ?pi') \<le> _")
+proof -
+ def a \<equiv> "2829469759662002867886529831139137601191652261996513014734415222704732791803 /
+ 1062141879292765061960538947347721564047051545995266466660439319087625011200 :: real"
+ def b \<equiv> "13355545553549848714922837267299490903143206628621657811747118592 /
+ 23792006023392488526789546722992491355941103837356113731091180925 :: real"
+ def c \<equiv> "28274063397213534906669125255762067746830085389618481175335056 /
+ 337877029279505250241149903214554249587517250716358486542628059 :: real"
+ let ?pi'' = "3882327391761098513316067116522233897127356523627918964967729040413954225768920394233198626889767468122598417405434625348404038165437924058179155035564590497837027530349 /
+ 1235783190199688165469648572769847552336447197542738425378629633275352407743112409829873464564018488572820294102599160968781449606552922108667790799771278860366957772800"
+ def eq \<equiv> "op = :: real \<Rightarrow> real \<Rightarrow> bool"
+
+ have "abs (pi - pi_approx2 4) \<le> inverse (2^183)" by (rule pi_approx2') simp_all
+ also have "pi_approx2 4 = 48 * arctan_approx 24 (1 / 18) +
+ 32 * arctan_approx 16 (1 / 57) -
+ 20 * arctan_approx 12 (1 / 239)"
+ unfolding pi_approx2_def by simp
+ also have [unfolded eq_def]: "eq (48 * arctan_approx 24 (1 / 18)) a"
+ by (simp add: arctan_approx_def' power2_eq_square,
+ simp add: expand_arctan_approx, unfold a_def eq_def, rule refl)
+ also have [unfolded eq_def]: "eq (32 * arctan_approx 16 (1 / 57::real)) b"
+ by (simp add: arctan_approx_def' power2_eq_square,
+ simp add: expand_arctan_approx, unfold b_def eq_def, rule refl)
+ also have [unfolded eq_def]: "eq (20 * arctan_approx 12 (1 / 239::real)) c"
+ by (simp add: arctan_approx_def' power2_eq_square,
+ simp add: expand_arctan_approx, unfold c_def eq_def, rule refl)
+ also have [unfolded eq_def]:
+ "eq (a + b) (34326487387865555303797183505809267914709125998469664969258315922216638779011304447624792548723974104030355722677 /
+ 10642967245546718617684989689985787964158885991018703366677373121531695267093031090059801733340658960857196134400)"
+ by (unfold a_def b_def c_def, simp, unfold eq_def, rule refl)
+ also have [unfolded eq_def]: "eq (\<dots> - c) ?pi''"
+ by (unfold a_def b_def c_def, simp, unfold eq_def, rule refl)
+ -- \<open>This is incredibly slow because the numerators and denominators are huge.\<close>
+ finally show ?thesis by (rule approx_coarsen) simp
+qed
+
+text \<open>A 128 bit approximation of pi:\<close>
+lemma pi_approx_128:
+ "abs (pi - 1069028584064966747859680373161870783301 / 2^128) \<le> inverse (2^128)"
+ by (rule approx_coarsen[OF pi_approx_54_decimals]) simp
+
+text \<open>A 64 bit approximation of pi:\<close>
+lemma pi_approx_64:
+ "abs (pi - 57952155664616982739 / 2^64 :: real) \<le> inverse (2^64)"
+ by (rule approx_coarsen[OF pi_approx_54_decimals]) simp
end
--- a/src/HOL/Probability/Sinc_Integral.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy Fri Jan 08 15:49:01 2016 +0100
@@ -126,7 +126,7 @@
by (auto simp: isCont_def sinc_at_0)
next
assume "x \<noteq> 0" show ?thesis
- by (rule continuous_transform_at [where d = "abs x" and f = "\<lambda>x. sin x / x"])
+ by (rule continuous_transform_within [where d = "abs x" and f = "\<lambda>x. sin x / x"])
(auto simp add: dist_real_def \<open>x \<noteq> 0\<close>)
qed
--- a/src/HOL/Real_Vector_Spaces.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Jan 08 15:49:01 2016 +0100
@@ -1056,6 +1056,8 @@
shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
by (simp add: zero_less_dist_iff)
+declare dist_nz [symmetric, simp]
+
lemma dist_triangle_le:
shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
by (rule order_trans [OF dist_triangle2])
@@ -1673,7 +1675,7 @@
lemma eventually_at:
fixes a :: "'a :: metric_space"
shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
- unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_nz)
+ unfolding eventually_at_filter eventually_nhds_metric by auto
lemma eventually_at_le:
fixes a :: "'a::metric_space"
--- a/src/HOL/Relation.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Relation.thy Fri Jan 08 15:49:01 2016 +0100
@@ -515,6 +515,8 @@
lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r"
by (simp add: total_on_def)
+lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}"
+ by force
subsubsection \<open>Diagonal: identity over a set\<close>
@@ -873,6 +875,12 @@
lemma snd_eq_Range: "snd ` R = Range R"
by force
+lemma range_fst [simp]: "range fst = UNIV"
+ by (auto simp: fst_eq_Domain)
+
+lemma range_snd [simp]: "range snd = UNIV"
+ by (auto simp: snd_eq_Range)
+
lemma Domain_empty [simp]: "Domain {} = {}"
by auto
--- a/src/HOL/Series.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Series.thy Fri Jan 08 15:49:01 2016 +0100
@@ -30,6 +30,12 @@
where
"suminf f = (THE s. f sums s)"
+lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
+ apply (simp add: sums_def)
+ apply (subst LIMSEQ_Suc_iff [symmetric])
+ apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
+ done
+
subsection \<open>Infinite summability on topological monoids\<close>
lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
@@ -674,7 +680,7 @@
text\<open>Relations among convergence and absolute convergence for power series.\<close>
-lemma abel_lemma:
+lemma Abel_lemma:
fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
shows "summable (\<lambda>n. norm (a n) * r^n)"
@@ -792,10 +798,10 @@
by (rule Cauchy_product_sums [THEN sums_unique])
lemma summable_Cauchy_product:
- assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))"
+ assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))"
"summable (\<lambda>k. norm (b k))"
shows "summable (\<lambda>k. \<Sum>i\<le>k. a i * b (k - i))"
- using Cauchy_product_sums[OF assms] by (simp add: sums_iff)
+ using Cauchy_product_sums[OF assms] by (simp add: sums_iff)
subsection \<open>Series on @{typ real}s\<close>
--- a/src/HOL/Set.thy Thu Jan 07 16:50:52 2016 +0100
+++ b/src/HOL/Set.thy Fri Jan 08 15:49:01 2016 +0100
@@ -846,7 +846,10 @@
lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
by blast
-lemma diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"
+lemma Diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"
+ by blast
+
+lemma subset_Diff_insert: "A \<subseteq> B - (insert x C) \<longleftrightarrow> A \<subseteq> B - C \<and> x \<notin> A"
by blast
lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"