SSL HTranscendental.thy

(*  Title:      HOL/Nonstandard_Analysis/HTranscendental.thy
  Author: Jacques D. Fleuriot
  Copyright: 2001 University of Edinburgh
 
 Converted to Isar and polished by lcp
*)

section‹Nonstandard Extensions of Transcendental Functions›

theory HTranscendental
imports Complex_Main HSeries HDeriv
begin

definition
  exphr :: "real ==> hypreal" where
    🍋 ‹define exponential function using standard part›
  "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‹Nonstandard Extension of Square Root Function›

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)🪙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🪙2] ==> ( *f* sqrt) x < u"
proof transfer
  show "∧x u. [0 < u; x < u🪙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🪙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🪙2 + y🪙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 hypreal_sqrt_pow2_iff power2_eq_square)

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 ‹NSDERIV exp 0 :> 1› 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<----🪙N🪙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‹exp maps infinities to infinities›
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: ‹0 ≤ x›)
  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‹exp maps infinitesimals to infinitesimals›
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 ‹x = - y› 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 ‹u ∈ ℝ› 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 ‹Proving $\sin* (1/n) \times 1/(1/n) \approx 1$ for $n = \infty$ ›

lemma lemma_sin_pi:
  "n ∈ HNatInfinite
      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) ≈ 1"
  by (simp add: STAR_sin_Infinitesimal_divide zero_less_HNatInfinite)

lemma STAR_sin_inverse_HNatInfinite:
     "n ∈ HNatInfinite
      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n ≈ 1"
  by (metis field_class.field_divide_inverse inverse_inverse_eq lemma_sin_pi)

lemma Infinitesimal_pi_divide_HNatInfinite: 
     "N ∈ HNatInfinite
      ==> hypreal_of_real pi/(hypreal_of_hypnat N) ∈ 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
      ==> hypreal_of_hypnat n * ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) ≈ 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)) <----🪙N🪙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))<----🪙N🪙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)) <----🪙N🪙S pi"
  using NSLIMSEQ_cos_one NSLIMSEQ_mult NSLIMSEQ_sin_pi by force


text‹A familiar approximation to 🍋‹cos x› when 🍋‹x› is small›

lemma STAR_cos_Infinitesimal_approx:
  fixes x :: "'a::{real_normed_field,banach} star"
  shows "x ∈ Infinitesimal ==> ( *f* cos) x ≈ 1 - x🪙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🪙2)/2"
proof -
  have "1 ≈ 1 - x🪙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