src/HOL/Nonstandard_Analysis/HSeries.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64604 2bf8cfc98c4d
child 68644 242d298526a3
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Nonstandard_Analysis/HSeries.thy
     2     Author:     Jacques D. Fleuriot
     3     Copyright:  1998  University of Cambridge
     4 
     5 Converted to Isar and polished by lcp
     6 *)
     7 
     8 section \<open>Finite Summation and Infinite Series for Hyperreals\<close>
     9 
    10 theory HSeries
    11   imports HSEQ
    12 begin
    13 
    14 definition sumhr :: "hypnat \<times> hypnat \<times> (nat \<Rightarrow> real) \<Rightarrow> hypreal"
    15   where "sumhr = (\<lambda>(M,N,f). starfun2 (\<lambda>m n. sum f {m..<n}) M N)"
    16 
    17 definition NSsums :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"  (infixr "NSsums" 80)
    18   where "f NSsums s = (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
    19 
    20 definition NSsummable :: "(nat \<Rightarrow> real) \<Rightarrow> bool"
    21   where "NSsummable f \<longleftrightarrow> (\<exists>s. f NSsums s)"
    22 
    23 definition NSsuminf :: "(nat \<Rightarrow> real) \<Rightarrow> real"
    24   where "NSsuminf f = (THE s. f NSsums s)"
    25 
    26 lemma sumhr_app: "sumhr (M, N, f) = ( *f2* (\<lambda>m n. sum f {m..<n})) M N"
    27   by (simp add: sumhr_def)
    28 
    29 text \<open>Base case in definition of @{term sumr}.\<close>
    30 lemma sumhr_zero [simp]: "\<And>m. sumhr (m, 0, f) = 0"
    31   unfolding sumhr_app by transfer simp
    32 
    33 text \<open>Recursive case in definition of @{term sumr}.\<close>
    34 lemma sumhr_if:
    35   "\<And>m n. sumhr (m, n + 1, f) = (if n + 1 \<le> m then 0 else sumhr (m, n, f) + ( *f* f) n)"
    36   unfolding sumhr_app by transfer simp
    37 
    38 lemma sumhr_Suc_zero [simp]: "\<And>n. sumhr (n + 1, n, f) = 0"
    39   unfolding sumhr_app by transfer simp
    40 
    41 lemma sumhr_eq_bounds [simp]: "\<And>n. sumhr (n, n, f) = 0"
    42   unfolding sumhr_app by transfer simp
    43 
    44 lemma sumhr_Suc [simp]: "\<And>m. sumhr (m, m + 1, f) = ( *f* f) m"
    45   unfolding sumhr_app by transfer simp
    46 
    47 lemma sumhr_add_lbound_zero [simp]: "\<And>k m. sumhr (m + k, k, f) = 0"
    48   unfolding sumhr_app by transfer simp
    49 
    50 lemma sumhr_add: "\<And>m n. sumhr (m, n, f) + sumhr (m, n, g) = sumhr (m, n, \<lambda>i. f i + g i)"
    51   unfolding sumhr_app by transfer (rule sum.distrib [symmetric])
    52 
    53 lemma sumhr_mult: "\<And>m n. hypreal_of_real r * sumhr (m, n, f) = sumhr (m, n, \<lambda>n. r * f n)"
    54   unfolding sumhr_app by transfer (rule sum_distrib_left)
    55 
    56 lemma sumhr_split_add: "\<And>n p. n < p \<Longrightarrow> sumhr (0, n, f) + sumhr (n, p, f) = sumhr (0, p, f)"
    57   unfolding sumhr_app by transfer (simp add: sum_add_nat_ivl)
    58 
    59 lemma sumhr_split_diff: "n < p \<Longrightarrow> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n, p, f)"
    60   by (drule sumhr_split_add [symmetric, where f = f]) simp
    61 
    62 lemma sumhr_hrabs: "\<And>m n. \<bar>sumhr (m, n, f)\<bar> \<le> sumhr (m, n, \<lambda>i. \<bar>f i\<bar>)"
    63   unfolding sumhr_app by transfer (rule sum_abs)
    64 
    65 text \<open>Other general version also needed.\<close>
    66 lemma sumhr_fun_hypnat_eq:
    67   "(\<forall>r. m \<le> r \<and> r < n \<longrightarrow> f r = g r) \<longrightarrow>
    68     sumhr (hypnat_of_nat m, hypnat_of_nat n, f) =
    69     sumhr (hypnat_of_nat m, hypnat_of_nat n, g)"
    70   unfolding sumhr_app by transfer simp
    71 
    72 lemma sumhr_const: "\<And>n. sumhr (0, n, \<lambda>i. r) = hypreal_of_hypnat n * hypreal_of_real r"
    73   unfolding sumhr_app by transfer simp
    74 
    75 lemma sumhr_less_bounds_zero [simp]: "\<And>m n. n < m \<Longrightarrow> sumhr (m, n, f) = 0"
    76   unfolding sumhr_app by transfer simp
    77 
    78 lemma sumhr_minus: "\<And>m n. sumhr (m, n, \<lambda>i. - f i) = - sumhr (m, n, f)"
    79   unfolding sumhr_app by transfer (rule sum_negf)
    80 
    81 lemma sumhr_shift_bounds:
    82   "\<And>m n. sumhr (m + hypnat_of_nat k, n + hypnat_of_nat k, f) =
    83     sumhr (m, n, \<lambda>i. f (i + k))"
    84   unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
    85 
    86 
    87 subsection \<open>Nonstandard Sums\<close>
    88 
    89 text \<open>Infinite sums are obtained by summing to some infinite hypernatural
    90   (such as @{term whn}).\<close>
    91 lemma sumhr_hypreal_of_hypnat_omega: "sumhr (0, whn, \<lambda>i. 1) = hypreal_of_hypnat whn"
    92   by (simp add: sumhr_const)
    93 
    94 lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, \<lambda>i. 1) = \<omega> - 1"
    95   apply (simp add: sumhr_const)
    96     (* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
    97     (* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
    98   apply (unfold star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def)
    99   apply (simp add: starfun_star_n starfun2_star_n)
   100   done
   101 
   102 lemma sumhr_minus_one_realpow_zero [simp]: "\<And>N. sumhr (0, N + N, \<lambda>i. (-1) ^ (i + 1)) = 0"
   103   unfolding sumhr_app
   104   apply transfer
   105   apply (simp del: power_Suc add: mult_2 [symmetric])
   106   apply (induct_tac N)
   107    apply simp_all
   108   done
   109 
   110 lemma sumhr_interval_const:
   111   "(\<forall>n. m \<le> Suc n \<longrightarrow> f n = r) \<and> m \<le> na \<Longrightarrow>
   112     sumhr (hypnat_of_nat m, hypnat_of_nat na, f) = hypreal_of_nat (na - m) * hypreal_of_real r"
   113   unfolding sumhr_app by transfer simp
   114 
   115 lemma starfunNat_sumr: "\<And>N. ( *f* (\<lambda>n. sum f {0..<n})) N = sumhr (0, N, f)"
   116   unfolding sumhr_app by transfer (rule refl)
   117 
   118 lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f) \<approx> sumhr (0, N, f) \<Longrightarrow> \<bar>sumhr (M, N, f)\<bar> \<approx> 0"
   119   using linorder_less_linear [where x = M and y = N]
   120   apply auto
   121   apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
   122   apply (auto dest: approx_hrabs simp add: sumhr_split_diff)
   123   done
   124 
   125 
   126 subsection \<open>Infinite sums: Standard and NS theorems\<close>
   127 
   128 lemma sums_NSsums_iff: "f sums l \<longleftrightarrow> f NSsums l"
   129   by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
   130 
   131 lemma summable_NSsummable_iff: "summable f \<longleftrightarrow> NSsummable f"
   132   by (simp add: summable_def NSsummable_def sums_NSsums_iff)
   133 
   134 lemma suminf_NSsuminf_iff: "suminf f = NSsuminf f"
   135   by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
   136 
   137 lemma NSsums_NSsummable: "f NSsums l \<Longrightarrow> NSsummable f"
   138   unfolding NSsums_def NSsummable_def by blast
   139 
   140 lemma NSsummable_NSsums: "NSsummable f \<Longrightarrow> f NSsums (NSsuminf f)"
   141   unfolding NSsummable_def NSsuminf_def NSsums_def
   142   by (blast intro: theI NSLIMSEQ_unique)
   143 
   144 lemma NSsums_unique: "f NSsums s \<Longrightarrow> s = NSsuminf f"
   145   by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
   146 
   147 lemma NSseries_zero: "\<forall>m. n \<le> Suc m \<longrightarrow> f m = 0 \<Longrightarrow> f NSsums (sum f {..<n})"
   148   by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
   149 
   150 lemma NSsummable_NSCauchy:
   151   "NSsummable f \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr (M, N, f)\<bar> \<approx> 0)"
   152   apply (auto simp add: summable_NSsummable_iff [symmetric]
   153       summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
   154       NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
   155   apply (cut_tac x = M and y = N in linorder_less_linear)
   156   apply auto
   157    apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   158    apply (rule_tac [2] approx_minus_iff [THEN iffD2])
   159    apply (auto dest: approx_hrabs_zero_cancel simp: sumhr_split_diff atLeast0LessThan[symmetric])
   160   done
   161 
   162 text \<open>Terms of a convergent series tend to zero.\<close>
   163 lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   164   apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
   165   apply (drule bspec)
   166    apply auto
   167   apply (drule_tac x = "N + 1 " in bspec)
   168    apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
   169   done
   170 
   171 text \<open>Nonstandard comparison test.\<close>
   172 lemma NSsummable_comparison_test: "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable f"
   173   apply (fold summable_NSsummable_iff)
   174   apply (rule summable_comparison_test, simp, assumption)
   175   done
   176 
   177 lemma NSsummable_rabs_comparison_test:
   178   "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable (\<lambda>k. \<bar>f k\<bar>)"
   179   by (rule NSsummable_comparison_test) auto
   180 
   181 end