src/HOL/Probability/SeriesPlus.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 33536 fd28b7399f2b
child 35704 5007843dae33
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
paulson@33271
     1
theory SeriesPlus
paulson@33271
     2
  imports Complex_Main Nat_Int_Bij 
paulson@33271
     3
begin
paulson@33271
     4
paulson@33271
     5
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
paulson@33271
     6
paulson@33271
     7
lemma choice2: "(!!x. \<exists>y z. Q x y z) ==> \<exists>f g. \<forall>x. Q x (f x) (g x)"
paulson@33271
     8
  by metis
paulson@33271
     9
paulson@33271
    10
lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B"
paulson@33271
    11
  by blast
paulson@33271
    12
paulson@33271
    13
paulson@33271
    14
lemma suminf_2dimen:
paulson@33271
    15
  fixes f:: "nat * nat \<Rightarrow> real"
paulson@33271
    16
  assumes f_nneg: "!!m n. 0 \<le> f(m,n)"
paulson@33271
    17
      and fsums: "!!m. (\<lambda>n. f (m,n)) sums (g m)"
paulson@33271
    18
      and sumg: "summable g"
paulson@33271
    19
  shows "(f o nat_to_nat2) sums suminf g"
paulson@33271
    20
proof (simp add: sums_def)
paulson@33271
    21
  {
paulson@33271
    22
    fix x
paulson@33271
    23
    have "0 \<le> f x"
paulson@33271
    24
      by (cases x) (simp add: f_nneg) 
paulson@33271
    25
  } note [iff]  = this
paulson@33271
    26
  have g_nneg: "!!m. 0 \<le> g m"
paulson@33271
    27
    proof -
paulson@33271
    28
      fix m
paulson@33271
    29
      have "0 \<le> suminf (\<lambda>n. f (m,n))"
wenzelm@33536
    30
        by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
paulson@33271
    31
      thus "0 \<le> g m" using fsums [of m] 
wenzelm@33536
    32
        by (auto simp add: sums_iff) 
paulson@33271
    33
    qed
paulson@33271
    34
  show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
paulson@33271
    35
  proof (rule increasing_LIMSEQ, simp add: f_nneg)
paulson@33271
    36
    fix n
paulson@33271
    37
    def i \<equiv> "Max (Domain (nat_to_nat2 ` {0..<n}))"
paulson@33271
    38
    def j \<equiv> "Max (Range (nat_to_nat2 ` {0..<n}))"
paulson@33271
    39
    have ij: "nat_to_nat2 ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})" 
paulson@33271
    40
      by (force simp add: i_def j_def 
paulson@33271
    41
                intro: finite_imageI Max_ge finite_Domain finite_Range)  
paulson@33271
    42
    have "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) = setsum f (nat_to_nat2 ` {0..<n})" 
paulson@33271
    43
      using setsum_reindex [of nat_to_nat2 "{0..<n}" f] 
paulson@33271
    44
      by (simp add: o_def)
paulson@33271
    45
         (metis nat_to_nat2_inj subset_inj_on subset_UNIV nat_to_nat2_inj) 
paulson@33271
    46
    also have "... \<le> setsum f ({0..i} \<times> {0..j})"
paulson@33271
    47
      by (rule setsum_mono2) (auto simp add: ij) 
paulson@33271
    48
    also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
paulson@33271
    49
      by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost
wenzelm@33536
    50
                setsum_cartesian_product split_eta) 
paulson@33271
    51
    also have "... \<le> setsum g {0..<Suc i}" 
paulson@33271
    52
      proof (rule setsum_mono, simp add: less_Suc_eq_le) 
wenzelm@33536
    53
        fix m
wenzelm@33536
    54
        assume m: "m \<le> i"
wenzelm@33536
    55
        thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
wenzelm@33536
    56
          by (auto simp add: sums_iff) 
wenzelm@33536
    57
           (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg) 
paulson@33271
    58
      qed
paulson@33271
    59
    finally have  "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
paulson@33271
    60
    also have "... \<le> suminf g" 
paulson@33271
    61
      by (rule series_pos_le [OF sumg]) (simp add: g_nneg) 
paulson@33271
    62
    finally show "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> suminf g" .
paulson@33271
    63
  next
paulson@33271
    64
    fix e :: real
paulson@33271
    65
    assume e: "0 < e"
paulson@33271
    66
    with summable_sums [OF sumg]
paulson@33271
    67
    obtain N where "\<bar>setsum g {0..<N} - suminf g\<bar> < e/2" and nz: "N>0"
paulson@33271
    68
      by (simp add: sums_def LIMSEQ_iff_nz dist_real_def)
paulson@33271
    69
         (metis e half_gt_zero le_refl that)
paulson@33271
    70
    hence gless: "suminf g < setsum g {0..<N} + e/2" using series_pos_le [OF sumg]
paulson@33271
    71
      by (simp add: g_nneg)
paulson@33271
    72
    { fix m
paulson@33271
    73
      assume m: "m<N"
paulson@33271
    74
      hence enneg: "0 < e / (2 * real N)" using e
wenzelm@33536
    75
        by (simp add: zero_less_divide_iff) 
paulson@33271
    76
      hence  "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)"
wenzelm@33536
    77
        using fsums [of m] m
paulson@33271
    78
        by (force simp add: sums_def LIMSEQ_def dist_real_def)
paulson@33271
    79
      hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)" 
wenzelm@33536
    80
        using fsums [of m]
wenzelm@33536
    81
        by (auto simp add: sums_iff) 
paulson@33271
    82
           (metis abs_diff_less_iff add_less_cancel_right eq_diff_eq') 
paulson@33271
    83
    }
paulson@33271
    84
    hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
paulson@33271
    85
      by (force intro: choice) 
paulson@33271
    86
    then obtain jj where jj:
paulson@33271
    87
          "!!m. m<N \<Longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
paulson@33271
    88
      by auto
paulson@33271
    89
    def IJ \<equiv> "SIGMA i : {0..<N}. {0..<jj i}"
paulson@33271
    90
    have "setsum g {0..<N} <
paulson@33271
    91
             (\<Sum>m = 0..<N. (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N))"
paulson@33271
    92
      by (auto simp add: nz jj intro: setsum_strict_mono) 
paulson@33271
    93
    also have "... = (\<Sum>m = 0..<N. \<Sum>n = 0..<jj m. f (m, n)) + e/2" using nz
paulson@33271
    94
      by (auto simp add: setsum_addf real_of_nat_def) 
paulson@33271
    95
    also have "... = setsum f IJ + e/2" 
paulson@33271
    96
      by (simp add: IJ_def setsum_Sigma) 
paulson@33271
    97
    finally have "setsum g {0..<N} < setsum f IJ + e/2" .
paulson@33271
    98
    hence glessf: "suminf g < setsum f IJ + e" using gless 
paulson@33271
    99
      by auto
paulson@33271
   100
    have finite_IJ: "finite IJ"
paulson@33271
   101
      by (simp add: IJ_def) 
paulson@33271
   102
    def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
paulson@33271
   103
    have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
paulson@33271
   104
      proof (auto simp add: NIJ_def)
wenzelm@33536
   105
        fix i j
wenzelm@33536
   106
        assume ij:"(i,j) \<in> IJ"
wenzelm@33536
   107
        hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
wenzelm@33536
   108
          by (metis nat_to_nat2_surj surj_f_inv_f) 
wenzelm@33536
   109
        thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
wenzelm@33536
   110
          by (rule image_eqI) 
wenzelm@33536
   111
             (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
paulson@33271
   112
                    nat_to_nat2_surj surj_f_inv_f) 
paulson@33271
   113
      qed
paulson@33271
   114
    have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
paulson@33271
   115
      by (rule setsum_mono2) (auto simp add: IJsb) 
paulson@33271
   116
    also have "... = (\<Sum>k = 0..NIJ. f (nat_to_nat2 k))"
paulson@33271
   117
      by (simp add: setsum_reindex subset_inj_on [OF nat_to_nat2_inj subset_UNIV]) 
paulson@33271
   118
    also have "... = (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))"
paulson@33271
   119
      by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost)
paulson@33271
   120
    finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (nat_to_nat2 k))" .
paulson@33271
   121
    thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (nat_to_nat2 x)) + e" using glessf
paulson@33271
   122
      by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym)
paulson@33271
   123
  qed
paulson@33271
   124
qed
paulson@33271
   125
paulson@33271
   126
end