author  paulson <lp15@cam.ac.uk> 
Thu, 16 Mar 2017 13:55:29 +0000  
changeset 65273  917ae0ba03a2 
parent 65109  a79c1080f1e9 
child 65395  7504569a73c7 
permissions  rwrr 
63627  1 
(* Title: HOL/Analysis/Harmonic_Numbers.thy 
62055
755fda743c49
MultivariateAnalysis: 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
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

4 

755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

5 
section \<open>Harmonic Numbers\<close> 
755fda743c49
MultivariateAnalysis: 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
HOLMultivariate_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
HOLMultivariate_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
MultivariateAnalysis: 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 EulerMascheroni constant. 
63594
bd218a9320b5
HOLMultivariate_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 EulerMascheroni constant. 
62055
755fda743c49
MultivariateAnalysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents:
62049
diff
changeset

18 
\<close> 
755fda743c49
MultivariateAnalysis: 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
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

39 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

40 
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

41 
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

42 

63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

43 
lemma harm_expand: 
62065  44 
"harm 0 = 0" 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

45 
"harm (Suc 0) = 1" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

46 
"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

47 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

48 
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

49 
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

50 
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

51 
finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" . 
62065  52 
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

53 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

54 
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

55 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

56 
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

57 
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

58 
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

59 
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

60 
also have "... \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. inverse (of_nat (Suc k)) :: real)" 
64267  61 
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

62 
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

63 
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

64 
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

65 
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

66 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

67 

62065  68 
lemma harm_pos_iff [simp]: "harm n > (0 :: 'a :: {real_normed_field,linordered_field}) \<longleftrightarrow> n > 0" 
69 
by (rule iffI, cases n, simp add: harm_expand, simp, rule harm_pos) 

70 

71 
lemma ln_diff_le_inverse: 

72 
assumes "x \<ge> (1::real)" 

73 
shows "ln (x + 1)  ln x < 1 / x" 

74 
proof  

75 
from assms have "\<exists>z>x. z < x + 1 \<and> ln (x + 1)  ln x = (x + 1  x) * inverse z" 

76 
by (intro MVT2) (auto intro!: derivative_eq_intros simp: field_simps) 

77 
then obtain z where z: "z > x" "z < x + 1" "ln (x + 1)  ln x = inverse z" by auto 

78 
have "ln (x + 1)  ln x = inverse z" by fact 

79 
also from z(1,2) assms have "\<dots> < 1 / x" by (simp add: field_simps) 

80 
finally show ?thesis . 

81 
qed 

82 

83 
lemma ln_le_harm: "ln (real n + 1) \<le> (harm n :: real)" 

84 
proof (induction n) 

85 
fix n assume IH: "ln (real n + 1) \<le> harm n" 

86 
have "ln (real (Suc n) + 1) = ln (real n + 1) + (ln (real n + 2)  ln (real n + 1))" by simp 

87 
also have "(ln (real n + 2)  ln (real n + 1)) \<le> 1 / real (Suc n)" 

88 
using ln_diff_le_inverse[of "real n + 1"] by (simp add: add_ac) 

89 
also note IH 

90 
also have "harm n + 1 / real (Suc n) = harm (Suc n)" by (simp add: harm_Suc field_simps) 

91 
finally show "ln (real (Suc n) + 1) \<le> harm (Suc n)" by  simp 

92 
qed (simp_all add: harm_def) 

93 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

94 

62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

95 
subsection \<open>The EulerMascheroni constant\<close> 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

96 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

97 
text \<open> 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

98 
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

99 
(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

100 
\<close> 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

101 
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

102 
"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

103 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

104 
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

105 
by (simp add: euler_mascheroni_def) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

106 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

107 
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

108 
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

109 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

110 
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

111 
"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

112 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

113 
have "harm (Suc n) = (\<Sum>k=0..n. inverse (of_nat k + 1) :: real)" unfolding harm_def 
64267  114 
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

115 
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

116 
{0..of_nat n}" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

117 
by (intro fundamental_theorem_of_calculus) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

118 
(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

119 
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

120 
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

121 
by (auto dest!: integral_unique) 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

122 
ultimately show ?thesis 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

123 
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

124 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

125 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

126 
lemma euler_mascheroni_sequence_decreasing: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

127 
"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

128 
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

129 
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

130 
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

131 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

132 
lemma euler_mascheroni_sequence_nonneg: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

133 
"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

134 
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

135 
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

136 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

137 
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

138 
proof  
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

139 
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

140 
euler_mascheroni.sum_integral_diff_series" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

141 
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

142 
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

143 
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

144 
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

145 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

146 

63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

147 
lemma euler_mascheroni_LIMSEQ: 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

148 
"(\<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

149 
unfolding euler_mascheroni_def 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

150 
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

151 

63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

152 
lemma euler_mascheroni_LIMSEQ_of_real: 
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

153 
"(\<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

154 
(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

155 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

156 
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

157 
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

158 
thus ?thesis by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

159 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

160 

63721  161 
lemma euler_mascheroni_sum_real: 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

162 
"(\<lambda>n. inverse (of_nat (n+1)) + ln (of_nat (n+1))  ln (of_nat (n+2)) :: real) 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

163 
sums euler_mascheroni" 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

164 
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

165 
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

166 
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

167 

63721  168 
lemma euler_mascheroni_sum: 
169 
"(\<lambda>n. inverse (of_nat (n+1)) + of_real (ln (of_nat (n+1)))  of_real (ln (of_nat (n+2)))) 

170 
sums (euler_mascheroni :: 'a :: {banach, real_normed_field})" 

171 
proof  

172 
have "(\<lambda>n. of_real (inverse (of_nat (n+1)) + ln (of_nat (n+1))  ln (of_nat (n+2)))) 

173 
sums (of_real euler_mascheroni :: 'a :: {banach, real_normed_field})" 

174 
by (subst sums_of_real_iff) (rule euler_mascheroni_sum_real) 

175 
thus ?thesis by simp 

176 
qed 

177 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

178 
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

179 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

180 
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

181 
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

182 
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

183 
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

184 
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

185 
proof eventually_elim 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

186 
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

187 
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

188 
(\<Sum>k<2*n. ((1)^k + ?g k) / of_nat (Suc k))  (\<Sum>k<2*n. ?g k / of_nat (Suc k))" 
64267  189 
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

190 
also have "(\<Sum>k<2*n. ((1)^k + ?g k) / real_of_nat (Suc k)) = harm (2*n)" 
64267  191 
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

192 
also have "(\<Sum>k<2*n. ?g k / real_of_nat (Suc k)) = (\<Sum>kk<2*n \<and> odd k. ?g k / of_nat (Suc k))" 
64267  193 
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

194 
also have "\<dots> = (\<Sum>kk<2*n \<and> odd k. 2 / (real_of_nat (Suc k)))" 
64267  195 
by (intro sum.cong) auto 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

196 
also have "(\<Sum>kk<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

197 
unfolding harm_altdef 
64267  198 
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

199 
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

200 
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

201 
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

202 
qed 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

203 
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

204 
\<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

205 
by (intro tendsto_intros euler_mascheroni_LIMSEQ filterlim_compose[OF euler_mascheroni_LIMSEQ] 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

206 
filterlim_subseq) (auto simp: subseq_def) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

207 
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

208 
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

209 
by (rule Lim_transform_eventually) 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

210 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

211 
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

212 
using LIMSEQ_inverse_real_of_nat 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

213 
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

214 
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

215 
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

216 
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

217 
have "(\<lambda>n. \<Sum>k<2*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

218 
by (simp add: subseq_def) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

219 
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

220 
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

221 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

222 

63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

223 
lemma alternating_harmonic_series_sums': 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

224 
"(\<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

225 
unfolding sums_def 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

226 
proof (rule Lim_transform_eventually) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

227 
show "(\<lambda>n. \<Sum>k<2*n. (1)^k / (real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2" 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

228 
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

229 
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

230 
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

231 
(\<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

232 
proof (intro always_eventually allI) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

233 
fix n :: nat 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

234 
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

235 
(\<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

236 
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

237 
qed 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

238 
qed 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

239 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

240 

62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

241 
subsection \<open>Bounds on the EulerMascheroni constant\<close> 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

242 

62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

243 
(* TODO: Move? *) 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

244 
lemma ln_inverse_approx_le: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

245 
assumes "(x::real) > 0" "a > 0" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

246 
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

247 
proof  
63040  248 
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

249 
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

250 
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

251 
let ?F = "\<lambda>t. (t  x)^2 * f' / 2 + t * inverse x" 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

252 
have diff: "\<forall>t\<in>{x..x+a}. (?F has_vector_derivative ?f t) 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

253 
(at t within {x..x+a})" using assms 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

254 
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

255 
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

256 
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

257 
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

258 
(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

259 
intro!: derivative_eq_intros) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

260 
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
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

261 
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

262 
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

263 
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

264 
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

265 
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

266 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

267 
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

268 
by (intro fundamental_theorem_of_calculus) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

269 
(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

270 
intro!: derivative_eq_intros) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

271 
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

272 
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

273 
proof 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

274 
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

275 
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

276 
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

277 
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

278 
also from assms have "convex_on {x..x+a} inverse" by (intro convex_on_inverse) auto 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

279 
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

280 
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

281 
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

282 
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

283 
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

284 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

285 
hence "integral {x..x+a} inverse \<le> integral {x..x+a} ?f" using f'_nonpos assms 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

286 
by (intro integral_le has_integral_integrable[OF int1] has_integral_integrable[OF int2] ineq) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

287 
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

288 
finally show ?thesis . 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

289 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

290 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

291 
lemma ln_inverse_approx_ge: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

292 
assumes "(x::real) > 0" "x < y" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

293 
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

294 
proof  
63040  295 
define m where "m = (x+y)/2" 
296 
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

297 
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

298 
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

299 
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

300 
by (intro fundamental_theorem_of_calculus) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

301 
(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

302 
intro!: derivative_eq_intros) 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

303 
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

304 
by (simp add: field_simps) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

305 
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

306 
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

307 
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

308 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

309 
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

310 
by (intro fundamental_theorem_of_calculus) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

311 
(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

312 
intro!: derivative_eq_intros) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

313 
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

314 
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

315 
proof 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

316 
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

317 
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

318 
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

319 
(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

320 
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

321 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

322 
hence "integral {x..y} inverse \<ge> integral {x..y} (\<lambda>t. (t  m) * f' + inverse m)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

323 
using int1 int2 by (intro integral_le has_integral_integrable) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

324 
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

325 
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

326 
finally show ?thesis . 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

327 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

328 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

329 

63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

330 
lemma euler_mascheroni_lower: 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

331 
"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

332 
and euler_mascheroni_upper: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

333 
"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

334 
proof  
63040  335 
define D :: "_ \<Rightarrow> real" 
336 
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

337 
let ?g = "\<lambda>n. ln (of_nat (n+2))  ln (of_nat (n+1))  inverse (of_nat (n+1)) :: real" 
63040  338 
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

339 
fix n :: nat 
63721  340 
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

341 
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

342 
unfolding inv_def 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

343 
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

344 
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

345 
unfolding inv_def 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

346 
by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat) 
63721  347 
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

348 
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

349 
also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)" 
63721  350 
by (subst suminf_split_initial_segment[OF summable, of "Suc n"], 
351 
subst lessThan_Suc_atMost) simp 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

352 
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

353 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

354 
note sum 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

355 
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

356 
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

357 
fix k' :: nat 
63040  358 
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

359 
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

360 
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

361 
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

362 
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

363 
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

364 
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

365 
by (simp add: field_simps) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

366 
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

367 
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

368 
by (simp add: k_def) 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

369 
from sums_summable[OF sums] 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

370 
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

371 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

372 
also from sums have "\<dots> = inv (n+2) / 2" by (simp add: sums_iff) 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

373 
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

374 
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

375 
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  376 
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

377 
also have "(\<Sum>k\<le>n. ln (real_of_nat (Suc k+1))  ln (of_nat (k+1))) = ln (of_nat (n+2))" 
64267  378 
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

379 
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

380 
by simp 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

381 

62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

382 
note sum 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

383 
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

384 
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

385 
fix k' :: nat 
63040  386 
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

387 
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

388 
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

389 
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

390 
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

391 
by (simp add: add_ac) 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

392 
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

393 
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

394 
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

395 
also have "\<dots> \<le> inv (2*k*(k+1))" unfolding inv_def using k 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

396 
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

397 
(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

398 
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

399 
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

400 
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

401 
next 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

402 
from sums_summable[OF sums'] 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

403 
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

404 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

405 
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

406 
by (simp add: sums_iff) 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

407 
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

408 
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

409 
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  410 
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

411 
also have "(\<Sum>k\<le>n. ln (real_of_nat (Suc k+1))  ln (of_nat (k+1))) = ln (of_nat (n+2))" 
64267  412 
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

413 
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

414 
by simp 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

415 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

416 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

417 
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

418 
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

419 

62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

420 
context 
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

421 
begin 
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

422 

5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

423 
private lemma ln_approx_aux: 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

424 
fixes n :: nat and x :: real 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

425 
defines "y \<equiv> (x1)/(x+1)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

426 
assumes x: "x > 0" "x \<noteq> 1" 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

427 
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

428 
{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

429 
proof  
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

430 
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

431 
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

432 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

433 
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

434 
note sums = ln_series_quadratic[OF x(1)] 
63040  435 
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

436 
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

437 
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

438 
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

439 
moreover { 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

440 
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

441 
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

442 
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

443 
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

444 
(\<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

445 
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

446 
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

447 
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

448 
} note sums' = this 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

449 
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

450 
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

451 
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

452 
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

453 
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

454 
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

455 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

456 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

457 
lemma 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

458 
fixes n :: nat and x :: real 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

459 
defines "y \<equiv> (x1)/(x+1)" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

460 
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

461 
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

462 
assumes x: "x > 1" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

463 
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

464 
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

465 
proof  
63040  466 
define c where "c = 2*y^(2*n+1)" 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

467 
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

468 
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

469 
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

470 
{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

471 
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

472 
hence "inverse c * (ln x  (\<Sum>k<n. 2*y^(2*k+1)/of_nat (2*k+1))) \<le> (1 / (1y^2) / of_nat (2*n+1))" 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

473 
by simp 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

474 
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

475 
by (auto simp add: divide_simps) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

476 
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

477 
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

478 
moreover { 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

479 
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

480 
by (intro mult_nonneg_nonneg[of c]) simp_all 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

481 
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

482 
by (simp add: mult_ac) 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

483 
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

484 
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

485 
} 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

486 
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

487 
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

488 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

489 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

490 
end 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

491 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

492 
lemma euler_mascheroni_bounds: 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

493 
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

494 
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

495 
using assms euler_mascheroni_upper[of "n1"] euler_mascheroni_lower[of "n1"] 
62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

496 
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

497 

b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

498 
lemma euler_mascheroni_bounds': 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

499 
fixes n :: nat assumes "n \<ge> 1" "ln (real_of_nat (Suc n)) \<in> {l<..<u}" 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

500 
shows "euler_mascheroni \<in> 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

501 
{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

502 
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

503 

62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

504 

5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

505 
text \<open> 
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

506 
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

507 
bound is accurate to about 0.0015. 
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

508 
\<close> 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

509 
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

510 
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

511 
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

512 

5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

513 

5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

514 
text \<open> 
63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset

515 
Approximation of the EulerMascheroni 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

516 
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

517 
\<close> 
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

518 
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

519 
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

520 
proof  
65109  521 
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

522 
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

523 
by (simp add: eval_nat_numeral) 
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

524 
finally have "ln (real (Suc 7)) \<in> \<dots>" . 
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

525 
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

526 
thus ?th1 ?th2 by blast+ 
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

527 
qed 
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff
changeset

528 

62085
5b7758af429e
Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
62065
diff
changeset

529 
end 