equal
deleted
inserted
replaced
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"] |