|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Fraction_Field.thy
Sprache: Isabelle
|
|
(* Title: HOL/Nonstandard_Analysis/HTranscendental.thy
Author: Jacques D. Fleuriot
Copyright: 2001 University of Edinburgh
Converted to Isar and polished by lcp
*)
section\<open>Nonstandard Extensions of Transcendental Functions\<close>
theory HTranscendental
imports Complex_Main HSeries HDeriv
begin
definition
exphr :: "real \ hypreal" where
\<comment> \<open>define exponential function using standard part\<close>
"exphr x \ st(sumhr (0, whn, \n. inverse (fact n) * (x ^ n)))"
definition
sinhr :: "real \ hypreal" where
"sinhr x \ st(sumhr (0, whn, \n. sin_coeff n * x ^ n))"
definition
coshr :: "real \ hypreal" where
"coshr x \ st(sumhr (0, whn, \n. cos_coeff n * x ^ n))"
subsection\<open>Nonstandard Extension of Square Root Function\<close>
lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
by (simp add: starfun star_n_zero_num)
lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
by (simp add: starfun star_n_one_num)
lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \ x)"
proof (cases x)
case (star_n X)
then show ?thesis
by (simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff del: hpowr_Suc power_Suc)
qed
lemma hypreal_sqrt_gt_zero_pow2: "\x. 0 < x \ ( *f* sqrt) (x) ^ 2 = x"
by transfer simp
lemma hypreal_sqrt_pow2_gt_zero: "0 < x \ 0 < ( *f* sqrt) (x) ^ 2"
by (frule hypreal_sqrt_gt_zero_pow2, auto)
lemma hypreal_sqrt_not_zero: "0 < x \ ( *f* sqrt) (x) \ 0"
using hypreal_sqrt_gt_zero_pow2 by fastforce
lemma hypreal_inverse_sqrt_pow2:
"0 < x \ inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
by (simp add: hypreal_sqrt_gt_zero_pow2 power_inverse)
lemma hypreal_sqrt_mult_distrib:
"\x y. \0 < x; 0 \
( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
by transfer (auto intro: real_sqrt_mult)
lemma hypreal_sqrt_mult_distrib2:
"\0\x; 0\y\ \ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
lemma hypreal_sqrt_approx_zero [simp]:
assumes "0 < x"
shows "(( *f* sqrt) x \ 0) \ (x \ 0)"
proof -
have "( *f* sqrt) x \ Infinitesimal \ ((*f* sqrt) x)\<^sup>2 \ Infinitesimal"
by (metis Infinitesimal_hrealpow pos2 power2_eq_square Infinitesimal_square_iff)
also have "... \ x \ Infinitesimal"
by (simp add: assms hypreal_sqrt_gt_zero_pow2)
finally show ?thesis
using mem_infmal_iff by blast
qed
lemma hypreal_sqrt_approx_zero2 [simp]:
"0 \ x \ (( *f* sqrt)(x) \ 0) = (x \ 0)"
by (auto simp add: order_le_less)
lemma hypreal_sqrt_gt_zero: "\x. 0 < x \ 0 < ( *f* sqrt)(x)"
by transfer (simp add: real_sqrt_gt_zero)
lemma hypreal_sqrt_ge_zero: "0 \ x \ 0 \ ( *f* sqrt)(x)"
by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
lemma hypreal_sqrt_lessI:
"\x u. \0 < u; x < u\<^sup>2\ \ ( *f* sqrt) x < u"
proof transfer
show "\x u. \0 < u; x < u\<^sup>2\ \ sqrt x < u"
by (metis less_le real_sqrt_less_iff real_sqrt_pow2 real_sqrt_power)
qed
lemma hypreal_sqrt_hrabs [simp]: "\x. ( *f* sqrt)(x\<^sup>2) = \x\"
by transfer simp
lemma hypreal_sqrt_hrabs2 [simp]: "\x. ( *f* sqrt)(x*x) = \x\"
by transfer simp
lemma hypreal_sqrt_hyperpow_hrabs [simp]:
"\x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \x\"
by transfer simp
lemma star_sqrt_HFinite: "\x \ HFinite; 0 \ x\ \ ( *f* sqrt) x \ HFinite"
by (metis HFinite_square_iff hypreal_sqrt_pow2_iff power2_eq_square)
lemma st_hypreal_sqrt:
assumes "x \ HFinite" "0 \ x"
shows "st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
proof (rule power_inject_base)
show "st ((*f* sqrt) x) ^ Suc 1 = (*f* sqrt) (st x) ^ Suc 1"
using assms hypreal_sqrt_pow2_iff [of x]
by (metis HFinite_square_iff hypreal_sqrt_hrabs2 power2_eq_square st_hrabs st_mult)
show "0 \ st ((*f* sqrt) x)"
by (simp add: assms hypreal_sqrt_ge_zero st_zero_le star_sqrt_HFinite)
show "0 \ (*f* sqrt) (st x)"
by (simp add: assms hypreal_sqrt_ge_zero st_zero_le)
qed
lemma hypreal_sqrt_sum_squares_ge1 [simp]: "\x y. x \ ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
by transfer (rule real_sqrt_sum_squares_ge1)
lemma HFinite_hypreal_sqrt_imp_HFinite:
"\0 \ x; ( *f* sqrt) x \ HFinite\ \ x \ HFinite"
by (metis HFinite_mult hrealpow_two hypreal_sqrt_pow2_iff numeral_2_eq_2)
lemma HFinite_hypreal_sqrt_iff [simp]:
"0 \ x \ (( *f* sqrt) x \ HFinite) = (x \ HFinite)"
by (blast intro: star_sqrt_HFinite HFinite_hypreal_sqrt_imp_HFinite)
lemma Infinitesimal_hypreal_sqrt:
"\0 \ x; x \ Infinitesimal\ \ ( *f* sqrt) x \ Infinitesimal"
by (simp add: mem_infmal_iff)
lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
"\0 \ x; ( *f* sqrt) x \ Infinitesimal\ \ x \ Infinitesimal"
using hypreal_sqrt_approx_zero2 mem_infmal_iff by blast
lemma Infinitesimal_hypreal_sqrt_iff [simp]:
"0 \ x \ (( *f* sqrt) x \ Infinitesimal) = (x \ Infinitesimal)"
by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
lemma HInfinite_hypreal_sqrt:
"\0 \ x; x \ HInfinite\ \ ( *f* sqrt) x \ HInfinite"
by (simp add: HInfinite_HFinite_iff)
lemma HInfinite_hypreal_sqrt_imp_HInfinite:
"\0 \ x; ( *f* sqrt) x \ HInfinite\ \ x \ HInfinite"
using HFinite_hypreal_sqrt_iff HInfinite_HFinite_iff by blast
lemma HInfinite_hypreal_sqrt_iff [simp]:
"0 \ x \ (( *f* sqrt) x \ HInfinite) = (x \ HInfinite)"
by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
lemma HFinite_exp [simp]:
"sumhr (0, whn, \n. inverse (fact n) * x ^ n) \ HFinite"
unfolding sumhr_app star_zero_def starfun2_star_of atLeast0LessThan
by (metis NSBseqD2 NSconvergent_NSBseq convergent_NSconvergent_iff summable_iff_convergent summable_exp)
lemma exphr_zero [simp]: "exphr 0 = 1"
proof -
have "\x>1. 1 = sumhr (0, 1, \n. inverse (fact n) * 0 ^ n) + sumhr (1, x, \n. inverse (fact n) * 0 ^ n)"
unfolding sumhr_app by transfer (simp add: power_0_left)
then have "sumhr (0, 1, \n. inverse (fact n) * 0 ^ n) + sumhr (1, whn, \n. inverse (fact n) * 0 ^ n) \ 1"
by auto
then show ?thesis
unfolding exphr_def
using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto
qed
lemma coshr_zero [simp]: "coshr 0 = 1"
proof -
have "\x>1. 1 = sumhr (0, 1, \n. cos_coeff n * 0 ^ n) + sumhr (1, x, \n. cos_coeff n * 0 ^ n)"
unfolding sumhr_app by transfer (simp add: power_0_left)
then have "sumhr (0, 1, \n. cos_coeff n * 0 ^ n) + sumhr (1, whn, \n. cos_coeff n * 0 ^ n) \ 1"
by auto
then show ?thesis
unfolding coshr_def
using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto
qed
lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \ 1"
proof -
have "(*f* exp) (0::real star) = 1"
by transfer simp
then show ?thesis
by auto
qed
lemma STAR_exp_Infinitesimal:
assumes "x \ Infinitesimal" shows "( *f* exp) (x::hypreal) \ 1"
proof (cases "x = 0")
case False
have "NSDERIV exp 0 :> 1"
by (metis DERIV_exp NSDERIV_DERIV_iff exp_zero)
then have "((*f* exp) x - 1) / x \ 1"
using nsderiv_def False NSDERIVD2 assms by fastforce
then have "(*f* exp) x - 1 \ x"
using NSDERIVD4 \<open>NSDERIV exp 0 :> 1\<close> assms by fastforce
then show ?thesis
by (meson Infinitesimal_approx approx_minus_iff approx_trans2 assms not_Infinitesimal_not_zero)
qed auto
lemma STAR_exp_epsilon [simp]: "( *f* exp) \ \ 1"
by (auto intro: STAR_exp_Infinitesimal)
lemma STAR_exp_add:
"\(x::'a:: {banach,real_normed_field} star) y. ( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
by transfer (rule exp_add)
lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
proof -
have "(\n. inverse (fact n) * x ^ n) sums exp x"
using exp_converges [of x] by simp
then have "(\n. \n\<^sub>N\<^sub>S exp x"
using NSsums_def sums_NSsums_iff by blast
then have "hypreal_of_real (exp x) \ sumhr (0, whn, \n. inverse (fact n) * x ^ n)"
unfolding starfunNat_sumr [symmetric] atLeast0LessThan
using HNatInfinite_whn NSLIMSEQ_def approx_sym by blast
then show ?thesis
unfolding exphr_def using st_eq_approx_iff by auto
qed
lemma starfun_exp_ge_add_one_self [simp]: "\x::hypreal. 0 \ x \ (1 + x) \ ( *f* exp) x"
by transfer (rule exp_ge_add_one_self_aux)
text\<open>exp maps infinities to infinities\<close>
lemma starfun_exp_HInfinite:
fixes x :: hypreal
assumes "x \ HInfinite" "0 \ x"
shows "( *f* exp) x \ HInfinite"
proof -
have "x \ 1 + x"
by simp
also have "\ \ (*f* exp) x"
by (simp add: \<open>0 \<le> x\<close>)
finally show ?thesis
using HInfinite_ge_HInfinite assms by blast
qed
lemma starfun_exp_minus:
"\x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
by transfer (rule exp_minus)
text\<open>exp maps infinitesimals to infinitesimals\<close>
lemma starfun_exp_Infinitesimal:
fixes x :: hypreal
assumes "x \ HInfinite" "x \ 0"
shows "( *f* exp) x \ Infinitesimal"
proof -
obtain y where "x = -y" "y \ 0"
by (metis abs_of_nonpos assms(2) eq_abs_iff')
then have "( *f* exp) y \ HInfinite"
using HInfinite_minus_iff assms(1) starfun_exp_HInfinite by blast
then show ?thesis
by (simp add: HInfinite_inverse_Infinitesimal \<open>x = - y\<close> starfun_exp_minus)
qed
lemma starfun_exp_gt_one [simp]: "\x::hypreal. 0 < x \ 1 < ( *f* exp) x"
by transfer (rule exp_gt_one)
abbreviation real_ln :: "real \ real" where
"real_ln \ ln"
lemma starfun_ln_exp [simp]: "\x. ( *f* real_ln) (( *f* exp) x) = x"
by transfer (rule ln_exp)
lemma starfun_exp_ln_iff [simp]: "\x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
by transfer (rule exp_ln_iff)
lemma starfun_exp_ln_eq: "\u x. ( *f* exp) u = x \ ( *f* real_ln) x = u"
by transfer (rule ln_unique)
lemma starfun_ln_less_self [simp]: "\x. 0 < x \ ( *f* real_ln) x < x"
by transfer (rule ln_less_self)
lemma starfun_ln_ge_zero [simp]: "\x. 1 \ x \ 0 \ ( *f* real_ln) x"
by transfer (rule ln_ge_zero)
lemma starfun_ln_gt_zero [simp]: "\x .1 < x \ 0 < ( *f* real_ln) x"
by transfer (rule ln_gt_zero)
lemma starfun_ln_not_eq_zero [simp]: "\x. \0 < x; x \ 1\ \ ( *f* real_ln) x \ 0"
by transfer simp
lemma starfun_ln_HFinite: "\x \ HFinite; 1 \ x\ \ ( *f* real_ln) x \ HFinite"
by (metis HFinite_HInfinite_iff less_le_trans starfun_exp_HInfinite starfun_exp_ln_iff starfun_ln_ge_zero zero_less_one)
lemma starfun_ln_inverse: "\x. 0 < x \ ( *f* real_ln) (inverse x) = -( *f* ln) x"
by transfer (rule ln_inverse)
lemma starfun_abs_exp_cancel: "\x. \( *f* exp) (x::hypreal)\ = ( *f* exp) x"
by transfer (rule abs_exp_cancel)
lemma starfun_exp_less_mono: "\x y::hypreal. x < y \ ( *f* exp) x < ( *f* exp) y"
by transfer (rule exp_less_mono)
lemma starfun_exp_HFinite:
fixes x :: hypreal
assumes "x \ HFinite"
shows "( *f* exp) x \ HFinite"
proof -
obtain u where "u \ \" "\x\ < u"
using HFiniteD assms by force
with assms have "\(*f* exp) x\ < (*f* exp) u"
using starfun_abs_exp_cancel starfun_exp_less_mono by auto
with \<open>u \<in> \<real>\<close> show ?thesis
by (force simp: HFinite_def Reals_eq_Standard)
qed
lemma starfun_exp_add_HFinite_Infinitesimal_approx:
fixes x :: hypreal
shows "\x \ Infinitesimal; z \ HFinite\ \ ( *f* exp) (z + x::hypreal) \ ( *f* exp) z"
using STAR_exp_Infinitesimal approx_mult2 starfun_exp_HFinite by (fastforce simp add: STAR_exp_add)
lemma starfun_ln_HInfinite:
"\x \ HInfinite; 0 < x\ \ ( *f* real_ln) x \ HInfinite"
by (metis HInfinite_HFinite_iff starfun_exp_HFinite starfun_exp_ln_iff)
lemma starfun_exp_HInfinite_Infinitesimal_disj:
fixes x :: hypreal
shows "x \ HInfinite \ ( *f* exp) x \ HInfinite \ ( *f* exp) (x::hypreal) \ Infinitesimal"
by (meson linear starfun_exp_HInfinite starfun_exp_Infinitesimal)
lemma starfun_ln_HFinite_not_Infinitesimal:
"\x \ HFinite - Infinitesimal; 0 < x\ \ ( *f* real_ln) x \ HFinite"
by (metis DiffD1 DiffD2 HInfinite_HFinite_iff starfun_exp_HInfinite_Infinitesimal_disj starfun_exp_ln_iff)
(* we do proof by considering ln of 1/x *)
lemma starfun_ln_Infinitesimal_HInfinite:
assumes "x \ Infinitesimal" "0 < x"
shows "( *f* real_ln) x \ HInfinite"
proof -
have "inverse x \ HInfinite"
using Infinitesimal_inverse_HInfinite assms by blast
then show ?thesis
using HInfinite_minus_iff assms(2) starfun_ln_HInfinite starfun_ln_inverse by fastforce
qed
lemma starfun_ln_less_zero: "\x. \0 < x; x < 1\ \ ( *f* real_ln) x < 0"
by transfer (rule ln_less_zero)
lemma starfun_ln_Infinitesimal_less_zero:
"\x \ Infinitesimal; 0 < x\ \ ( *f* real_ln) x < 0"
by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
lemma starfun_ln_HInfinite_gt_zero:
"\x \ HInfinite; 0 < x\ \ 0 < ( *f* real_ln) x"
by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
lemma HFinite_sin [simp]: "sumhr (0, whn, \n. sin_coeff n * x ^ n) \ HFinite"
proof -
have "summable (\i. sin_coeff i * x ^ i)"
using summable_norm_sin [of x] by (simp add: summable_rabs_cancel)
then have "(*f* (\n. \n HFinite"
unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_def
using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast
then show ?thesis
unfolding sumhr_app
by (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
qed
lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
by transfer (rule sin_zero)
lemma STAR_sin_Infinitesimal [simp]:
fixes x :: "'a::{real_normed_field,banach} star"
assumes "x \ Infinitesimal"
shows "( *f* sin) x \ x"
proof (cases "x = 0")
case False
have "NSDERIV sin 0 :> 1"
by (metis DERIV_sin NSDERIV_DERIV_iff cos_zero)
then have "(*f* sin) x / x \ 1"
using False NSDERIVD2 assms by fastforce
with assms show ?thesis
unfolding star_one_def
by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite)
qed auto
lemma HFinite_cos [simp]: "sumhr (0, whn, \n. cos_coeff n * x ^ n) \ HFinite"
proof -
have "summable (\i. cos_coeff i * x ^ i)"
using summable_norm_cos [of x] by (simp add: summable_rabs_cancel)
then have "(*f* (\n. \n HFinite"
unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_def
using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast
then show ?thesis
unfolding sumhr_app
by (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
qed
lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
by transfer (rule cos_zero)
lemma STAR_cos_Infinitesimal [simp]:
fixes x :: "'a::{real_normed_field,banach} star"
assumes "x \ Infinitesimal"
shows "( *f* cos) x \ 1"
proof (cases "x = 0")
case False
have "NSDERIV cos 0 :> 0"
by (metis DERIV_cos NSDERIV_DERIV_iff add.inverse_neutral sin_zero)
then have "(*f* cos) x - 1 \ 0"
using NSDERIV_approx assms by fastforce
with assms show ?thesis
using approx_minus_iff by blast
qed auto
lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
by transfer (rule tan_zero)
lemma STAR_tan_Infinitesimal [simp]:
assumes "x \ Infinitesimal"
shows "( *f* tan) x \ x"
proof (cases "x = 0")
case False
have "NSDERIV tan 0 :> 1"
using DERIV_tan [of 0] by (simp add: NSDERIV_DERIV_iff)
then have "(*f* tan) x / x \ 1"
using False NSDERIVD2 assms by fastforce
with assms show ?thesis
unfolding star_one_def
by (metis False Infinitesimal_approx Infinitesimal_ratio approx_star_of_HFinite)
qed auto
lemma STAR_sin_cos_Infinitesimal_mult:
fixes x :: "'a::{real_normed_field,banach} star"
shows "x \ Infinitesimal \ ( *f* sin) x * ( *f* cos) x \ x"
using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1]
by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
lemma HFinite_pi: "hypreal_of_real pi \ HFinite"
by simp
lemma STAR_sin_Infinitesimal_divide:
fixes x :: "'a::{real_normed_field,banach} star"
shows "\x \ Infinitesimal; x \ 0\ \ ( *f* sin) x/x \ 1"
using DERIV_sin [of "0::'a"]
by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
subsection \<open>Proving $\sin* (1/n) \times 1/(1/n) \approx 1$ for $n = \infty$ \<close>
lemma lemma_sin_pi:
"n \ HNatInfinite
\<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
by (simp add: STAR_sin_Infinitesimal_divide zero_less_HNatInfinite)
lemma STAR_sin_inverse_HNatInfinite:
"n \ HNatInfinite
\<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
by (metis field_class.field_divide_inverse inverse_inverse_eq lemma_sin_pi)
lemma Infinitesimal_pi_divide_HNatInfinite:
"N \ HNatInfinite
\<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
by (simp add: Infinitesimal_HFinite_mult2 field_class.field_divide_inverse)
lemma pi_divide_HNatInfinite_not_zero [simp]:
"N \ HNatInfinite \ hypreal_of_real pi/(hypreal_of_hypnat N) \ 0"
by (simp add: zero_less_HNatInfinite)
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
assumes "n \ HNatInfinite"
shows "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) * hypreal_of_hypnat n \
hypreal_of_real pi"
proof -
have "(*f* sin) (hypreal_of_real pi / hypreal_of_hypnat n) / (hypreal_of_real pi / hypreal_of_hypnat n) \ 1"
using Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal_divide assms pi_divide_HNatInfinite_not_zero by blast
then have "hypreal_of_hypnat n * star_of sin \ (hypreal_of_real pi / hypreal_of_hypnat n) / hypreal_of_real pi \ 1"
by (simp add: mult.commute starfun_def)
then show ?thesis
apply (simp add: starfun_def field_simps)
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)
qed
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
"n \ HNatInfinite
\<Longrightarrow> hypreal_of_hypnat n * ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \<approx> hypreal_of_real pi"
by (metis STAR_sin_pi_divide_HNatInfinite_approx_pi mult.commute)
lemma starfunNat_pi_divide_n_Infinitesimal:
"N \ HNatInfinite \ ( *f* (\x. pi / real x)) N \ Infinitesimal"
by (simp add: Infinitesimal_HFinite_mult2 divide_inverse starfunNat_real_of_nat)
lemma STAR_sin_pi_divide_n_approx:
assumes "N \ HNatInfinite"
shows "( *f* sin) (( *f* (\x. pi / real x)) N) \ hypreal_of_real pi/(hypreal_of_hypnat N)"
proof -
have "\s. (*f* sin) ((*f* (\n. pi / real n)) N) \ s \ hypreal_of_real pi / hypreal_of_hypnat N \ s"
by (metis (lifting) Infinitesimal_approx Infinitesimal_pi_divide_HNatInfinite STAR_sin_Infinitesimal assms starfunNat_pi_divide_n_Infinitesimal)
then show ?thesis
by (meson approx_trans2)
qed
lemma NSLIMSEQ_sin_pi: "(\n. real n * sin (pi / real n)) \\<^sub>N\<^sub>S pi"
proof -
have *: "hypreal_of_hypnat N * (*f* sin) ((*f* (\x. pi / real x)) N) \ hypreal_of_real pi"
if "N \ HNatInfinite"
for N :: "nat star"
using that
by simp (metis STAR_sin_pi_divide_HNatInfinite_approx_pi2 starfunNat_real_of_nat)
show ?thesis
by (simp add: NSLIMSEQ_def starfunNat_real_of_nat) (metis * starfun_o2)
qed
lemma NSLIMSEQ_cos_one: "(\n. cos (pi / real n))\\<^sub>N\<^sub>S 1"
proof -
have "(*f* cos) ((*f* (\x. pi / real x)) N) \ 1"
if "N \ HNatInfinite" for N
using that STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal by blast
then show ?thesis
by (simp add: NSLIMSEQ_def) (metis STAR_cos_Infinitesimal starfunNat_pi_divide_n_Infinitesimal starfun_o2)
qed
lemma NSLIMSEQ_sin_cos_pi:
"(\n. real n * sin (pi / real n) * cos (pi / real n)) \\<^sub>N\<^sub>S pi"
using NSLIMSEQ_cos_one NSLIMSEQ_mult NSLIMSEQ_sin_pi by force
text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close>
lemma STAR_cos_Infinitesimal_approx:
fixes x :: "'a::{real_normed_field,banach} star"
shows "x \ Infinitesimal \ ( *f* cos) x \ 1 - x\<^sup>2"
by (metis Infinitesimal_square_iff STAR_cos_Infinitesimal approx_diff approx_sym diff_zero mem_infmal_iff power2_eq_square)
lemma STAR_cos_Infinitesimal_approx2:
fixes x :: hypreal
assumes "x \ Infinitesimal"
shows "( *f* cos) x \ 1 - (x\<^sup>2)/2"
proof -
have "1 \ 1 - x\<^sup>2 / 2"
using assms
by (auto intro: Infinitesimal_SReal_divide simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
then show ?thesis
using STAR_cos_Infinitesimal approx_trans assms by blast
qed
end
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
