303 with \<open>u \<in> \<real>\<close> show ?thesis |
300 with \<open>u \<in> \<real>\<close> show ?thesis |
304 by (force simp: HFinite_def Reals_eq_Standard) |
301 by (force simp: HFinite_def Reals_eq_Standard) |
305 qed |
302 qed |
306 |
303 |
307 lemma starfun_exp_add_HFinite_Infinitesimal_approx: |
304 lemma starfun_exp_add_HFinite_Infinitesimal_approx: |
308 "\<lbrakk>x \<in> Infinitesimal; z \<in> HFinite\<rbrakk> \<Longrightarrow> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z" |
305 fixes x :: hypreal |
309 apply (simp add: STAR_exp_add) |
306 shows "\<lbrakk>x \<in> Infinitesimal; z \<in> HFinite\<rbrakk> \<Longrightarrow> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z" |
310 apply (frule STAR_exp_Infinitesimal) |
307 using STAR_exp_Infinitesimal approx_mult2 starfun_exp_HFinite by (fastforce simp add: STAR_exp_add) |
311 apply (drule approx_mult2) |
308 |
312 apply (auto intro: starfun_exp_HFinite) |
|
313 done |
|
314 |
|
315 (* using previous result to get to result *) |
|
316 lemma starfun_ln_HInfinite: |
309 lemma starfun_ln_HInfinite: |
317 "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite" |
310 "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite" |
318 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) |
311 by (metis HInfinite_HFinite_iff starfun_exp_HFinite starfun_exp_ln_iff) |
319 apply (drule starfun_exp_HFinite) |
|
320 apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff) |
|
321 done |
|
322 |
312 |
323 lemma starfun_exp_HInfinite_Infinitesimal_disj: |
313 lemma starfun_exp_HInfinite_Infinitesimal_disj: |
324 "x \<in> HInfinite \<Longrightarrow> ( *f* exp) x \<in> HInfinite \<or> ( *f* exp) (x::hypreal) \<in> Infinitesimal" |
314 fixes x :: hypreal |
325 apply (insert linorder_linear [of x 0]) |
315 shows "x \<in> HInfinite \<Longrightarrow> ( *f* exp) x \<in> HInfinite \<or> ( *f* exp) (x::hypreal) \<in> Infinitesimal" |
326 apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal) |
316 by (meson linear starfun_exp_HInfinite starfun_exp_Infinitesimal) |
327 done |
317 |
328 |
|
329 (* check out this proof\<And>! *) |
|
330 lemma starfun_ln_HFinite_not_Infinitesimal: |
318 lemma starfun_ln_HFinite_not_Infinitesimal: |
331 "\<lbrakk>x \<in> HFinite - Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite" |
319 "\<lbrakk>x \<in> HFinite - Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite" |
332 apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2]) |
320 by (metis DiffD1 DiffD2 HInfinite_HFinite_iff starfun_exp_HInfinite_Infinitesimal_disj starfun_exp_ln_iff) |
333 apply (drule starfun_exp_HInfinite_Infinitesimal_disj) |
|
334 apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff |
|
335 del: starfun_exp_ln_iff) |
|
336 done |
|
337 |
321 |
338 (* we do proof by considering ln of 1/x *) |
322 (* we do proof by considering ln of 1/x *) |
339 lemma starfun_ln_Infinitesimal_HInfinite: |
323 lemma starfun_ln_Infinitesimal_HInfinite: |
340 "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite" |
324 assumes "x \<in> Infinitesimal" "0 < x" |
341 apply (drule Infinitesimal_inverse_HInfinite) |
325 shows "( *f* real_ln) x \<in> HInfinite" |
342 apply (frule positive_imp_inverse_positive) |
326 proof - |
343 apply (drule_tac [2] starfun_ln_HInfinite) |
327 have "inverse x \<in> HInfinite" |
344 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff) |
328 using Infinitesimal_inverse_HInfinite assms by blast |
345 done |
329 then show ?thesis |
|
330 using HInfinite_minus_iff assms(2) starfun_ln_HInfinite starfun_ln_inverse by fastforce |
|
331 qed |
346 |
332 |
347 lemma starfun_ln_less_zero: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0" |
333 lemma starfun_ln_less_zero: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0" |
348 by transfer (rule ln_less_zero) |
334 by transfer (rule ln_less_zero) |
349 |
335 |
350 lemma starfun_ln_Infinitesimal_less_zero: |
336 lemma starfun_ln_Infinitesimal_less_zero: |
351 "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0" |
337 "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0" |
352 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) |
338 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) |
353 |
339 |
354 lemma starfun_ln_HInfinite_gt_zero: |
340 lemma starfun_ln_HInfinite_gt_zero: |
355 "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> 0 < ( *f* real_ln) x" |
341 "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> 0 < ( *f* real_ln) x" |
356 by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) |
342 by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) |
357 |
343 |
358 |
|
359 (* |
|
360 Goalw [NSLIM_def] "(\<lambda>h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x" |
|
361 *) |
|
362 |
344 |
363 lemma HFinite_sin [simp]: "sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n) \<in> HFinite" |
345 lemma HFinite_sin [simp]: "sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n) \<in> HFinite" |
364 unfolding sumhr_app |
346 proof - |
365 apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan) |
347 have "summable (\<lambda>i. sin_coeff i * x ^ i)" |
366 apply (rule NSBseqD2) |
348 using summable_norm_sin [of x] by (simp add: summable_rabs_cancel) |
367 apply (rule NSconvergent_NSBseq) |
349 then have "(*f* (\<lambda>n. \<Sum>n<n. sin_coeff n * x ^ n)) whn \<in> HFinite" |
368 apply (rule convergent_NSconvergent_iff [THEN iffD1]) |
350 unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_iff |
369 apply (rule summable_iff_convergent [THEN iffD1]) |
351 using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast |
370 using summable_norm_sin [of x] |
352 then show ?thesis |
371 apply (simp add: summable_rabs_cancel) |
353 unfolding sumhr_app |
372 done |
354 by (simp only: star_zero_def starfun2_star_of atLeast0LessThan) |
|
355 qed |
373 |
356 |
374 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0" |
357 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0" |
375 by transfer (rule sin_zero) |
358 by transfer (rule sin_zero) |
376 |
359 |
377 lemma STAR_sin_Infinitesimal [simp]: |
360 lemma STAR_sin_Infinitesimal [simp]: |
378 fixes x :: "'a::{real_normed_field,banach} star" |
361 fixes x :: "'a::{real_normed_field,banach} star" |
379 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x \<approx> x" |
362 assumes "x \<in> Infinitesimal" |
380 apply (case_tac "x = 0") |
363 shows "( *f* sin) x \<approx> x" |
381 apply (cut_tac [2] x = 0 in DERIV_sin) |
364 proof (cases "x = 0") |
382 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
365 case False |
383 apply (drule bspec [where x = x], auto) |
366 have "NSDERIV sin 0 :> 1" |
384 apply (drule approx_mult1 [where c = x]) |
367 by (metis DERIV_sin NSDERIV_DERIV_iff cos_zero) |
385 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
368 then have "(*f* sin) x / x \<approx> 1" |
386 simp add: mult.assoc) |
369 using False NSDERIVD2 assms by fastforce |
387 done |
370 with assms show ?thesis |
|
371 unfolding star_one_def |
|
372 by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite) |
|
373 qed auto |
388 |
374 |
389 lemma HFinite_cos [simp]: "sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n) \<in> HFinite" |
375 lemma HFinite_cos [simp]: "sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n) \<in> HFinite" |
390 unfolding sumhr_app |
376 proof - |
391 apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan) |
377 have "summable (\<lambda>i. cos_coeff i * x ^ i)" |
392 apply (rule NSBseqD2) |
378 using summable_norm_cos [of x] by (simp add: summable_rabs_cancel) |
393 apply (rule NSconvergent_NSBseq) |
379 then have "(*f* (\<lambda>n. \<Sum>n<n. cos_coeff n * x ^ n)) whn \<in> HFinite" |
394 apply (rule convergent_NSconvergent_iff [THEN iffD1]) |
380 unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_iff |
395 apply (rule summable_iff_convergent [THEN iffD1]) |
381 using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast |
396 using summable_norm_cos [of x] |
382 then show ?thesis |
397 apply (simp add: summable_rabs_cancel) |
383 unfolding sumhr_app |
398 done |
384 by (simp only: star_zero_def starfun2_star_of atLeast0LessThan) |
|
385 qed |
399 |
386 |
400 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1" |
387 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1" |
401 by transfer (rule cos_zero) |
388 by transfer (rule cos_zero) |
402 |
389 |
403 lemma STAR_cos_Infinitesimal [simp]: |
390 lemma STAR_cos_Infinitesimal [simp]: |
404 fixes x :: "'a::{real_normed_field,banach} star" |
391 fixes x :: "'a::{real_normed_field,banach} star" |
405 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1" |
392 assumes "x \<in> Infinitesimal" |
406 apply (case_tac "x = 0") |
393 shows "( *f* cos) x \<approx> 1" |
407 apply (cut_tac [2] x = 0 in DERIV_cos) |
394 proof (cases "x = 0") |
408 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
395 case False |
409 apply (drule bspec [where x = x]) |
396 have "NSDERIV cos 0 :> 0" |
410 apply auto |
397 by (metis DERIV_cos NSDERIV_DERIV_iff add.inverse_neutral sin_zero) |
411 apply (drule approx_mult1 [where c = x]) |
398 then have "(*f* cos) x - 1 \<approx> 0" |
412 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
399 using NSDERIV_approx assms by fastforce |
413 simp add: mult.assoc) |
400 with assms show ?thesis |
414 apply (rule approx_add_right_cancel [where d = "-1"]) |
401 using approx_minus_iff by blast |
415 apply simp |
402 qed auto |
416 done |
|
417 |
403 |
418 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0" |
404 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0" |
419 by transfer (rule tan_zero) |
405 by transfer (rule tan_zero) |
420 |
406 |
421 lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> ( *f* tan) x \<approx> x" |
407 lemma STAR_tan_Infinitesimal [simp]: |
422 apply (case_tac "x = 0") |
408 assumes "x \<in> Infinitesimal" |
423 apply (cut_tac [2] x = 0 in DERIV_tan) |
409 shows "( *f* tan) x \<approx> x" |
424 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
410 proof (cases "x = 0") |
425 apply (drule bspec [where x = x], auto) |
411 case False |
426 apply (drule approx_mult1 [where c = x]) |
412 have "NSDERIV tan 0 :> 1" |
427 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] |
413 using DERIV_tan [of 0] by (simp add: NSDERIV_DERIV_iff) |
428 simp add: mult.assoc) |
414 then have "(*f* tan) x / x \<approx> 1" |
429 done |
415 using False NSDERIVD2 assms by fastforce |
|
416 with assms show ?thesis |
|
417 unfolding star_one_def |
|
418 by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite) |
|
419 qed auto |
430 |
420 |
431 lemma STAR_sin_cos_Infinitesimal_mult: |
421 lemma STAR_sin_cos_Infinitesimal_mult: |
432 fixes x :: "'a::{real_normed_field,banach} star" |
422 fixes x :: "'a::{real_normed_field,banach} star" |
433 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x * ( *f* cos) x \<approx> x" |
423 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x * ( *f* cos) x \<approx> x" |
434 using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] |
424 using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] |
435 by (simp add: Infinitesimal_subset_HFinite [THEN subsetD]) |
425 by (simp add: Infinitesimal_subset_HFinite [THEN subsetD]) |
436 |
426 |
437 lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite" |
427 lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite" |
438 by simp |
428 by simp |
439 |
429 |
440 (* lemmas *) |
|
441 |
|
442 lemma lemma_split_hypreal_of_real: |
|
443 "N \<in> HNatInfinite |
|
444 \<Longrightarrow> hypreal_of_real a = |
|
445 hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)" |
|
446 by (simp add: mult.assoc [symmetric] zero_less_HNatInfinite) |
|
447 |
430 |
448 lemma STAR_sin_Infinitesimal_divide: |
431 lemma STAR_sin_Infinitesimal_divide: |
449 fixes x :: "'a::{real_normed_field,banach} star" |
432 fixes x :: "'a::{real_normed_field,banach} star" |
450 shows "\<lbrakk>x \<in> Infinitesimal; x \<noteq> 0\<rbrakk> \<Longrightarrow> ( *f* sin) x/x \<approx> 1" |
433 shows "\<lbrakk>x \<in> Infinitesimal; x \<noteq> 0\<rbrakk> \<Longrightarrow> ( *f* sin) x/x \<approx> 1" |
451 using DERIV_sin [of "0::'a"] |
434 using DERIV_sin [of "0::'a"] |
452 by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
435 by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def) |
453 |
436 |
454 (*------------------------------------------------------------------------*) |
437 subsection \<open>Proving $\sin* (1/n) \times 1/(1/n) \approx 1$ for $n = \infty$ \<close> |
455 (* sin* (1/n) * 1/(1/n) \<approx> 1 for n = oo *) |
|
456 (*------------------------------------------------------------------------*) |
|
457 |
438 |
458 lemma lemma_sin_pi: |
439 lemma lemma_sin_pi: |
459 "n \<in> HNatInfinite |
440 "n \<in> HNatInfinite |
460 \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1" |
441 \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1" |
461 apply (rule STAR_sin_Infinitesimal_divide) |
442 by (simp add: STAR_sin_Infinitesimal_divide zero_less_HNatInfinite) |
462 apply (auto simp add: zero_less_HNatInfinite) |
|
463 done |
|
464 |
443 |
465 lemma STAR_sin_inverse_HNatInfinite: |
444 lemma STAR_sin_inverse_HNatInfinite: |
466 "n \<in> HNatInfinite |
445 "n \<in> HNatInfinite |
467 \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1" |
446 \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1" |
468 apply (frule lemma_sin_pi) |
447 by (metis field_class.field_divide_inverse inverse_inverse_eq lemma_sin_pi) |
469 apply (simp add: divide_inverse) |
|
470 done |
|
471 |
448 |
472 lemma Infinitesimal_pi_divide_HNatInfinite: |
449 lemma Infinitesimal_pi_divide_HNatInfinite: |
473 "N \<in> HNatInfinite |
450 "N \<in> HNatInfinite |
474 \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal" |
451 \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal" |
475 apply (simp add: divide_inverse) |
452 by (simp add: Infinitesimal_HFinite_mult2 field_class.field_divide_inverse) |
476 apply (auto intro: Infinitesimal_HFinite_mult2) |
|
477 done |
|
478 |
453 |
479 lemma pi_divide_HNatInfinite_not_zero [simp]: |
454 lemma pi_divide_HNatInfinite_not_zero [simp]: |
480 "N \<in> HNatInfinite \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0" |
455 "N \<in> HNatInfinite \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0" |
481 by (simp add: zero_less_HNatInfinite) |
456 by (simp add: zero_less_HNatInfinite) |
482 |
457 |
483 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi: |
458 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi: |
484 "n \<in> HNatInfinite |
459 assumes "n \<in> HNatInfinite" |
485 \<Longrightarrow> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n |
460 shows "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) * hypreal_of_hypnat n \<approx> |
486 \<approx> hypreal_of_real pi" |
461 hypreal_of_real pi" |
487 apply (frule STAR_sin_Infinitesimal_divide |
462 proof - |
488 [OF Infinitesimal_pi_divide_HNatInfinite |
463 have "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) / (hypreal_of_real pi / hypreal_of_hypnat n) \<approx> 1" |
489 pi_divide_HNatInfinite_not_zero]) |
464 using Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal_divide assms pi_divide_HNatInfinite_not_zero by blast |
490 apply (auto) |
465 then have "hypreal_of_hypnat n * star_of sin \<star> (hypreal_of_real pi / hypreal_of_hypnat n) / hypreal_of_real pi \<approx> 1" |
491 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"]) |
466 by (simp add: mult.commute starfun_def) |
492 apply (auto intro: Reals_inverse simp add: divide_inverse ac_simps) |
467 then show ?thesis |
493 done |
468 apply (simp add: starfun_def field_simps) |
|
469 by (metis (no_types, lifting) approx_mult_subst_star_of approx_refl mult_cancel_right1 nonzero_eq_divide_eq pi_neq_zero star_of_eq_0) |
|
470 qed |
494 |
471 |
495 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2: |
472 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2: |
496 "n \<in> HNatInfinite |
473 "n \<in> HNatInfinite |
497 \<Longrightarrow> hypreal_of_hypnat n * |
474 \<Longrightarrow> hypreal_of_hypnat n * ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \<approx> hypreal_of_real pi" |
498 ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) |
475 by (metis STAR_sin_pi_divide_HNatInfinite_approx_pi mult.commute) |
499 \<approx> hypreal_of_real pi" |
|
500 apply (rule mult.commute [THEN subst]) |
|
501 apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi) |
|
502 done |
|
503 |
476 |
504 lemma starfunNat_pi_divide_n_Infinitesimal: |
477 lemma starfunNat_pi_divide_n_Infinitesimal: |
505 "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. pi / real x)) N \<in> Infinitesimal" |
478 "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. pi / real x)) N \<in> Infinitesimal" |
506 by (auto intro!: Infinitesimal_HFinite_mult2 |
479 by (simp add: Infinitesimal_HFinite_mult2 divide_inverse starfunNat_real_of_nat) |
507 simp add: starfun_mult [symmetric] divide_inverse |
|
508 starfun_inverse [symmetric] starfunNat_real_of_nat) |
|
509 |
480 |
510 lemma STAR_sin_pi_divide_n_approx: |
481 lemma STAR_sin_pi_divide_n_approx: |
511 "N \<in> HNatInfinite \<Longrightarrow> |
482 assumes "N \<in> HNatInfinite" |
512 ( *f* sin) (( *f* (\<lambda>x. pi / real x)) N) \<approx> |
483 shows "( *f* sin) (( *f* (\<lambda>x. pi / real x)) N) \<approx> hypreal_of_real pi/(hypreal_of_hypnat N)" |
513 hypreal_of_real pi/(hypreal_of_hypnat N)" |
484 proof - |
514 apply (simp add: starfunNat_real_of_nat [symmetric]) |
485 have "\<exists>s. (*f* sin) ((*f* (\<lambda>n. pi / real n)) N) \<approx> s \<and> hypreal_of_real pi / hypreal_of_hypnat N \<approx> s" |
515 apply (rule STAR_sin_Infinitesimal) |
486 by (metis (lifting) Infinitesimal_approx Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal assms starfunNat_pi_divide_n_Infinitesimal) |
516 apply (simp add: divide_inverse) |
487 then show ?thesis |
517 apply (rule Infinitesimal_HFinite_mult2) |
488 by (meson approx_trans2) |
518 apply (subst starfun_inverse) |
489 qed |
519 apply (erule starfunNat_inverse_real_of_nat_Infinitesimal) |
|
520 apply simp |
|
521 done |
|
522 |
490 |
523 lemma NSLIMSEQ_sin_pi: "(\<lambda>n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi" |
491 lemma NSLIMSEQ_sin_pi: "(\<lambda>n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi" |
524 apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat) |
492 proof - |
525 apply (rule_tac f1 = sin in starfun_o2 [THEN subst]) |
493 have *: "hypreal_of_hypnat N * (*f* sin) ((*f* (\<lambda>x. pi / real x)) N) \<approx> hypreal_of_real pi" |
526 apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse) |
494 if "N \<in> HNatInfinite" |
527 apply (rule_tac f1 = inverse in starfun_o2 [THEN subst]) |
495 for N :: "nat star" |
528 apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi |
496 using that |
529 simp add: starfunNat_real_of_nat mult.commute divide_inverse) |
497 by simp (metis STAR_sin_pi_divide_HNatInfinite_approx_pi2 starfunNat_real_of_nat) |
530 done |
498 show ?thesis |
|
499 by (simp add: NSLIMSEQ_def starfunNat_real_of_nat) (metis * starfun_o2) |
|
500 qed |
531 |
501 |
532 lemma NSLIMSEQ_cos_one: "(\<lambda>n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1" |
502 lemma NSLIMSEQ_cos_one: "(\<lambda>n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1" |
533 apply (simp add: NSLIMSEQ_def, auto) |
503 proof - |
534 apply (rule_tac f1 = cos in starfun_o2 [THEN subst]) |
504 have "(*f* cos) ((*f* (\<lambda>x. pi / real x)) N) \<approx> 1" |
535 apply (rule STAR_cos_Infinitesimal) |
505 if "N \<in> HNatInfinite" for N |
536 apply (auto intro!: Infinitesimal_HFinite_mult2 |
506 using that STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal by blast |
537 simp add: starfun_mult [symmetric] divide_inverse |
507 then show ?thesis |
538 starfun_inverse [symmetric] starfunNat_real_of_nat) |
508 by (simp add: NSLIMSEQ_def) (metis STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal starfun_o2) |
539 done |
509 qed |
540 |
510 |
541 lemma NSLIMSEQ_sin_cos_pi: |
511 lemma NSLIMSEQ_sin_cos_pi: |
542 "(\<lambda>n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi" |
512 "(\<lambda>n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi" |
543 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp) |
513 using NSLIMSEQ_cos_one NSLIMSEQ_mult NSLIMSEQ_sin_pi by force |
544 |
514 |
545 |
515 |
546 text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close> |
516 text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close> |
547 |
517 |
548 lemma STAR_cos_Infinitesimal_approx: |
518 lemma STAR_cos_Infinitesimal_approx: |
549 fixes x :: "'a::{real_normed_field,banach} star" |
519 fixes x :: "'a::{real_normed_field,banach} star" |
550 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - x\<^sup>2" |
520 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - x\<^sup>2" |
551 apply (rule STAR_cos_Infinitesimal [THEN approx_trans]) |
521 by (metis Infinitesimal_square_iff STAR_cos_Infinitesimal approx_diff approx_sym diff_zero mem_infmal_iff power2_eq_square) |
552 apply (auto simp add: Infinitesimal_approx_minus [symmetric] |
|
553 add.assoc [symmetric] numeral_2_eq_2) |
|
554 done |
|
555 |
522 |
556 lemma STAR_cos_Infinitesimal_approx2: |
523 lemma STAR_cos_Infinitesimal_approx2: |
557 fixes x :: hypreal \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close> |
524 fixes x :: hypreal \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close> |
558 shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2" |
525 assumes "x \<in> Infinitesimal" |
559 apply (rule STAR_cos_Infinitesimal [THEN approx_trans]) |
526 shows "( *f* cos) x \<approx> 1 - (x\<^sup>2)/2" |
560 apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult |
527 proof - |
561 simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2) |
528 have "1 \<approx> 1 - x\<^sup>2 / 2" |
562 done |
529 using assms |
|
530 by (auto intro: Infinitesimal_SReal_divide simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2) |
|
531 then show ?thesis |
|
532 using STAR_cos_Infinitesimal approx_trans assms by blast |
|
533 qed |
563 |
534 |
564 end |
535 end |