src/HOL/Analysis/Harmonic_Numbers.thy
author paulson <lp15@cam.ac.uk>
Thu, 16 Mar 2017 13:55:29 +0000
changeset 65273 917ae0ba03a2
parent 65109 a79c1080f1e9
child 65395 7504569a73c7
permissions -rw-r--r--
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63627
6ddb43c6b711 rename HOL-Multivariate_Analysis to HOL-Analysis.
hoelzl
parents: 63594
diff changeset
     1
(*  Title:    HOL/Analysis/Harmonic_Numbers.thy
62055
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     2
    Author:   Manuel Eberl, TU München
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
     3
*)
62055
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     4
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     5
section \<open>Harmonic Numbers\<close>
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
     6
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
     7
theory Harmonic_Numbers
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
     8
imports
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
     9
  Complex_Transcendental
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
    10
  Summation_Tests
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    11
  Integral_Test
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    12
begin
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    13
62055
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
    14
text \<open>
62174
fae6233c5f37 eliminated spurious Unicode;
wenzelm
parents: 62085
diff changeset
    15
  The definition of the Harmonic Numbers and the Euler-Mascheroni constant.
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
    16
  Also provides a reasonably accurate approximation of @{term "ln 2 :: real"}
62174
fae6233c5f37 eliminated spurious Unicode;
wenzelm
parents: 62085
diff changeset
    17
  and the Euler-Mascheroni constant.
62055
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
    18
\<close>
755fda743c49 Multivariate-Analysis: fixed headers and a LaTex error (c.f. Isabelle b0f941e207cf)
hoelzl
parents: 62049
diff changeset
    19
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    20
subsection \<open>The Harmonic numbers\<close>
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    21
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    22
definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    23
  "harm n = (\<Sum>k=1..n. inverse (of_nat k))"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    24
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    25
lemma harm_altdef: "harm n = (\<Sum>k<n. inverse (of_nat (Suc k)))"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    26
  unfolding harm_def by (induction n) simp_all
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    27
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    28
lemma harm_Suc: "harm (Suc n) = harm n + inverse (of_nat (Suc n))"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    29
  by (simp add: harm_def)
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    30
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    31
lemma harm_nonneg: "harm n \<ge> (0 :: 'a :: {real_normed_field,linordered_field})"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
    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
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    34
lemma harm_pos: "n > 0 \<Longrightarrow> harm n > (0 :: 'a :: {real_normed_field,linordered_field})"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
    35
  unfolding harm_def by (intro sum_pos) simp_all
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    36
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    37
lemma of_real_harm: "of_real (harm n) = harm n"
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
    38
  unfolding harm_def by simp
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
    39
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 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
    43
lemma harm_expand:
62065
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    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
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    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
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
    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
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    68
lemma harm_pos_iff [simp]: "harm n > (0 :: 'a :: {real_normed_field,linordered_field}) \<longleftrightarrow> n > 0"
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    69
  by (rule iffI, cases n, simp add: harm_expand, simp, rule harm_pos)
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    70
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    71
lemma ln_diff_le_inverse:
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    72
  assumes "x \<ge> (1::real)"
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    73
  shows   "ln (x + 1) - ln x < 1 / x"
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    74
proof -
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    75
  from assms have "\<exists>z>x. z < x + 1 \<and> ln (x + 1) - ln x = (x + 1 - x) * inverse z"
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    76
    by (intro MVT2) (auto intro!: derivative_eq_intros simp: field_simps)
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    77
  then obtain z where z: "z > x" "z < x + 1" "ln (x + 1) - ln x = inverse z" by auto
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    78
  have "ln (x + 1) - ln x = inverse z" by fact
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    79
  also from z(1,2) assms have "\<dots> < 1 / x" by (simp add: field_simps)
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    80
  finally show ?thesis .
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    81
qed
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    82
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    83
lemma ln_le_harm: "ln (real n + 1) \<le> (harm n :: real)"
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    84
proof (induction n)
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    85
  fix n assume IH: "ln (real n + 1) \<le> harm n"
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    86
  have "ln (real (Suc n) + 1) = ln (real n + 1) + (ln (real n + 2) - ln (real n + 1))" by simp
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    87
  also have "(ln (real n + 2) - ln (real n + 1)) \<le> 1 / real (Suc n)"
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    88
    using ln_diff_le_inverse[of "real n + 1"] by (simp add: add_ac)
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    89
  also note IH
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    90
  also have "harm n + 1 / real (Suc n) = harm (Suc n)" by (simp add: harm_Suc field_simps)
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    91
  finally show "ln (real (Suc n) + 1) \<le> harm (Suc n)" by - simp
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    92
qed (simp_all add: harm_def)
1546a042e87b Added some facts about polynomials
eberlm
parents: 62055
diff changeset
    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 Euler--Mascheroni 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
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   152
lemma euler_mascheroni_LIMSEQ_of_real:
bd218a9320b5 HOL-Multivariate_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
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   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 HOL-Multivariate_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
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   168
lemma euler_mascheroni_sum:
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   169
  "(\<lambda>n. inverse (of_nat (n+1)) + of_real (ln (of_nat (n+1))) - of_real (ln (of_nat (n+2))))
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   170
       sums (euler_mascheroni :: 'a :: {banach, real_normed_field})"
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   171
proof -
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   172
  have "(\<lambda>n. of_real (inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))))
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   173
       sums (of_real euler_mascheroni :: 'a :: {banach, real_normed_field})"
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   174
    by (subst sums_of_real_iff) (rule euler_mascheroni_sum_real)
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   175
  thus ?thesis by simp
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   176
qed
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   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
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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>k|k<2*n \<and> odd k. ?g k / of_nat (Suc k))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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>k|k<2*n \<and> odd k. 2 / (real_of_nat (Suc k)))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   195
      by (intro sum.cong) auto
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   196
    also have "(\<Sum>k|k<2*n \<and> odd k. 2 / (real_of_nat (Suc k))) = harm n"
62049
b0f941e207cf Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
diff changeset
   197
      unfolding harm_altdef
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_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 Euler--Mascheroni 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
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_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
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   295
  define m where "m = (x+y)/2"
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   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 HOL-Multivariate_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 HOL-Multivariate_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
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   335
  define D :: "_ \<Rightarrow> real"
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   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
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   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
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   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
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   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
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   350
    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], 
492bb53c3420 More analysis lemmas
Manuel Eberl <eberlm@in.tum.de>
parents: 63627
diff changeset
   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
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   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 HOL-Multivariate_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 HOL-Multivariate_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
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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 HOL-Multivariate_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
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_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
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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
b9a1486e79be setsum -> sum
nipkow
parents: 63721
diff changeset
   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> (x-1)/(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 HOL-Multivariate_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
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   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> (x-1)/(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
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62174
diff changeset
   466
  define c where "c = 2*y^(2*n+1)"
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   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 / (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
   473
    by simp
63594
bd218a9320b5 HOL-Multivariate_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 HOL-Multivariate_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 "n-1"] euler_mascheroni_lower[of "n-1"]
62085
5b7758af429e Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 62065
diff changeset
   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 HOL-Multivariate_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 HOL-Multivariate_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 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   515
  Approximation of the Euler--Mascheroni constant. The lower bound is accurate to about 0.0015;
62085
5b7758af429e Tuned approximations in Multivariate_Analysis
Manuel Eberl <eberlm@in.tum.de>
parents: 62065
diff changeset
   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
a79c1080f1e9 added numeral_powr_numeral
nipkow
parents: 64267
diff changeset
   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