--- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Aug 25 15:50:43 2016 +0200
@@ -1396,6 +1396,22 @@
ultimately show ?thesis by (simp add: sums_iff)
qed
+lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
+ by (drule Ln_series) (simp add: power_minus')
+
+lemma ln_series':
+ assumes "abs (x::real) < 1"
+ shows "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
+proof -
+ from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
+ by (intro Ln_series') simp_all
+ also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
+ by (rule ext) simp
+ also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
+ by (subst Ln_of_real [symmetric]) simp_all
+ finally show ?thesis by (subst (asm) sums_of_real_iff)
+qed
+
lemma Ln_approx_linear:
fixes z :: complex
assumes "norm z < 1"
--- a/src/HOL/Analysis/Gamma_Function.thy Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Thu Aug 25 15:50:43 2016 +0200
@@ -709,6 +709,37 @@
using uniformly_convergent_imp_convergent[OF Polygamma_converges[OF assms, of 1], of z]
by (simp add: summable_iff_convergent)
+lemma Digamma_LIMSEQ:
+ fixes z :: "'a :: {banach,real_normed_field}"
+ assumes z: "z \<noteq> 0"
+ shows "(\<lambda>m. of_real (ln (real m)) - (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
+proof -
+ have "(\<lambda>n. of_real (ln (real n / (real (Suc n))))) \<longlonglongrightarrow> (of_real (ln 1) :: 'a)"
+ by (intro tendsto_intros LIMSEQ_n_over_Suc_n) simp_all
+ hence "(\<lambda>n. of_real (ln (real n / (real n + 1)))) \<longlonglongrightarrow> (0 :: 'a)" by (simp add: add_ac)
+ hence lim: "(\<lambda>n. of_real (ln (real n)) - of_real (ln (real n + 1))) \<longlonglongrightarrow> (0::'a)"
+ proof (rule Lim_transform_eventually [rotated])
+ show "eventually (\<lambda>n. of_real (ln (real n / (real n + 1))) =
+ of_real (ln (real n)) - (of_real (ln (real n + 1)) :: 'a)) at_top"
+ using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: ln_div)
+ qed
+
+ from summable_Digamma[OF z]
+ have "(\<lambda>n. inverse (of_nat (n+1)) - inverse (z + of_nat n))
+ sums (Digamma z + euler_mascheroni)"
+ by (simp add: Digamma_def summable_sums)
+ from sums_diff[OF this euler_mascheroni_sum]
+ have "(\<lambda>n. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)) - inverse (z + of_nat n))
+ sums Digamma z" by (simp add: add_ac)
+ hence "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1))) -
+ (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
+ by (simp add: sums_def setsum_subtractf)
+ also have "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)))) =
+ (\<lambda>m. of_real (ln (m + 1)) :: 'a)"
+ by (subst setsum_lessThan_telescope) simp_all
+ finally show ?thesis by (rule Lim_transform) (insert lim, simp)
+qed
+
lemma has_field_derivative_ln_Gamma_complex [derivative_intros]:
fixes z :: complex
assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
@@ -1641,6 +1672,12 @@
using Polygamma_real_strict_mono[OF assms(1) _ assms(3), of y] assms(2)
by (cases "x = y") simp_all
+lemma Digamma_real_strict_mono: "(0::real) < x \<Longrightarrow> x < y \<Longrightarrow> Digamma x < Digamma y"
+ by (rule Polygamma_real_strict_mono) simp_all
+
+lemma Digamma_real_mono: "(0::real) < x \<Longrightarrow> x \<le> y \<Longrightarrow> Digamma x \<le> Digamma y"
+ by (rule Polygamma_real_mono) simp_all
+
lemma Digamma_real_ge_three_halves_pos:
assumes "x \<ge> 3/2"
shows "Digamma (x :: real) > 0"
@@ -2871,6 +2908,18 @@
using tendsto_divide[OF sin_product_formula_real[of x] tendsto_const[of "pi * x"]] assms
by simp
+theorem wallis: "(\<lambda>n. \<Prod>k=1..n. (4*real k^2) / (4*real k^2 - 1)) \<longlonglongrightarrow> pi / 2"
+proof -
+ from tendsto_inverse[OF tendsto_mult[OF
+ sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
+ have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
+ by (simp add: setprod_inversef [symmetric])
+ also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
+ (\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
+ by (intro ext setprod.cong refl) (simp add: divide_simps)
+ finally show ?thesis .
+qed
+
subsection \<open>The Solution to the Basel problem\<close>
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Thu Aug 25 15:50:43 2016 +0200
@@ -173,13 +173,23 @@
thus ?thesis by simp
qed
-lemma euler_mascheroni_sum:
+lemma euler_mascheroni_sum_real:
"(\<lambda>n. inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2)) :: real)
sums euler_mascheroni"
using sums_add[OF telescope_sums[OF LIMSEQ_Suc[OF euler_mascheroni_LIMSEQ]]
telescope_sums'[OF LIMSEQ_inverse_real_of_nat]]
by (simp_all add: harm_def algebra_simps)
+lemma euler_mascheroni_sum:
+ "(\<lambda>n. inverse (of_nat (n+1)) + of_real (ln (of_nat (n+1))) - of_real (ln (of_nat (n+2))))
+ sums (euler_mascheroni :: 'a :: {banach, real_normed_field})"
+proof -
+ have "(\<lambda>n. of_real (inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))))
+ sums (of_real euler_mascheroni :: 'a :: {banach, real_normed_field})"
+ by (subst sums_of_real_iff) (rule euler_mascheroni_sum_real)
+ thus ?thesis by simp
+qed
+
lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
proof -
let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
@@ -342,17 +352,18 @@
let ?g = "\<lambda>n. ln (of_nat (n+2)) - ln (of_nat (n+1)) - inverse (of_nat (n+1)) :: real"
define inv where [abs_def]: "inv n = inverse (real_of_nat n)" for n
fix n :: nat
- note summable = sums_summable[OF euler_mascheroni_sum, folded D_def]
+ note summable = sums_summable[OF euler_mascheroni_sum_real, folded D_def]
have sums: "(\<lambda>k. (inv (Suc (k + (n+1))) - inv (Suc (Suc k + (n+1))))/2) sums ((inv (Suc (0 + (n+1))) - 0)/2)"
unfolding inv_def
by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
have sums': "(\<lambda>k. (inv (Suc (k + n)) - inv (Suc (Suc k + n)))/2) sums ((inv (Suc (0 + n)) - 0)/2)"
unfolding inv_def
by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
- from euler_mascheroni_sum have "euler_mascheroni = (\<Sum>k. D k)"
+ from euler_mascheroni_sum_real have "euler_mascheroni = (\<Sum>k. D k)"
by (simp add: sums_iff D_def)
also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)"
- by (subst suminf_split_initial_segment[OF summable, of "Suc n"], subst lessThan_Suc_atMost) simp
+ by (subst suminf_split_initial_segment[OF summable, of "Suc n"],
+ subst lessThan_Suc_atMost) simp
finally have sum: "(\<Sum>k\<le>n. D k) - euler_mascheroni = -(\<Sum>k. D (k + Suc n))" by simp
note sum
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Aug 25 15:50:43 2016 +0200
@@ -12533,4 +12533,101 @@
shows "(\<lambda>x. x powr a) integrable_on {0..c}"
using has_integral_powr_from_0[OF assms] unfolding integrable_on_def by blast
+lemma has_integral_powr_to_inf:
+ fixes a e :: real
+ assumes "e < -1" "a > 0"
+ shows "((\<lambda>x. x powr e) has_integral -(a powr (e + 1)) / (e + 1)) {a..}"
+proof -
+ define f :: "nat \<Rightarrow> real \<Rightarrow> real" where "f = (\<lambda>n x. if x \<in> {a..n} then x powr e else 0)"
+ define F where "F = (\<lambda>x. x powr (e + 1) / (e + 1))"
+
+ have has_integral_f: "(f n has_integral (F n - F a)) {a..}"
+ if n: "n \<ge> a" for n :: nat
+ proof -
+ from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
+ by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
+ simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
+ hence "(f n has_integral (F n - F a)) {a..n}"
+ by (rule has_integral_eq [rotated]) (simp add: f_def)
+ thus "(f n has_integral (F n - F a)) {a..}"
+ by (rule has_integral_on_superset [rotated 2]) (auto simp: f_def)
+ qed
+ have integral_f: "integral {a..} (f n) = (if n \<ge> a then F n - F a else 0)" for n :: nat
+ proof (cases "n \<ge> a")
+ case True
+ with has_integral_f[OF this] show ?thesis by (simp add: integral_unique)
+ next
+ case False
+ have "(f n has_integral 0) {a}" by (rule has_integral_refl)
+ hence "(f n has_integral 0) {a..}"
+ by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
+ with False show ?thesis by (simp add: integral_unique)
+ qed
+
+ have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and>
+ (\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> integral {a..} (\<lambda>x. x powr e)"
+ proof (intro monotone_convergence_increasing allI ballI)
+ fix n :: nat
+ from assms have "(\<lambda>x. x powr e) integrable_on {a..n}"
+ by (auto intro!: integrable_continuous_real continuous_intros)
+ hence "f n integrable_on {a..n}"
+ by (rule integrable_eq [rotated]) (auto simp: f_def)
+ thus "f n integrable_on {a..}"
+ by (rule integrable_on_superset [rotated 2]) (auto simp: f_def)
+ next
+ fix n :: nat and x :: real
+ show "f n x \<le> f (Suc n) x" by (auto simp: f_def)
+ next
+ fix x :: real assume x: "x \<in> {a..}"
+ from filterlim_real_sequentially
+ have "eventually (\<lambda>n. real n \<ge> x) at_top"
+ by (simp add: filterlim_at_top)
+ with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
+ by (auto elim!: eventually_mono simp: f_def)
+ thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
+ next
+ have "norm (integral {a..} (f n)) \<le> -F a" for n :: nat
+ proof (cases "n \<ge> a")
+ case True
+ with assms have "a powr (e + 1) \<ge> n powr (e + 1)"
+ by (intro powr_mono2') simp_all
+ with assms show ?thesis by (auto simp: divide_simps F_def integral_f)
+ qed (insert assms, simp add: integral_f F_def divide_simps)
+ thus "bounded {integral {a..} (f n) |n. True}"
+ unfolding bounded_iff by (intro exI[of _ "-F a"]) auto
+ qed
+
+ from filterlim_real_sequentially
+ have "eventually (\<lambda>n. real n \<ge> a) at_top"
+ by (simp add: filterlim_at_top)
+ hence "eventually (\<lambda>n. F n - F a = integral {a..} (f n)) at_top"
+ by eventually_elim (simp add: integral_f)
+ moreover have "(\<lambda>n. F n - F a) \<longlonglongrightarrow> 0 / (e + 1) - F a" unfolding F_def
+ by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
+ filterlim_ident filterlim_real_sequentially | simp)+)
+ hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
+ ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
+ from conjunct2[OF *] and this
+ have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
+ with conjunct1[OF *] show ?thesis
+ by (simp add: has_integral_integral F_def)
+qed
+
+lemma has_integral_inverse_power_to_inf:
+ fixes a :: real and n :: nat
+ assumes "n > 1" "a > 0"
+ shows "((\<lambda>x. 1 / x ^ n) has_integral 1 / (real (n - 1) * a ^ (n - 1))) {a..}"
+proof -
+ from assms have "real_of_int (-int n) < -1" by simp
+ note has_integral_powr_to_inf[OF this \<open>a > 0\<close>]
+ also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) =
+ 1 / (real (n - 1) * a powr (real (n - 1)))" using assms
+ by (simp add: divide_simps powr_add [symmetric] of_nat_diff)
+ also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
+ by (intro powr_realpow)
+ finally show ?thesis
+ by (rule has_integral_eq [rotated])
+ (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
+qed
+
end
--- a/src/HOL/Limits.thy Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Limits.thy Thu Aug 25 15:50:43 2016 +0200
@@ -1519,7 +1519,7 @@
unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp
lemma filterlim_pow_at_top:
- fixes f :: "real \<Rightarrow> real"
+ fixes f :: "'a \<Rightarrow> real"
assumes "0 < n"
and f: "LIM x F. f x :> at_top"
shows "LIM x F. (f x)^n :: real :> at_top"
--- a/src/HOL/NthRoot.thy Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/NthRoot.thy Thu Aug 25 15:50:43 2016 +0200
@@ -469,6 +469,14 @@
lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
+lemma real_sqrt_power_even:
+ assumes "even n" "x \<ge> 0"
+ shows "sqrt x ^ n = x ^ (n div 2)"
+proof -
+ from assms obtain k where "n = 2*k" by (auto elim!: evenE)
+ with assms show ?thesis by (simp add: power_mult)
+qed
+
lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
by (meson not_le real_less_rsqrt)
--- a/src/HOL/Set_Interval.thy Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Set_Interval.thy Thu Aug 25 15:50:43 2016 +0200
@@ -1846,6 +1846,14 @@
shows "(\<Sum>k\<in>{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"
by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)
+lemma setsum_lessThan_telescope:
+ "(\<Sum>n<m. f (Suc n) - f n :: 'a :: ab_group_add) = f m - f 0"
+ by (induction m) (simp_all add: algebra_simps)
+
+lemma setsum_lessThan_telescope':
+ "(\<Sum>n<m. f n - f (Suc n) :: 'a :: ab_group_add) = f 0 - f m"
+ by (induction m) (simp_all add: algebra_simps)
+
subsubsection \<open>The formula for geometric sums\<close>
--- a/src/HOL/Transcendental.thy Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Transcendental.thy Thu Aug 25 15:50:43 2016 +0200
@@ -794,6 +794,44 @@
using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
by (force simp del: of_real_add)
+lemma termdiffs_strong':
+ fixes z :: "'a :: {real_normed_field,banach}"
+ assumes "\<And>z. norm z < K \<Longrightarrow> summable (\<lambda>n. c n * z ^ n)"
+ assumes "norm z < K"
+ shows "((\<lambda>z. \<Sum>n. c n * z^n) has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
+proof (rule termdiffs_strong)
+ define L :: real where "L = (norm z + K) / 2"
+ have "0 \<le> norm z" by simp
+ also note \<open>norm z < K\<close>
+ finally have K: "K \<ge> 0" by simp
+ from assms K have L: "L \<ge> 0" "norm z < L" "L < K" by (simp_all add: L_def)
+ from L show "norm z < norm (of_real L :: 'a)" by simp
+ from L show "summable (\<lambda>n. c n * of_real L ^ n)" by (intro assms(1)) simp_all
+qed
+
+lemma termdiffs_sums_strong:
+ fixes z :: "'a :: {banach,real_normed_field}"
+ assumes sums: "\<And>z. norm z < K \<Longrightarrow> (\<lambda>n. c n * z ^ n) sums f z"
+ assumes deriv: "(f has_field_derivative f') (at z)"
+ assumes norm: "norm z < K"
+ shows "(\<lambda>n. diffs c n * z ^ n) sums f'"
+proof -
+ have summable: "summable (\<lambda>n. diffs c n * z^n)"
+ by (intro termdiff_converges[OF norm] sums_summable[OF sums])
+ from norm have "eventually (\<lambda>z. z \<in> norm -` {..<K}) (nhds z)"
+ by (intro eventually_nhds_in_open open_vimage)
+ (simp_all add: continuous_on_norm continuous_on_id)
+ hence eq: "eventually (\<lambda>z. (\<Sum>n. c n * z^n) = f z) (nhds z)"
+ by eventually_elim (insert sums, simp add: sums_iff)
+
+ have "((\<lambda>z. \<Sum>n. c n * z^n) has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
+ by (intro termdiffs_strong'[OF _ norm] sums_summable[OF sums])
+ hence "(f has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
+ by (subst (asm) DERIV_cong_ev[OF refl eq refl])
+ from this and deriv have "(\<Sum>n. diffs c n * z^n) = f'" by (rule DERIV_unique)
+ with summable show ?thesis by (simp add: sums_iff)
+qed
+
lemma isCont_powser:
fixes K x :: "'a::{real_normed_field,banach}"
assumes "summable (\<lambda>n. c n * K ^ n)"
@@ -1114,6 +1152,18 @@
from for_subinterval[OF this] show ?thesis .
qed
+lemma geometric_deriv_sums:
+ fixes z :: "'a :: {real_normed_field,banach}"
+ assumes "norm z < 1"
+ shows "(\<lambda>n. of_nat (Suc n) * z ^ n) sums (1 / (1 - z)^2)"
+proof -
+ have "(\<lambda>n. diffs (\<lambda>n. 1) n * z^n) sums (1 / (1 - z)^2)"
+ proof (rule termdiffs_sums_strong)
+ fix z :: 'a assume "norm z < 1"
+ thus "(\<lambda>n. 1 * z^n) sums (1 / (1 - z))" by (simp add: geometric_sums)
+ qed (insert assms, auto intro!: derivative_eq_intros simp: power2_eq_square)
+ thus ?thesis unfolding diffs_def by simp
+qed
lemma isCont_pochhammer [continuous_intros]: "isCont (\<lambda>z. pochhammer z n) z"
for z :: "'a::real_normed_field"