equal
deleted
inserted
replaced
1685 have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)" |
1685 have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)" |
1686 using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto |
1686 using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto |
1687 |
1687 |
1688 have "norm x < 1" using assms by auto |
1688 have "norm x < 1" using assms by auto |
1689 have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric] |
1689 have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric] |
1690 using LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto |
1690 using tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto |
1691 { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) } |
1691 { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) } |
1692 { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric] |
1692 { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric] |
1693 proof (rule mult_mono) |
1693 proof (rule mult_mono) |
1694 show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) |
1694 show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) |
1695 have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric] |
1695 have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric] |