src/HOL/Series.thy
changeset 36409 d323e7773aa8
parent 36349 39be26d1bc28
child 36657 f376af79f6b7
equal deleted inserted replaced
36350:bc7982c54e37 36409:d323e7773aa8
   379 lemma summable_geometric:
   379 lemma summable_geometric:
   380   fixes x :: "'a::{real_normed_field}"
   380   fixes x :: "'a::{real_normed_field}"
   381   shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   381   shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   382 by (rule geometric_sums [THEN sums_summable])
   382 by (rule geometric_sums [THEN sums_summable])
   383 
   383 
   384 lemma half: "0 < 1 / (2::'a::{number_ring,division_ring_inverse_zero,linordered_field})"
   384 lemma half: "0 < 1 / (2::'a::{number_ring,linordered_field_inverse_zero})"
   385   by arith 
   385   by arith 
   386 
   386 
   387 lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
   387 lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
   388 proof -
   388 proof -
   389   have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
   389   have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]