# HG changeset patch # User paulson # Date 1493134794 -3600 # Node ID e4997c181ccef3dc8b96ddf7ee60933d0189d3ea # Parent 32d4117ad6e8070a813a393bb40da97732af4f60 New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- 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 \ 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 "\valid_path \; z \ path_image \; w \ z; \a::real. 0 < a \ z + a*(w - z) \ path_image \\ - \ \Re(winding_number \ z)\ < 1" + \ Re(winding_number \ z) < 1" by (auto simp: not_less dest: winding_number_big_meets) text\One way of proving that WN=1 for a loop.\ @@ -6532,6 +6531,21 @@ apply (force simp add: summable_Re o_def nonneg_Reals_cmod_eq_Re image_subset_iff) done +text\Sometimes convenient to compare with a complex series of positive reals. (?)\ +lemma series_differentiable_comparison_complex: + fixes S :: "complex set" + assumes S: "open S" + and hfd: "\n x. x \ S \ f n field_differentiable (at x)" + and to_g: "\x. x \ S \ \d h. 0 < d \ summable h \ range h \ \\<^sub>\\<^sub>0 \ (\\<^sub>F n in sequentially. \y\ball x d \ S. cmod(f n y) \ cmod (h n))" + obtains g where "\x \ S. ((\n. f n x) sums g x) \ g field_differentiable (at x)" +proof - + have hfd': "\n x. x \ S \ (f n has_field_derivative deriv (f n) x) (at x)" + using hfd field_differentiable_derivI by blast + have "\g g'. \x \ S. ((\n. f n x) sums g x) \ ((\n. deriv (f n) x) sums g' x) \ (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\In particular, a power series is analytic inside circle of convergence.\ @@ -7441,5 +7455,4 @@ homotopic_paths_imp_homotopic_loops) using valid_path_imp_path by blast - end diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Complex_Transcendental.thy --- 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\An odd contrast with the much more easily proved @{thm exp_le}\ 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 \ 0 \ ((\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)+ diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Conformal_Mappings.thy --- 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] \y0 \ T\ \y1 \ T\ - 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 diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Gamma_Function.thy --- 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 \ Gamma x" proof (rule tendsto_upperbound) from G_lower[of x] show "eventually (\n. Gamma_series x n \ 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 \ Gamma x" @@ -1891,7 +1891,7 @@ thus "(\n. Gamma_series x n * (1 + x / real n)) \ Gamma x" by simp next from G_upper[of x] show "eventually (\n. Gamma_series x n * (1 + x / real n) \ 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' = "\n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))" from z have z': "z \ 0" by auto - have "eventually (\n. ?r' n = ?r n) sequentially" using eventually_gt_at_top[of "0::nat"] + have "eventually (\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' \ exp (z * of_real (ln 1))" by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all ultimately show "?r \ 1" by (force dest!: Lim_transform_eventually) diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- 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: "\x x'. \x \ cbox a b; x' \ cbox a b; dist x' x < d\ \ 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: "(\x. ball x d) fine p" + using fine_division_exists[OF gauge_ball[OF \0 < d\], of a b] . have *: "\i\snd ` p. \g. (\x\i. norm (f x - g x) \ e) \ g integrable_on i" proof (safe, unfold snd_conv) fix x l assume as: "(x, l) \ 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 \ cbox a b" + using as ptag by auto show "\g. (\x\l. norm (f x - g x) \ e) \ g integrable_on l" apply (rule_tac x="\y. f x" in exI) proof safe show "(\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 \ 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 \ ball x d" + using as finep by fastforce then show "norm (f y - f x) \ 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 \ 0" by auto - from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g . - then show "\g. (\x\cbox a b. norm (f x - g x) \ e) \ g integrable_on cbox a b" - by auto + from approximable_on_division[OF this division_of_tagged_division[OF ptag] *] + show "\g. (\x\cbox a b. norm (f x - g x) \ e) \ g integrable_on cbox a b" + by metis qed lemma integrable_continuous_interval: @@ -6278,89 +6280,6 @@ qed -subsection \Geometric progression\ - -text \FIXME: Should one or more of these theorems be moved to - \<^file>\~~/src/HOL/Set_Interval.thy\, alongside \geometric_sum\?\ - -lemma sum_gp_basic: - fixes x :: "'a::ring_1" - shows "(1 - x) * sum (\i. x^i) {0 .. n} = (1 - x^(Suc n))" -proof - - define y where "y = 1 - x" - have "y * (\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 \ 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 \ 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 \ op + m = (\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 "\ n < m" - then have nm: "m \ n" - by arith - { - assume x: "x = 1" - then have ?thesis - by simp - } - moreover - { - assume x: "x \ 1" - then have nz: "1 - x \ 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 \Monotone convergence (bounded interval first)\ lemma monotone_convergence_interval: diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Poly_Roots.thy --- 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\Geometric progressions\ - -lemma sum_gp_basic: - fixes x :: "'a::{comm_ring,monoid_mult}" - shows "(1 - x) * (\i\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 "(\i\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 "(\i\I. x^(m+i)) = x^m * (\i\I. x^i)" - by (simp add: sum_distrib_left power_add) - -lemma sum_power_shift: - fixes x :: "'a::{comm_ring,monoid_mult}" - assumes "m \ n" - shows "(\i=m..n. x^i) = x^m * (\i\n-m. x^i)" -proof - - have "(\i=m..n. x^i) = x^m * (\i=m..n. x^(i-m))" - by (simp add: sum_distrib_left power_add [symmetric]) - also have "(\i=m..n. x^(i-m)) = (\i\n-m. x^i)" - using \m \ n\ by (intro sum.reindex_bij_witness[where j="\i. i - m" and i="\i. i + m"]) auto - finally show ?thesis . -qed - -lemma sum_gp_multiplied: - fixes x :: "'a::{comm_ring,monoid_mult}" - assumes "m \ n" - shows "(1 - x) * (\i=m..n. x^i) = x^m - x^Suc n" -proof - - have "(1 - x) * (\i=m..n. x^i) = x^m * (1 - x) * (\i\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 "(\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 "(\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 "(\iBasics about polynomial functions: extremal behaviour and root counts.\ lemma sub_polyfun: diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Summation_Tests.thy --- 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 \ 0") let ?l = "\n. complex_of_real (ln (of_nat n))" case False - with eventually_gt_at_top[of "0::nat"] - have "eventually (\n. norm (1 :: real) \ norm (exp (?l n * s))) sequentially" - by (auto intro!: ge_one_powr_ge_zero elim!: eventually_mono) + have "eventually (\n. norm (1 :: real) \ 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 = "\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 \ N" for n using that N[of n] N[of "Suc n"] by (simp add: field_simps) - have "p n * f n \ p N * f N" if "n \ 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 (\n. norm (p N * f N * inverse (p n)) \ f n) sequentially" - by (auto elim!: eventually_mono simp: field_simps abs_of_pos) + have B: "p n * f n \ p N * f N" if "n \ N" for n using that and A + by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans) + have "eventually (\n. norm (p N * f N * inverse (p n)) \ 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 \summable f\ have "summable (\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 (\n. ereal (root n (norm (c ^ n * f n)))) = limsup (\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 "\ = ereal (norm c) * limsup (\n. ereal (root n (norm (f n))))" using assms by (subst Limsup_ereal_mult_left[symmetric]) simp_all finally have A: "limsup (\n. ereal (root n (norm (c ^ n * f n)))) = diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Weierstrass_Theorems.thy --- 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 \k>0\ \\>0\ NN k\ apply (force simp add: field_simps)+ done - have NN0: "\e. e>0 \ (1/(k*\))^NN e < e" - apply (subst Transcendental.ln_less_cancel_iff [symmetric]) - prefer 3 apply (subst ln_realpow) - using \k>0\ \\>0\ NN k\ - apply (force simp add: field_simps ln_div)+ - done + have NN0: "(1/(k*\)) ^ (NN e) < e" if "e>0" for e + proof - + have "0 < ln (real k) + ln \" + using \01(1) \0 < k\ k\(1) ln_gt_zero by fastforce + then have "real (NN e) * ln (1 / (real k * \)) < ln e" + using k\(1) NN(2) [of e] that by (simp add: ln_div divide_simps) + then have "exp (real (NN e) * ln (1 / (real k * \))) < e" + by (metis exp_less_mono exp_ln that) + then show ?thesis + by (simp add: \01(1) \0 < k\) + qed { fix t and e::real assume "e>0" have "t \ S \ V \ 1 - q (NN e) t < e" "t \ S - U \ q (NN e) t < e" diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Complex.thy --- 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 \Numerals, Arithmetic, and Embedding from Reals\ +subsection \Numerals, Arithmetic, and Embedding from \\ abbreviation complex_of_real :: "real \ complex" where "complex_of_real \ 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 \ Reals \ Re (z / r) = Re z / Re r" +lemma Re_divide_Reals [simp]: "r \ \ \ Re (z / r) = Re z / Re r" by (metis Re_divide_of_real of_real_Re) -lemma Im_divide_Reals: "r \ Reals \ Im (z / r) = Im z / Re r" +lemma Im_divide_Reals [simp]: "r \ \ \ Im (z / r) = Im z / Re r" by (metis Im_divide_of_real of_real_Re) lemma Re_sum[simp]: "Re (sum f s) = (\x\s. Re (f x))" @@ -691,6 +691,12 @@ lemma in_Reals_norm: "z \ \ \ norm z = \Re z\" by (simp add: complex_is_Real_iff norm_complex_def) +lemma Re_Reals_divide: "r \ \ \ 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 \ \ \ 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 \ 'a::banach" assumes sg: "summable g" diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Computational_Algebra/Formal_Power_Series.thy --- 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) diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Decision_Procs/Approximation.thy --- 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 \real ?num \ 0\ by auto also have "\ = exp (x / ?num) ^ ?num" - unfolding exp_real_of_nat_mult .. + unfolding exp_of_nat_mult .. also have "\ \ 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 "\ = exp (?num * (x / ?num))" - unfolding exp_real_of_nat_mult .. + unfolding exp_of_nat_mult .. also have "\ = exp x" using \real ?num \ 0\ by auto finally show ?thesis @@ -2050,7 +2050,7 @@ hence "real_of_float (Float 1 (- 2)) ^ ?num \ exp (x / (- floor_fl x)) ^ ?num" by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral) also have "\ = exp x" - unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] + unfolding num_eq fl_eq exp_of_nat_mult[symmetric] using \real_of_float (floor_fl x) \ 0\ by auto finally show ?thesis unfolding lb_exp.simps if_not_P[OF \\ 0 < x\] if_P[OF \x < - 1\] diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Filter.thy --- 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 (\x. (c::_::linorder) \ 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 (\x::'a::{no_top, linorder}. x \ c) at_top" +lemma eventually_at_top_not_equal [simp]: "eventually (\x::'a::{no_top, linorder}. x \ c) at_top" unfolding eventually_at_top_dense by auto -lemma eventually_gt_at_top: "eventually (\x. (c::_::{no_top, linorder}) < x) at_top" +lemma eventually_gt_at_top [simp]: "eventually (\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 (\x. x \ (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 (\x::'a::{no_bot, linorder}. x \ c) at_bot" +lemma eventually_at_bot_not_equal [simp]: "eventually (\x::'a::{no_bot, linorder}. x \ c) at_bot" unfolding eventually_at_bot_dense by auto -lemma eventually_gt_at_bot: +lemma eventually_gt_at_bot [simp]: "eventually (\x. x < (c::_::unbounded_dense_linorder)) at_bot" unfolding eventually_at_bot_dense by auto diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Limits.thy --- 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 \An unbounded sequence's inverse tends to 0.\ -lemma LIMSEQ_inverse_zero: "\r::real. \N. \n\N. r < X n \ (\n. inverse (X n)) \ 0" +lemma LIMSEQ_inverse_zero: + assumes "\r::real. \N. \n\N. r < X n" + shows "(\n. inverse (X n)) \ 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 \The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\ @@ -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 \ l) F \ ((\x. f x - l) \ 0) F" - for f :: "'a::topological_space \ 'b::real_normed_vector" + for f :: "'a \ 'b::real_normed_vector" unfolding tendsto_iff dist_norm by simp lemma LIM_zero_cancel: - fixes f :: "'a::topological_space \ 'b::real_normed_vector" + fixes f :: "'a \ 'b::real_normed_vector" shows "((\x. f x - l) \ 0) F \ (f \ l) F" unfolding tendsto_iff dist_norm by simp lemma LIM_zero_iff: "((\x. f x - l) \ 0) F = (f \ l) F" - for f :: "'a::metric_space \ 'b::real_normed_vector" + for f :: "'a \ 'b::real_normed_vector" unfolding tendsto_iff dist_norm by simp lemma LIM_imp_LIM: diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Probability/Sinc_Integral.thy --- 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 \ \x * sin t + cos t\ / (1 + x\<^sup>2) \ (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 \ t \ 0 < x \ \?F x t\ \ exp (- x) * (x + 1)" for x t :: real + then have "1 \ t \ 0 < x \ \?F x t\ \ 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 "\\<^sub>F i in at_top. AE x in lborel. 0 < x \ \?F x i\ \ exp (- x) * (x + 1)" - using eventually_ge_at_top[of "1::real"] ** by (auto elim: eventually_mono) + then show "\\<^sub>F i in at_top. AE x in lborel. 0 < x \ \?F x i\ \ exp (- x) * (x + 1)" + by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"]) show "AE x in lborel. 0 < x \ (?F x \ 0) at_top" proof (intro always_eventually impI allI) fix x :: real assume "0 < x" diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Real_Vector_Spaces.thy --- 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 \ real)" by (rule ext) (simp add: of_real_def) diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Set_Interval.thy --- 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 \The formula for geometric sums\ +subsection \The formula for geometric sums\ lemma geometric_sum: assumes "x \ 1" @@ -1947,6 +1947,71 @@ shows "n \ 0 \ 1 - x^n = (1 - x) * (\ii\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 \ n" + shows "(\i=m..n. x^i) = x^m * (\i\n-m. x^i)" +proof - + have "(\i=m..n. x^i) = x^m * (\i=m..n. x^(i-m))" + by (simp add: sum_distrib_left power_add [symmetric]) + also have "(\i=m..n. x^(i-m)) = (\i\n-m. x^i)" + using \m \ n\ by (intro sum.reindex_bij_witness[where j="\i. i - m" and i="\i. i + m"]) auto + finally show ?thesis . +qed + +lemma sum_gp_multiplied: + fixes x :: "'a::{comm_ring,monoid_mult}" + assumes "m \ n" + shows "(1 - x) * (\i=m..n. x^i) = x^m - x^Suc n" +proof - + have "(1 - x) * (\i=m..n. x^i) = x^m * (1 - x) * (\i\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 "(\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\Geometric progressions\ + +lemma sum_gp0: + fixes x :: "'a::{comm_ring,division_ring}" + shows "(\i\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 "(\i\I. x^(m+i)) = x^m * (\i\I. x^i)" + by (simp add: sum_distrib_left power_add) + +lemma sum_gp_offset: + fixes x :: "'a::{comm_ring,division_ring}" + shows "(\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 "(\iThe formula for arithmetic sums\ diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Transcendental.thy --- 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 \ exp (sum f I) = prod (\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 \ 0 < y \ ln (x * y) = ln x + ln y" +lemma ln_mult [simp]: "0 < x \ 0 < y \ 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 \ real" by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos) -lemma ln_inverse: "0 < x \ ln (inverse x) = - ln x" +lemma ln_inverse [simp]: "0 < x \ 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 \ ln (x^n) = real n * ln x" - by (rule ln_unique) (simp add: exp_real_of_nat_mult) +lemma ln_realpow [simp]: "0 < x \ ln (x^n) = real n * ln x" + by (rule ln_unique) simp lemma ln_less_cancel_iff [simp]: "0 < x \ 0 < y \ ln x < ln y \ 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: "\x::real. 0 < x \ y \ ln x \ exp y \ x" + using exp_le_cancel_iff exp_total by force + lemma ln_ge_zero [simp]: "1 \ x \ 0 \ 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) \ 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)) \ 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 \ x powr (real n) = x^n" by (induct n) (simp_all add: ac_simps powr_add) -lemma powr_numeral: "0 < x \ x powr (numeral n :: real) = x ^ (numeral n)" +lemma powr_numeral [simp]: "0 < x \ 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 \ a \ 0 \ x \ x \ y \ x powr a \ y powr a" +lemma powr_mono2: "x powr a \ y powr a" if "0 \ a" "0 \ x" "x \ 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 \a \ 0\) + qed +qed + +lemma powr_le1: "0 \ a \ 0 \ x \ x \ 1 \ x powr a \ 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 \ a" "a \ b" "1 \ x" "x \ y" + shows "x powr a \ y powr b" + by (meson assms order.trans powr_mono powr_mono2 zero_le_one) + lemma powr_inj: "0 < a \ a \ 1 \ a powr x = a powr y \ x = y" for x :: real unfolding powr_def exp_inj_iff by simp