src/HOL/Series.thy
changeset 36096 abc6a2ea4b88
parent 35028 108662d50512
child 36349 39be26d1bc28
equal deleted inserted replaced
36095:059c3568fdc8 36096:abc6a2ea4b88
   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_by_zero,ordered_field})"
   384 lemma half: "0 < 1 / (2::'a::{number_ring,division_by_zero,linordered_field})"
   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"]