src/HOL/Transcendental.thy

closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text

(*  Title       : Transcendental.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 1998,1999 University of Cambridge
                  1999,2001 University of Edinburgh
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)

header{*Power Series, Transcendental Functions etc.*}

theory Transcendental
imports Fact Series Deriv NthRoot
begin

subsection {* Properties of Power Series *}

lemma lemma_realpow_diff:
  fixes y :: "'a::monoid_mult"
  shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
proof -
  assume "p \<le> n"
  hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
  thus ?thesis by (simp add: power_commutes)
qed

lemma lemma_realpow_diff_sumr:
  fixes y :: "'a::{comm_semiring_0,monoid_mult}" shows
     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =  
      y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
         del: setsum_op_ivl_Suc cong: strong_setsum_cong)

lemma lemma_realpow_diff_sumr2:
  fixes y :: "'a::{comm_ring,monoid_mult}" shows
     "x ^ (Suc n) - y ^ (Suc n) =  
      (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
apply (induct n, simp)
apply (simp del: setsum_op_ivl_Suc)
apply (subst setsum_op_ivl_Suc)
apply (subst lemma_realpow_diff_sumr)
apply (simp add: right_distrib del: setsum_op_ivl_Suc)
apply (subst mult_left_commute [where a="x - y"])
apply (erule subst)
apply (simp add: algebra_simps)
done

lemma lemma_realpow_rev_sumr:
     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
apply (rule inj_onI, simp)
apply auto
apply (rule_tac x="n - x" in image_eqI, simp, simp)
done

text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}

lemma powser_insidea:
  fixes x z :: "'a::{real_normed_field,banach}"
  assumes 1: "summable (\<lambda>n. f n * x ^ n)"
  assumes 2: "norm z < norm x"
  shows "summable (\<lambda>n. norm (f n * z ^ n))"
proof -
  from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
  from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
    by (rule summable_LIMSEQ_zero)
  hence "convergent (\<lambda>n. f n * x ^ n)"
    by (rule convergentI)
  hence "Cauchy (\<lambda>n. f n * x ^ n)"
    by (simp add: Cauchy_convergent_iff)
  hence "Bseq (\<lambda>n. f n * x ^ n)"
    by (rule Cauchy_Bseq)
  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
    by (simp add: Bseq_def, safe)
  have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
                   K * norm (z ^ n) * inverse (norm (x ^ n))"
  proof (intro exI allI impI)
    fix n::nat assume "0 \<le> n"
    have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
          norm (f n * x ^ n) * norm (z ^ n)"
      by (simp add: norm_mult abs_mult)
    also have "\<dots> \<le> K * norm (z ^ n)"
      by (simp only: mult_right_mono 4 norm_ge_zero)
    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
      by (simp add: x_neq_0)
    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
      by (simp only: mult_assoc)
    finally show "norm (norm (f n * z ^ n)) \<le>
                  K * norm (z ^ n) * inverse (norm (x ^ n))"
      by (simp add: mult_le_cancel_right x_neq_0)
  qed
  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
  proof -
    from 2 have "norm (norm (z * inverse x)) < 1"
      using x_neq_0
      by (simp add: nonzero_norm_divide divide_inverse [symmetric])
    hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
      by (rule summable_geometric)
    hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
      by (rule summable_mult)
    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
      using x_neq_0
      by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
                    power_inverse norm_power mult_assoc)
  qed
  ultimately show "summable (\<lambda>n. norm (f n * z ^ n))"
    by (rule summable_comparison_test)
qed

lemma powser_inside:
  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}" shows
     "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |]  
      ==> summable (%n. f(n) * (z ^ n))"
by (rule powser_insidea [THEN summable_norm_cancel])

lemma sum_split_even_odd: fixes f :: "nat \<Rightarrow> real" shows
  "(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) = 
   (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1))"
proof (induct n)
  case (Suc n)
  have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) = 
        (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
    using Suc.hyps unfolding One_nat_def by auto
  also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto
  finally show ?case .
qed auto

lemma sums_if': fixes g :: "nat \<Rightarrow> real" assumes "g sums x"
  shows "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
  unfolding sums_def
proof (rule LIMSEQ_I)
  fix r :: real assume "0 < r"
  from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this]
  obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g { 0..<n } - x) < r)" by blast

  let ?SUM = "\<lambda> m. \<Sum> i = 0 ..< m. if even i then 0 else g ((i - 1) div 2)"
  { fix m assume "m \<ge> 2 * no" hence "m div 2 \<ge> no" by auto
    have sum_eq: "?SUM (2 * (m div 2)) = setsum g { 0 ..< m div 2 }" 
      using sum_split_even_odd by auto
    hence "(norm (?SUM (2 * (m div 2)) - x) < r)" using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
    moreover
    have "?SUM (2 * (m div 2)) = ?SUM m"
    proof (cases "even m")
      case True show ?thesis unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] ..
    next
      case False hence "even (Suc m)" by auto
      from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]] odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]]
      have eq: "Suc (2 * (m div 2)) = m" by auto
      hence "even (2 * (m div 2))" using `odd m` by auto
      have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
      also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
      finally show ?thesis by auto
    qed
    ultimately have "(norm (?SUM m - x) < r)" by auto
  }
  thus "\<exists> no. \<forall> m \<ge> no. norm (?SUM m - x) < r" by blast
qed

lemma sums_if: fixes g :: "nat \<Rightarrow> real" assumes "g sums x" and "f sums y"
  shows "(\<lambda> n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)"
proof -
  let ?s = "\<lambda> n. if even n then 0 else f ((n - 1) div 2)"
  { fix B T E have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
      by (cases B) auto } note if_sum = this
  have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x" using sums_if'[OF `g sums x`] .
  { 
    have "?s 0 = 0" by auto
    have Suc_m1: "\<And> n. Suc n - 1 = n" by auto
    { fix B T E have "(if \<not> B then T else E) = (if B then E else T)" by auto } note if_eq = this

    have "?s sums y" using sums_if'[OF `f sums y`] .
    from this[unfolded sums_def, THEN LIMSEQ_Suc] 
    have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
      unfolding sums_def setsum_shift_lb_Suc0_0_upt[where f="?s", OF `?s 0 = 0`, symmetric]
                image_Suc_atLeastLessThan[symmetric] setsum_reindex[OF inj_Suc, unfolded comp_def]
                even_Suc Suc_m1 if_eq .
  } from sums_add[OF g_sums this]
  show ?thesis unfolding if_sum .
qed

subsection {* Alternating series test / Leibniz formula *}

lemma sums_alternating_upper_lower:
  fixes a :: "nat \<Rightarrow> real"
  assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
  shows "\<exists>l. ((\<forall>n. (\<Sum>i=0..<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i=0..<2*n. -1^i*a i) ----> l) \<and> 
             ((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. -1^i*a i) ----> l)"
  (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
proof -
  have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto

  have "\<forall> n. ?f n \<le> ?f (Suc n)"
  proof fix n show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto qed
  moreover
  have "\<forall> n. ?g (Suc n) \<le> ?g n"
  proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
    unfolding One_nat_def by auto qed
  moreover
  have "\<forall> n. ?f n \<le> ?g n" 
  proof fix n show "?f n \<le> ?g n" using fg_diff a_pos
    unfolding One_nat_def by auto qed
  moreover
  have "(\<lambda> n. ?f n - ?g n) ----> 0" unfolding fg_diff
  proof (rule LIMSEQ_I)
    fix r :: real assume "0 < r"
    with `a ----> 0`[THEN LIMSEQ_D] 
    obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r" by auto
    hence "\<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
    thus "\<exists> N. \<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
  qed
  ultimately
  show ?thesis by (rule lemma_nest_unique)
qed 

lemma summable_Leibniz': fixes a :: "nat \<Rightarrow> real"
  assumes a_zero: "a ----> 0" and a_pos: "\<And> n. 0 \<le> a n"
  and a_monotone: "\<And> n. a (Suc n) \<le> a n"
  shows summable: "summable (\<lambda> n. (-1)^n * a n)"
  and "\<And>n. (\<Sum>i=0..<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"