70 by (simp add: harm_def) |
70 by (simp add: harm_def) |
71 |
71 |
72 lemma harm_nonneg: "harm n \<ge> (0 :: 'a :: {real_normed_field,linordered_field})" |
72 lemma harm_nonneg: "harm n \<ge> (0 :: 'a :: {real_normed_field,linordered_field})" |
73 unfolding harm_def by (intro setsum_nonneg) simp_all |
73 unfolding harm_def by (intro setsum_nonneg) simp_all |
74 |
74 |
|
75 lemma harm_pos: "n > 0 \<Longrightarrow> harm n > (0 :: 'a :: {real_normed_field,linordered_field})" |
|
76 unfolding harm_def by (intro setsum_pos) simp_all |
|
77 |
75 lemma of_real_harm: "of_real (harm n) = harm n" |
78 lemma of_real_harm: "of_real (harm n) = harm n" |
76 unfolding harm_def by simp |
79 unfolding harm_def by simp |
77 |
80 |
78 lemma norm_harm: "norm (harm n) = harm n" |
81 lemma norm_harm: "norm (harm n) = harm n" |
79 by (subst of_real_harm [symmetric]) (simp add: harm_nonneg) |
82 by (subst of_real_harm [symmetric]) (simp add: harm_nonneg) |
80 |
83 |
81 lemma harm_expand: |
84 lemma harm_expand: |
|
85 "harm 0 = 0" |
82 "harm (Suc 0) = 1" |
86 "harm (Suc 0) = 1" |
83 "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" |
87 "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" |
84 proof - |
88 proof - |
85 have "numeral n = Suc (pred_numeral n)" by simp |
89 have "numeral n = Suc (pred_numeral n)" by simp |
86 also have "harm \<dots> = harm (pred_numeral n) + inverse (numeral n)" |
90 also have "harm \<dots> = harm (pred_numeral n) + inverse (numeral n)" |
87 by (subst harm_Suc, subst numeral_eq_Suc[symmetric]) simp |
91 by (subst harm_Suc, subst numeral_eq_Suc[symmetric]) simp |
88 finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" . |
92 finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" . |
89 qed (simp add: harm_def) |
93 qed (simp_all add: harm_def) |
90 |
94 |
91 lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)" |
95 lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)" |
92 proof - |
96 proof - |
93 have "convergent (\<lambda>n. norm (harm n :: 'a)) \<longleftrightarrow> |
97 have "convergent (\<lambda>n. norm (harm n :: 'a)) \<longleftrightarrow> |
94 convergent (harm :: nat \<Rightarrow> real)" by (simp add: norm_harm) |
98 convergent (harm :: nat \<Rightarrow> real)" by (simp add: norm_harm) |
99 also have "... \<longleftrightarrow> summable (\<lambda>n. inverse (of_nat n) :: real)" |
103 also have "... \<longleftrightarrow> summable (\<lambda>n. inverse (of_nat n) :: real)" |
100 by (subst summable_Suc_iff [symmetric]) (simp add: summable_iff_convergent') |
104 by (subst summable_Suc_iff [symmetric]) (simp add: summable_iff_convergent') |
101 also have "\<not>..." by (rule not_summable_harmonic) |
105 also have "\<not>..." by (rule not_summable_harmonic) |
102 finally show ?thesis by (blast dest: convergent_norm) |
106 finally show ?thesis by (blast dest: convergent_norm) |
103 qed |
107 qed |
|
108 |
|
109 lemma harm_pos_iff [simp]: "harm n > (0 :: 'a :: {real_normed_field,linordered_field}) \<longleftrightarrow> n > 0" |
|
110 by (rule iffI, cases n, simp add: harm_expand, simp, rule harm_pos) |
|
111 |
|
112 lemma ln_diff_le_inverse: |
|
113 assumes "x \<ge> (1::real)" |
|
114 shows "ln (x + 1) - ln x < 1 / x" |
|
115 proof - |
|
116 from assms have "\<exists>z>x. z < x + 1 \<and> ln (x + 1) - ln x = (x + 1 - x) * inverse z" |
|
117 by (intro MVT2) (auto intro!: derivative_eq_intros simp: field_simps) |
|
118 then obtain z where z: "z > x" "z < x + 1" "ln (x + 1) - ln x = inverse z" by auto |
|
119 have "ln (x + 1) - ln x = inverse z" by fact |
|
120 also from z(1,2) assms have "\<dots> < 1 / x" by (simp add: field_simps) |
|
121 finally show ?thesis . |
|
122 qed |
|
123 |
|
124 lemma ln_le_harm: "ln (real n + 1) \<le> (harm n :: real)" |
|
125 proof (induction n) |
|
126 fix n assume IH: "ln (real n + 1) \<le> harm n" |
|
127 have "ln (real (Suc n) + 1) = ln (real n + 1) + (ln (real n + 2) - ln (real n + 1))" by simp |
|
128 also have "(ln (real n + 2) - ln (real n + 1)) \<le> 1 / real (Suc n)" |
|
129 using ln_diff_le_inverse[of "real n + 1"] by (simp add: add_ac) |
|
130 also note IH |
|
131 also have "harm n + 1 / real (Suc n) = harm (Suc n)" by (simp add: harm_Suc field_simps) |
|
132 finally show "ln (real (Suc n) + 1) \<le> harm (Suc n)" by - simp |
|
133 qed (simp_all add: harm_def) |
104 |
134 |
105 |
135 |
106 subsection \<open>The Euler–Mascheroni constant\<close> |
136 subsection \<open>The Euler–Mascheroni constant\<close> |
107 |
137 |
108 text \<open> |
138 text \<open> |