src/HOL/Transcendental.thy
 changeset 44568 e6f291cb5810 parent 44319 806e0390de53 child 44710 9caf6883f1f4
```     1.1 --- a/src/HOL/Transcendental.thy	Sat Aug 27 17:26:14 2011 +0200
1.2 +++ b/src/HOL/Transcendental.thy	Sun Aug 28 09:20:12 2011 -0700
1.3 @@ -294,7 +294,7 @@
1.4      hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n" by auto
1.5      { fix n have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n] by auto }
1.6      note monotone = this
1.7 -    note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF LIMSEQ_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
1.8 +    note leibniz = summable_Leibniz'[OF _ ge0, of "\<lambda>x. x", OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
1.9      have "summable (\<lambda> n. (-1)^n * ?a n)" using leibniz(1) by auto
1.10      then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l" unfolding summable_def by auto
1.11      from this[THEN sums_minus]
1.12 @@ -308,7 +308,7 @@
1.13
1.14      have ?pos using `0 \<le> ?a 0` by auto
1.15      moreover have ?neg using leibniz(2,4) unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le by auto
1.16 -    moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN LIMSEQ_minus_cancel] by auto
1.17 +    moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel] by auto
1.18      ultimately show ?thesis by auto
1.19    qed
1.20    from this[THEN conjunct1] this[THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct1] this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1]
1.21 @@ -2582,21 +2582,21 @@
1.22
1.23  lemma zeroseq_arctan_series: fixes x :: real
1.24    assumes "\<bar>x\<bar> \<le> 1" shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
1.25 -proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: LIMSEQ_const)
1.26 +proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: tendsto_const)
1.27  next
1.28    case False
1.29    have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
1.30    show "?a ----> 0"
1.31    proof (cases "\<bar>x\<bar> < 1")
1.32      case True hence "norm x < 1" by auto
1.33 -    from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
1.34 +    from tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
1.35      have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
1.36        unfolding inverse_eq_divide Suc_eq_plus1 by simp
1.37      then show ?thesis using pos2 by (rule LIMSEQ_linear)
1.38    next
1.39      case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
1.40      hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
1.41 -    from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
1.42 +    from tendsto_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] tendsto_const[of x]]
1.43      show ?thesis unfolding n_eq Suc_eq_plus1 by auto
1.44    qed
1.45  qed
1.46 @@ -2775,8 +2775,8 @@
1.47        hence "?diff 1 n \<le> ?a 1 n" by auto
1.48      }
1.49      have "?a 1 ----> 0"
1.50 -      unfolding LIMSEQ_rabs_zero power_one divide_inverse One_nat_def
1.51 -      by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
1.52 +      unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
1.53 +      by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
1.54      have "?diff 1 ----> 0"
1.55      proof (rule LIMSEQ_I)
1.56        fix r :: real assume "0 < r"
1.57 @@ -2785,7 +2785,7 @@
1.58          have "norm (?diff 1 n - 0) < r" by auto }
1.59        thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
1.60      qed
1.61 -    from this[unfolded LIMSEQ_rabs_zero diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
1.62 +    from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus]
1.63      have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
1.64      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
1.65
```