348 also have "\<dots> = ereal (\<Sum> i\<in>{1..n}. (2 powr -real i) * (real ?a))" by simp |
348 also have "\<dots> = ereal (\<Sum> i\<in>{1..n}. (2 powr -real i) * (real ?a))" by simp |
349 also have "\<dots> = ereal ((\<Sum> i\<in>{1..n}. (2 powr -real i)) * real ?a)" |
349 also have "\<dots> = ereal ((\<Sum> i\<in>{1..n}. (2 powr -real i)) * real ?a)" |
350 by (simp add: setsum_left_distrib) |
350 by (simp add: setsum_left_distrib) |
351 also have "\<dots> < ereal (1 * real ?a)" unfolding less_ereal.simps |
351 also have "\<dots> < ereal (1 * real ?a)" unfolding less_ereal.simps |
352 proof (rule mult_strict_right_mono) |
352 proof (rule mult_strict_right_mono) |
353 have "(\<Sum>i\<in>{1..n}. 2 powr - real i) = (\<Sum>i\<in>{1..<Suc n}. (1/2) ^ i)" |
353 have "(\<Sum>i = 1..n. 2 powr - real i) = (\<Sum>i = 1..<Suc n. (1/2) ^ i)" |
354 by (rule setsum.cong) |
354 by (rule setsum.cong) (auto simp: powr_realpow powr_divide powr_minus_divide) |
355 (auto simp: powr_realpow[symmetric] powr_minus powr_divide inverse_eq_divide) |
|
356 also have "{1..<Suc n} = {..<Suc n} - {0}" by auto |
355 also have "{1..<Suc n} = {..<Suc n} - {0}" by auto |
357 also have "setsum (op ^ (1 / 2::real)) ({..<Suc n} - {0}) = |
356 also have "setsum (op ^ (1 / 2::real)) ({..<Suc n} - {0}) = |
358 setsum (op ^ (1 / 2)) ({..<Suc n}) - 1" by (auto simp: setsum_diff1) |
357 setsum (op ^ (1 / 2)) ({..<Suc n}) - 1" by (auto simp: setsum_diff1) |
359 also have "\<dots> < 1" by (subst geometric_sum) auto |
358 also have "\<dots> < 1" by (subst geometric_sum) auto |
360 finally show "(\<Sum>i = 1..n. 2 powr - real i) < 1" . |
359 finally show "(\<Sum>i = 1..n. 2 powr - real i) < 1" . |