1272 hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)" |
1272 hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)" |
1273 unfolding power_add by (simp add: mult_ac del: fact_Suc) } |
1273 unfolding power_add by (simp add: mult_ac del: fact_Suc) } |
1274 note aux1 = this |
1274 note aux1 = this |
1275 have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))" |
1275 have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))" |
1276 by (intro sums_mult geometric_sums, simp) |
1276 by (intro sums_mult geometric_sums, simp) |
1277 hence aux2: "(\<lambda>n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2" |
1277 hence aux2: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2" |
1278 by simp |
1278 by simp |
1279 have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2" |
1279 have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x\<^sup>2" |
1280 proof - |
1280 proof - |
1281 have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= |
1281 have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= |
1282 suminf (%n. (x^2/2) * ((1/2)^n))" |
1282 suminf (%n. (x\<^sup>2/2) * ((1/2)^n))" |
1283 apply (rule summable_le) |
1283 apply (rule summable_le) |
1284 apply (rule allI, rule aux1) |
1284 apply (rule allI, rule aux1) |
1285 apply (rule summable_exp [THEN summable_ignore_initial_segment]) |
1285 apply (rule summable_exp [THEN summable_ignore_initial_segment]) |
1286 by (rule sums_summable, rule aux2) |
1286 by (rule sums_summable, rule aux2) |
1287 also have "... = x^2" |
1287 also have "... = x\<^sup>2" |
1288 by (rule sums_unique [THEN sym], rule aux2) |
1288 by (rule sums_unique [THEN sym], rule aux2) |
1289 finally show ?thesis . |
1289 finally show ?thesis . |
1290 qed |
1290 qed |
1291 thus ?thesis unfolding exp_first_two_terms by auto |
1291 thus ?thesis unfolding exp_first_two_terms by auto |
1292 qed |
1292 qed |
1293 |
1293 |
1294 lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x" |
1294 lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x" |
1295 proof - |
1295 proof - |
1296 assume a: "0 <= (x::real)" and b: "x < 1" |
1296 assume a: "0 <= (x::real)" and b: "x < 1" |
1297 have "(1 - x) * (1 + x + x^2) = (1 - x^3)" |
1297 have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)" |
1298 by (simp add: algebra_simps power2_eq_square power3_eq_cube) |
1298 by (simp add: algebra_simps power2_eq_square power3_eq_cube) |
1299 also have "... <= 1" |
1299 also have "... <= 1" |
1300 by (auto simp add: a) |
1300 by (auto simp add: a) |
1301 finally have "(1 - x) * (1 + x + x ^ 2) <= 1" . |
1301 finally have "(1 - x) * (1 + x + x\<^sup>2) <= 1" . |
1302 moreover have c: "0 < 1 + x + x\<^sup>2" |
1302 moreover have c: "0 < 1 + x + x\<^sup>2" |
1303 by (simp add: add_pos_nonneg a) |
1303 by (simp add: add_pos_nonneg a) |
1304 ultimately have "1 - x <= 1 / (1 + x + x^2)" |
1304 ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)" |
1305 by (elim mult_imp_le_div_pos) |
1305 by (elim mult_imp_le_div_pos) |
1306 also have "... <= 1 / exp x" |
1306 also have "... <= 1 / exp x" |
1307 apply (rule divide_left_mono) |
1307 apply (rule divide_left_mono) |
1308 apply (rule exp_bound, rule a) |
1308 apply (rule exp_bound, rule a) |
1309 apply (rule b [THEN less_imp_le]) |
1309 apply (rule b [THEN less_imp_le]) |
1341 apply simp |
1341 apply simp |
1342 apply (rule ln_one_minus_pos_upper_bound) |
1342 apply (rule ln_one_minus_pos_upper_bound) |
1343 apply auto |
1343 apply auto |
1344 done |
1344 done |
1345 |
1345 |
1346 lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> x - x^2 <= ln (1 + x)" |
1346 lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> x - x\<^sup>2 <= ln (1 + x)" |
1347 proof - |
1347 proof - |
1348 assume a: "0 <= x" and b: "x <= 1" |
1348 assume a: "0 <= x" and b: "x <= 1" |
1349 have "exp (x - x^2) = exp x / exp (x^2)" |
1349 have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)" |
1350 by (rule exp_diff) |
1350 by (rule exp_diff) |
1351 also have "... <= (1 + x + x^2) / exp (x ^2)" |
1351 also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)" |
1352 apply (rule divide_right_mono) |
1352 apply (rule divide_right_mono) |
1353 apply (rule exp_bound) |
1353 apply (rule exp_bound) |
1354 apply (rule a, rule b) |
1354 apply (rule a, rule b) |
1355 apply simp |
1355 apply simp |
1356 done |
1356 done |
1357 also have "... <= (1 + x + x^2) / (1 + x^2)" |
1357 also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)" |
1358 apply (rule divide_left_mono) |
1358 apply (rule divide_left_mono) |
1359 apply (simp add: exp_ge_add_one_self_aux) |
1359 apply (simp add: exp_ge_add_one_self_aux) |
1360 apply (simp add: a) |
1360 apply (simp add: a) |
1361 apply (simp add: mult_pos_pos add_pos_nonneg) |
1361 apply (simp add: mult_pos_pos add_pos_nonneg) |
1362 done |
1362 done |
1363 also from a have "... <= 1 + x" |
1363 also from a have "... <= 1 + x" |
1364 by (simp add: field_simps add_strict_increasing zero_le_mult_iff) |
1364 by (simp add: field_simps add_strict_increasing zero_le_mult_iff) |
1365 finally have "exp (x - x^2) <= 1 + x" . |
1365 finally have "exp (x - x\<^sup>2) <= 1 + x" . |
1366 also have "... = exp (ln (1 + x))" |
1366 also have "... = exp (ln (1 + x))" |
1367 proof - |
1367 proof - |
1368 from a have "0 < 1 + x" by auto |
1368 from a have "0 < 1 + x" by auto |
1369 thus ?thesis |
1369 thus ?thesis |
1370 by (auto simp only: exp_ln_iff [THEN sym]) |
1370 by (auto simp only: exp_ln_iff [THEN sym]) |
1371 qed |
1371 qed |
1372 finally have "exp (x - x ^ 2) <= exp (ln (1 + x))" . |
1372 finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" . |
1373 thus ?thesis by (auto simp only: exp_le_cancel_iff) |
1373 thus ?thesis by (auto simp only: exp_le_cancel_iff) |
1374 qed |
1374 qed |
1375 |
1375 |
1376 lemma aux5: "x < 1 ==> ln(1 - x) = - ln(1 + x / (1 - x))" |
1376 lemma aux5: "x < 1 ==> ln(1 - x) = - ln(1 + x / (1 - x))" |
1377 proof - |
1377 proof - |
1390 also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps) |
1390 also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps) |
1391 finally show ?thesis . |
1391 finally show ?thesis . |
1392 qed |
1392 qed |
1393 |
1393 |
1394 lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==> |
1394 lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==> |
1395 - x - 2 * x^2 <= ln (1 - x)" |
1395 - x - 2 * x\<^sup>2 <= ln (1 - x)" |
1396 proof - |
1396 proof - |
1397 assume a: "0 <= x" and b: "x <= (1 / 2)" |
1397 assume a: "0 <= x" and b: "x <= (1 / 2)" |
1398 from b have c: "x < 1" |
1398 from b have c: "x < 1" |
1399 by auto |
1399 by auto |
1400 then have "ln (1 - x) = - ln (1 + x / (1 - x))" |
1400 then have "ln (1 - x) = - ln (1 + x / (1 - x))" |
1410 qed |
1410 qed |
1411 also have "- (x / (1 - x)) = -x / (1 - x)" |
1411 also have "- (x / (1 - x)) = -x / (1 - x)" |
1412 by auto |
1412 by auto |
1413 finally have d: "- x / (1 - x) <= ln (1 - x)" . |
1413 finally have d: "- x / (1 - x) <= ln (1 - x)" . |
1414 have "0 < 1 - x" using a b by simp |
1414 have "0 < 1 - x" using a b by simp |
1415 hence e: "-x - 2 * x^2 <= - x / (1 - x)" |
1415 hence e: "-x - 2 * x\<^sup>2 <= - x / (1 - x)" |
1416 using mult_right_le_one_le[of "x*x" "2*x"] a b |
1416 using mult_right_le_one_le[of "x*x" "2*x"] a b |
1417 by (simp add:field_simps power2_eq_square) |
1417 by (simp add:field_simps power2_eq_square) |
1418 from e d show "- x - 2 * x^2 <= ln (1 - x)" |
1418 from e d show "- x - 2 * x\<^sup>2 <= ln (1 - x)" |
1419 by (rule order_trans) |
1419 by (rule order_trans) |
1420 qed |
1420 qed |
1421 |
1421 |
1422 lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x" |
1422 lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x" |
1423 apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp) |
1423 apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp) |
1424 apply (subst ln_le_cancel_iff) |
1424 apply (subst ln_le_cancel_iff) |
1425 apply auto |
1425 apply auto |
1426 done |
1426 done |
1427 |
1427 |
1428 lemma abs_ln_one_plus_x_minus_x_bound_nonneg: |
1428 lemma abs_ln_one_plus_x_minus_x_bound_nonneg: |
1429 "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2" |
1429 "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x\<^sup>2" |
1430 proof - |
1430 proof - |
1431 assume x: "0 <= x" |
1431 assume x: "0 <= x" |
1432 assume x1: "x <= 1" |
1432 assume x1: "x <= 1" |
1433 from x have "ln (1 + x) <= x" |
1433 from x have "ln (1 + x) <= x" |
1434 by (rule ln_add_one_self_le_self) |
1434 by (rule ln_add_one_self_le_self) |
1436 by simp |
1436 by simp |
1437 then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)" |
1437 then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)" |
1438 by (rule abs_of_nonpos) |
1438 by (rule abs_of_nonpos) |
1439 also have "... = x - ln (1 + x)" |
1439 also have "... = x - ln (1 + x)" |
1440 by simp |
1440 by simp |
1441 also have "... <= x^2" |
1441 also have "... <= x\<^sup>2" |
1442 proof - |
1442 proof - |
1443 from x x1 have "x - x^2 <= ln (1 + x)" |
1443 from x x1 have "x - x\<^sup>2 <= ln (1 + x)" |
1444 by (intro ln_one_plus_pos_lower_bound) |
1444 by (intro ln_one_plus_pos_lower_bound) |
1445 thus ?thesis |
1445 thus ?thesis |
1446 by simp |
1446 by simp |
1447 qed |
1447 qed |
1448 finally show ?thesis . |
1448 finally show ?thesis . |
1449 qed |
1449 qed |
1450 |
1450 |
1451 lemma abs_ln_one_plus_x_minus_x_bound_nonpos: |
1451 lemma abs_ln_one_plus_x_minus_x_bound_nonpos: |
1452 "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2" |
1452 "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x\<^sup>2" |
1453 proof - |
1453 proof - |
1454 assume a: "-(1 / 2) <= x" |
1454 assume a: "-(1 / 2) <= x" |
1455 assume b: "x <= 0" |
1455 assume b: "x <= 0" |
1456 have "abs(ln (1 + x) - x) = x - ln(1 - (-x))" |
1456 have "abs(ln (1 + x) - x) = x - ln(1 - (-x))" |
1457 apply (subst abs_of_nonpos) |
1457 apply (subst abs_of_nonpos) |
1458 apply simp |
1458 apply simp |
1459 apply (rule ln_add_one_self_le_self2) |
1459 apply (rule ln_add_one_self_le_self2) |
1460 using a apply auto |
1460 using a apply auto |
1461 done |
1461 done |
1462 also have "... <= 2 * x^2" |
1462 also have "... <= 2 * x\<^sup>2" |
1463 apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))") |
1463 apply (subgoal_tac "- (-x) - 2 * (-x)\<^sup>2 <= ln (1 - (-x))") |
1464 apply (simp add: algebra_simps) |
1464 apply (simp add: algebra_simps) |
1465 apply (rule ln_one_minus_pos_lower_bound) |
1465 apply (rule ln_one_minus_pos_lower_bound) |
1466 using a b apply auto |
1466 using a b apply auto |
1467 done |
1467 done |
1468 finally show ?thesis . |
1468 finally show ?thesis . |
1469 qed |
1469 qed |
1470 |
1470 |
1471 lemma abs_ln_one_plus_x_minus_x_bound: |
1471 lemma abs_ln_one_plus_x_minus_x_bound: |
1472 "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x^2" |
1472 "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x\<^sup>2" |
1473 apply (case_tac "0 <= x") |
1473 apply (case_tac "0 <= x") |
1474 apply (rule order_trans) |
1474 apply (rule order_trans) |
1475 apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) |
1475 apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) |
1476 apply auto |
1476 apply auto |
1477 apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos) |
1477 apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos) |
2188 lemma DERIV_fun_cos: |
2188 lemma DERIV_fun_cos: |
2189 "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m" |
2189 "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m" |
2190 by (auto intro!: DERIV_intros) |
2190 by (auto intro!: DERIV_intros) |
2191 |
2191 |
2192 lemma sin_cos_add_lemma: |
2192 lemma sin_cos_add_lemma: |
2193 "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 + |
2193 "(sin (x + y) - (sin x * cos y + cos x * sin y))\<^sup>2 + |
2194 (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = 0" |
2194 (cos (x + y) - (cos x * cos y - sin x * sin y))\<^sup>2 = 0" |
2195 (is "?f x = 0") |
2195 (is "?f x = 0") |
2196 proof - |
2196 proof - |
2197 have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0" |
2197 have "\<forall>x. DERIV (\<lambda>x. ?f x) x :> 0" |
2198 by (auto intro!: DERIV_intros simp add: algebra_simps) |
2198 by (auto intro!: DERIV_intros simp add: algebra_simps) |
2199 hence "?f x = ?f 0" |
2199 hence "?f x = ?f 0" |
2713 ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))" |
2713 ==> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))" |
2714 by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def) |
2714 by (simp add: add_tan_eq lemma_tan_add1, simp add: tan_def) |
2715 |
2715 |
2716 lemma tan_double: |
2716 lemma tan_double: |
2717 "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |] |
2717 "[| cos x \<noteq> 0; cos (2 * x) \<noteq> 0 |] |
2718 ==> tan (2 * x) = (2 * tan x)/(1 - (tan(x) ^ 2))" |
2718 ==> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)" |
2719 using tan_add [of x x] by (simp add: power2_eq_square) |
2719 using tan_add [of x x] by (simp add: power2_eq_square) |
2720 |
2720 |
2721 lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x" |
2721 lemma tan_gt_zero: "[| 0 < x; x < pi/2 |] ==> 0 < tan x" |
2722 by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi) |
2722 by (simp add: tan_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi) |
2723 |
2723 |
2816 done |
2816 done |
2817 |
2817 |
2818 lemma tan_monotone: assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2" |
2818 lemma tan_monotone: assumes "- (pi / 2) < y" and "y < x" and "x < pi / 2" |
2819 shows "tan y < tan x" |
2819 shows "tan y < tan x" |
2820 proof - |
2820 proof - |
2821 have "\<forall> x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse (cos x'^2)" |
2821 have "\<forall> x'. y \<le> x' \<and> x' \<le> x \<longrightarrow> DERIV tan x' :> inverse ((cos x')\<^sup>2)" |
2822 proof (rule allI, rule impI) |
2822 proof (rule allI, rule impI) |
2823 fix x' :: real assume "y \<le> x' \<and> x' \<le> x" |
2823 fix x' :: real assume "y \<le> x' \<and> x' \<le> x" |
2824 hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto |
2824 hence "-(pi/2) < x'" and "x' < pi/2" using assms by auto |
2825 from cos_gt_zero_pi[OF this] |
2825 from cos_gt_zero_pi[OF this] |
2826 have "cos x' \<noteq> 0" by auto |
2826 have "cos x' \<noteq> 0" by auto |
2827 thus "DERIV tan x' :> inverse (cos x'^2)" by (rule DERIV_tan) |
2827 thus "DERIV tan x' :> inverse ((cos x')\<^sup>2)" by (rule DERIV_tan) |
2828 qed |
2828 qed |
2829 from MVT2[OF `y < x` this] |
2829 from MVT2[OF `y < x` this] |
2830 obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto |
2830 obtain z where "y < z" and "z < x" and tan_diff: "tan x - tan y = (x - y) * inverse ((cos z)\<^sup>2)" by auto |
2831 hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto |
2831 hence "- (pi / 2) < z" and "z < pi / 2" using assms by auto |
2832 hence "0 < cos z" using cos_gt_zero_pi by auto |
2832 hence "0 < cos z" using cos_gt_zero_pi by auto |
3056 lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)" |
3056 lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<^sup>2)" |
3057 using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]] |
3057 using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]] |
3058 using tan_arctan [of x] unfolding tan_def cos_arctan |
3058 using tan_arctan [of x] unfolding tan_def cos_arctan |
3059 by (simp add: eq_divide_eq) |
3059 by (simp add: eq_divide_eq) |
3060 |
3060 |
3061 lemma tan_sec: "cos x \<noteq> 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2" |
3061 lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2" |
3062 apply (rule power_inverse [THEN subst]) |
3062 apply (rule power_inverse [THEN subst]) |
3063 apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1]) |
3063 apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1]) |
3064 apply (auto dest: field_power_not_zero |
3064 apply (auto dest: field_power_not_zero |
3065 simp add: power_mult_distrib distrib_right power_divide tan_def |
3065 simp add: power_mult_distrib distrib_right power_divide tan_def |
3066 mult_assoc power_inverse [symmetric]) |
3066 mult_assoc power_inverse [symmetric]) |
3425 |
3425 |
3426 lemma summable_arctan_series: fixes x :: real and n :: nat |
3426 lemma summable_arctan_series: fixes x :: real and n :: nat |
3427 assumes "\<bar>x\<bar> \<le> 1" shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))" (is "summable (?c x)") |
3427 assumes "\<bar>x\<bar> \<le> 1" shows "summable (\<lambda> k. (-1)^k * (1 / real (k*2+1) * x ^ (k*2+1)))" (is "summable (?c x)") |
3428 by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms]) |
3428 by (rule summable_Leibniz(1), rule zeroseq_arctan_series[OF assms], rule monoseq_arctan_series[OF assms]) |
3429 |
3429 |
3430 lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x^2 < 1" |
3430 lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x\<^sup>2 < 1" |
3431 proof - |
3431 proof - |
3432 from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]] |
3432 from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]] |
3433 have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto |
3433 have "\<bar>x\<^sup>2\<bar> < 1" using `\<bar>x\<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto |
3434 thus ?thesis using zero_le_power2 by auto |
3434 thus ?thesis using zero_le_power2 by auto |
3435 qed |
3435 qed |
3436 |
3436 |
3437 lemma DERIV_arctan_series: assumes "\<bar> x \<bar> < 1" |
3437 lemma DERIV_arctan_series: assumes "\<bar> x \<bar> < 1" |
3438 shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))" (is "DERIV ?arctan _ :> ?Int") |
3438 shows "DERIV (\<lambda> x'. \<Sum> k. (-1)^k * (1 / real (k*2+1) * x' ^ (k*2+1))) x :> (\<Sum> k. (-1)^k * x^(k*2))" (is "DERIV ?arctan _ :> ?Int") |
3440 let "?f n" = "if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0" |
3440 let "?f n" = "if even n then (-1)^(n div 2) * 1 / real (Suc n) else 0" |
3441 |
3441 |
3442 { fix n :: nat assume "even n" hence "2 * (n div 2) = n" by presburger } note n_even=this |
3442 { fix n :: nat assume "even n" hence "2 * (n div 2) = n" by presburger } note n_even=this |
3443 have if_eq: "\<And> n x'. ?f n * real (Suc n) * x'^n = (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)" using n_even by auto |
3443 have if_eq: "\<And> n x'. ?f n * real (Suc n) * x'^n = (if even n then (-1)^(n div 2) * x'^(2 * (n div 2)) else 0)" using n_even by auto |
3444 |
3444 |
3445 { fix x :: real assume "\<bar>x\<bar> < 1" hence "x^2 < 1" by (rule less_one_imp_sqr_less_one) |
3445 { fix x :: real assume "\<bar>x\<bar> < 1" hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one) |
3446 have "summable (\<lambda> n. -1 ^ n * (x^2) ^n)" |
3446 have "summable (\<lambda> n. -1 ^ n * (x\<^sup>2) ^n)" |
3447 by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x^2 < 1` order_less_imp_le[OF `x^2 < 1`]) |
3447 by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`]) |
3448 hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult . |
3448 hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult . |
3449 } note summable_Integral = this |
3449 } note summable_Integral = this |
3450 |
3450 |
3451 { fix f :: "nat \<Rightarrow> real" |
3451 { fix f :: "nat \<Rightarrow> real" |
3452 have "\<And> x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x" |
3452 have "\<And> x. f sums x = (\<lambda> n. if even n then f (n div 2) else 0) sums x" |
3516 show "a < b" and "a \<le> x" and "x \<le> b" using `a < b` `a \<le> x` `x \<le> b` by auto |
3516 show "a < b" and "a \<le> x" and "x \<le> b" using `a < b` `a \<le> x` `x \<le> b` by auto |
3517 have "\<forall> x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0" |
3517 have "\<forall> x. -r < x \<and> x < r \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0" |
3518 proof (rule allI, rule impI) |
3518 proof (rule allI, rule impI) |
3519 fix x assume "-r < x \<and> x < r" hence "\<bar>x\<bar> < r" by auto |
3519 fix x assume "-r < x \<and> x < r" hence "\<bar>x\<bar> < r" by auto |
3520 hence "\<bar>x\<bar> < 1" using `r < 1` by auto |
3520 hence "\<bar>x\<bar> < 1" using `r < 1` by auto |
3521 have "\<bar> - (x^2) \<bar> < 1" using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto |
3521 have "\<bar> - (x\<^sup>2) \<bar> < 1" using less_one_imp_sqr_less_one[OF `\<bar>x\<bar> < 1`] by auto |
3522 hence "(\<lambda> n. (- (x^2)) ^ n) sums (1 / (1 - (- (x^2))))" unfolding real_norm_def[symmetric] by (rule geometric_sums) |
3522 hence "(\<lambda> n. (- (x\<^sup>2)) ^ n) sums (1 / (1 - (- (x\<^sup>2))))" unfolding real_norm_def[symmetric] by (rule geometric_sums) |
3523 hence "(?c' x) sums (1 / (1 - (- (x^2))))" unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto |
3523 hence "(?c' x) sums (1 / (1 - (- (x\<^sup>2))))" unfolding power_mult_distrib[symmetric] power_mult nat_mult_commute[of _ 2] by auto |
3524 hence suminf_c'_eq_geom: "inverse (1 + x^2) = suminf (?c' x)" using sums_unique unfolding inverse_eq_divide by auto |
3524 hence suminf_c'_eq_geom: "inverse (1 + x\<^sup>2) = suminf (?c' x)" using sums_unique unfolding inverse_eq_divide by auto |
3525 have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x^2))" unfolding suminf_c'_eq_geom |
3525 have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))" unfolding suminf_c'_eq_geom |
3526 by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`]) |
3526 by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`]) |
3527 from DERIV_add_minus[OF this DERIV_arctan] |
3527 from DERIV_add_minus[OF this DERIV_arctan] |
3528 show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0" unfolding diff_minus by auto |
3528 show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0" unfolding diff_minus by auto |
3529 qed |
3529 qed |
3530 hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0" using `-r < a` `b < r` by auto |
3530 hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0" using `-r < a` `b < r` by auto |
3630 qed |
3630 qed |
3631 qed |
3631 qed |
3632 qed |
3632 qed |
3633 |
3633 |
3634 lemma arctan_half: fixes x :: real |
3634 lemma arctan_half: fixes x :: real |
3635 shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x^2)))" |
3635 shows "arctan x = 2 * arctan (x / (1 + sqrt(1 + x\<^sup>2)))" |
3636 proof - |
3636 proof - |
3637 obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x" using tan_total by blast |
3637 obtain y where low: "- (pi / 2) < y" and high: "y < pi / 2" and y_eq: "tan y = x" using tan_total by blast |
3638 hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2" by auto |
3638 hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2" by auto |
3639 |
3639 |
3640 have divide_nonzero_divide: "\<And> A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)" by auto |
3640 have divide_nonzero_divide: "\<And> A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)" by auto |
3641 |
3641 |
3642 have "0 < cos y" using cos_gt_zero_pi[OF low high] . |
3642 have "0 < cos y" using cos_gt_zero_pi[OF low high] . |
3643 hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y) ^ 2) = cos y" by auto |
3643 hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y" by auto |
3644 |
3644 |
3645 have "1 + (tan y)^2 = 1 + sin y^2 / cos y^2" unfolding tan_def power_divide .. |
3645 have "1 + (tan y)\<^sup>2 = 1 + (sin y)\<^sup>2 / (cos y)\<^sup>2" unfolding tan_def power_divide .. |
3646 also have "\<dots> = cos y^2 / cos y^2 + sin y^2 / cos y^2" using `cos y \<noteq> 0` by auto |
3646 also have "\<dots> = (cos y)\<^sup>2 / (cos y)\<^sup>2 + (sin y)\<^sup>2 / (cos y)\<^sup>2" using `cos y \<noteq> 0` by auto |
3647 also have "\<dots> = 1 / cos y^2" unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 .. |
3647 also have "\<dots> = 1 / (cos y)\<^sup>2" unfolding add_divide_distrib[symmetric] sin_cos_squared_add2 .. |
3648 finally have "1 + (tan y)^2 = 1 / cos y^2" . |
3648 finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" . |
3649 |
3649 |
3650 have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)" unfolding tan_def divide_nonzero_divide[OF `cos y \<noteq> 0`, symmetric] .. |
3650 have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)" unfolding tan_def divide_nonzero_divide[OF `cos y \<noteq> 0`, symmetric] .. |
3651 also have "\<dots> = tan y / (1 + 1 / cos y)" using `cos y \<noteq> 0` unfolding add_divide_distrib by auto |
3651 also have "\<dots> = tan y / (1 + 1 / cos y)" using `cos y \<noteq> 0` unfolding add_divide_distrib by auto |
3652 also have "\<dots> = tan y / (1 + 1 / sqrt(cos y^2))" unfolding cos_sqrt .. |
3652 also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))" unfolding cos_sqrt .. |
3653 also have "\<dots> = tan y / (1 + sqrt(1 / cos y^2))" unfolding real_sqrt_divide by auto |
3653 also have "\<dots> = tan y / (1 + sqrt (1 / (cos y)\<^sup>2))" unfolding real_sqrt_divide by auto |
3654 finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)^2))" unfolding `1 + (tan y)^2 = 1 / cos y^2` . |
3654 finally have eq: "sin y / (cos y + 1) = tan y / (1 + sqrt(1 + (tan y)\<^sup>2))" unfolding `1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2` . |
3655 |
3655 |
3656 have "arctan x = y" using arctan_tan low high y_eq by auto |
3656 have "arctan x = y" using arctan_tan low high y_eq by auto |
3657 also have "\<dots> = 2 * (arctan (tan (y/2)))" using arctan_tan[OF low2 high2] by auto |
3657 also have "\<dots> = 2 * (arctan (tan (y/2)))" using arctan_tan[OF low2 high2] by auto |
3658 also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))" unfolding tan_half by auto |
3658 also have "\<dots> = 2 * (arctan (sin y / (cos y + 1)))" unfolding tan_half by auto |
3659 finally show ?thesis unfolding eq `tan y = x` . |
3659 finally show ?thesis unfolding eq `tan y = x` . |