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