Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Nonstandard_Analysis/HSeries.thy
    Author:     Jacques D. Fleuriot
    Copyright:  1998  University of Cambridge

Converted to Isar and polished by lcp
*)

section \<open>Finite Summation and Infinite Series for Hyperreals\<close>

theory HSeries
  imports HSEQ
begin

definition sumhr :: "hypnat \ hypnat \ (nat \ real) \ hypreal"
  where "sumhr = (\(M,N,f). starfun2 (\m n. sum f {m..

definition NSsums :: "(nat \ real) \ real \ bool" (infixr "NSsums" 80)
  where "f NSsums s = (\n. sum f {..\<^sub>N\<^sub>S s"

definition NSsummable :: "(nat \ real) \ bool"
  where "NSsummable f \ (\s. f NSsums s)"

definition NSsuminf :: "(nat \ real) \ real"
  where "NSsuminf f = (THE s. f NSsums s)"

lemma sumhr_app: "sumhr (M, N, f) = ( *f2* (\m n. sum f {m..
  by (simp add: sumhr_def)

text \<open>Base case in definition of \<^term>\<open>sumr\<close>.\<close>
lemma sumhr_zero [simp]: "\m. sumhr (m, 0, f) = 0"
  unfolding sumhr_app by transfer simp

text \<open>Recursive case in definition of \<^term>\<open>sumr\<close>.\<close>
lemma sumhr_if:
  "\m n. sumhr (m, n + 1, f) = (if n + 1 \ m then 0 else sumhr (m, n, f) + ( *f* f) n)"
  unfolding sumhr_app by transfer simp

lemma sumhr_Suc_zero [simp]: "\n. sumhr (n + 1, n, f) = 0"
  unfolding sumhr_app by transfer simp

lemma sumhr_eq_bounds [simp]: "\n. sumhr (n, n, f) = 0"
  unfolding sumhr_app by transfer simp

lemma sumhr_Suc [simp]: "\m. sumhr (m, m + 1, f) = ( *f* f) m"
  unfolding sumhr_app by transfer simp

lemma sumhr_add_lbound_zero [simp]: "\k m. sumhr (m + k, k, f) = 0"
  unfolding sumhr_app by transfer simp

lemma sumhr_add: "\m n. sumhr (m, n, f) + sumhr (m, n, g) = sumhr (m, n, \i. f i + g i)"
  unfolding sumhr_app by transfer (rule sum.distrib [symmetric])

lemma sumhr_mult: "\m n. hypreal_of_real r * sumhr (m, n, f) = sumhr (m, n, \n. r * f n)"
  unfolding sumhr_app by transfer (rule sum_distrib_left)

lemma sumhr_split_add: "\n p. n < p \ sumhr (0, n, f) + sumhr (n, p, f) = sumhr (0, p, f)"
  unfolding sumhr_app by transfer (simp add: sum.atLeastLessThan_concat)

lemma sumhr_split_diff: "n < p \ sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n, p, f)"
  by (drule sumhr_split_add [symmetric, where f = f]) simp

lemma sumhr_hrabs: "\m n. \sumhr (m, n, f)\ \ sumhr (m, n, \i. \f i\)"
  unfolding sumhr_app by transfer (rule sum_abs)

text \<open>Other general version also needed.\<close>
lemma sumhr_fun_hypnat_eq:
  "(\r. m \ r \ r < n \ f r = g r) \
    sumhr (hypnat_of_nat m, hypnat_of_nat n, f) =
    sumhr (hypnat_of_nat m, hypnat_of_nat n, g)"
  unfolding sumhr_app by transfer simp

lemma sumhr_const: "\n. sumhr (0, n, \i. r) = hypreal_of_hypnat n * hypreal_of_real r"
  unfolding sumhr_app by transfer simp

lemma sumhr_less_bounds_zero [simp]: "\m n. n < m \ sumhr (m, n, f) = 0"
  unfolding sumhr_app by transfer simp

lemma sumhr_minus: "\m n. sumhr (m, n, \i. - f i) = - sumhr (m, n, f)"
  unfolding sumhr_app by transfer (rule sum_negf)

lemma sumhr_shift_bounds:
  "\m n. sumhr (m + hypnat_of_nat k, n + hypnat_of_nat k, f) =
    sumhr (m, n, \<lambda>i. f (i + k))"
  unfolding sumhr_app by transfer (rule sum.shift_bounds_nat_ivl)

subsection \<open>Nonstandard Sums\<close>

text \<open>Infinite sums are obtained by summing to some infinite hypernatural
  (such as \<^term>\<open>whn\<close>).\<close>
lemma sumhr_hypreal_of_hypnat_omega: "sumhr (0, whn, \i. 1) = hypreal_of_hypnat whn"
  by (simp add: sumhr_const)

lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, \i. 1) = \ - 1"
  apply (simp add: sumhr_const)
    (* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
    (* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
  apply (unfold star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def)
  apply (simp add: starfun_star_n starfun2_star_n)
  done

lemma sumhr_minus_one_realpow_zero [simp]: "\N. sumhr (0, N + N, \i. (-1) ^ (i + 1)) = 0"
  unfolding sumhr_app
  apply transfer
  apply (simp del: power_Suc add: mult_2 [symmetric])
  apply (induct_tac N)
   apply simp_all
  done

lemma sumhr_interval_const:
  "(\n. m \ Suc n \ f n = r) \ m \ na \
    sumhr (hypnat_of_nat m, hypnat_of_nat na, f) = hypreal_of_nat (na - m) * hypreal_of_real r"
  unfolding sumhr_app by transfer simp

lemma starfunNat_sumr: "\N. ( *f* (\n. sum f {0..
  unfolding sumhr_app by transfer (rule refl)

lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f) \ sumhr (0, N, f) \ \sumhr (M, N, f)\ \ 0"
  using linorder_less_linear [where x = M and y = N]
  by (metis (no_types, lifting) abs_zero approx_hrabs approx_minus_iff approx_refl approx_sym sumhr_eq_bounds sumhr_less_bounds_zero sumhr_split_diff)

subsection \<open>Infinite sums: Standard and NS theorems\<close>

lemma sums_NSsums_iff: "f sums l \ f NSsums l"
  by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)

lemma summable_NSsummable_iff: "summable f \ NSsummable f"
  by (simp add: summable_def NSsummable_def sums_NSsums_iff)

lemma suminf_NSsuminf_iff: "suminf f = NSsuminf f"
  by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)

lemma NSsums_NSsummable: "f NSsums l \ NSsummable f"
  unfolding NSsums_def NSsummable_def by blast

lemma NSsummable_NSsums: "NSsummable f \ f NSsums (NSsuminf f)"
  unfolding NSsummable_def NSsuminf_def NSsums_def
  by (blast intro: theI NSLIMSEQ_unique)

lemma NSsums_unique: "f NSsums s \ s = NSsuminf f"
  by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)

lemma NSseries_zero: "\m. n \ Suc m \ f m = 0 \ f NSsums (sum f {..
  by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)

lemma NSsummable_NSCauchy:
  "NSsummable f \ (\M \ HNatInfinite. \N \ HNatInfinite. \sumhr (M, N, f)\ \ 0)"
  apply (auto simp add: summable_NSsummable_iff [symmetric]
      summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
      NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
  apply (cut_tac x = M and y = N in linorder_less_linear)
  by (metis approx_hrabs_zero_cancel approx_minus_iff approx_refl approx_sym sumhr_split_diff)

text \<open>Terms of a convergent series tend to zero.\<close>
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \ f \\<^sub>N\<^sub>S 0"
  apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
  by (metis HNatInfinite_add approx_hrabs_zero_cancel sumhr_Suc)

text \<open>Nonstandard comparison test.\<close>
lemma NSsummable_comparison_test: "\N. \n. N \ n \ \f n\ \ g n \ NSsummable g \ NSsummable f"
  by (metis real_norm_def summable_NSsummable_iff summable_comparison_test)

lemma NSsummable_rabs_comparison_test:
  "\N. \n. N \ n \ \f n\ \ g n \ NSsummable g \ NSsummable (\k. \f k\)"
  by (rule NSsummable_comparison_test) auto

end

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.