src/HOL/Analysis/Harmonic_Numbers.thy
 changeset 66495 0b46bd081228 parent 66447 a1f5c5c26fa6 child 66554 19bf4d5966dc
```     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Aug 23 00:38:53 2017 +0100
1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Aug 23 19:54:11 2017 +0100
1.3 @@ -38,7 +38,7 @@
1.4    unfolding harm_def by simp
1.5
1.6  lemma abs_harm [simp]: "(abs (harm n) :: real) = harm n"
1.7 -  using harm_nonneg[of n] by (rule abs_of_nonneg)
1.8 +  using harm_nonneg[of n] by (rule abs_of_nonneg)
1.9
1.10  lemma norm_harm: "norm (harm n) = harm n"
1.11    by (subst of_real_harm [symmetric]) (simp add: harm_nonneg)
1.12 @@ -99,12 +99,12 @@
1.13    show "eventually (\<lambda>n. harm n \<ge> ln (real (Suc n))) at_top"
1.15    show "filterlim (\<lambda>n. ln (real (Suc n))) at_top sequentially"
1.16 -    by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially]
1.17 +    by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially]
1.18                filterlim_Suc)
1.19  qed
1.20
1.21
1.22 -subsection \<open>The Euler--Mascheroni constant\<close>
1.23 +subsection \<open>The Euler-Mascheroni constant\<close>
1.24
1.25  text \<open>
1.26    The limit of the difference between the partial harmonic sum and the natural logarithm
1.27 @@ -250,7 +250,7 @@
1.28  qed
1.29
1.30
1.31 -subsection \<open>Bounds on the Euler--Mascheroni constant\<close>
1.32 +subsection \<open>Bounds on the Euler-Mascheroni constant\<close>
1.33
1.34  (* TODO: Move? *)
1.35  lemma ln_inverse_approx_le:
1.36 @@ -295,7 +295,7 @@
1.37      finally show "inverse t \<le> (t - x) * f' + inverse x" .
1.38    qed
1.39    hence "integral {x..x+a} inverse \<le> integral {x..x+a} ?f" using f'_nonpos assms
1.40 -    by (intro integral_le has_integral_integrable[OF int1] has_integral_integrable[OF int2] ineq)
1.41 +    by (blast intro: integral_le has_integral_integrable[OF int1] has_integral_integrable[OF int2] ineq)
1.42    also have "\<dots> = ?A" using int1 by (rule integral_unique)
1.43    finally show ?thesis .
1.44  qed
1.45 @@ -332,7 +332,7 @@
1.46      thus "(t - m) * f' + inverse m \<le> inverse t" by (simp add: algebra_simps)
1.47    qed
1.48    hence "integral {x..y} inverse \<ge> integral {x..y} (\<lambda>t. (t - m) * f' + inverse m)"
1.49 -    using int1 int2 by (intro integral_le has_integral_integrable)
1.50 +    using int1 int2 by (blast intro: integral_le has_integral_integrable)
1.51    also have "integral {x..y} (\<lambda>t. (t - m) * f' + inverse m) = ?A"
1.52      using integral_unique[OF int1] by simp
1.53    finally show ?thesis .
1.54 @@ -359,7 +359,7 @@
1.55    from euler_mascheroni_sum_real have "euler_mascheroni = (\<Sum>k. D k)"
1.56      by (simp add: sums_iff D_def)
1.57    also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)"
1.58 -    by (subst suminf_split_initial_segment[OF summable, of "Suc n"],
1.59 +    by (subst suminf_split_initial_segment[OF summable, of "Suc n"],
1.60          subst lessThan_Suc_atMost) simp
1.61    finally have sum: "(\<Sum>k\<le>n. D k) - euler_mascheroni = -(\<Sum>k. D (k + Suc n))" by simp
1.62
1.63 @@ -524,7 +524,7 @@
1.64
1.65
1.66  text \<open>
1.67 -  Approximation of the Euler--Mascheroni constant. The lower bound is accurate to about 0.0015;
1.68 +  Approximation of the Euler-Mascheroni constant. The lower bound is accurate to about 0.0015;
1.69    the upper bound is accurate to about 0.015.
1.70  \<close>
1.71  lemma euler_mascheroni_gt_19_over_33: "(euler_mascheroni :: real) > 19/33" (is ?th1)
```