author | haftmann |
Sun, 08 Oct 2017 22:28:20 +0200 | |
changeset 66804 | 3f9bb52082c4 |
parent 66554 | 19bf4d5966dc |
child 67399 | eab6ce8368fa |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/Harmonic_Numbers.thy |
62055
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
2 |
Author: Manuel Eberl, TU München |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
3 |
*) |
62055
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
4 |
|
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
5 |
section \<open>Harmonic Numbers\<close> |
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
6 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
7 |
theory Harmonic_Numbers |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
8 |
imports |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
9 |
Complex_Transcendental |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
10 |
Summation_Tests |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
11 |
Integral_Test |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
12 |
begin |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
13 |
|
62055
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
14 |
text \<open> |
62174 | 15 |
The definition of the Harmonic Numbers and the Euler-Mascheroni constant. |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
16 |
Also provides a reasonably accurate approximation of @{term "ln 2 :: real"} |
62174 | 17 |
and the Euler-Mascheroni constant. |
62055
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
18 |
\<close> |
755fda743c49
Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset
|
19 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
20 |
subsection \<open>The Harmonic numbers\<close> |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
21 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
22 |
definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
23 |
"harm n = (\<Sum>k=1..n. inverse (of_nat k))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
24 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
25 |
lemma harm_altdef: "harm n = (\<Sum>k<n. inverse (of_nat (Suc k)))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
26 |
unfolding harm_def by (induction n) simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
27 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
28 |
lemma harm_Suc: "harm (Suc n) = harm n + inverse (of_nat (Suc n))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
29 |
by (simp add: harm_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
30 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
31 |
lemma harm_nonneg: "harm n \<ge> (0 :: 'a :: {real_normed_field,linordered_field})" |
64267 | 32 |
unfolding harm_def by (intro sum_nonneg) simp_all |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
33 |
|
62065 | 34 |
lemma harm_pos: "n > 0 \<Longrightarrow> harm n > (0 :: 'a :: {real_normed_field,linordered_field})" |
64267 | 35 |
unfolding harm_def by (intro sum_pos) simp_all |
62065 | 36 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
37 |
lemma of_real_harm: "of_real (harm n) = harm n" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
38 |
unfolding harm_def by simp |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
39 |
|
65395
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
40 |
lemma abs_harm [simp]: "(abs (harm n) :: real) = harm n" |
66495
0b46bd081228
More tidying up of monotone_convergence_interval
paulson <lp15@cam.ac.uk>
parents:
66447
diff
changeset
|
41 |
using harm_nonneg[of n] by (rule abs_of_nonneg) |
65395
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
42 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
43 |
lemma norm_harm: "norm (harm n) = harm n" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
44 |
by (subst of_real_harm [symmetric]) (simp add: harm_nonneg) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
45 |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
46 |
lemma harm_expand: |
62065 | 47 |
"harm 0 = 0" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
48 |
"harm (Suc 0) = 1" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
49 |
"harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
50 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
51 |
have "numeral n = Suc (pred_numeral n)" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
52 |
also have "harm \<dots> = harm (pred_numeral n) + inverse (numeral n)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
53 |
by (subst harm_Suc, subst numeral_eq_Suc[symmetric]) simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
54 |
finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" . |
62065 | 55 |
qed (simp_all add: harm_def) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
56 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
57 |
lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
58 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
59 |
have "convergent (\<lambda>n. norm (harm n :: 'a)) \<longleftrightarrow> |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
60 |
convergent (harm :: nat \<Rightarrow> real)" by (simp add: norm_harm) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
61 |
also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k=Suc 0..Suc n. inverse (of_nat k) :: real)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
62 |
unfolding harm_def[abs_def] by (subst convergent_Suc_iff) simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
63 |
also have "... \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. inverse (of_nat (Suc k)) :: real)" |
64267 | 64 |
by (subst sum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
65 |
also have "... \<longleftrightarrow> summable (\<lambda>n. inverse (of_nat n) :: real)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
66 |
by (subst summable_Suc_iff [symmetric]) (simp add: summable_iff_convergent') |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
67 |
also have "\<not>..." by (rule not_summable_harmonic) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
68 |
finally show ?thesis by (blast dest: convergent_norm) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
69 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
70 |
|
62065 | 71 |
lemma harm_pos_iff [simp]: "harm n > (0 :: 'a :: {real_normed_field,linordered_field}) \<longleftrightarrow> n > 0" |
72 |
by (rule iffI, cases n, simp add: harm_expand, simp, rule harm_pos) |
|
73 |
||
74 |
lemma ln_diff_le_inverse: |
|
75 |
assumes "x \<ge> (1::real)" |
|
76 |
shows "ln (x + 1) - ln x < 1 / x" |
|
77 |
proof - |
|
78 |
from assms have "\<exists>z>x. z < x + 1 \<and> ln (x + 1) - ln x = (x + 1 - x) * inverse z" |
|
79 |
by (intro MVT2) (auto intro!: derivative_eq_intros simp: field_simps) |
|
80 |
then obtain z where z: "z > x" "z < x + 1" "ln (x + 1) - ln x = inverse z" by auto |
|
81 |
have "ln (x + 1) - ln x = inverse z" by fact |
|
82 |
also from z(1,2) assms have "\<dots> < 1 / x" by (simp add: field_simps) |
|
83 |
finally show ?thesis . |
|
84 |
qed |
|
85 |
||
86 |
lemma ln_le_harm: "ln (real n + 1) \<le> (harm n :: real)" |
|
87 |
proof (induction n) |
|
88 |
fix n assume IH: "ln (real n + 1) \<le> harm n" |
|
89 |
have "ln (real (Suc n) + 1) = ln (real n + 1) + (ln (real n + 2) - ln (real n + 1))" by simp |
|
90 |
also have "(ln (real n + 2) - ln (real n + 1)) \<le> 1 / real (Suc n)" |
|
91 |
using ln_diff_le_inverse[of "real n + 1"] by (simp add: add_ac) |
|
92 |
also note IH |
|
93 |
also have "harm n + 1 / real (Suc n) = harm (Suc n)" by (simp add: harm_Suc field_simps) |
|
94 |
finally show "ln (real (Suc n) + 1) \<le> harm (Suc n)" by - simp |
|
95 |
qed (simp_all add: harm_def) |
|
96 |
||
65395
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
97 |
lemma harm_at_top: "filterlim (harm :: nat \<Rightarrow> real) at_top sequentially" |
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
98 |
proof (rule filterlim_at_top_mono) |
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
99 |
show "eventually (\<lambda>n. harm n \<ge> ln (real (Suc n))) at_top" |
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
100 |
using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac) |
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
101 |
show "filterlim (\<lambda>n. ln (real (Suc n))) at_top sequentially" |
66495
0b46bd081228
More tidying up of monotone_convergence_interval
paulson <lp15@cam.ac.uk>
parents:
66447
diff
changeset
|
102 |
by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially] |
65395
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
103 |
filterlim_Suc) |
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
104 |
qed |
7504569a73c7
moved material from AFP to distribution
eberlm <eberlm@in.tum.de>
parents:
65273
diff
changeset
|
105 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
106 |
|
66495
0b46bd081228
More tidying up of monotone_convergence_interval
paulson <lp15@cam.ac.uk>
parents:
66447
diff
changeset
|
107 |
subsection \<open>The Euler-Mascheroni constant\<close> |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
108 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
109 |
text \<open> |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
110 |
The limit of the difference between the partial harmonic sum and the natural logarithm |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
111 |
(approximately 0.577216). This value occurs e.g. in the definition of the Gamma function. |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
112 |
\<close> |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
113 |
definition euler_mascheroni :: "'a :: real_normed_algebra_1" where |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
114 |
"euler_mascheroni = of_real (lim (\<lambda>n. harm n - ln (of_nat n)))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
115 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
116 |
lemma of_real_euler_mascheroni [simp]: "of_real euler_mascheroni = euler_mascheroni" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
117 |
by (simp add: euler_mascheroni_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
118 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
119 |
interpretation euler_mascheroni: antimono_fun_sum_integral_diff "\<lambda>x. inverse (x + 1)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
120 |
by unfold_locales (auto intro!: continuous_intros) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
121 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
122 |
lemma euler_mascheroni_sum_integral_diff_series: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
123 |
"euler_mascheroni.sum_integral_diff_series n = harm (Suc n) - ln (of_nat (Suc n))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
124 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
125 |
have "harm (Suc n) = (\<Sum>k=0..n. inverse (of_nat k + 1) :: real)" unfolding harm_def |
64267 | 126 |
unfolding One_nat_def by (subst sum_shift_bounds_cl_Suc_ivl) (simp add: add_ac) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
127 |
moreover have "((\<lambda>x. inverse (x + 1) :: real) has_integral ln (of_nat n + 1) - ln (0 + 1)) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
128 |
{0..of_nat n}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
129 |
by (intro fundamental_theorem_of_calculus) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
130 |
(auto intro!: derivative_eq_intros simp: divide_inverse |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
131 |
has_field_derivative_iff_has_vector_derivative[symmetric]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
132 |
hence "integral {0..of_nat n} (\<lambda>x. inverse (x + 1) :: real) = ln (of_nat (Suc n))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
133 |
by (auto dest!: integral_unique) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
134 |
ultimately show ?thesis |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
135 |
by (simp add: euler_mascheroni.sum_integral_diff_series_def atLeast0AtMost) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
136 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
137 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
138 |
lemma euler_mascheroni_sequence_decreasing: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
139 |
"m > 0 \<Longrightarrow> m \<le> n \<Longrightarrow> harm n - ln (of_nat n) \<le> harm m - ln (of_nat m :: real)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
140 |
by (cases m, simp, cases n, simp, hypsubst, |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
141 |
subst (1 2) euler_mascheroni_sum_integral_diff_series [symmetric], |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
142 |
rule euler_mascheroni.sum_integral_diff_series_antimono, simp) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
143 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
144 |
lemma euler_mascheroni_sequence_nonneg: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
145 |
"n > 0 \<Longrightarrow> harm n - ln (of_nat n) \<ge> (0::real)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
146 |
by (cases n, simp, hypsubst, subst euler_mascheroni_sum_integral_diff_series [symmetric], |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
147 |
rule euler_mascheroni.sum_integral_diff_series_nonneg) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
148 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
149 |
lemma euler_mascheroni_convergent: "convergent (\<lambda>n. harm n - ln (of_nat n) :: real)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
150 |
proof - |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
151 |
have A: "(\<lambda>n. harm (Suc n) - ln (of_nat (Suc n))) = |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
152 |
euler_mascheroni.sum_integral_diff_series" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
153 |
by (subst euler_mascheroni_sum_integral_diff_series [symmetric]) (rule refl) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
154 |
have "convergent (\<lambda>n. harm (Suc n) - ln (of_nat (Suc n) :: real))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
155 |
by (subst A) (fact euler_mascheroni.sum_integral_diff_series_convergent) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
156 |
thus ?thesis by (subst (asm) convergent_Suc_iff) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
157 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
158 |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
159 |
lemma euler_mascheroni_LIMSEQ: |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
160 |
"(\<lambda>n. harm n - ln (of_nat n) :: real) \<longlonglongrightarrow> euler_mascheroni" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
161 |
unfolding euler_mascheroni_def |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
162 |
by (simp add: convergent_LIMSEQ_iff [symmetric] euler_mascheroni_convergent) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
163 |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
164 |
lemma euler_mascheroni_LIMSEQ_of_real: |
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
165 |
"(\<lambda>n. of_real (harm n - ln (of_nat n))) \<longlonglongrightarrow> |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
166 |
(euler_mascheroni :: 'a :: {real_normed_algebra_1, topological_space})" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
167 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
168 |
have "(\<lambda>n. of_real (harm n - ln (of_nat n))) \<longlonglongrightarrow> (of_real (euler_mascheroni) :: 'a)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
169 |
by (intro tendsto_of_real euler_mascheroni_LIMSEQ) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
170 |
thus ?thesis by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
171 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
172 |
|
63721 | 173 |
lemma euler_mascheroni_sum_real: |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
174 |
"(\<lambda>n. inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2)) :: real) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
175 |
sums euler_mascheroni" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
176 |
using sums_add[OF telescope_sums[OF LIMSEQ_Suc[OF euler_mascheroni_LIMSEQ]] |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
177 |
telescope_sums'[OF LIMSEQ_inverse_real_of_nat]] |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
178 |
by (simp_all add: harm_def algebra_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
179 |
|
63721 | 180 |
lemma euler_mascheroni_sum: |
181 |
"(\<lambda>n. inverse (of_nat (n+1)) + of_real (ln (of_nat (n+1))) - of_real (ln (of_nat (n+2)))) |
|
182 |
sums (euler_mascheroni :: 'a :: {banach, real_normed_field})" |
|
183 |
proof - |
|
184 |
have "(\<lambda>n. of_real (inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2)))) |
|
185 |
sums (of_real euler_mascheroni :: 'a :: {banach, real_normed_field})" |
|
186 |
by (subst sums_of_real_iff) (rule euler_mascheroni_sum_real) |
|
187 |
thus ?thesis by simp |
|
188 |
qed |
|
189 |
||
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
190 |
lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
191 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
192 |
let ?f = "\<lambda>n. harm n - ln (real_of_nat n)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
193 |
let ?g = "\<lambda>n. if even n then 0 else (2::real)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
194 |
let ?em = "\<lambda>n. harm n - ln (real_of_nat n)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
195 |
have "eventually (\<lambda>n. ?em (2*n) - ?em n + ln 2 = (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) at_top" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
196 |
using eventually_gt_at_top[of "0::nat"] |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
197 |
proof eventually_elim |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
198 |
fix n :: nat assume n: "n > 0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
199 |
have "(\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) = |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
200 |
(\<Sum>k<2*n. ((-1)^k + ?g k) / of_nat (Suc k)) - (\<Sum>k<2*n. ?g k / of_nat (Suc k))" |
64267 | 201 |
by (simp add: sum.distrib algebra_simps divide_inverse) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
202 |
also have "(\<Sum>k<2*n. ((-1)^k + ?g k) / real_of_nat (Suc k)) = harm (2*n)" |
64267 | 203 |
unfolding harm_altdef by (intro sum.cong) (auto simp: field_simps) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
204 |
also have "(\<Sum>k<2*n. ?g k / real_of_nat (Suc k)) = (\<Sum>k|k<2*n \<and> odd k. ?g k / of_nat (Suc k))" |
64267 | 205 |
by (intro sum.mono_neutral_right) auto |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
206 |
also have "\<dots> = (\<Sum>k|k<2*n \<and> odd k. 2 / (real_of_nat (Suc k)))" |
64267 | 207 |
by (intro sum.cong) auto |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
208 |
also have "(\<Sum>k|k<2*n \<and> odd k. 2 / (real_of_nat (Suc k))) = harm n" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
209 |
unfolding harm_altdef |
64267 | 210 |
by (intro sum.reindex_cong[of "\<lambda>n. 2*n+1"]) (auto simp: inj_on_def field_simps elim!: oddE) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
211 |
also have "harm (2*n) - harm n = ?em (2*n) - ?em n + ln 2" using n |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
212 |
by (simp_all add: algebra_simps ln_mult) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
213 |
finally show "?em (2*n) - ?em n + ln 2 = (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))" .. |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
214 |
qed |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
215 |
moreover have "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real)) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
216 |
\<longlonglongrightarrow> euler_mascheroni - euler_mascheroni + ln 2" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
217 |
by (intro tendsto_intros euler_mascheroni_LIMSEQ filterlim_compose[OF euler_mascheroni_LIMSEQ] |
66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
65395
diff
changeset
|
218 |
filterlim_subseq) (auto simp: strict_mono_def) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
219 |
hence "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real)) \<longlonglongrightarrow> ln 2" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
220 |
ultimately have "(\<lambda>n. (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
221 |
by (rule Lim_transform_eventually) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
222 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
223 |
moreover have "summable (\<lambda>k. (-1)^k * inverse (real_of_nat (Suc k)))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
224 |
using LIMSEQ_inverse_real_of_nat |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
225 |
by (intro summable_Leibniz(1) decseq_imp_monoseq decseq_SucI) simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
226 |
hence A: "(\<lambda>n. \<Sum>k<n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
227 |
by (simp add: summable_sums_iff divide_inverse sums_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
228 |
from filterlim_compose[OF this filterlim_subseq[of "op * (2::nat)"]] |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
229 |
have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))" |
66447
a1f5c5c26fa6
Replaced subseq with strict_mono
eberlm <eberlm@in.tum.de>
parents:
65395
diff
changeset
|
230 |
by (simp add: strict_mono_def) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
231 |
ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
232 |
with A show ?thesis by (simp add: sums_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
233 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
234 |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
235 |
lemma alternating_harmonic_series_sums': |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
236 |
"(\<lambda>k. inverse (real_of_nat (2*k+1)) - inverse (real_of_nat (2*k+2))) sums ln 2" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
237 |
unfolding sums_def |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
238 |
proof (rule Lim_transform_eventually) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
239 |
show "(\<lambda>n. \<Sum>k<2*n. (-1)^k / (real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2" |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
240 |
using alternating_harmonic_series_sums unfolding sums_def |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
241 |
by (rule filterlim_compose) (rule mult_nat_left_at_top, simp) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
242 |
show "eventually (\<lambda>n. (\<Sum>k<2*n. (-1)^k / (real_of_nat (Suc k))) = |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
243 |
(\<Sum>k<n. inverse (real_of_nat (2*k+1)) - inverse (real_of_nat (2*k+2)))) sequentially" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
244 |
proof (intro always_eventually allI) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
245 |
fix n :: nat |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
246 |
show "(\<Sum>k<2*n. (-1)^k / (real_of_nat (Suc k))) = |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
247 |
(\<Sum>k<n. inverse (real_of_nat (2*k+1)) - inverse (real_of_nat (2*k+2)))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
248 |
by (induction n) (simp_all add: inverse_eq_divide) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
249 |
qed |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
250 |
qed |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
251 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
252 |
|
66495
0b46bd081228
More tidying up of monotone_convergence_interval
paulson <lp15@cam.ac.uk>
parents:
66447
diff
changeset
|
253 |
subsection \<open>Bounds on the Euler-Mascheroni constant\<close> |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
254 |
|
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
255 |
(* TODO: Move? *) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
256 |
lemma ln_inverse_approx_le: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
257 |
assumes "(x::real) > 0" "a > 0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
258 |
shows "ln (x + a) - ln x \<le> a * (inverse x + inverse (x + a))/2" (is "_ \<le> ?A") |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
259 |
proof - |
63040 | 260 |
define f' where "f' = (inverse (x + a) - inverse x)/a" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
261 |
have f'_nonpos: "f' \<le> 0" using assms by (simp add: f'_def divide_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
262 |
let ?f = "\<lambda>t. (t - x) * f' + inverse x" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
263 |
let ?F = "\<lambda>t. (t - x)^2 * f' / 2 + t * inverse x" |
66554
19bf4d5966dc
correction to my previous commit
paulson <lp15@cam.ac.uk>
parents:
66495
diff
changeset
|
264 |
have diff: "\<And>t. t \<in> {x..x+a} \<Longrightarrow> (?F has_vector_derivative ?f t) (at t within {x..x+a})" |
19bf4d5966dc
correction to my previous commit
paulson <lp15@cam.ac.uk>
parents:
66495
diff
changeset
|
265 |
using assms |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
266 |
by (auto intro!: derivative_eq_intros |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
267 |
simp: has_field_derivative_iff_has_vector_derivative[symmetric]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
268 |
from assms have "(?f has_integral (?F (x+a) - ?F x)) {x..x+a}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
269 |
by (intro fundamental_theorem_of_calculus[OF _ diff]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
270 |
(auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] field_simps |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
271 |
intro!: derivative_eq_intros) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
272 |
also have "?F (x+a) - ?F x = (a*2 + f'*a\<^sup>2*x) / (2*x)" using assms by (simp add: field_simps) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
273 |
also have "f'*a^2 = - (a^2) / (x*(x + a))" using assms |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
274 |
by (simp add: divide_simps f'_def power2_eq_square) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
275 |
also have "(a*2 + - a\<^sup>2/(x*(x+a))*x) / (2*x) = ?A" using assms |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
276 |
by (simp add: divide_simps power2_eq_square) (simp add: algebra_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
277 |
finally have int1: "((\<lambda>t. (t - x) * f' + inverse x) has_integral ?A) {x..x + a}" . |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
278 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
279 |
from assms have int2: "(inverse has_integral (ln (x + a) - ln x)) {x..x+a}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
280 |
by (intro fundamental_theorem_of_calculus) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
281 |
(auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] divide_simps |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
282 |
intro!: derivative_eq_intros) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
283 |
hence "ln (x + a) - ln x = integral {x..x+a} inverse" by (simp add: integral_unique) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
284 |
also have ineq: "\<forall>xa\<in>{x..x + a}. inverse xa \<le> (xa - x) * f' + inverse x" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
285 |
proof |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
286 |
fix t assume t': "t \<in> {x..x+a}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
287 |
with assms have t: "0 \<le> (t - x) / a" "(t - x) / a \<le> 1" by simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
288 |
have "inverse t = inverse ((1 - (t - x) / a) *\<^sub>R x + ((t - x) / a) *\<^sub>R (x + a))" (is "_ = ?A") |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
289 |
using assms t' by (simp add: field_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
290 |
also from assms have "convex_on {x..x+a} inverse" by (intro convex_on_inverse) auto |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
291 |
from convex_onD_Icc[OF this _ t] assms |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
292 |
have "?A \<le> (1 - (t - x) / a) * inverse x + (t - x) / a * inverse (x + a)" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
293 |
also have "\<dots> = (t - x) * f' + inverse x" using assms |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
294 |
by (simp add: f'_def divide_simps) (simp add: f'_def field_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
295 |
finally show "inverse t \<le> (t - x) * f' + inverse x" . |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
296 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
297 |
hence "integral {x..x+a} inverse \<le> integral {x..x+a} ?f" using f'_nonpos assms |
66495
0b46bd081228
More tidying up of monotone_convergence_interval
paulson <lp15@cam.ac.uk>
parents:
66447
diff
changeset
|
298 |
by (blast intro: integral_le has_integral_integrable[OF int1] has_integral_integrable[OF int2] ineq) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
299 |
also have "\<dots> = ?A" using int1 by (rule integral_unique) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
300 |
finally show ?thesis . |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
301 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
302 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
303 |
lemma ln_inverse_approx_ge: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
304 |
assumes "(x::real) > 0" "x < y" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
305 |
shows "ln y - ln x \<ge> 2 * (y - x) / (x + y)" (is "_ \<ge> ?A") |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
306 |
proof - |
63040 | 307 |
define m where "m = (x+y)/2" |
308 |
define f' where "f' = -inverse (m^2)" |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
309 |
from assms have m: "m > 0" by (simp add: m_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
310 |
let ?F = "\<lambda>t. (t - m)^2 * f' / 2 + t / m" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
311 |
from assms have "((\<lambda>t. (t - m) * f' + inverse m) has_integral (?F y - ?F x)) {x..y}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
312 |
by (intro fundamental_theorem_of_calculus) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
313 |
(auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] divide_simps |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
314 |
intro!: derivative_eq_intros) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
315 |
also from m have "?F y - ?F x = ((y - m)^2 - (x - m)^2) * f' / 2 + (y - x) / m" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
316 |
by (simp add: field_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
317 |
also have "((y - m)^2 - (x - m)^2) = 0" by (simp add: m_def power2_eq_square field_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
318 |
also have "0 * f' / 2 + (y - x) / m = ?A" by (simp add: m_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
319 |
finally have int1: "((\<lambda>t. (t - m) * f' + inverse m) has_integral ?A) {x..y}" . |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
320 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
321 |
from assms have int2: "(inverse has_integral (ln y - ln x)) {x..y}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
322 |
by (intro fundamental_theorem_of_calculus) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
323 |
(auto simp: has_field_derivative_iff_has_vector_derivative[symmetric] divide_simps |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
324 |
intro!: derivative_eq_intros) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
325 |
hence "ln y - ln x = integral {x..y} inverse" by (simp add: integral_unique) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
326 |
also have ineq: "\<forall>xa\<in>{x..y}. inverse xa \<ge> (xa - m) * f' + inverse m" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
327 |
proof |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
328 |
fix t assume t: "t \<in> {x..y}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
329 |
from t assms have "inverse t - inverse m \<ge> f' * (t - m)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
330 |
by (intro convex_on_imp_above_tangent[of "{0<..}"] convex_on_inverse) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
331 |
(auto simp: m_def interior_open f'_def power2_eq_square intro!: derivative_eq_intros) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
332 |
thus "(t - m) * f' + inverse m \<le> inverse t" by (simp add: algebra_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
333 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
334 |
hence "integral {x..y} inverse \<ge> integral {x..y} (\<lambda>t. (t - m) * f' + inverse m)" |
66495
0b46bd081228
More tidying up of monotone_convergence_interval
paulson <lp15@cam.ac.uk>
parents:
66447
diff
changeset
|
335 |
using int1 int2 by (blast intro: integral_le has_integral_integrable) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
336 |
also have "integral {x..y} (\<lambda>t. (t - m) * f' + inverse m) = ?A" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
337 |
using integral_unique[OF int1] by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
338 |
finally show ?thesis . |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
339 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
340 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
341 |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
342 |
lemma euler_mascheroni_lower: |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
343 |
"euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
344 |
and euler_mascheroni_upper: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
345 |
"euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
346 |
proof - |
63040 | 347 |
define D :: "_ \<Rightarrow> real" |
348 |
where "D n = inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))" for n |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
349 |
let ?g = "\<lambda>n. ln (of_nat (n+2)) - ln (of_nat (n+1)) - inverse (of_nat (n+1)) :: real" |
63040 | 350 |
define inv where [abs_def]: "inv n = inverse (real_of_nat n)" for n |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
351 |
fix n :: nat |
63721 | 352 |
note summable = sums_summable[OF euler_mascheroni_sum_real, folded D_def] |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
353 |
have sums: "(\<lambda>k. (inv (Suc (k + (n+1))) - inv (Suc (Suc k + (n+1))))/2) sums ((inv (Suc (0 + (n+1))) - 0)/2)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
354 |
unfolding inv_def |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
355 |
by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
356 |
have sums': "(\<lambda>k. (inv (Suc (k + n)) - inv (Suc (Suc k + n)))/2) sums ((inv (Suc (0 + n)) - 0)/2)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
357 |
unfolding inv_def |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
358 |
by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat) |
63721 | 359 |
from euler_mascheroni_sum_real have "euler_mascheroni = (\<Sum>k. D k)" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
360 |
by (simp add: sums_iff D_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
361 |
also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)" |
66495
0b46bd081228
More tidying up of monotone_convergence_interval
paulson <lp15@cam.ac.uk>
parents:
66447
diff
changeset
|
362 |
by (subst suminf_split_initial_segment[OF summable, of "Suc n"], |
63721 | 363 |
subst lessThan_Suc_atMost) simp |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
364 |
finally have sum: "(\<Sum>k\<le>n. D k) - euler_mascheroni = -(\<Sum>k. D (k + Suc n))" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
365 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
366 |
note sum |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
367 |
also have "\<dots> \<le> -(\<Sum>k. (inv (k + Suc n + 1) - inv (k + Suc n + 2)) / 2)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
368 |
proof (intro le_imp_neg_le suminf_le allI summable_ignore_initial_segment[OF summable]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
369 |
fix k' :: nat |
63040 | 370 |
define k where "k = k' + Suc n" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
371 |
hence k: "k > 0" by (simp add: k_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
372 |
have "real_of_nat (k+1) > 0" by (simp add: k_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
373 |
with ln_inverse_approx_le[OF this zero_less_one] |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
374 |
have "ln (of_nat k + 2) - ln (of_nat k + 1) \<le> (inv (k+1) + inv (k+2))/2" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
375 |
by (simp add: inv_def add_ac) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
376 |
hence "(inv (k+1) - inv (k+2))/2 \<le> inv (k+1) + ln (of_nat (k+1)) - ln (of_nat (k+2))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
377 |
by (simp add: field_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
378 |
also have "\<dots> = D k" unfolding D_def inv_def .. |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
379 |
finally show "D (k' + Suc n) \<ge> (inv (k' + Suc n + 1) - inv (k' + Suc n + 2)) / 2" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
380 |
by (simp add: k_def) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
381 |
from sums_summable[OF sums] |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
382 |
show "summable (\<lambda>k. (inv (k + Suc n + 1) - inv (k + Suc n + 2))/2)" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
383 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
384 |
also from sums have "\<dots> = -inv (n+2) / 2" by (simp add: sums_iff) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
385 |
finally have "euler_mascheroni \<ge> (\<Sum>k\<le>n. D k) + 1 / (of_nat (2 * (n+2)))" |
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
386 |
by (simp add: inv_def field_simps) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
387 |
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)))" |
64267 | 388 |
unfolding harm_altdef D_def by (subst lessThan_Suc_atMost) (simp add: sum.distrib sum_subtractf) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
389 |
also have "(\<Sum>k\<le>n. ln (real_of_nat (Suc k+1)) - ln (of_nat (k+1))) = ln (of_nat (n+2))" |
64267 | 390 |
by (subst atLeast0AtMost [symmetric], subst sum_Suc_diff) simp_all |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
391 |
finally show "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
392 |
by simp |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
393 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
394 |
note sum |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
395 |
also have "-(\<Sum>k. D (k + Suc n)) \<ge> -(\<Sum>k. (inv (Suc (k + n)) - inv (Suc (Suc k + n)))/2)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
396 |
proof (intro le_imp_neg_le suminf_le allI summable_ignore_initial_segment[OF summable]) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
397 |
fix k' :: nat |
63040 | 398 |
define k where "k = k' + Suc n" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
399 |
hence k: "k > 0" by (simp add: k_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
400 |
have "real_of_nat (k+1) > 0" by (simp add: k_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
401 |
from ln_inverse_approx_ge[of "of_nat k + 1" "of_nat k + 2"] |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
402 |
have "2 / (2 * real_of_nat k + 3) \<le> ln (of_nat (k+2)) - ln (real_of_nat (k+1))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
403 |
by (simp add: add_ac) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
404 |
hence "D k \<le> 1 / real_of_nat (k+1) - 2 / (2 * real_of_nat k + 3)" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
405 |
by (simp add: D_def inverse_eq_divide inv_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
406 |
also have "\<dots> = inv ((k+1)*(2*k+3))" unfolding inv_def by (simp add: field_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
407 |
also have "\<dots> \<le> inv (2*k*(k+1))" unfolding inv_def using k |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
408 |
by (intro le_imp_inverse_le) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
409 |
(simp add: algebra_simps, simp del: of_nat_add) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
410 |
also have "\<dots> = (inv k - inv (k+1))/2" unfolding inv_def using k |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
411 |
by (simp add: divide_simps del: of_nat_mult) (simp add: algebra_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
412 |
finally show "D k \<le> (inv (Suc (k' + n)) - inv (Suc (Suc k' + n)))/2" unfolding k_def by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
413 |
next |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
414 |
from sums_summable[OF sums'] |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
415 |
show "summable (\<lambda>k. (inv (Suc (k + n)) - inv (Suc (Suc k + n)))/2)" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
416 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
417 |
also from sums' have "(\<Sum>k. (inv (Suc (k + n)) - inv (Suc (Suc k + n)))/2) = inv (n+1)/2" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
418 |
by (simp add: sums_iff) |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
419 |
finally have "euler_mascheroni \<le> (\<Sum>k\<le>n. D k) + 1 / of_nat (2 * (n+1))" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
420 |
by (simp add: inv_def field_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
421 |
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)))" |
64267 | 422 |
unfolding harm_altdef D_def by (subst lessThan_Suc_atMost) (simp add: sum.distrib sum_subtractf) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
423 |
also have "(\<Sum>k\<le>n. ln (real_of_nat (Suc k+1)) - ln (of_nat (k+1))) = ln (of_nat (n+2))" |
64267 | 424 |
by (subst atLeast0AtMost [symmetric], subst sum_Suc_diff) simp_all |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
425 |
finally show "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
426 |
by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
427 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
428 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
429 |
lemma euler_mascheroni_pos: "euler_mascheroni > (0::real)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
430 |
using euler_mascheroni_lower[of 0] ln_2_less_1 by (simp add: harm_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
431 |
|
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
432 |
context |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
433 |
begin |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
434 |
|
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
435 |
private lemma ln_approx_aux: |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
436 |
fixes n :: nat and x :: real |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
437 |
defines "y \<equiv> (x-1)/(x+1)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
438 |
assumes x: "x > 0" "x \<noteq> 1" |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
439 |
shows "inverse (2*y^(2*n+1)) * (ln x - (\<Sum>k<n. 2*y^(2*k+1) / of_nat (2*k+1))) \<in> |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
440 |
{0..(1 / (1 - y^2) / of_nat (2*n+1))}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
441 |
proof - |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
442 |
from x have norm_y: "norm y < 1" unfolding y_def by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
443 |
from power_strict_mono[OF this, of 2] have norm_y': "norm y^2 < 1" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
444 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
445 |
let ?f = "\<lambda>k. 2 * y ^ (2*k+1) / of_nat (2*k+1)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
446 |
note sums = ln_series_quadratic[OF x(1)] |
63040 | 447 |
define c where "c = inverse (2*y^(2*n+1))" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
448 |
let ?d = "c * (ln x - (\<Sum>k<n. ?f k))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
449 |
have "\<forall>k. y\<^sup>2^k / of_nat (2*(k+n)+1) \<le> y\<^sup>2 ^ k / of_nat (2*n+1)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
450 |
by (intro allI divide_left_mono mult_right_mono mult_pos_pos zero_le_power[of "y^2"]) simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
451 |
moreover { |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
452 |
have "(\<lambda>k. ?f (k + n)) sums (ln x - (\<Sum>k<n. ?f k))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
453 |
using sums_split_initial_segment[OF sums] by (simp add: y_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
454 |
hence "(\<lambda>k. c * ?f (k + n)) sums ?d" by (rule sums_mult) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
455 |
also have "(\<lambda>k. c * (2*y^(2*(k+n)+1) / of_nat (2*(k+n)+1))) = |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
456 |
(\<lambda>k. (c * (2*y^(2*n+1))) * ((y^2)^k / of_nat (2*(k+n)+1)))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
457 |
by (simp only: ring_distribs power_add power_mult) (simp add: mult_ac) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
458 |
also from x have "c * (2*y^(2*n+1)) = 1" by (simp add: c_def y_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
459 |
finally have "(\<lambda>k. (y^2)^k / of_nat (2*(k+n)+1)) sums ?d" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
460 |
} note sums' = this |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
461 |
moreover from norm_y' have "(\<lambda>k. (y^2)^k / of_nat (2*n+1)) sums (1 / (1 - y^2) / of_nat (2*n+1))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
462 |
by (intro sums_divide geometric_sums) (simp_all add: norm_power) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
463 |
ultimately have "?d \<le> (1 / (1 - y^2) / of_nat (2*n+1))" by (rule sums_le) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
464 |
moreover have "c * (ln x - (\<Sum>k<n. 2 * y ^ (2 * k + 1) / real_of_nat (2 * k + 1))) \<ge> 0" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
465 |
by (intro sums_le[OF _ sums_zero sums']) simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
466 |
ultimately show ?thesis unfolding c_def by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
467 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
468 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
469 |
lemma |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
470 |
fixes n :: nat and x :: real |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
471 |
defines "y \<equiv> (x-1)/(x+1)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
472 |
defines "approx \<equiv> (\<Sum>k<n. 2*y^(2*k+1) / of_nat (2*k+1))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
473 |
defines "d \<equiv> y^(2*n+1) / (1 - y^2) / of_nat (2*n+1)" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
474 |
assumes x: "x > 1" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
475 |
shows ln_approx_bounds: "ln x \<in> {approx..approx + 2*d}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
476 |
and ln_approx_abs: "abs (ln x - (approx + d)) \<le> d" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
477 |
proof - |
63040 | 478 |
define c where "c = 2*y^(2*n+1)" |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
479 |
from x have c_pos: "c > 0" unfolding c_def y_def |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
480 |
by (intro mult_pos_pos zero_less_power) simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
481 |
have A: "inverse c * (ln x - (\<Sum>k<n. 2*y^(2*k+1) / of_nat (2*k+1))) \<in> |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
482 |
{0.. (1 / (1 - y^2) / of_nat (2*n+1))}" using assms unfolding y_def c_def |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
483 |
by (intro ln_approx_aux) simp_all |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
484 |
hence "inverse c * (ln x - (\<Sum>k<n. 2*y^(2*k+1)/of_nat (2*k+1))) \<le> (1 / (1-y^2) / of_nat (2*n+1))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
485 |
by simp |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
486 |
hence "(ln x - (\<Sum>k<n. 2*y^(2*k+1) / of_nat (2*k+1))) / c \<le> (1 / (1 - y^2) / of_nat (2*n+1))" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
487 |
by (auto simp add: divide_simps) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
488 |
with c_pos have "ln x \<le> c / (1 - y^2) / of_nat (2*n+1) + approx" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
489 |
by (subst (asm) pos_divide_le_eq) (simp_all add: mult_ac approx_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
490 |
moreover { |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
491 |
from A c_pos have "0 \<le> c * (inverse c * (ln x - (\<Sum>k<n. 2*y^(2*k+1) / of_nat (2*k+1))))" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
492 |
by (intro mult_nonneg_nonneg[of c]) simp_all |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
493 |
also have "\<dots> = (c * inverse c) * (ln x - (\<Sum>k<n. 2*y^(2*k+1) / of_nat (2*k+1)))" |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
494 |
by (simp add: mult_ac) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
495 |
also from c_pos have "c * inverse c = 1" by simp |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
496 |
finally have "ln x \<ge> approx" by (simp add: approx_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
497 |
} |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
498 |
ultimately show "ln x \<in> {approx..approx + 2*d}" by (simp add: c_def d_def) |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
499 |
thus "abs (ln x - (approx + d)) \<le> d" by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
500 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
501 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
502 |
end |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
503 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
504 |
lemma euler_mascheroni_bounds: |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
505 |
fixes n :: nat assumes "n \<ge> 1" defines "t \<equiv> harm n - ln (of_nat (Suc n)) :: real" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
506 |
shows "euler_mascheroni \<in> {t + inverse (of_nat (2*(n+1)))..t + inverse (of_nat (2*n))}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
507 |
using assms euler_mascheroni_upper[of "n-1"] euler_mascheroni_lower[of "n-1"] |
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
508 |
unfolding t_def by (cases n) (simp_all add: harm_Suc t_def inverse_eq_divide) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
509 |
|
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
510 |
lemma euler_mascheroni_bounds': |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
511 |
fixes n :: nat assumes "n \<ge> 1" "ln (real_of_nat (Suc n)) \<in> {l<..<u}" |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
512 |
shows "euler_mascheroni \<in> |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
513 |
{harm n - u + inverse (of_nat (2*(n+1)))<..<harm n - l + inverse (of_nat (2*n))}" |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
514 |
using euler_mascheroni_bounds[OF assms(1)] assms(2) by auto |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
515 |
|
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
516 |
|
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
517 |
text \<open> |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
518 |
Approximation of @{term "ln 2"}. The lower bound is accurate to about 0.03; the upper |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
519 |
bound is accurate to about 0.0015. |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
520 |
\<close> |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
521 |
lemma ln2_ge_two_thirds: "2/3 \<le> ln (2::real)" |
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
522 |
and ln2_le_25_over_36: "ln (2::real) \<le> 25/36" |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
523 |
using ln_approx_bounds[of 2 1, simplified, simplified eval_nat_numeral, simplified] by simp_all |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
524 |
|
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
525 |
|
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
526 |
text \<open> |
66495
0b46bd081228
More tidying up of monotone_convergence_interval
paulson <lp15@cam.ac.uk>
parents:
66447
diff
changeset
|
527 |
Approximation of the Euler-Mascheroni constant. The lower bound is accurate to about 0.0015; |
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
528 |
the upper bound is accurate to about 0.015. |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
529 |
\<close> |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
530 |
lemma euler_mascheroni_gt_19_over_33: "(euler_mascheroni :: real) > 19/33" (is ?th1) |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
531 |
and euler_mascheroni_less_13_over_22: "(euler_mascheroni :: real) < 13/22" (is ?th2) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
532 |
proof - |
65109 | 533 |
have "ln (real (Suc 7)) = 3 * ln 2" by (simp add: ln_powr [symmetric]) |
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
534 |
also from ln_approx_bounds[of 2 3] have "\<dots> \<in> {3*307/443<..<3*4615/6658}" |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
535 |
by (simp add: eval_nat_numeral) |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
536 |
finally have "ln (real (Suc 7)) \<in> \<dots>" . |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
537 |
from euler_mascheroni_bounds'[OF _ this] have "?th1 \<and> ?th2" by (simp_all add: harm_expand) |
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
538 |
thus ?th1 ?th2 by blast+ |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
539 |
qed |
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset
|
540 |
|
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset
|
541 |
end |