src/HOL/Series.thy
 changeset 36409 d323e7773aa8 parent 36349 39be26d1bc28 child 36657 f376af79f6b7
equal 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"]`