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