equal
deleted
inserted
replaced
369 hence "0 < real x" using `0 \<le> real x` by auto |
369 hence "0 < real x" using `0 \<le> real x` by auto |
370 hence prem: "0 < 1 / (0 * 2 + (1::nat)) * real x ^ (0 * 2 + 1)" by auto |
370 hence prem: "0 < 1 / (0 * 2 + (1::nat)) * real x ^ (0 * 2 + 1)" by auto |
371 |
371 |
372 have "\<bar> real x \<bar> \<le> 1" using `0 \<le> real x` `real x \<le> 1` by auto |
372 have "\<bar> real x \<bar> \<le> 1" using `0 \<le> real x` `real x \<le> 1` by auto |
373 from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded `2 * m = n`] |
373 from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded `2 * m = n`] |
374 show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_eq_plus1 . |
374 show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_eq_plus1 atLeast0LessThan . |
375 qed auto |
375 qed auto |
376 note arctan_bounds = this[unfolded atLeastAtMost_iff] |
376 note arctan_bounds = this[unfolded atLeastAtMost_iff] |
377 |
377 |
378 have F: "\<And>n. 2 * Suc n + 1 = 2 * n + 1 + 2" by auto |
378 have F: "\<And>n. 2 * Suc n + 1 = 2 * n + 1 + 2" by auto |
379 |
379 |
742 proof - |
742 proof - |
743 have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto |
743 have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto |
744 also have "\<dots> = |
744 also have "\<dots> = |
745 (\<Sum> j = 0 ..< n. -1 ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto |
745 (\<Sum> j = 0 ..< n. -1 ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto |
746 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then -1 ^ (i div 2) / (real (fact i)) * x ^ i else 0)" |
746 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then -1 ^ (i div 2) / (real (fact i)) * x ^ i else 0)" |
747 unfolding sum_split_even_odd .. |
747 unfolding sum_split_even_odd atLeast0LessThan .. |
748 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then -1 ^ (i div 2) / (real (fact i)) else 0) * x ^ i)" |
748 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then -1 ^ (i div 2) / (real (fact i)) else 0) * x ^ i)" |
749 by (rule setsum_cong2) auto |
749 by (rule setsum_cong2) auto |
750 finally show ?thesis by assumption |
750 finally show ?thesis by assumption |
751 qed } note morph_to_if_power = this |
751 qed } note morph_to_if_power = this |
752 |
752 |
756 obtain t where "0 < t" and "t < real x" and |
756 obtain t where "0 < t" and "t < real x" and |
757 cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i) |
757 cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i) |
758 + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)" |
758 + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)" |
759 (is "_ = ?SUM + ?rest / ?fact * ?pow") |
759 (is "_ = ?SUM + ?rest / ?fact * ?pow") |
760 using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`] |
760 using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`] |
761 unfolding cos_coeff_def by auto |
761 unfolding cos_coeff_def atLeast0LessThan by auto |
762 |
762 |
763 have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto |
763 have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto |
764 also have "\<dots> = cos (t + n * pi)" using cos_add by auto |
764 also have "\<dots> = cos (t + n * pi)" using cos_add by auto |
765 also have "\<dots> = ?rest" by auto |
765 also have "\<dots> = ?rest" by auto |
766 finally have "cos t * -1^n = ?rest" . |
766 finally have "cos t * -1^n = ?rest" . |
858 = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _") |
858 = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _") |
859 proof - |
859 proof - |
860 have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto |
860 have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto |
861 have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto |
861 have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto |
862 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)" |
862 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)" |
863 unfolding sum_split_even_odd .. |
863 unfolding sum_split_even_odd atLeast0LessThan .. |
864 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)" |
864 also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)" |
865 by (rule setsum_cong2) auto |
865 by (rule setsum_cong2) auto |
866 finally show ?thesis by assumption |
866 finally show ?thesis by assumption |
867 qed } note setsum_morph = this |
867 qed } note setsum_morph = this |
868 |
868 |
871 obtain t where "0 < t" and "t < real x" and |
871 obtain t where "0 < t" and "t < real x" and |
872 sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i) |
872 sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i) |
873 + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)" |
873 + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)" |
874 (is "_ = ?SUM + ?rest / ?fact * ?pow") |
874 (is "_ = ?SUM + ?rest / ?fact * ?pow") |
875 using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`] |
875 using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`] |
876 unfolding sin_coeff_def by auto |
876 unfolding sin_coeff_def atLeast0LessThan by auto |
877 |
877 |
878 have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto |
878 have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto |
879 moreover |
879 moreover |
880 have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto |
880 have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto |
881 hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto |
881 hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto |
1342 { have "lb_exp_horner prec (get_even n) 1 1 x \<le> (\<Sum>j = 0..<get_even n. 1 / real (fact j) * real x ^ j)" |
1342 { have "lb_exp_horner prec (get_even n) 1 1 x \<le> (\<Sum>j = 0..<get_even n. 1 / real (fact j) * real x ^ j)" |
1343 using bounds(1) by auto |
1343 using bounds(1) by auto |
1344 also have "\<dots> \<le> exp x" |
1344 also have "\<dots> \<le> exp x" |
1345 proof - |
1345 proof - |
1346 obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)" |
1346 obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)" |
1347 using Maclaurin_exp_le by blast |
1347 using Maclaurin_exp_le unfolding atLeast0LessThan by blast |
1348 moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)" |
1348 moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)" |
1349 by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: zero_le_even_power) |
1349 by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: zero_le_even_power) |
1350 ultimately show ?thesis |
1350 ultimately show ?thesis |
1351 using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg) |
1351 using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg) |
1352 qed |
1352 qed |
1362 case False hence "real x < 0" using `real x \<le> 0` by auto |
1362 case False hence "real x < 0" using `real x \<le> 0` by auto |
1363 show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq `real x < 0`) |
1363 show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq `real x < 0`) |
1364 qed |
1364 qed |
1365 |
1365 |
1366 obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / real (fact m)) + exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n)" |
1366 obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / real (fact m)) + exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n)" |
1367 using Maclaurin_exp_le by blast |
1367 using Maclaurin_exp_le unfolding atLeast0LessThan by blast |
1368 moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0" |
1368 moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0" |
1369 by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero) |
1369 by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero) |
1370 ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / real (fact j) * real x ^ j)" |
1370 ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / real (fact j) * real x ^ j)" |
1371 using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg) |
1371 using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg) |
1372 also have "\<dots> \<le> ub_exp_horner prec (get_odd n) 1 1 x" |
1372 also have "\<dots> \<le> ub_exp_horner prec (get_odd n) 1 1 x" |
1601 have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric] |
1601 have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric] |
1602 by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) |
1602 by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) |
1603 thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto |
1603 thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto |
1604 qed auto } |
1604 qed auto } |
1605 from summable_Leibniz'(2,4)[OF `?a ----> 0` `\<And>n. 0 \<le> ?a n`, OF `\<And>n. ?a (Suc n) \<le> ?a n`, unfolded ln_eq] |
1605 from summable_Leibniz'(2,4)[OF `?a ----> 0` `\<And>n. 0 \<le> ?a n`, OF `\<And>n. ?a (Suc n) \<le> ?a n`, unfolded ln_eq] |
1606 show "?lb" and "?ub" by auto |
1606 show "?lb" and "?ub" unfolding atLeast0LessThan by auto |
1607 qed |
1607 qed |
1608 |
1608 |
1609 lemma ln_float_bounds: |
1609 lemma ln_float_bounds: |
1610 assumes "0 \<le> real x" and "real x < 1" |
1610 assumes "0 \<le> real x" and "real x < 1" |
1611 shows "x * lb_ln_horner prec (get_even n) 1 x \<le> ln (x + 1)" (is "?lb \<le> ?ln") |
1611 shows "x * lb_ln_horner prec (get_even n) 1 x \<le> ln (x + 1)" (is "?lb \<le> ?ln") |
3029 from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False] |
3029 from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False] |
3030 obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x" |
3030 obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x" |
3031 and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) = |
3031 and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) = |
3032 (\<Sum>m = 0..<Suc n'. F m c / real (fact m) * (xs ! x - c) ^ m) + |
3032 (\<Sum>m = 0..<Suc n'. F m c / real (fact m) * (xs ! x - c) ^ m) + |
3033 F (Suc n') t / real (fact (Suc n')) * (xs ! x - c) ^ Suc n'" |
3033 F (Suc n') t / real (fact (Suc n')) * (xs ! x - c) ^ Suc n'" |
3034 by blast |
3034 unfolding atLeast0LessThan by blast |
3035 |
3035 |
3036 from t_bnd bnd_xs bnd_c have *: "t \<in> {lx .. ux}" |
3036 from t_bnd bnd_xs bnd_c have *: "t \<in> {lx .. ux}" |
3037 by (cases "xs ! x < c", auto) |
3037 by (cases "xs ! x < c", auto) |
3038 |
3038 |
3039 have "interpret_floatarith f (xs[x := xs ! x]) = ?taylor t" |
3039 have "interpret_floatarith f (xs[x := xs ! x]) = ?taylor t" |