108 from \<open>0 < n\<close> f_the_inv_into_f[OF inj_sgn_power[OF \<open>0 < n\<close>] this] show ?thesis |
108 from \<open>0 < n\<close> f_the_inv_into_f[OF inj_sgn_power[OF \<open>0 < n\<close>] this] show ?thesis |
109 by (simp add: root_def) |
109 by (simp add: root_def) |
110 qed |
110 qed |
111 |
111 |
112 lemma split_root: "P (root n x) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (0 < n \<longrightarrow> (\<forall>y. sgn y * \<bar>y\<bar>^n = x \<longrightarrow> P y))" |
112 lemma split_root: "P (root n x) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (0 < n \<longrightarrow> (\<forall>y. sgn y * \<bar>y\<bar>^n = x \<longrightarrow> P y))" |
113 apply (cases "n = 0") |
113 proof (cases "n = 0") |
114 apply simp_all |
114 case True |
115 apply (metis root_sgn_power sgn_power_root) |
115 then show ?thesis by simp |
116 done |
116 next |
|
117 case False |
|
118 then show ?thesis |
|
119 by simp (metis root_sgn_power sgn_power_root) |
|
120 qed |
117 |
121 |
118 lemma real_root_zero [simp]: "root n 0 = 0" |
122 lemma real_root_zero [simp]: "root n 0 = 0" |
119 by (simp split: split_root add: sgn_zero_iff) |
123 by (simp split: split_root add: sgn_zero_iff) |
120 |
124 |
121 lemma real_root_minus: "root n (- x) = - root n x" |
125 lemma real_root_minus: "root n (- x) = - root n x" |
174 |
178 |
175 lemma real_root_le_mono: "0 < n \<Longrightarrow> x \<le> y \<Longrightarrow> root n x \<le> root n y" |
179 lemma real_root_le_mono: "0 < n \<Longrightarrow> x \<le> y \<Longrightarrow> root n x \<le> root n y" |
176 by (auto simp add: order_le_less real_root_less_mono) |
180 by (auto simp add: order_le_less real_root_less_mono) |
177 |
181 |
178 lemma real_root_less_iff [simp]: "0 < n \<Longrightarrow> root n x < root n y \<longleftrightarrow> x < y" |
182 lemma real_root_less_iff [simp]: "0 < n \<Longrightarrow> root n x < root n y \<longleftrightarrow> x < y" |
179 apply (cases "x < y") |
183 by (cases "x < y") (simp_all add: real_root_less_mono linorder_not_less real_root_le_mono) |
180 apply (simp add: real_root_less_mono) |
|
181 apply (simp add: linorder_not_less real_root_le_mono) |
|
182 done |
|
183 |
184 |
184 lemma real_root_le_iff [simp]: "0 < n \<Longrightarrow> root n x \<le> root n y \<longleftrightarrow> x \<le> y" |
185 lemma real_root_le_iff [simp]: "0 < n \<Longrightarrow> root n x \<le> root n y \<longleftrightarrow> x \<le> y" |
185 apply (cases "x \<le> y") |
186 by (cases "x \<le> y") (simp_all add: real_root_le_mono linorder_not_le real_root_less_mono) |
186 apply (simp add: real_root_le_mono) |
|
187 apply (simp add: linorder_not_le real_root_less_mono) |
|
188 done |
|
189 |
187 |
190 lemma real_root_eq_iff [simp]: "0 < n \<Longrightarrow> root n x = root n y \<longleftrightarrow> x = y" |
188 lemma real_root_eq_iff [simp]: "0 < n \<Longrightarrow> root n x = root n y \<longleftrightarrow> x = y" |
191 by (simp add: order_eq_iff) |
189 by (simp add: order_eq_iff) |
192 |
190 |
193 lemmas real_root_gt_0_iff [simp] = real_root_less_iff [where x=0, simplified] |
191 lemmas real_root_gt_0_iff [simp] = real_root_less_iff [where x=0, simplified] |
246 by (simp add: real_root_mult_exp [symmetric] mult.commute) |
244 by (simp add: real_root_mult_exp [symmetric] mult.commute) |
247 |
245 |
248 |
246 |
249 text \<open>Monotonicity in first argument.\<close> |
247 text \<open>Monotonicity in first argument.\<close> |
250 |
248 |
251 lemma real_root_strict_decreasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 1 < x \<Longrightarrow> root N x < root n x" |
249 lemma real_root_strict_decreasing: |
252 apply (subgoal_tac "root n (root N x) ^ n < root N (root n x) ^ N") |
250 assumes "0 < n" "n < N" "1 < x" |
253 apply simp |
251 shows "root N x < root n x" |
254 apply (simp add: real_root_commute power_strict_increasing del: real_root_pow_pos2) |
252 proof - |
255 done |
253 from assms have "root n (root N x) ^ n < root N (root n x) ^ N" |
256 |
254 by (simp add: real_root_commute power_strict_increasing del: real_root_pow_pos2) |
257 lemma real_root_strict_increasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 0 < x \<Longrightarrow> x < 1 \<Longrightarrow> root n x < root N x" |
255 with assms show ?thesis by simp |
258 apply (subgoal_tac "root N (root n x) ^ N < root n (root N x) ^ n") |
256 qed |
259 apply simp |
257 |
260 apply (simp add: real_root_commute power_strict_decreasing del: real_root_pow_pos2) |
258 lemma real_root_strict_increasing: |
261 done |
259 assumes "0 < n" "n < N" "0 < x" "x < 1" |
|
260 shows "root n x < root N x" |
|
261 proof - |
|
262 from assms have "root N (root n x) ^ N < root n (root N x) ^ n" |
|
263 by (simp add: real_root_commute power_strict_decreasing del: real_root_pow_pos2) |
|
264 with assms show ?thesis by simp |
|
265 qed |
262 |
266 |
263 lemma real_root_decreasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 1 \<le> x \<Longrightarrow> root N x \<le> root n x" |
267 lemma real_root_decreasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 1 \<le> x \<Longrightarrow> root N x \<le> root n x" |
264 by (auto simp add: order_le_less real_root_strict_decreasing) |
268 by (auto simp add: order_le_less real_root_strict_decreasing) |
265 |
269 |
266 lemma real_root_increasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> root n x \<le> root N x" |
270 lemma real_root_increasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> root n x \<le> root N x" |
363 show "isCont (root n) x" |
367 show "isCont (root n) x" |
364 by (rule isCont_real_root) |
368 by (rule isCont_real_root) |
365 qed |
369 qed |
366 |
370 |
367 lemma DERIV_real_root_generic: |
371 lemma DERIV_real_root_generic: |
368 assumes "0 < n" and "x \<noteq> 0" |
372 assumes "0 < n" |
369 and "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" |
373 and "x \<noteq> 0" |
370 and "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))" |
374 and "even n \<Longrightarrow> 0 < x \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" |
|
375 and "even n \<Longrightarrow> x < 0 \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))" |
371 and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" |
376 and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" |
372 shows "DERIV (root n) x :> D" |
377 shows "DERIV (root n) x :> D" |
373 using assms |
378 using assms |
374 by (cases "even n", cases "0 < x", |
379 by (cases "even n", cases "0 < x") |
375 auto intro: DERIV_real_root[THEN DERIV_cong] |
380 (auto intro: DERIV_real_root[THEN DERIV_cong] |
376 DERIV_odd_real_root[THEN DERIV_cong] |
381 DERIV_odd_real_root[THEN DERIV_cong] |
377 DERIV_even_real_root[THEN DERIV_cong]) |
382 DERIV_even_real_root[THEN DERIV_cong]) |
378 |
383 |
379 |
384 |
380 subsection \<open>Square Root\<close> |
385 subsection \<open>Square Root\<close> |
381 |
386 |
382 definition sqrt :: "real \<Rightarrow> real" |
387 definition sqrt :: "real \<Rightarrow> real" |
388 lemma real_sqrt_unique: "y\<^sup>2 = x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt x = y" |
393 lemma real_sqrt_unique: "y\<^sup>2 = x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt x = y" |
389 unfolding sqrt_def by (rule real_root_pos_unique [OF pos2]) |
394 unfolding sqrt_def by (rule real_root_pos_unique [OF pos2]) |
390 |
395 |
391 lemma real_sqrt_abs [simp]: "sqrt (x\<^sup>2) = \<bar>x\<bar>" |
396 lemma real_sqrt_abs [simp]: "sqrt (x\<^sup>2) = \<bar>x\<bar>" |
392 apply (rule real_sqrt_unique) |
397 apply (rule real_sqrt_unique) |
393 apply (rule power2_abs) |
398 apply (rule power2_abs) |
394 apply (rule abs_ge_zero) |
399 apply (rule abs_ge_zero) |
395 done |
400 done |
396 |
401 |
397 lemma real_sqrt_pow2 [simp]: "0 \<le> x \<Longrightarrow> (sqrt x)\<^sup>2 = x" |
402 lemma real_sqrt_pow2 [simp]: "0 \<le> x \<Longrightarrow> (sqrt x)\<^sup>2 = x" |
398 unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2]) |
403 unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2]) |
399 |
404 |
400 lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<^sup>2 = x) = (0 \<le> x)" |
405 lemma real_sqrt_pow2_iff [simp]: "(sqrt x)\<^sup>2 = x \<longleftrightarrow> 0 \<le> x" |
401 apply (rule iffI) |
406 apply (rule iffI) |
402 apply (erule subst) |
407 apply (erule subst) |
403 apply (rule zero_le_power2) |
408 apply (rule zero_le_power2) |
404 apply (erule real_sqrt_pow2) |
409 apply (erule real_sqrt_pow2) |
405 done |
410 done |
406 |
411 |
407 lemma real_sqrt_zero [simp]: "sqrt 0 = 0" |
412 lemma real_sqrt_zero [simp]: "sqrt 0 = 0" |
408 unfolding sqrt_def by (rule real_root_zero) |
413 unfolding sqrt_def by (rule real_root_zero) |
441 unfolding sqrt_def by (rule real_root_less_mono [OF pos2]) |
446 unfolding sqrt_def by (rule real_root_less_mono [OF pos2]) |
442 |
447 |
443 lemma real_sqrt_le_mono: "x \<le> y \<Longrightarrow> sqrt x \<le> sqrt y" |
448 lemma real_sqrt_le_mono: "x \<le> y \<Longrightarrow> sqrt x \<le> sqrt y" |
444 unfolding sqrt_def by (rule real_root_le_mono [OF pos2]) |
449 unfolding sqrt_def by (rule real_root_le_mono [OF pos2]) |
445 |
450 |
446 lemma real_sqrt_less_iff [simp]: "(sqrt x < sqrt y) = (x < y)" |
451 lemma real_sqrt_less_iff [simp]: "sqrt x < sqrt y \<longleftrightarrow> x < y" |
447 unfolding sqrt_def by (rule real_root_less_iff [OF pos2]) |
452 unfolding sqrt_def by (rule real_root_less_iff [OF pos2]) |
448 |
453 |
449 lemma real_sqrt_le_iff [simp]: "(sqrt x \<le> sqrt y) = (x \<le> y)" |
454 lemma real_sqrt_le_iff [simp]: "sqrt x \<le> sqrt y \<longleftrightarrow> x \<le> y" |
450 unfolding sqrt_def by (rule real_root_le_iff [OF pos2]) |
455 unfolding sqrt_def by (rule real_root_le_iff [OF pos2]) |
451 |
456 |
452 lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)" |
457 lemma real_sqrt_eq_iff [simp]: "sqrt x = sqrt y \<longleftrightarrow> x = y" |
453 unfolding sqrt_def by (rule real_root_eq_iff [OF pos2]) |
458 unfolding sqrt_def by (rule real_root_eq_iff [OF pos2]) |
454 |
459 |
455 lemma real_less_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y\<^sup>2 \<Longrightarrow> sqrt x < y" |
460 lemma real_less_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y\<^sup>2 \<Longrightarrow> sqrt x < y" |
456 using real_sqrt_less_iff[of x "y\<^sup>2"] by simp |
461 using real_sqrt_less_iff[of x "y\<^sup>2"] by simp |
457 |
462 |
523 |
528 |
524 declare |
529 declare |
525 DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros] |
530 DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros] |
526 DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros] |
531 DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros] |
527 |
532 |
528 lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0" for x :: real |
533 lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0" |
|
534 for x :: real |
529 apply auto |
535 apply auto |
530 apply (cut_tac x = x and y = 0 in linorder_less_linear) |
536 using linorder_less_linear [where x = x and y = 0] |
531 apply (simp add: zero_less_mult_iff) |
537 apply (simp add: zero_less_mult_iff) |
532 done |
538 done |
533 |
539 |
534 lemma real_sqrt_abs2 [simp]: "sqrt (x * x) = \<bar>x\<bar>" |
540 lemma real_sqrt_abs2 [simp]: "sqrt (x * x) = \<bar>x\<bar>" |
535 apply (subst power2_eq_square [symmetric]) |
541 apply (subst power2_eq_square [symmetric]) |
564 power2_eq_square [symmetric] real_inv_sqrt_pow2 pos False) |
570 power2_eq_square [symmetric] real_inv_sqrt_pow2 pos False) |
565 qed |
571 qed |
566 qed |
572 qed |
567 |
573 |
568 lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x" |
574 lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x" |
569 apply (cases "x = 0") |
575 by (cases "x = 0") (simp_all add: sqrt_divide_self_eq [of x] field_simps) |
570 apply simp_all |
576 |
571 using sqrt_divide_self_eq[of x] |
577 lemma real_divide_square_eq [simp]: "(r * a) / (r * r) = a / r" |
572 apply (simp add: field_simps) |
578 for a r :: real |
573 done |
579 by (cases "r = 0") (simp_all add: divide_inverse ac_simps) |
574 |
|
575 lemma real_divide_square_eq [simp]: "(r * a) / (r * r) = a / r" for a r :: real |
|
576 apply (simp add: divide_inverse) |
|
577 apply (case_tac "r = 0") |
|
578 apply (auto simp add: ac_simps) |
|
579 done |
|
580 |
580 |
581 lemma lemma_real_divide_sqrt_less: "0 < u \<Longrightarrow> u / sqrt 2 < u" |
581 lemma lemma_real_divide_sqrt_less: "0 < u \<Longrightarrow> u / sqrt 2 < u" |
582 by (simp add: divide_less_eq) |
582 by (simp add: divide_less_eq) |
583 |
583 |
584 lemma four_x_squared: "4 * x\<^sup>2 = (2 * x)\<^sup>2" for x :: real |
584 lemma four_x_squared: "4 * x\<^sup>2 = (2 * x)\<^sup>2" |
|
585 for x :: real |
585 by (simp add: power2_eq_square) |
586 by (simp add: power2_eq_square) |
586 |
587 |
587 lemma sqrt_at_top: "LIM x at_top. sqrt x :: real :> at_top" |
588 lemma sqrt_at_top: "LIM x at_top. sqrt x :: real :> at_top" |
588 by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="power2"]) |
589 by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="power2"]) |
589 (auto intro: eventually_gt_at_top) |
590 (auto intro: eventually_gt_at_top) |
590 |
591 |
591 |
592 |
592 subsection \<open>Square Root of Sum of Squares\<close> |
593 subsection \<open>Square Root of Sum of Squares\<close> |
593 |
594 |
594 lemma sum_squares_bound: "2 * x * y \<le> x\<^sup>2 + y\<^sup>2" for x y :: "'a::linordered_field" |
595 lemma sum_squares_bound: "2 * x * y \<le> x\<^sup>2 + y\<^sup>2" |
|
596 for x y :: "'a::linordered_field" |
595 proof - |
597 proof - |
596 have "(x - y)\<^sup>2 = x * x - 2 * x * y + y * y" |
598 have "(x - y)\<^sup>2 = x * x - 2 * x * y + y * y" |
597 by algebra |
599 by algebra |
598 then have "0 \<le> x\<^sup>2 - 2 * x * y + y\<^sup>2" |
600 then have "0 \<le> x\<^sup>2 - 2 * x * y + y\<^sup>2" |
599 by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square) |
601 by (metis sum_power2_ge_zero zero_le_double_add_iff_zero_le_single_add power2_eq_square) |
610 apply (auto simp: zero_le_mult_iff) |
612 apply (auto simp: zero_le_mult_iff) |
611 apply (auto simp: algebra_simps power2_eq_square) |
613 apply (auto simp: algebra_simps power2_eq_square) |
612 done |
614 done |
613 |
615 |
614 lemma arith_geo_mean_sqrt: |
616 lemma arith_geo_mean_sqrt: |
615 fixes x::real assumes "x\<ge>0" "y\<ge>0" shows "sqrt(x*y) \<le> (x + y)/2" |
617 fixes x :: real |
|
618 assumes "x \<ge> 0" "y \<ge> 0" |
|
619 shows "sqrt (x * y) \<le> (x + y)/2" |
616 apply (rule arith_geo_mean) |
620 apply (rule arith_geo_mean) |
617 using assms |
621 using assms |
618 apply (auto simp: zero_le_mult_iff) |
622 apply (auto simp: zero_le_mult_iff) |
619 done |
623 done |
620 |
624 |
621 lemma real_sqrt_sum_squares_mult_ge_zero [simp]: "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2)*(xa\<^sup>2 + ya\<^sup>2))" |
625 lemma real_sqrt_sum_squares_mult_ge_zero [simp]: "0 \<le> sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2))" |
622 by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero) |
626 by (metis real_sqrt_ge_0_iff split_mult_pos_le sum_power2_ge_zero) |
623 |
627 |
624 lemma real_sqrt_sum_squares_mult_squared_eq [simp]: |
628 lemma real_sqrt_sum_squares_mult_squared_eq [simp]: |
625 "(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)" |
629 "(sqrt ((x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)))\<^sup>2 = (x\<^sup>2 + y\<^sup>2) * (xa\<^sup>2 + ya\<^sup>2)" |
626 by (simp add: zero_le_mult_iff) |
630 by (simp add: zero_le_mult_iff) |
647 by (simp add: power2_eq_square [symmetric]) |
651 by (simp add: power2_eq_square [symmetric]) |
648 |
652 |
649 lemma real_sqrt_sum_squares_triangle_ineq: |
653 lemma real_sqrt_sum_squares_triangle_ineq: |
650 "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)" |
654 "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)" |
651 apply (rule power2_le_imp_le) |
655 apply (rule power2_le_imp_le) |
652 apply simp |
656 apply simp |
653 apply (simp add: power2_sum) |
657 apply (simp add: power2_sum) |
654 apply (simp only: mult.assoc distrib_left [symmetric]) |
658 apply (simp only: mult.assoc distrib_left [symmetric]) |
655 apply (rule mult_left_mono) |
659 apply (rule mult_left_mono) |
656 apply (rule power2_le_imp_le) |
660 apply (rule power2_le_imp_le) |
657 apply (simp add: power2_sum power_mult_distrib) |
661 apply (simp add: power2_sum power_mult_distrib) |
658 apply (simp add: ring_distribs) |
662 apply (simp add: ring_distribs) |
659 apply (subgoal_tac "0 \<le> b\<^sup>2 * c\<^sup>2 + a\<^sup>2 * d\<^sup>2 - 2 * (a * c) * (b * d)") |
663 apply (subgoal_tac "0 \<le> b\<^sup>2 * c\<^sup>2 + a\<^sup>2 * d\<^sup>2 - 2 * (a * c) * (b * d)") |
660 apply simp |
664 apply simp |
661 apply (rule_tac b="(a * d - b * c)\<^sup>2" in ord_le_eq_trans) |
665 apply (rule_tac b="(a * d - b * c)\<^sup>2" in ord_le_eq_trans) |
662 apply (rule zero_le_power2) |
666 apply (rule zero_le_power2) |
663 apply (simp add: power2_diff power_mult_distrib) |
667 apply (simp add: power2_diff power_mult_distrib) |
664 apply simp |
668 apply simp |
665 apply simp |
669 apply simp |
666 apply (simp add: add_increasing) |
670 apply (simp add: add_increasing) |
667 done |
671 done |
668 |
672 |
669 lemma real_sqrt_sum_squares_less: "\<bar>x\<bar> < u / sqrt 2 \<Longrightarrow> \<bar>y\<bar> < u / sqrt 2 \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u" |
673 lemma real_sqrt_sum_squares_less: "\<bar>x\<bar> < u / sqrt 2 \<Longrightarrow> \<bar>y\<bar> < u / sqrt 2 \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u" |
670 apply (rule power2_less_imp_less) |
674 apply (rule power2_less_imp_less) |
671 apply simp |
675 apply simp |
672 apply (drule power_strict_mono [OF _ abs_ge_zero pos2]) |
676 apply (drule power_strict_mono [OF _ abs_ge_zero pos2]) |
673 apply (drule power_strict_mono [OF _ abs_ge_zero pos2]) |
677 apply (drule power_strict_mono [OF _ abs_ge_zero pos2]) |
674 apply (simp add: power_divide) |
678 apply (simp add: power_divide) |
675 apply (drule order_le_less_trans [OF abs_ge_zero]) |
679 apply (drule order_le_less_trans [OF abs_ge_zero]) |
676 apply (simp add: zero_less_divide_iff) |
680 apply (simp add: zero_less_divide_iff) |
677 done |
681 done |
678 |
682 |
679 lemma sqrt2_less_2: "sqrt 2 < (2::real)" |
683 lemma sqrt2_less_2: "sqrt 2 < (2::real)" |
683 |
687 |
684 text \<open>Needed for the infinitely close relation over the nonstandard complex numbers.\<close> |
688 text \<open>Needed for the infinitely close relation over the nonstandard complex numbers.\<close> |
685 lemma lemma_sqrt_hcomplex_capprox: |
689 lemma lemma_sqrt_hcomplex_capprox: |
686 "0 < u \<Longrightarrow> x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u" |
690 "0 < u \<Longrightarrow> x < u/2 \<Longrightarrow> y < u/2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) < u" |
687 apply (rule real_sqrt_sum_squares_less) |
691 apply (rule real_sqrt_sum_squares_less) |
688 apply (auto simp add: abs_if field_simps) |
692 apply (auto simp add: abs_if field_simps) |
689 apply (rule le_less_trans [where y = "x*2"]) |
693 apply (rule le_less_trans [where y = "x*2"]) |
690 using less_eq_real_def sqrt2_less_2 |
694 using less_eq_real_def sqrt2_less_2 |
691 apply force |
695 apply force |
692 apply assumption |
696 apply assumption |
693 apply (rule le_less_trans [where y = "y*2"]) |
697 apply (rule le_less_trans [where y = "y*2"]) |
694 using less_eq_real_def sqrt2_less_2 mult_le_cancel_left |
698 using less_eq_real_def sqrt2_less_2 mult_le_cancel_left |
695 apply auto |
699 apply auto |
696 done |
700 done |
697 |
701 |
698 lemma LIMSEQ_root: "(\<lambda>n. root n n) \<longlonglongrightarrow> 1" |
702 lemma LIMSEQ_root: "(\<lambda>n. root n n) \<longlonglongrightarrow> 1" |
699 proof - |
703 proof - |
700 define x where "x n = root n n - 1" for n |
704 define x where "x n = root n n - 1" for n |