Quelle HSeries.thy Sprache: 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 whn_eq_\<omega>m1: "hypreal_of_hypnat whn = \<omega> - 1"
  unfolding star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def
  by (simp add: starfun_star_n starfun2_star_n)

lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, \i. 1) = \ - 1"
  by (simp add: sumhr_const whn_eq_\<omega>m1)

lemma sumhr_minus_one_realpow_zero [simp]: "\N. sumhr (0, N + N, \i. (-1) ^ (i + 1)) = 0"
  unfolding sumhr_app
  by transfer (induct_tac N, auto)

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)" (is "?L=?R")
proof -
  have "?L = (\M\HNatInfinite. \N\HNatInfinite. sumhr (0, M, f) \ sumhr (0, N, f))"
    by (auto simp add: summable_iff_convergent convergent_NSconvergent_iff NSCauchy_def starfunNat_sumr
        simp flip: NSCauchy_NSconvergent_iff summable_NSsummable_iff atLeast0LessThan)
  also have "... \ ?R"
    by (metis approx_hrabs_zero_cancel approx_minus_iff approx_refl approx_sym linorder_less_linear sumhr_hrabs_approx sumhr_split_diff)
  finally show ?thesis .
qed

text \<open>Terms of a convergent series tend to zero.\<close>
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \ f \\<^sub>N\<^sub>S 0"
  by (metis HNatInfinite_add NSLIMSEQ_def NSsummable_NSCauchy approx_hrabs_zero_cancel star_of_zero 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

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.