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