New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Apr 25 16:39:54 2017 +0100
@@ -1727,8 +1727,7 @@
next
case False
then have k: "0 < k" "k < 1" "complex_of_real k \<noteq> 1"
- using assms apply auto
- using of_real_eq_iff by fastforce
+ using assms by auto
have c': "c = k *\<^sub>R (b - a) + a"
by (metis diff_add_cancel c)
have bc: "(b - c) = (1 - k) *\<^sub>R (b - a)"
@@ -3871,7 +3870,7 @@
shows
"\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
\<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
- \<Longrightarrow> \<bar>Re(winding_number \<gamma> z)\<bar> < 1"
+ \<Longrightarrow> Re(winding_number \<gamma> z) < 1"
by (auto simp: not_less dest: winding_number_big_meets)
text\<open>One way of proving that WN=1 for a loop.\<close>
@@ -6532,6 +6531,21 @@
apply (force simp add: summable_Re o_def nonneg_Reals_cmod_eq_Re image_subset_iff)
done
+text\<open>Sometimes convenient to compare with a complex series of positive reals. (?)\<close>
+lemma series_differentiable_comparison_complex:
+ fixes S :: "complex set"
+ assumes S: "open S"
+ and hfd: "\<And>n x. x \<in> S \<Longrightarrow> f n field_differentiable (at x)"
+ and to_g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>d h. 0 < d \<and> summable h \<and> range h \<subseteq> \<real>\<^sub>\<ge>\<^sub>0 \<and> (\<forall>\<^sub>F n in sequentially. \<forall>y\<in>ball x d \<inter> S. cmod(f n y) \<le> cmod (h n))"
+ obtains g where "\<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> g field_differentiable (at x)"
+proof -
+ have hfd': "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative deriv (f n) x) (at x)"
+ using hfd field_differentiable_derivI by blast
+ have "\<exists>g g'. \<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. deriv (f n) x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
+ by (metis series_and_derivative_comparison_complex [OF S hfd' to_g])
+ then show ?thesis
+ using field_differentiable_def that by blast
+qed
text\<open>In particular, a power series is analytic inside circle of convergence.\<close>
@@ -7441,5 +7455,4 @@
homotopic_paths_imp_homotopic_loops)
using valid_path_imp_path by blast
-
end
--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Apr 25 16:39:54 2017 +0100
@@ -709,6 +709,7 @@
apply (simp only: pos_le_divide_eq [symmetric], linarith)
done
+text\<open>An odd contrast with the much more easily proved @{thm exp_le}\<close>
lemma e_less_3: "exp 1 < (3::real)"
using e_approx_32
by (simp add: abs_if split: if_split_asm)
@@ -1752,7 +1753,7 @@
declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
-lemma has_field_derivative_powr_right:
+lemma has_field_derivative_powr_right [derivative_intros]:
"w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
apply (simp add: powr_def)
apply (intro derivative_eq_intros | simp)+
--- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Apr 25 16:39:54 2017 +0100
@@ -1244,7 +1244,7 @@
by (meson Tsb min.cobounded1 order_trans r subset_ball)
ultimately have False
using inj_onD [OF injf, of y0 y1] \<open>y0 \<in> T\<close> \<open>y1 \<in> T\<close>
- using fd [of y0] fd [of y1] complex_root_unity [of n 1]
+ using fd [of y0] fd [of y1] complex_root_unity [of n 1] n_ne
apply (simp add: y0 y1 power_mult_distrib)
apply (force simp: algebra_simps)
done
--- a/src/HOL/Analysis/Gamma_Function.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Tue Apr 25 16:39:54 2017 +0100
@@ -1880,7 +1880,7 @@
show "G x \<ge> Gamma x"
proof (rule tendsto_upperbound)
from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
- using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
+ using x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "1::nat"]])
qed (simp_all add: Gamma_series_LIMSEQ)
next
show "G x \<le> Gamma x"
@@ -1891,7 +1891,7 @@
thus "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x" by simp
next
from G_upper[of x] show "eventually (\<lambda>n. Gamma_series x n * (1 + x / real n) \<ge> G x) sequentially"
- using eventually_ge_at_top[of "2::nat"] x by (auto elim!: eventually_mono)
+ using x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "2::nat"]])
qed simp_all
qed
@@ -2472,9 +2472,9 @@
let ?r' = "\<lambda>n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))"
from z have z': "z \<noteq> 0" by auto
- have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" using eventually_gt_at_top[of "0::nat"]
+ have "eventually (\<lambda>n. ?r' n = ?r n) sequentially"
using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac
- elim!: eventually_mono dest: pochhammer_eq_0_imp_nonpos_Int)
+ intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int)
moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all
ultimately show "?r \<longlonglongrightarrow> 1" by (force dest!: Lim_transform_eventually)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Apr 25 16:39:54 2017 +0100
@@ -2578,36 +2578,38 @@
proof (rule integrable_uniform_limit, safe)
fix e :: real
assume e: "e > 0"
- from compact_uniformly_continuous[OF assms compact_cbox,unfolded uniformly_continuous_on_def,rule_format,OF e] guess d ..
- note d=conjunctD2[OF this,rule_format]
- from fine_division_exists[OF gauge_ball[OF d(1)], of a b] guess p . note p=this
- note p' = tagged_division_ofD[OF p(1)]
+ then obtain d where "0 < d" and d: "\<And>x x'. \<lbrakk>x \<in> cbox a b; x' \<in> cbox a b; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+ using compact_uniformly_continuous[OF assms compact_cbox] unfolding uniformly_continuous_on_def by metis
+ obtain p where ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x d) fine p"
+ using fine_division_exists[OF gauge_ball[OF \<open>0 < d\<close>], of a b] .
have *: "\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
proof (safe, unfold snd_conv)
fix x l
assume as: "(x, l) \<in> p"
- from p'(4)[OF this] guess a b by (elim exE) note l=this
+ obtain a b where l: "l = cbox a b"
+ using as ptag by blast
+ then have x: "x \<in> cbox a b"
+ using as ptag by auto
show "\<exists>g. (\<forall>x\<in>l. norm (f x - g x) \<le> e) \<and> g integrable_on l"
apply (rule_tac x="\<lambda>y. f x" in exI)
proof safe
show "(\<lambda>y. f x) integrable_on l"
- unfolding integrable_on_def l
- apply rule
- apply (rule has_integral_const)
- done
+ unfolding integrable_on_def l by blast
+ next
fix y
assume y: "y \<in> l"
- note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
- note d(2)[OF _ _ this[unfolded mem_ball]]
+ then have "y \<in> ball x d"
+ using as finep by fastforce
then show "norm (f y - f x) \<le> e"
- using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce
+ using d x y as l
+ by (metis dist_commute dist_norm less_imp_le mem_ball ptag subsetCE tagged_division_ofD(3))
qed
qed
from e have "e \<ge> 0"
by auto
- from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
- then show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
- by auto
+ from approximable_on_division[OF this division_of_tagged_division[OF ptag] *]
+ show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+ by metis
qed
lemma integrable_continuous_interval:
@@ -6278,89 +6280,6 @@
qed
-subsection \<open>Geometric progression\<close>
-
-text \<open>FIXME: Should one or more of these theorems be moved to
- \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
-
-lemma sum_gp_basic:
- fixes x :: "'a::ring_1"
- shows "(1 - x) * sum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
-proof -
- define y where "y = 1 - x"
- have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
- by (induct n) (simp_all add: algebra_simps)
- then show ?thesis
- unfolding y_def by simp
-qed
-
-lemma sum_gp_multiplied:
- assumes mn: "m \<le> n"
- shows "((1::'a::{field}) - x) * sum (op ^ x) {m..n} = x^m - x^ Suc n"
- (is "?lhs = ?rhs")
-proof -
- let ?S = "{0..(n - m)}"
- from mn have mn': "n - m \<ge> 0"
- by arith
- let ?f = "op + m"
- have i: "inj_on ?f ?S"
- unfolding inj_on_def by auto
- have f: "?f ` ?S = {m..n}"
- using mn
- apply (auto simp add: image_iff Bex_def)
- apply presburger
- done
- have th: "op ^ x \<circ> op + m = (\<lambda>i. x^m * x^i)"
- by (rule ext) (simp add: power_add power_mult)
- from sum.reindex[OF i, of "op ^ x", unfolded f th sum_distrib_left[symmetric]]
- have "?lhs = x^m * ((1 - x) * sum (op ^ x) {0..n - m})"
- by simp
- then show ?thesis
- unfolding sum_gp_basic
- using mn
- by (simp add: field_simps power_add[symmetric])
-qed
-
-lemma sum_gp:
- "sum (op ^ (x::'a::{field})) {m .. n} =
- (if n < m then 0
- else if x = 1 then of_nat ((n + 1) - m)
- else (x^ m - x^ (Suc n)) / (1 - x))"
-proof -
- {
- assume nm: "n < m"
- then have ?thesis by simp
- }
- moreover
- {
- assume "\<not> n < m"
- then have nm: "m \<le> n"
- by arith
- {
- assume x: "x = 1"
- then have ?thesis
- by simp
- }
- moreover
- {
- assume x: "x \<noteq> 1"
- then have nz: "1 - x \<noteq> 0"
- by simp
- from sum_gp_multiplied[OF nm, of x] nz have ?thesis
- by (simp add: field_simps)
- }
- ultimately have ?thesis by blast
- }
- ultimately show ?thesis by blast
-qed
-
-lemma sum_gp_offset:
- "sum (op ^ (x::'a::{field})) {m .. m+n} =
- (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
- unfolding sum_gp[of x m "m + n"] power_Suc
- by (simp add: field_simps power_add)
-
-
subsection \<open>Monotone convergence (bounded interval first)\<close>
lemma monotone_convergence_interval:
--- a/src/HOL/Analysis/Poly_Roots.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Poly_Roots.thy Tue Apr 25 16:39:54 2017 +0100
@@ -8,73 +8,6 @@
imports Complex_Main
begin
-subsection\<open>Geometric progressions\<close>
-
-lemma sum_gp_basic:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
- by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
-
-lemma sum_gp0:
- fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
- using sum_gp_basic[of x n]
- by (simp add: mult.commute divide_simps)
-
-lemma sum_power_add:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
- by (simp add: sum_distrib_left power_add)
-
-lemma sum_power_shift:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- assumes "m \<le> n"
- shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
-proof -
- have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
- by (simp add: sum_distrib_left power_add [symmetric])
- also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
- using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
- finally show ?thesis .
-qed
-
-lemma sum_gp_multiplied:
- fixes x :: "'a::{comm_ring,monoid_mult}"
- assumes "m \<le> n"
- shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
-proof -
- have "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
- by (metis mult.assoc mult.commute assms sum_power_shift)
- also have "... =x^m * (1 - x^Suc(n-m))"
- by (metis mult.assoc sum_gp_basic)
- also have "... = x^m - x^Suc n"
- using assms
- by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
- finally show ?thesis .
-qed
-
-lemma sum_gp:
- fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i=m..n. x^i) =
- (if n < m then 0
- else if x = 1 then of_nat((n + 1) - m)
- else (x^m - x^Suc n) / (1 - x))"
-using sum_gp_multiplied [of m n x]
-apply auto
-by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
-
-lemma sum_gp_offset:
- fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i=m..m+n. x^i) =
- (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
- using sum_gp [of x m "m+n"]
- by (auto simp: power_add algebra_simps)
-
-lemma sum_gp_strict:
- fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
- by (induct n) (auto simp: algebra_simps divide_simps)
-
subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
lemma sub_polyfun:
--- a/src/HOL/Analysis/Summation_Tests.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy Tue Apr 25 16:39:54 2017 +0100
@@ -246,9 +246,9 @@
proof (cases "Re s \<le> 0")
let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
case False
- with eventually_gt_at_top[of "0::nat"]
- have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
- by (auto intro!: ge_one_powr_ge_zero elim!: eventually_mono)
+ have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
+ apply (rule eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
+ using False ge_one_powr_ge_zero by auto
from summable_comparison_test_ev[OF this] False show ?thesis by (auto simp: summable_const_iff)
next
let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
@@ -387,11 +387,11 @@
by (auto simp: eventually_at_top_linorder)
hence A: "p n * f n < p (Suc n) * f (Suc n)" if "n \<ge> N" for n using that N[of n] N[of "Suc n"]
by (simp add: field_simps)
- have "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
- by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
- from eventually_ge_at_top[of N] N this
- have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
- by (auto elim!: eventually_mono simp: field_simps abs_of_pos)
+ have B: "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
+ by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
+ have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
+ apply (rule eventually_mono [OF eventually_ge_at_top[of N]])
+ using B N by (auto simp: field_simps abs_of_pos)
from this and \<open>summable f\<close> have "summable (\<lambda>n. p N * f N * inverse (p n))"
by (rule summable_comparison_test_ev)
from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl]
@@ -779,9 +779,8 @@
proof -
have "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
limsup (\<lambda>n. ereal (norm c) * ereal (root n (norm (f n))))"
- using eventually_gt_at_top[of "0::nat"]
- by (intro Limsup_eq)
- (auto elim!: eventually_mono simp: norm_mult norm_power real_root_mult real_root_power)
+ by (intro Limsup_eq eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
+ (auto simp: norm_mult norm_power real_root_mult real_root_power)
also have "\<dots> = ereal (norm c) * limsup (\<lambda>n. ereal (root n (norm (f n))))"
using assms by (subst Limsup_ereal_mult_left[symmetric]) simp_all
finally have A: "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Tue Apr 25 16:39:54 2017 +0100
@@ -398,12 +398,17 @@
using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
apply (force simp add: field_simps)+
done
- have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e"
- apply (subst Transcendental.ln_less_cancel_iff [symmetric])
- prefer 3 apply (subst ln_realpow)
- using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
- apply (force simp add: field_simps ln_div)+
- done
+ have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e
+ proof -
+ have "0 < ln (real k) + ln \<delta>"
+ using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero by fastforce
+ then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e"
+ using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps)
+ then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
+ by (metis exp_less_mono exp_ln that)
+ then show ?thesis
+ by (simp add: \<delta>01(1) \<open>0 < k\<close>)
+ qed
{ fix t and e::real
assume "e>0"
have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e"
--- a/src/HOL/Complex.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Complex.thy Tue Apr 25 16:39:54 2017 +0100
@@ -138,7 +138,7 @@
end
-subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>
+subsection \<open>Numerals, Arithmetic, and Embedding from \<real>\<close>
abbreviation complex_of_real :: "real \<Rightarrow> complex"
where "complex_of_real \<equiv> of_real"
@@ -649,10 +649,10 @@
lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
by (simp add: Im_divide power2_eq_square)
-lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
+lemma Re_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Re (z / r) = Re z / Re r"
by (metis Re_divide_of_real of_real_Re)
-lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
+lemma Im_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Im (z / r) = Im z / Re r"
by (metis Im_divide_of_real of_real_Re)
lemma Re_sum[simp]: "Re (sum f s) = (\<Sum>x\<in>s. Re (f x))"
@@ -691,6 +691,12 @@
lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm z = \<bar>Re z\<bar>"
by (simp add: complex_is_Real_iff norm_complex_def)
+lemma Re_Reals_divide: "r \<in> \<real> \<Longrightarrow> Re (r / z) = Re r * Re z / (norm z)\<^sup>2"
+ by (simp add: Re_divide complex_is_Real_iff cmod_power2)
+
+lemma Im_Reals_divide: "r \<in> \<real> \<Longrightarrow> Im (r / z) = -Re r * Im z / (norm z)\<^sup>2"
+ by (simp add: Im_divide complex_is_Real_iff cmod_power2)
+
lemma series_comparison_complex:
fixes f:: "nat \<Rightarrow> 'a::banach"
assumes sg: "summable g"
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Apr 25 16:39:54 2017 +0100
@@ -913,7 +913,7 @@
then have "exp (real k * ln y + ln x) > exp 0"
by (simp add: ac_simps)
then have "y ^ k * x > 1"
- unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
+ unfolding exp_zero exp_add exp_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
by simp
then have "x > (1 / y)^k" using yp
by (simp add: field_simps)
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Apr 25 16:39:54 2017 +0100
@@ -1987,7 +1987,7 @@
have "exp x = exp (?num * (x / ?num))"
using \<open>real ?num \<noteq> 0\<close> by auto
also have "\<dots> = exp (x / ?num) ^ ?num"
- unfolding exp_real_of_nat_mult ..
+ unfolding exp_of_nat_mult ..
also have "\<dots> \<le> exp (float_divr prec x (- floor_fl x)) ^ ?num"
unfolding num_eq fl_eq
by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
@@ -2023,7 +2023,7 @@
unfolding num_eq fl_eq
using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
also have "\<dots> = exp (?num * (x / ?num))"
- unfolding exp_real_of_nat_mult ..
+ unfolding exp_of_nat_mult ..
also have "\<dots> = exp x"
using \<open>real ?num \<noteq> 0\<close> by auto
finally show ?thesis
@@ -2050,7 +2050,7 @@
hence "real_of_float (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
also have "\<dots> = exp x"
- unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric]
+ unfolding num_eq fl_eq exp_of_nat_mult[symmetric]
using \<open>real_of_float (floor_fl x) \<noteq> 0\<close> by auto
finally show ?thesis
unfolding lb_exp.simps if_not_P[OF \<open>\<not> 0 < x\<close>] if_P[OF \<open>x < - 1\<close>]
--- a/src/HOL/Filter.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Filter.thy Tue Apr 25 16:39:54 2017 +0100
@@ -624,7 +624,7 @@
shows "eventually P at_top"
using assms by (auto simp: eventually_at_top_linorder)
-lemma eventually_ge_at_top:
+lemma eventually_ge_at_top [simp]:
"eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
unfolding eventually_at_top_linorder by auto
@@ -638,10 +638,10 @@
finally show ?thesis .
qed
-lemma eventually_at_top_not_equal: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
+lemma eventually_at_top_not_equal [simp]: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
unfolding eventually_at_top_dense by auto
-lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
+lemma eventually_gt_at_top [simp]: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
unfolding eventually_at_top_dense by auto
lemma eventually_all_ge_at_top:
@@ -664,7 +664,7 @@
unfolding at_bot_def
by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
-lemma eventually_le_at_bot:
+lemma eventually_le_at_bot [simp]:
"eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
unfolding eventually_at_bot_linorder by auto
@@ -678,10 +678,10 @@
finally show ?thesis .
qed
-lemma eventually_at_bot_not_equal: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
+lemma eventually_at_bot_not_equal [simp]: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
unfolding eventually_at_bot_dense by auto
-lemma eventually_gt_at_bot:
+lemma eventually_gt_at_bot [simp]:
"eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
unfolding eventually_at_bot_dense by auto
--- a/src/HOL/Limits.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Limits.thy Tue Apr 25 16:39:54 2017 +0100
@@ -1799,10 +1799,12 @@
using assms by simp
text \<open>An unbounded sequence's inverse tends to 0.\<close>
-lemma LIMSEQ_inverse_zero: "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
+lemma LIMSEQ_inverse_zero:
+ assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n"
+ shows "(\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
apply (rule filterlim_compose[OF tendsto_inverse_0])
apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
- apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
+ apply (metis assms abs_le_D1 linorder_le_cases linorder_not_le)
done
text \<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\<close>
@@ -2189,16 +2191,16 @@
using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F"
- for f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ for f :: "'a \<Rightarrow> 'b::real_normed_vector"
unfolding tendsto_iff dist_norm by simp
lemma LIM_zero_cancel:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F"
unfolding tendsto_iff dist_norm by simp
lemma LIM_zero_iff: "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F = (f \<longlongrightarrow> l) F"
- for f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ for f :: "'a \<Rightarrow> 'b::real_normed_vector"
unfolding tendsto_iff dist_norm by simp
lemma LIM_imp_LIM:
--- a/src/HOL/Probability/Sinc_Integral.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy Tue Apr 25 16:39:54 2017 +0100
@@ -219,12 +219,11 @@
have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real
by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
(auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
- then have **: "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
+ then have "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right
intro!: mult_mono)
-
- show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
- using eventually_ge_at_top[of "1::real"] ** by (auto elim: eventually_mono)
+ then show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
+ by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"])
show "AE x in lborel. 0 < x \<longrightarrow> (?F x \<longlongrightarrow> 0) at_top"
proof (intro always_eventually impI allI)
fix x :: real assume "0 < x"
--- a/src/HOL/Real_Vector_Spaces.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Apr 25 16:39:54 2017 +0100
@@ -364,6 +364,7 @@
by (auto intro: injI)
lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
+lemmas of_real_eq_1_iff [simp] = of_real_eq_iff [of _ 1, simplified]
lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
by (rule ext) (simp add: of_real_def)
--- a/src/HOL/Set_Interval.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Set_Interval.thy Tue Apr 25 16:39:54 2017 +0100
@@ -1892,7 +1892,7 @@
by (induction m) (simp_all add: algebra_simps)
-subsubsection \<open>The formula for geometric sums\<close>
+subsection \<open>The formula for geometric sums\<close>
lemma geometric_sum:
assumes "x \<noteq> 1"
@@ -1947,6 +1947,71 @@
shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
by (metis one_diff_power_eq' [of n x] nat_diff_sum_reindex)
+lemma sum_gp_basic:
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
+ by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
+
+lemma sum_power_shift:
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ assumes "m \<le> n"
+ shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
+proof -
+ have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
+ by (simp add: sum_distrib_left power_add [symmetric])
+ also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
+ using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
+ finally show ?thesis .
+qed
+
+lemma sum_gp_multiplied:
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ assumes "m \<le> n"
+ shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
+proof -
+ have "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
+ by (metis mult.assoc mult.commute assms sum_power_shift)
+ also have "... =x^m * (1 - x^Suc(n-m))"
+ by (metis mult.assoc sum_gp_basic)
+ also have "... = x^m - x^Suc n"
+ using assms
+ by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
+ finally show ?thesis .
+qed
+
+lemma sum_gp:
+ fixes x :: "'a::{comm_ring,division_ring}"
+ shows "(\<Sum>i=m..n. x^i) =
+ (if n < m then 0
+ else if x = 1 then of_nat((n + 1) - m)
+ else (x^m - x^Suc n) / (1 - x))"
+using sum_gp_multiplied [of m n x] apply auto
+by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
+
+subsection\<open>Geometric progressions\<close>
+
+lemma sum_gp0:
+ fixes x :: "'a::{comm_ring,division_ring}"
+ shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
+ using sum_gp_basic[of x n]
+ by (simp add: mult.commute divide_simps)
+
+lemma sum_power_add:
+ fixes x :: "'a::{comm_ring,monoid_mult}"
+ shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
+ by (simp add: sum_distrib_left power_add)
+
+lemma sum_gp_offset:
+ fixes x :: "'a::{comm_ring,division_ring}"
+ shows "(\<Sum>i=m..m+n. x^i) =
+ (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
+ using sum_gp [of x m "m+n"]
+ by (auto simp: power_add algebra_simps)
+
+lemma sum_gp_strict:
+ fixes x :: "'a::{comm_ring,division_ring}"
+ shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
+ by (induct n) (auto simp: algebra_simps divide_simps)
subsubsection \<open>The formula for arithmetic sums\<close>
--- a/src/HOL/Transcendental.thy Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Transcendental.thy Tue Apr 25 16:39:54 2017 +0100
@@ -1506,7 +1506,7 @@
finally show False by simp
qed
-lemma exp_minus_inverse: "exp x * exp (- x) = 1"
+lemma exp_minus_inverse [simp]: "exp x * exp (- x) = 1"
by (simp add: exp_add_commuting[symmetric])
lemma exp_minus: "exp (- x) = inverse (exp x)"
@@ -1517,17 +1517,18 @@
for x :: "'a::{real_normed_field,banach}"
using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
-lemma exp_of_nat_mult: "exp (of_nat n * x) = exp x ^ n"
+lemma exp_of_nat_mult [simp]: "exp (of_nat n * x) = exp x ^ n"
for x :: "'a::{real_normed_field,banach}"
by (induct n) (auto simp add: distrib_left exp_add mult.commute)
-corollary exp_real_of_nat_mult: "exp (real n * x) = exp x ^ n"
- by (simp add: exp_of_nat_mult)
+corollary exp_of_nat2_mult [simp]: "exp (x * of_nat n) = exp x ^ n"
+ for x :: "'a::{real_normed_field,banach}"
+ by (metis exp_of_nat_mult mult_of_nat_commute)
lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = prod (\<lambda>x. exp (f x)) I"
by (induct I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
-lemma exp_divide_power_eq:
+lemma exp_divide_power_eq [simp]:
fixes x :: "'a::{real_normed_field,banach}"
assumes "n > 0"
shows "exp (x / of_nat n) ^ n = exp x"
@@ -1742,7 +1743,7 @@
for x :: real
by (erule subst) (rule ln_exp)
-lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
+lemma ln_mult [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
for x :: real
by (rule ln_unique) (simp add: exp_add)
@@ -1750,7 +1751,7 @@
for f :: "'a \<Rightarrow> real"
by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
-lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
+lemma ln_inverse [simp]: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
for x :: real
by (rule ln_unique) (simp add: exp_minus)
@@ -1758,8 +1759,8 @@
for x :: real
by (rule ln_unique) (simp add: exp_diff)
-lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
- by (rule ln_unique) (simp add: exp_real_of_nat_mult)
+lemma ln_realpow [simp]: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
+ by (rule ln_unique) simp
lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
for x :: real
@@ -1781,6 +1782,9 @@
for x :: real
by (rule order_less_le_trans [where y = "ln (1 + x)"]) simp_all
+lemma ln_ge_iff: "\<And>x::real. 0 < x \<Longrightarrow> y \<le> ln x \<longleftrightarrow> exp y \<le> x"
+ using exp_le_cancel_iff exp_total by force
+
lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
for x :: real
using ln_le_cancel_iff [of 1 x] by simp
@@ -2298,7 +2302,7 @@
also from assms False have "ln (1 + x / real n) \<le> x / real n"
by (intro ln_add_one_self_le_self2) (simp_all add: field_simps)
with assms have "exp (of_nat n * ln (1 + x / of_nat n)) \<le> exp x"
- by (simp add: field_simps)
+ by (simp add: field_simps del: exp_of_nat_mult)
finally show ?thesis .
next
case True
@@ -2701,7 +2705,7 @@
lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
by (induct n) (simp_all add: ac_simps powr_add)
-lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
+lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
by (metis of_nat_numeral powr_realpow)
lemma numeral_powr_numeral[simp]:
@@ -2841,14 +2845,26 @@
for x :: real
by (simp add: powr_def)
-lemma powr_mono2: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> x powr a \<le> y powr a"
+lemma powr_mono2: "x powr a \<le> y powr a" if "0 \<le> a" "0 \<le> x" "x \<le> y"
for x :: real
- apply (case_tac "a = 0")
- apply simp
- apply (case_tac "x = y")
- apply simp
- apply (metis dual_order.strict_iff_order powr_less_mono2)
- done
+proof (cases "a = 0")
+ case True
+ with that show ?thesis by simp
+next
+ case False show ?thesis
+ proof (cases "x = y")
+ case True
+ then show ?thesis by simp
+ next
+ case False
+ then show ?thesis
+ by (metis dual_order.strict_iff_order powr_less_mono2 that \<open>a \<noteq> 0\<close>)
+ qed
+qed
+
+lemma powr_le1: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr a \<le> 1"
+ for x :: real
+ using powr_mono2 by fastforce
lemma powr_mono2':
fixes a x y :: real
@@ -2861,6 +2877,12 @@
by (auto simp add: powr_minus field_simps)
qed
+lemma powr_mono_both:
+ fixes x :: real
+ assumes "0 \<le> a" "a \<le> b" "1 \<le> x" "x \<le> y"
+ shows "x powr a \<le> y powr b"
+ by (meson assms order.trans powr_mono powr_mono2 zero_le_one)
+
lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
for x :: real
unfolding powr_def exp_inj_iff by simp