src/HOL/Analysis/Gamma_Function.thy
changeset 66936 cf8d8fc23891
parent 66526 322120e880c5
child 67278 c60e3d615b8c
     1.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -152,10 +152,10 @@
     1.4      fix z
     1.5      show "(\<Sum>n. of_real (sin_coeff (n+1)) * z^n)  = ?f z"
     1.6        by (cases "z = 0") (insert sin_z_over_z_series'[of z],
     1.7 -            simp_all add: scaleR_conv_of_real sums_iff powser_zero sin_coeff_def)
     1.8 +            simp_all add: scaleR_conv_of_real sums_iff sin_coeff_def)
     1.9    qed
    1.10    also have "(\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n + 1))) n * (0::'a) ^ n) =
    1.11 -                 diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by (simp add: powser_zero)
    1.12 +                 diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by simp
    1.13    also have "\<dots> = 0" by (simp add: sin_coeff_def diffs_def)
    1.14    finally show "((\<lambda>z::'a. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0)" .
    1.15  qed
    1.16 @@ -520,7 +520,7 @@
    1.17      unfolding pochhammer_prod
    1.18      by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
    1.19    also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
    1.20 -    unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
    1.21 +    unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def)
    1.22    finally show ?thesis .
    1.23  qed
    1.24  
    1.25 @@ -656,8 +656,7 @@
    1.26      also have "(\<Sum>n\<in>\<dots>. f n) = (\<Sum>n<k. f n) + (\<Sum>n=k..<m+k. f n)"
    1.27        by (rule sum.union_disjoint) auto
    1.28      also have "(\<Sum>n=k..<m+k. f n) = (\<Sum>n=0..<m+k-k. f (n + k))"
    1.29 -      by (intro sum.reindex_cong[of "\<lambda>n. n + k"])
    1.30 -         (simp, subst image_add_atLeastLessThan, auto)
    1.31 +      using sum_shift_bounds_nat_ivl [of f 0 k m] by simp
    1.32      finally show "(\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)) = (\<Sum>n<m+k. f n)" by (simp add: atLeast0LessThan)
    1.33    qed
    1.34    finally have "(\<lambda>a. sum f {..<a}) \<longlonglongrightarrow> lim (\<lambda>m. sum f {..<m + k})"
    1.35 @@ -2295,7 +2294,7 @@
    1.36      unfolding h_def using that by (auto intro!: Reals_mult Reals_add Reals_diff Polygamma_Real)
    1.37  
    1.38    from h'_zero h_h'_2 have "\<exists>c. \<forall>z\<in>UNIV. h z = c"
    1.39 -    by (intro has_field_derivative_zero_constant) (simp_all add: dist_0_norm)
    1.40 +    by (intro has_field_derivative_zero_constant) simp_all
    1.41    then obtain c where c: "\<And>z. h z = c" by auto
    1.42    have "\<exists>u. u \<in> closed_segment 0 1 \<and> Re (g 1) - Re (g 0) = Re (h u * g u * (1 - 0))"
    1.43      by (intro complex_mvt_line g_g')
    1.44 @@ -2861,7 +2860,7 @@
    1.45      have "((\<lambda>x. exp ((z - 1) * of_real (ln x)) * (1 - of_real x / of_nat n) ^ n)
    1.46              has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}" (is ?P)
    1.47        by (insert B, subst (asm) mult.assoc [symmetric], subst (asm) exp_add [symmetric])
    1.48 -         (simp add: Ln_of_nat algebra_simps)
    1.49 +         (simp add: algebra_simps)
    1.50      also have "?P \<longleftrightarrow> ((\<lambda>x. of_real x powr (z - 1) * (1 - of_real x / of_nat n) ^ n)
    1.51              has_integral (?I * exp ((z - 1) * ln (of_nat n)))) {0..real n}"
    1.52        by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real)