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.14      using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac)
    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)