add lemma following a proof suggestion by Joachim Breitner
authorAndreas Lochbihler
Fri Nov 21 13:18:56 2014 +0100 (2014-11-21)
changeset 59025d885cff91200
parent 59024 5fcfeae84b96
child 59026 30b8a5825a9c
add lemma following a proof suggestion by Joachim Breitner
src/HOL/Series.thy
     1.1 --- a/src/HOL/Series.thy	Fri Nov 21 12:24:59 2014 +0100
     1.2 +++ b/src/HOL/Series.thy	Fri Nov 21 13:18:56 2014 +0100
     1.3 @@ -676,4 +676,67 @@
     1.4      using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
     1.5  qed
     1.6  
     1.7 +lemma
     1.8 +   fixes f :: "nat \<Rightarrow> real"
     1.9 +   assumes "summable f"
    1.10 +   and "inj g"
    1.11 +   and pos: "!!x. 0 \<le> f x"
    1.12 +   shows summable_reindex: "summable (f o g)"
    1.13 +   and suminf_reindex_mono: "suminf (f o g) \<le> suminf f"
    1.14 +   and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"
    1.15 +proof -
    1.16 +  from \<open>inj g\<close> have [simp]: "\<And>A. inj_on g A" by(rule subset_inj_on) simp
    1.17 +
    1.18 +  have smaller: "\<forall>n. (\<Sum>i<n. (f \<circ> g) i) \<le> suminf f"
    1.19 +  proof
    1.20 +    fix n
    1.21 +    have "\<forall> n' \<in> (g ` {..<n}). n' < Suc (Max (g ` {..<n}))" 
    1.22 +      by(metis Max_ge finite_imageI finite_lessThan not_le not_less_eq)
    1.23 +    then obtain m where n: "\<And>n'. n' < n \<Longrightarrow> g n' < m" by blast
    1.24 +
    1.25 +    have "(\<Sum>i<n. f (g i)) = setsum f (g ` {..<n})"
    1.26 +      by (simp add: setsum.reindex)
    1.27 +    also have "\<dots> \<le> (\<Sum>i<m. f i)"
    1.28 +      by (rule setsum_mono3) (auto simp add: pos n[rule_format])
    1.29 +    also have "\<dots> \<le> suminf f"
    1.30 +      using `summable f` 
    1.31 +      by (rule setsum_le_suminf) (simp add: pos)
    1.32 +    finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f" by simp
    1.33 +  qed
    1.34 +
    1.35 +  have "incseq (\<lambda>n. \<Sum>i<n. (f \<circ> g) i)"
    1.36 +    by (rule incseq_SucI) (auto simp add: pos)
    1.37 +  then obtain  L where L: "(\<lambda> n. \<Sum>i<n. (f \<circ> g) i) ----> L"
    1.38 +    using smaller by(rule incseq_convergent)
    1.39 +  hence "(f \<circ> g) sums L" by (simp add: sums_def)
    1.40 +  thus "summable (f o g)" by (auto simp add: sums_iff)
    1.41 +
    1.42 +  hence "(\<lambda>n. \<Sum>i<n. (f \<circ> g) i) ----> suminf (f \<circ> g)"
    1.43 +    by(rule summable_LIMSEQ)
    1.44 +  thus le: "suminf (f \<circ> g) \<le> suminf f"
    1.45 +    by(rule LIMSEQ_le_const2)(blast intro: smaller[rule_format])
    1.46 +
    1.47 +  assume f: "\<And>x. x \<notin> range g \<Longrightarrow> f x = 0"
    1.48 +
    1.49 +  from \<open>summable f\<close> have "suminf f \<le> suminf (f \<circ> g)"
    1.50 +  proof(rule suminf_le_const)
    1.51 +    fix n
    1.52 +    have "\<forall> n' \<in> (g -` {..<n}). n' < Suc (Max (g -` {..<n}))"
    1.53 +      by(auto intro: Max_ge simp add: finite_vimageI less_Suc_eq_le)
    1.54 +    then obtain m where n: "\<And>n'. g n' < n \<Longrightarrow> n' < m" by blast
    1.55 +
    1.56 +    have "(\<Sum>i<n. f i) = (\<Sum>i\<in>{..<n} \<inter> range g. f i)"
    1.57 +      using f by(auto intro: setsum.mono_neutral_cong_right)
    1.58 +    also have "\<dots> = (\<Sum>i\<in>g -` {..<n}. (f \<circ> g) i)"
    1.59 +      by(rule setsum.reindex_cong[where l=g])(auto)
    1.60 +    also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)"
    1.61 +      by(rule setsum_mono3)(auto simp add: pos n)
    1.62 +    also have "\<dots> \<le> suminf (f \<circ> g)"
    1.63 +      using \<open>summable (f o g)\<close>
    1.64 +      by(rule setsum_le_suminf)(simp add: pos)
    1.65 +    finally show "setsum f {..<n} \<le> suminf (f \<circ> g)" .
    1.66 +  qed
    1.67 +  with le show "suminf (f \<circ> g) = suminf f" by(rule antisym)
    1.68 +qed
    1.69 +
    1.70  end