Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: insetspecialchar.h Sprache: C

Original von: Isabelle^©

(*  Title:      HOL/Transcendental.thy
    Author:     Jacques D. Fleuriot, University of Cambridge, University of Edinburgh
    Author:     Lawrence C Paulson
    Author:     Jeremy Avigad
*)

section \<open>Power Series, Transcendental Functions etc.\<close>

theory Transcendental
imports Series Deriv NthRoot
begin

text \<open>A theorem about the factcorial function on the reals.\<close>

lemma square_fact_le_2_fact: "fact n * fact n \ (fact (2 * n) :: real)"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "(fact (Suc n)) * (fact (Suc n)) = of_nat (Suc n) * of_nat (Suc n) * (fact n * fact n :: real)"
    by (simp add: field_simps)
  also have "\ \ of_nat (Suc n) * of_nat (Suc n) * fact (2 * n)"
    by (rule mult_left_mono [OF Suc]) simp
  also have "\ \ of_nat (Suc (Suc (2 * n))) * of_nat (Suc (2 * n)) * fact (2 * n)"
    by (rule mult_right_mono)+ (auto simp: field_simps)
  also have "\ = fact (2 * Suc n)" by (simp add: field_simps)
  finally show ?case .
qed

lemma fact_in_Reals: "fact n \ \"
  by (induction n) auto

lemma of_real_fact [simp]: "of_real (fact n) = fact n"
  by (metis of_nat_fact of_real_of_nat_eq)

lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
  by (simp add: pochhammer_prod)

lemma norm_fact [simp]: "norm (fact n :: 'a::real_normed_algebra_1) = fact n"
proof -
  have "(fact n :: 'a) = of_real (fact n)"
    by simp
  also have "norm \ = fact n"
    by (subst norm_of_real) simp
  finally show ?thesis .
qed

lemma root_test_convergence:
  fixes f :: "nat \ 'a::banach"
  assumes f: "(\n. root n (norm (f n))) \ x" \ \could be weakened to lim sup\
    and "x < 1"
  shows "summable f"
proof -
  have "0 \ x"
    by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
  from \<open>x < 1\<close> obtain z where z: "x < z" "z < 1"
    by (metis dense)
  from f \<open>x < z\<close> have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially"
    by (rule order_tendstoD)
  then have "eventually (\n. norm (f n) \ z^n) sequentially"
    using eventually_ge_at_top
  proof eventually_elim
    fix n
    assume less: "root n (norm (f n)) < z" and n: "1 \ n"
    from power_strict_mono[OF less, of n] n show "norm (f n) \ z ^ n"
      by simp
  qed
  then show "summable f"
    unfolding eventually_sequentially
    using z \<open>0 \<le> x\<close> by (auto intro!: summable_comparison_test[OF _  summable_geometric])
qed

subsection \<open>More facts about binomial coefficients\<close>

text \<open>
  These facts could have been proven before, but having real numbers
  makes the proofs a lot easier.
\<close>

lemma central_binomial_odd:
  "odd n \ n choose (Suc (n div 2)) = n choose (n div 2)"
proof -
  assume "odd n"
  hence "Suc (n div 2) \ n" by presburger
  hence "n choose (Suc (n div 2)) = n choose (n - Suc (n div 2))"
    by (rule binomial_symmetric)
  also from \<open>odd n\<close> have "n - Suc (n div 2) = n div 2" by presburger
  finally show ?thesis .
qed

lemma binomial_less_binomial_Suc:
  assumes k: "k < n div 2"
  shows   "n choose k < n choose (Suc k)"
proof -
  from k have k': "k \ n" "Suc k \ n" by simp_all
  from k' have "real (n choose k) = fact n / (fact k * fact (n - k))"
    by (simp add: binomial_fact)
  also from k' have "n - k = Suc (n - Suc k)" by simp
  also from k' have "fact \ = (real n - real k) * fact (n - Suc k)"
    by (subst fact_Suc) (simp_all add: of_nat_diff)
  also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps)
  also have "fact n / (fact (Suc k) / (real k + 1) * ((real n - real k) * fact (n - Suc k))) =
               (n choose (Suc k)) * ((real k + 1) / (real n - real k))"
    using k by (simp add: field_split_simps binomial_fact)
  also from assms have "(real k + 1) / (real n - real k) < 1" by simp
  finally show ?thesis using k by (simp add: mult_less_cancel_left)
qed

lemma binomial_strict_mono:
  assumes "k < k'" "2*k' \ n"
  shows   "n choose k < n choose k'"
proof -
  from assms have "k \ k' - 1" by simp
  thus ?thesis
  proof (induction rule: inc_induct)
    case base
    with assms binomial_less_binomial_Suc[of "k' - 1" n]
      show ?case by simp
  next
    case (step k)
    from step.prems step.hyps assms have "n choose k < n choose (Suc k)"
      by (intro binomial_less_binomial_Suc) simp_all
    also have "\ < n choose k'" by (rule step.IH)
    finally show ?case .
  qed
qed

lemma binomial_mono:
  assumes "k \ k'" "2*k' \ n"
  shows   "n choose k \ n choose k'"
  using assms binomial_strict_mono[of k k' n] by (cases "k = k'") simp_all

lemma binomial_strict_antimono:
  assumes "k < k'" "2 * k \ n" "k' \ n"
  shows   "n choose k > n choose k'"
proof -
  from assms have "n choose (n - k) > n choose (n - k')"
    by (intro binomial_strict_mono) (simp_all add: algebra_simps)
  with assms show ?thesis by (simp add: binomial_symmetric [symmetric])
qed

lemma binomial_antimono:
  assumes "k \ k'" "k \ n div 2" "k' \ n"
  shows   "n choose k \ n choose k'"
proof (cases "k = k'")
  case False
  note not_eq = False
  show ?thesis
  proof (cases "k = n div 2 \ odd n")
    case False
    with assms(2) have "2*k \ n" by presburger
    with not_eq assms binomial_strict_antimono[of k k' n]
      show ?thesis by simp
  next
    case True
    have "n choose k' \ n choose (Suc (n div 2))"
    proof (cases "k' = Suc (n div 2)")
      case False
      with assms True not_eq have "Suc (n div 2) < k'" by simp
      with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True
        show ?thesis by auto
    qed simp_all
    also from True have "\ = n choose k" by (simp add: central_binomial_odd)
    finally show ?thesis .
  qed
qed simp_all

lemma binomial_maximum: "n choose k \ n choose (n div 2)"
proof -
  have "k \ n div 2 \ 2*k \ n" by linarith
  consider "2*k \ n" | "2*k \ n" "k \ n" | "k > n" by linarith
  thus ?thesis
  proof cases
    case 1
    thus ?thesis by (intro binomial_mono) linarith+
  next
    case 2
    thus ?thesis by (intro binomial_antimono) simp_all
  qed (simp_all add: binomial_eq_0)
qed

lemma binomial_maximum': "(2*n) choose k \ (2*n) choose n"
  using binomial_maximum[of "2*n"] by simp

lemma central_binomial_lower_bound:
  assumes "n > 0"
  shows   "4^n / (2*real n) \ real ((2*n) choose n)"
proof -
  from binomial[of 1 1 "2*n"]
    have "4 ^ n = (\k\2*n. (2*n) choose k)"
    by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
  also have "{..2*n} = {0<..<2*n} \ {0,2*n}" by auto
  also have "(\k\\. (2*n) choose k) =
             (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
    by (subst sum.union_disjoint) auto
  also have "(\k\{0,2*n}. (2*n) choose k) \ (\k\1. (n choose k)\<^sup>2)"
    by (cases n) simp_all
  also from assms have "\ \ (\k\n. (n choose k)\<^sup>2)"
    by (intro sum_mono2) auto
  also have "\ = (2*n) choose n" by (rule choose_square_sum)
  also have "(\k\{0<..<2*n}. (2*n) choose k) \ (\k\{0<..<2*n}. (2*n) choose n)"
    by (intro sum_mono binomial_maximum')
  also have "\ = card {0<..<2*n} * ((2*n) choose n)" by simp
  also have "card {0<..<2*n} \ 2*n - 1" by (cases n) simp_all
  also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)"
    using assms by (simp add: algebra_simps)
  finally have "4 ^ n \ (2 * n choose n) * (2 * n)" by simp_all
  hence "real (4 ^ n) \ real ((2 * n choose n) * (2 * n))"
    by (subst of_nat_le_iff)
  with assms show ?thesis by (simp add: field_simps)
qed

subsection \<open>Properties of Power Series\<close>

lemma powser_zero [simp]: "(\n. f n * 0 ^ n) = f 0"
  for f :: "nat \ 'a::real_normed_algebra_1"
proof -
  have "(\n<1. f n * 0 ^ n) = (\n. f n * 0 ^ n)"
    by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
  then show ?thesis by simp
qed

lemma powser_sums_zero: "(\n. a n * 0^n) sums a 0"
  for a :: "nat \ 'a::real_normed_div_algebra"
  using sums_finite [of "{0}" "\n. a n * 0 ^ n"]
  by simp

lemma powser_sums_zero_iff [simp]: "(\n. a n * 0^n) sums x \ a 0 = x"
  for a :: "nat \ 'a::real_normed_div_algebra"
  using powser_sums_zero sums_unique2 by blast

text \<open>
  Power series has a circle or radius of convergence: if it sums for \<open>x\<close>,
  then it sums absolutely for \<open>z\<close> with \<^term>\<open>\<bar>z\<bar> < \<bar>x\<bar>\<close>.\<close>

lemma powser_insidea:
  fixes x z :: "'a::real_normed_div_algebra"
  assumes 1: "summable (\n. f n * x^n)"
    and 2: "norm z < norm x"
  shows "summable (\n. norm (f n * z ^ n))"
proof -
  from 2 have x_neq_0: "x \ 0" by clarsimp
  from 1 have "(\n. f n * x^n) \ 0"
    by (rule summable_LIMSEQ_zero)
  then have "convergent (\n. f n * x^n)"
    by (rule convergentI)
  then have "Cauchy (\n. f n * x^n)"
    by (rule convergent_Cauchy)
  then have "Bseq (\n. f n * x^n)"
    by (rule Cauchy_Bseq)
  then obtain K where 3: "0 < K" and 4: "\n. norm (f n * x^n) \ K"
    by (auto simp: Bseq_def)
  have "\N. \n\N. norm (norm (f n * z ^ n)) \ K * norm (z ^ n) * inverse (norm (x^n))"
  proof (intro exI allI impI)
    fix n :: nat
    assume "0 \ 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 "\ \ K * norm (z ^ n)"
      by (simp only: mult_right_mono 4 norm_ge_zero)
    also have "\ = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))"
      by (simp add: x_neq_0)
    also have "\ = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)"
      by (simp only: mult.assoc)
    finally show "norm (norm (f n * z ^ n)) \ K * norm (z ^ n) * inverse (norm (x^n))"
      by (simp add: mult_le_cancel_right x_neq_0)
  qed
  moreover have "summable (\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: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric])
    then have "summable (\n. norm (z * inverse x) ^ n)"
      by (rule summable_geometric)
    then have "summable (\n. K * norm (z * inverse x) ^ n)"
      by (rule summable_mult)
    then show "summable (\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 (\n. norm (f n * z ^ n))"
    by (rule summable_comparison_test)
qed

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

lemma powser_times_n_limit_0:
  fixes x :: "'a::{real_normed_div_algebra,banach}"
  assumes "norm x < 1"
    shows "(\n. of_nat n * x ^ n) \ 0"
proof -
  have "norm x / (1 - norm x) \ 0"
    using assms by (auto simp: field_split_simps)
  moreover obtain N where N: "norm x / (1 - norm x) < of_int N"
    using ex_le_of_int by (meson ex_less_of_int)
  ultimately have N0: "N>0"
    by auto
  then have *: "real_of_int (N + 1) * norm x / real_of_int N < 1"
    using N assms by (auto simp: field_simps)
  have **: "real_of_int N * (norm x * (real_of_nat (Suc n) * norm (x ^ n))) \
      real_of_nat n * (norm x * ((1 + N) * norm (x ^ n)))" if "N \<le> int n" for n :: nat
  proof -
    from that have "real_of_int N * real_of_nat (Suc n) \ real_of_nat n * real_of_int (1 + N)"
      by (simp add: algebra_simps)
    then have "(real_of_int N * real_of_nat (Suc n)) * (norm x * norm (x ^ n)) \
        (real_of_nat n *  (1 + N)) * (norm x * norm (x ^ n))"
      using N0 mult_mono by fastforce
    then show ?thesis
      by (simp add: algebra_simps)
  qed
  show ?thesis using *
    by (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"])
      (simp add: N0 norm_mult field_simps ** del: of_nat_Suc of_int_add)
qed

corollary lim_n_over_pown:
  fixes x :: "'a::{real_normed_field,banach}"
  shows "1 < norm x \ ((\n. of_nat n / x^n) \ 0) sequentially"
  using powser_times_n_limit_0 [of "inverse x"]
  by (simp add: norm_divide field_split_simps)

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

lemma sums_if':
  fixes g :: "nat \ real"
  assumes "g sums x"
  shows "(\ 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 \<open>g sums x\<close>[unfolded sums_def, THEN LIMSEQ_D, OF this]
  obtain no where no_eq: "\n. n \ no \ (norm (sum g {..
    by blast

  let ?SUM = "\ m. \i
  have "(norm (?SUM m - x) < r)" if "m \ 2 * no" for m
  proof -
    from that have "m div 2 \ no" by auto
    have sum_eq: "?SUM (2 * (m div 2)) = sum g {..< m div 2}"
      using sum_split_even_odd by auto
    then have "(norm (?SUM (2 * (m div 2)) - x) < r)"
      using no_eq unfolding sum_eq using \<open>m div 2 \<ge> no\<close> by auto
    moreover
    have "?SUM (2 * (m div 2)) = ?SUM m"
    proof (cases "even m")
      case True
      then show ?thesis
        by (auto simp: even_two_times_div_two)
    next
      case False
      then have eq: "Suc (2 * (m div 2)) = m" by simp
      then have "even (2 * (m div 2))" using \<open>odd m\<close> by auto
      have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
      also have "\ = ?SUM (2 * (m div 2))" using \even (2 * (m div 2))\ by auto
      finally show ?thesis by auto
    qed
    ultimately show ?thesis by auto
  qed
  then show "\no. \ m \ no. norm (?SUM m - x) < r"
    by blast
qed

lemma sums_if:
  fixes g :: "nat \ real"
  assumes "g sums x" and "f sums y"
  shows "(\ n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)"
proof -
  let ?s = "\ n. if even n then 0 else f ((n - 1) div 2)"
  have if_sum: "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
    for B T E
    by (cases B) auto
  have g_sums: "(\ n. if even n then 0 else g ((n - 1) div 2)) sums x"
    using sums_if'[OF \g sums x\] .
  have if_eq: "\B T E. (if \ B then T else E) = (if B then E else T)"
    by auto
  have "?s sums y" using sums_if'[OF \f sums y\] .
  from this[unfolded sums_def, THEN LIMSEQ_Suc]
  have "(\n. if even n then f (n div 2) else 0) sums y"
    by (simp add: lessThan_Suc_eq_insert_0 sum.atLeast1_atMost_eq image_Suc_lessThan
        if_eq sums_def cong del: if_weak_cong)
  from sums_add[OF g_sums this] show ?thesis
    by (simp only: if_sum)
qed

subsection \<open>Alternating series test / Leibniz formula\<close>
(* FIXME: generalise these results from the reals via type classes? *)

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

  show "\n. ?f n \ ?f (Suc n)"
  proof
    show "?f n \ ?f (Suc n)" for n
      using mono[of "2*n"] by auto
  qed
  show "\n. ?g (Suc n) \ ?g n"
  proof
    show "?g (Suc n) \ ?g n" for n
      using mono[of "Suc (2*n)"] by auto
  qed
  show "\n. ?f n \ ?g n"
  proof
    show "?f n \ ?g n" for n
      using fg_diff a_pos by auto
  qed
  show "(\n. ?f n - ?g n) \ 0"
    unfolding fg_diff
  proof (rule LIMSEQ_I)
    fix r :: real
    assume "0 < r"
    with \<open>a \<longlonglongrightarrow> 0\<close>[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r"
      by auto
    then have "\n \ N. norm (- a (2 * n) - 0) < r"
      by auto
    then show "\N. \n \ N. norm (- a (2 * n) - 0) < r"
      by auto
  qed
qed

lemma summable_Leibniz':
  fixes a :: "nat \ real"
  assumes a_zero: "a \ 0"
    and a_pos: "\n. 0 \ a n"
    and a_monotone: "\n. a (Suc n) \ a n"
  shows summable: "summable (\ n. (-1)^n * a n)"
    and "\n. (\i<2*n. (-1)^i*a i) \ (\i. (-1)^i*a i)"
    and "(\n. \i<2*n. (-1)^i*a i) \ (\i. (-1)^i*a i)"
    and "\n. (\i. (-1)^i*a i) \ (\i<2*n+1. (-1)^i*a i)"
    and "(\n. \i<2*n+1. (-1)^i*a i) \ (\i. (-1)^i*a i)"
proof -
  let ?S = "\n. (-1)^n * a n"
  let ?P = "\n. \i
  let ?f = "\n. ?P (2 * n)"
  let ?g = "\n. ?P (2 * n + 1)"
  obtain l :: real
    where below_l: "\ n. ?f n \ l"
      and "?f \ l"
      and above_l: "\ n. l \ ?g n"
      and "?g \ l"
    using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast

  let ?Sa = "\m. \n
  have "?Sa \ l"
  proof (rule LIMSEQ_I)
    fix r :: real
    assume "0 < r"
    with \<open>?f \<longlonglongrightarrow> l\<close>[THEN LIMSEQ_D]
    obtain f_no where f: "\n. n \ f_no \ norm (?f n - l) < r"
      by auto
    from \<open>0 < r\<close> \<open>?g \<longlonglongrightarrow> l\<close>[THEN LIMSEQ_D]
    obtain g_no where g: "\n. n \ g_no \ norm (?g n - l) < r"
      by auto
    have "norm (?Sa n - l) < r" if "n \ (max (2 * f_no) (2 * g_no))" for n
    proof -
      from that have "n \ 2 * f_no" and "n \ 2 * g_no" by auto
      show ?thesis
      proof (cases "even n")
        case True
        then have n_eq: "2 * (n div 2) = n"
          by (simp add: even_two_times_div_two)
        with \<open>n \<ge> 2 * f_no\<close> have "n div 2 \<ge> f_no"
          by auto
        from f[OF this] show ?thesis
          unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
      next
        case False
        then have "even (n - 1)" by simp
        then have n_eq: "2 * ((n - 1) div 2) = n - 1"
          by (simp add: even_two_times_div_two)
        then have range_eq: "n - 1 + 1 = n"
          using odd_pos[OF False] by auto
        from n_eq \<open>n \<ge> 2 * g_no\<close> have "(n - 1) div 2 \<ge> g_no"
          by auto
        from g[OF this] show ?thesis
          by (simp only: n_eq range_eq)
      qed
    qed
    then show "\no. \n \ no. norm (?Sa n - l) < r" by blast
  qed
  then have sums_l: "(\i. (-1)^i * a i) sums l"
    by (simp only: sums_def)
  then show "summable ?S"
    by (auto simp: summable_def)

  have "l = suminf ?S" by (rule sums_unique[OF sums_l])

  fix n
  show "suminf ?S \ ?g n"
    unfolding sums_unique[OF sums_l, symmetric] using above_l by auto
  show "?f n \ suminf ?S"
    unfolding sums_unique[OF sums_l, symmetric] using below_l by auto
  show "?g \ suminf ?S"
    using \<open>?g \<longlonglongrightarrow> l\<close> \<open>l = suminf ?S\<close> by auto
  show "?f \ suminf ?S"
    using \<open>?f \<longlonglongrightarrow> l\<close> \<open>l = suminf ?S\<close> by auto
qed

theorem summable_Leibniz:
  fixes a :: "nat \ real"
  assumes a_zero: "a \ 0"
    and "monoseq a"
  shows "summable (\ n. (-1)^n * a n)" (is "?summable")
    and "0 < a 0 \
      (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n. (- 1)^i * a i .. \<Sum>i<2*n+1. (- 1)^i * a i})" (is "?pos")
    and "a 0 < 0 \
      (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n+1. (- 1)^i * a i .. \<Sum>i<2*n. (- 1)^i * a i})" (is "?neg")
    and "(\n. \i<2*n. (- 1)^i*a i) \ (\i. (- 1)^i*a i)" (is "?f")
    and "(\n. \i<2*n+1. (- 1)^i*a i) \ (\i. (- 1)^i*a i)" (is "?g")
proof -
  have "?summable \ ?pos \ ?neg \ ?f \ ?g"
  proof (cases "(\n. 0 \ a n) \ (\m. \n\m. a n \ a m)")
    case True
    then have ord: "\n m. m \ n \ a n \ a m"
      and ge0: "\n. 0 \ a n"
      by auto
    have mono: "a (Suc n) \ a n" for n
      using ord[where n="Suc n" and m=n] by auto
    note leibniz = summable_Leibniz'[OF \a \ 0\ ge0]
    from leibniz[OF mono]
    show ?thesis using \<open>0 \<le> a 0\<close> by auto
  next
    let ?a = "\n. - a n"
    case False
    with monoseq_le[OF \<open>monoseq a\<close> \<open>a \<longlonglongrightarrow> 0\<close>]
    have "(\ n. a n \ 0) \ (\m. \n\m. a m \ a n)" by auto
    then have ord: "\n m. m \ n \ ?a n \ ?a m" and ge0: "\ n. 0 \ ?a n"
      by auto
    have monotone: "?a (Suc n) \ ?a n" for n
      using ord[where n="Suc n" and m=n] by auto
    note leibniz =
      summable_Leibniz'[OF _ ge0, of "\x. x",
        OF tendsto_minus[OF \<open>a \<longlonglongrightarrow> 0\<close>, unfolded minus_zero] monotone]
    have "summable (\ n. (-1)^n * ?a n)"
      using leibniz(1) by auto
    then obtain l where "(\ n. (-1)^n * ?a n) sums l"
      unfolding summable_def by auto
    from this[THEN sums_minus] have "(\ n. (-1)^n * a n) sums -l"
      by auto
    then have ?summable by (auto simp: summable_def)
    moreover
    have "\- a - - b\ = \a - b\" for a b :: real
      unfolding minus_diff_minus by auto

    from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
    have move_minus: "(\n. - ((- 1) ^ n * a n)) = - (\n. (- 1) ^ n * a n)"
      by auto

    have ?pos using \<open>0 \<le> ?a 0\<close> by auto
    moreover have ?neg
      using leibniz(2,4)
      unfolding mult_minus_right sum_negf move_minus neg_le_iff_le
      by auto
    moreover have ?f and ?g
      using leibniz(3,5)[unfolded mult_minus_right sum_negf move_minus, THEN tendsto_minus_cancel]
      by auto
    ultimately show ?thesis by auto
  qed
  then show ?summable and ?pos and ?neg and ?f and ?g
    by safe
qed

subsection \<open>Term-by-Term Differentiability of Power Series\<close>

definition diffs :: "(nat \ 'a::ring_1) \ nat \ 'a"
  where "diffs c = (\n. of_nat (Suc n) * c (Suc n))"

text \<open>Lemma about distributing negation over it.\<close>
lemma diffs_minus: "diffs (\n. - c n) = (\n. - diffs c n)"
  by (simp add: diffs_def)

lemma diffs_equiv:
  fixes x :: "'a::{real_normed_vector,ring_1}"
  shows "summable (\n. diffs c n * x^n) \
    (\<lambda>n. of_nat n * c n * x^(n - Suc 0)) sums (\<Sum>n. diffs c n * x^n)"
  unfolding diffs_def
  by (simp add: summable_sums sums_Suc_imp)

lemma lemma_termdiff1:
  fixes z :: "'a :: {monoid_mult,comm_ring}"
  shows "(\p
    (\<Sum>p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
  by (auto simp: algebra_simps power_add [symmetric])

lemma sumr_diff_mult_const2: "sum f {..i
  for r :: "'a::ring_1"
  by (simp add: sum_subtractf)

lemma lemma_termdiff2:
  fixes h :: "'a::field"
  assumes h: "h \ 0"
  shows "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
         h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
    (is "?lhs = ?rhs")
proof (cases n)
  case (Suc m)
  have 0: "\x k. (\n
                 (\<Sum>j<Suc k.  h * ((h + z) ^ j * z ^ (x + k - j)))"
    by (auto simp add: power_add [symmetric] mult.commute intro: sum.cong)
  have *: "(\i
           (\<Sum>i<m. \<Sum>j<m - i. h * ((z + h) ^ j * z ^ (m - Suc j)))"
    by (force simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
        simp del: sum.lessThan_Suc power_Suc intro: sum.cong)
  have "h * ?lhs = (z + h) ^ n - z ^ n - h * of_nat n * z ^ (n - Suc 0)"
    by (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
  also have "... = h * ((\p
    by (simp add: Suc diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
        del: power_Suc sum.lessThan_Suc of_nat_Suc)
  also have "... = h * ((\p
    by (subst sum.nat_diff_reindex[symmetric]) simp
  also have "... = h * (\i
    by (simp add: sum_subtractf)
  also have "... = h * ?rhs"
    by (simp add: lemma_termdiff1 sum_distrib_left Suc *)
  finally have "h * ?lhs = h * ?rhs" .
  then show ?thesis
    by (simp add: h)
qed auto

lemma real_sum_nat_ivl_bounded2:
  fixes K :: "'a::linordered_semidom"
  assumes f: "\p::nat. p < n \ f p \ K" and K: "0 \ K"
  shows "sum f {.. of_nat n * K"
proof -
  have "sum f {.. (\i
    by (rule sum_mono [OF f]) auto
  also have "... \ of_nat n * K"
    by (auto simp: mult_right_mono K)
  finally show ?thesis .
qed

lemma lemma_termdiff3:
  fixes h z :: "'a::real_normed_field"
  assumes 1: "h \ 0"
    and 2: "norm z \ K"
    and 3: "norm (z + h) \ K"
  shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) \
    of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
proof -
  have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
    norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
    by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult.commute norm_mult)
  also have "\ \ of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
  proof (rule mult_right_mono [OF _ norm_ge_zero])
    from norm_ge_zero 2 have K: "0 \ K"
      by (rule order_trans)
    have le_Kn: "norm ((z + h) ^ i * z ^ j) \ K ^ n" if "i + j = n" for i j n
    proof -
      have "norm (z + h) ^ i * norm z ^ j \ K ^ i * K ^ j"
        by (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
      also have "... = K^n"
        by (metis power_add that)
      finally show ?thesis
        by (simp add: norm_mult norm_power)
    qed
    then have "\p q.
       \<lbrakk>p < n; q < n - Suc 0\<rbrakk> \<Longrightarrow> norm ((z + h) ^ q * z ^ (n - 2 - q)) \<le> K ^ (n - 2)"
      by (simp del: subst_all)
    then
    show "norm (\pq
        of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
      by (intro order_trans [OF norm_sum]
          real_sum_nat_ivl_bounded2 mult_nonneg_nonneg of_nat_0_le_iff zero_le_power K)
  qed
  also have "\ = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
    by (simp only: mult.assoc)
  finally show ?thesis .
qed

lemma lemma_termdiff4:
  fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector"
    and k :: real
  assumes k: "0 < k"
    and le: "\h. h \ 0 \ norm h < k \ norm (f h) \ K * norm h"
  shows "f \0\ 0"
proof (rule tendsto_norm_zero_cancel)
  show "(\h. norm (f h)) \0\ 0"
  proof (rule real_tendsto_sandwich)
    show "eventually (\h. 0 \ norm (f h)) (at 0)"
      by simp
    show "eventually (\h. norm (f h) \ K * norm h) (at 0)"
      using k by (auto simp: eventually_at dist_norm le)
    show "(\h. 0) \(0::'a)\ (0::real)"
      by (rule tendsto_const)
    have "(\h. K * norm h) \(0::'a)\ K * norm (0::'a)"
      by (intro tendsto_intros)
    then show "(\h. K * norm h) \(0::'a)\ 0"
      by simp
  qed
qed

lemma lemma_termdiff5:
  fixes g :: "'a::real_normed_vector \ nat \ 'b::banach"
    and k :: real
  assumes k: "0 < k"
    and f: "summable f"
    and le: "\h n. h \ 0 \ norm h < k \ norm (g h n) \ f n * norm h"
  shows "(\h. suminf (g h)) \0\ 0"
proof (rule lemma_termdiff4 [OF k])
  fix h :: 'a
  assume "h \ 0" and "norm h < k"
  then have 1: "\n. norm (g h n) \ f n * norm h"
    by (simp add: le)
  then have "\N. \n\N. norm (norm (g h n)) \ f n * norm h"
    by simp
  moreover from f have 2: "summable (\n. f n * norm h)"
    by (rule summable_mult2)
  ultimately have 3: "summable (\n. norm (g h n))"
    by (rule summable_comparison_test)
  then have "norm (suminf (g h)) \ (\n. norm (g h n))"
    by (rule summable_norm)
  also from 1 3 2 have "(\n. norm (g h n)) \ (\n. f n * norm h)"
    by (simp add: suminf_le)
  also from f have "(\n. f n * norm h) = suminf f * norm h"
    by (rule suminf_mult2 [symmetric])
  finally show "norm (suminf (g h)) \ suminf f * norm h" .
qed

(* FIXME: Long proofs *)

lemma termdiffs_aux:
  fixes x :: "'a::{real_normed_field,banach}"
  assumes 1: "summable (\n. diffs (diffs c) n * K ^ n)"
    and 2: "norm x < norm K"
  shows "(\h. \n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \0\ 0"
proof -
  from dense [OF 2] obtain r where r1: "norm x < r" and r2: "r < norm K"
    by fast
  from norm_ge_zero r1 have r: "0 < r"
    by (rule order_le_less_trans)
  then have r_neq_0: "r \ 0" by simp
  show ?thesis
  proof (rule lemma_termdiff5)
    show "0 < r - norm x"
      using r1 by simp
    from r r2 have "norm (of_real r::'a) < norm K"
      by simp
    with 1 have "summable (\n. norm (diffs (diffs c) n * (of_real r ^ n)))"
      by (rule powser_insidea)
    then have "summable (\n. diffs (diffs (\n. norm (c n))) n * r ^ n)"
      using r by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
    then have "summable (\n. of_nat n * diffs (\n. norm (c n)) n * r ^ (n - Suc 0))"
      by (rule diffs_equiv [THEN sums_summable])
    also have "(\n. of_nat n * diffs (\n. norm (c n)) n * r ^ (n - Suc 0)) =
               (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
      by (simp add: diffs_def r_neq_0 fun_eq_iff split: nat_diff_split)
    finally have "summable
      (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
      by (rule diffs_equiv [THEN sums_summable])
    also have
      "(\n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0)) =
       (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
      by (rule ext) (simp add: r_neq_0 split: nat_diff_split)
    finally show "summable (\n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
  next
    fix h :: 'a and n
    assume h: "h \ 0"
    assume "norm h < r - norm x"
    then have "norm x + norm h < r" by simp
    with norm_triangle_ineq
    have xh: "norm (x + h) < r"
      by (rule order_le_less_trans)
    have "norm (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))
    \<le> real n * (real (n - Suc 0) * (r ^ (n - 2) * norm h))"
      by (metis (mono_tags, lifting) h mult.assoc lemma_termdiff3 less_eq_real_def r1 xh)
    then show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \
      norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
      by (simp only: norm_mult mult.assoc mult_left_mono [OF _ norm_ge_zero])
  qed
qed

lemma termdiffs:
  fixes K x :: "'a::{real_normed_field,banach}"
  assumes 1: "summable (\n. c n * K ^ n)"
    and 2: "summable (\n. (diffs c) n * K ^ n)"
    and 3: "summable (\n. (diffs (diffs c)) n * K ^ n)"
    and 4: "norm x < norm K"
  shows "DERIV (\x. \n. c n * x^n) x :> (\n. (diffs c) n * x^n)"
  unfolding DERIV_def
proof (rule LIM_zero_cancel)
  show "(\h. (suminf (\n. c n * (x + h) ^ n) - suminf (\n. c n * x^n)) / h
            - suminf (\<lambda>n. diffs c n * x^n)) \<midarrow>0\<rightarrow> 0"
  proof (rule LIM_equal2)
    show "0 < norm K - norm x"
      using 4 by (simp add: less_diff_eq)
  next
    fix h :: 'a
    assume "norm (h - 0) < norm K - norm x"
    then have "norm x + norm h < norm K" by simp
    then have 5: "norm (x + h) < norm K"
      by (rule norm_triangle_ineq [THEN order_le_less_trans])
    have "summable (\n. c n * x^n)"
      and "summable (\n. c n * (x + h) ^ n)"
      and "summable (\n. diffs c n * x^n)"
      using 1 2 4 5 by (auto elim: powser_inside)
    then have "((\n. c n * (x + h) ^ n) - (\n. c n * x^n)) / h - (\n. diffs c n * x^n) =
          (\<Sum>n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))"
      by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
    then show "((\n. c n * (x + h) ^ n) - (\n. c n * x^n)) / h - (\n. diffs c n * x^n) =
          (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
      by (simp add: algebra_simps)
  next
    show "(\h. \n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \0\ 0"
      by (rule termdiffs_aux [OF 3 4])
  qed
qed

subsection \<open>The Derivative of a Power Series Has the Same Radius of Convergence\<close>

lemma termdiff_converges:
  fixes x :: "'a::{real_normed_field,banach}"
  assumes K: "norm x < K"
    and sm: "\x. norm x < K \ summable(\n. c n * x ^ n)"
  shows "summable (\n. diffs c n * x ^ n)"
proof (cases "x = 0")
  case True
  then show ?thesis
    using powser_sums_zero sums_summable by auto
next
  case False
  then have "K > 0"
    using K less_trans zero_less_norm_iff by blast
  then obtain r :: real where r: "norm x < norm r" "norm r < K" "r > 0"
    using K False
    by (auto simp: field_simps abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"])
  have to0: "(\n. of_nat n * (x / of_real r) ^ n) \ 0"
    using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"])
  obtain N where N: "\n. n\N \ real_of_nat n * norm x ^ n < r ^ n"
    using r LIMSEQ_D [OF to0, of 1]
    by (auto simp: norm_divide norm_mult norm_power field_simps)
  have "summable (\n. (of_nat n * c n) * x ^ n)"
  proof (rule summable_comparison_test')
    show "summable (\n. norm (c n * of_real r ^ n))"
      apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
      using N r norm_of_real [of "r + K", where 'a = 'a] by auto
    show "\n. N \ n \ norm (of_nat n * c n * x ^ n) \ norm (c n * of_real r ^ n)"
      using N r by (fastforce simp add: norm_mult norm_power less_eq_real_def)
  qed
  then have "summable (\n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)"
    using summable_iff_shift [of "\n. of_nat n * c n * x ^ n" 1]
    by simp
  then have "summable (\n. (of_nat (Suc n) * c(Suc n)) * x ^ n)"
    using False summable_mult2 [of "\n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"]
    by (simp add: mult.assoc) (auto simp: ac_simps)
  then show ?thesis
    by (simp add: diffs_def)
qed

lemma termdiff_converges_all:
  fixes x :: "'a::{real_normed_field,banach}"
  assumes "\x. summable (\n. c n * x^n)"
  shows "summable (\n. diffs c n * x^n)"
  by (rule termdiff_converges [where K = "1 + norm x"]) (use assms in auto)

lemma termdiffs_strong:
  fixes K x :: "'a::{real_normed_field,banach}"
  assumes sm: "summable (\n. c n * K ^ n)"
    and K: "norm x < norm K"
  shows "DERIV (\x. \n. c n * x^n) x :> (\n. diffs c n * x^n)"
proof -
  have "norm K + norm x < norm K + norm K"
    using K by force
  then have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
    by (auto simp: norm_triangle_lt norm_divide field_simps)
  then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2"
    by simp
  have "summable (\n. c n * (of_real (norm x + norm K) / 2) ^ n)"
    by (metis K2 summable_norm_cancel [OF powser_insidea [OF sm]] add.commute of_real_add)
  moreover have "\x. norm x < norm K \ summable (\n. diffs c n * x ^ n)"
    by (blast intro: sm termdiff_converges powser_inside)
  moreover have "\x. norm x < norm K \ summable (\n. diffs(diffs c) n * x ^ n)"
    by (blast intro: sm termdiff_converges powser_inside)
  ultimately show ?thesis
    by (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
       (use K in \<open>auto simp: field_simps simp flip: of_real_add\<close>)
qed

lemma termdiffs_strong_converges_everywhere:
  fixes K x :: "'a::{real_normed_field,banach}"
  assumes "\y. summable (\n. c n * y ^ n)"
  shows "((\x. \n. c n * x^n) has_field_derivative (\n. diffs c n * x^n)) (at x)"
  using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
  by (force simp del: of_real_add)

lemma termdiffs_strong':
  fixes z :: "'a :: {real_normed_field,banach}"
  assumes "\z. norm z < K \ summable (\n. c n * z ^ n)"
  assumes "norm z < K"
  shows   "((\z. \n. c n * z^n) has_field_derivative (\n. diffs c n * z^n)) (at z)"
proof (rule termdiffs_strong)
  define L :: real where "L = (norm z + K) / 2"
  have "0 \ norm z" by simp
  also note \<open>norm z < K\<close>
  finally have K: "K \ 0" by simp
  from assms K have L: "L \ 0" "norm z < L" "L < K" by (simp_all add: L_def)
  from L show "norm z < norm (of_real L :: 'a)" by simp
  from L show "summable (\n. c n * of_real L ^ n)" by (intro assms(1)) simp_all
qed

lemma termdiffs_sums_strong:
  fixes z :: "'a :: {banach,real_normed_field}"
  assumes sums: "\z. norm z < K \ (\n. c n * z ^ n) sums f z"
  assumes deriv: "(f has_field_derivative f') (at z)"
  assumes norm: "norm z < K"
  shows   "(\n. diffs c n * z ^ n) sums f'"
proof -
  have summable: "summable (\n. diffs c n * z^n)"
    by (intro termdiff_converges[OF norm] sums_summable[OF sums])
  from norm have "eventually (\z. z \ norm -` {..
    by (intro eventually_nhds_in_open open_vimage)
       (simp_all add: continuous_on_norm)
  hence eq: "eventually (\z. (\n. c n * z^n) = f z) (nhds z)"
    by eventually_elim (insert sums, simp add: sums_iff)

  have "((\z. \n. c n * z^n) has_field_derivative (\n. diffs c n * z^n)) (at z)"
    by (intro termdiffs_strong'[OF _ norm] sums_summable[OF sums])
  hence "(f has_field_derivative (\n. diffs c n * z^n)) (at z)"
    by (subst (asm) DERIV_cong_ev[OF refl eq refl])
  from this and deriv have "(\n. diffs c n * z^n) = f'" by (rule DERIV_unique)
  with summable show ?thesis by (simp add: sums_iff)
qed

lemma isCont_powser:
  fixes K x :: "'a::{real_normed_field,banach}"
  assumes "summable (\n. c n * K ^ n)"
  assumes "norm x < norm K"
  shows "isCont (\x. \n. c n * x^n) x"
  using termdiffs_strong[OF assms] by (blast intro!: DERIV_isCont)

lemmas isCont_powser' = isCont_o2[OF _ isCont_powser]

lemma isCont_powser_converges_everywhere:
  fixes K x :: "'a::{real_normed_field,banach}"
  assumes "\y. summable (\n. c n * y ^ n)"
  shows "isCont (\x. \n. c n * x^n) x"
  using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
  by (force intro!: DERIV_isCont simp del: of_real_add)

lemma powser_limit_0:
  fixes a :: "nat \ 'a::{real_normed_field,banach}"
  assumes s: "0 < s"
    and sm: "\x. norm x < s \ (\n. a n * x ^ n) sums (f x)"
  shows "(f \ a 0) (at 0)"
proof -
  have "norm (of_real s / 2 :: 'a) < s"
    using s  by (auto simp: norm_divide)
  then have "summable (\n. a n * (of_real s / 2) ^ n)"
    by (rule sums_summable [OF sm])
  then have "((\x. \n. a n * x ^ n) has_field_derivative (\n. diffs a n * 0 ^ n)) (at 0)"
    by (rule termdiffs_strong) (use s in \<open>auto simp: norm_divide\<close>)
  then have "isCont (\x. \n. a n * x ^ n) 0"
    by (blast intro: DERIV_continuous)
  then have "((\x. \n. a n * x ^ n) \ a 0) (at 0)"
    by (simp add: continuous_within)
  moreover have "(\x. f x - (\n. a n * x ^ n)) \0\ 0"
    apply (clarsimp simp: LIM_eq)
    apply (rule_tac x=s in exI)
    using s sm sums_unique by fastforce
  ultimately show ?thesis
    by (rule Lim_transform)
qed

lemma powser_limit_0_strong:
  fixes a :: "nat \ 'a::{real_normed_field,banach}"
  assumes s: "0 < s"
    and sm: "\x. x \ 0 \ norm x < s \ (\n. a n * x ^ n) sums (f x)"
  shows "(f \ a 0) (at 0)"
proof -
  have *: "((\x. if x = 0 then a 0 else f x) \ a 0) (at 0)"
    by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
  show ?thesis
    using "*" by (auto cong: Lim_cong_within)
qed

subsection \<open>Derivability of power series\<close>

lemma DERIV_series':
  fixes f :: "real \ nat \ real"
  assumes DERIV_f: "\ n. DERIV (\ x. f x n) x0 :> (f' x0 n)"
    and allf_summable: "\ x. x \ {a <..< b} \ summable (f x)"
    and x0_in_I: "x0 \ {a <..< b}"
    and "summable (f' x0)"
    and "summable L"
    and L_def: "\n x y. x \ {a <..< b} \ y \ {a <..< b} \ \f x n - f y n\ \ L n * \x - y\"
  shows "DERIV (\ x. suminf (f x)) x0 :> (suminf (f' x0))"
  unfolding DERIV_def
proof (rule LIM_I)
  fix r :: real
  assume "0 < r" then have "0 < r/3" by auto

  obtain N_L where N_L: "\ n. N_L \ n \ \ \ i. L (i + n) \ < r/3"
    using suminf_exist_split[OF \<open>0 < r/3\<close> \<open>summable L\<close>] by auto

  obtain N_f' where N_f': "\ n. N_f' \ n \ \ \ i. f' x0 (i + n) \ < r/3"
    using suminf_exist_split[OF \<open>0 < r/3\<close> \<open>summable (f' x0)\<close>] by auto

  let ?N = "Suc (max N_L N_f')"
  have "\ \ i. f' x0 (i + ?N) \ < r/3" (is "?f'_part < r/3")
    and L_estimate: "\ \ i. L (i + ?N) \ < r/3"
    using N_L[of "?N"] and N_f' [of "?N"] by auto

  let ?diff = "\i x. (f (x0 + x) i - f x0 i) / x"

  let ?r = "r / (3 * real ?N)"
  from \<open>0 < r\<close> have "0 < ?r" by simp

  let ?s = "\n. SOME s. 0 < s \ (\ x. x \ 0 \ \ x \ < s \ \ ?diff n x - f' x0 n \ < ?r)"
  define S' where "S' = Min (?s ` {..< ?N })"

  have "0 < S'"
    unfolding S'_def
  proof (rule iffD2[OF Min_gr_iff])
    show "\x \ (?s ` {..< ?N }). 0 < x"
    proof
      fix x
      assume "x \ ?s ` {..
      then obtain n where "x = ?s n" and "n \ {..
        using image_iff[THEN iffD1] by blast
      from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF \<open>0 < ?r\<close>, unfolded real_norm_def]
      obtain s where s_bound: "0 < s \ (\x. x \ 0 \ \x\ < s \ \?diff n x - f' x0 n\ < ?r)"
        by auto
      have "0 < ?s n"
        by (rule someI2[where a=s]) (auto simp: s_bound simp del: of_nat_Suc)
      then show "0 < x" by (simp only: \<open>x = ?s n\<close>)
    qed
  qed auto

  define S where "S = min (min (x0 - a) (b - x0)) S'"
  then have "0 < S" and S_a: "S \ x0 - a" and S_b: "S \ b - x0"
    and "S \ S'" using x0_in_I and \0 < S'\
    by auto

  have "\(suminf (f (x0 + x)) - suminf (f x0)) / x - suminf (f' x0)\ < r"
    if "x \ 0" and "\x\ < S" for x
  proof -
    from that have x_in_I: "x0 + x \ {a <..< b}"
      using S_a S_b by auto

    note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
    note div_smbl = summable_divide[OF diff_smbl]
    note all_smbl = summable_diff[OF div_smbl \<open>summable (f' x0)\<close>]
    note ign = summable_ignore_initial_segment[where k="?N"]
    note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]]
    note div_shft_smbl = summable_divide[OF diff_shft_smbl]
    note all_shft_smbl = summable_diff[OF div_smbl ign[OF \<open>summable (f' x0)\<close>]]

    have 1: "\(\?diff (n + ?N) x\)\ \ L (n + ?N)" for n
    proof -
      have "\?diff (n + ?N) x\ \ L (n + ?N) * \(x0 + x) - x0\ / \x\"
        using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero]
        by (simp only: abs_divide)
      with \<open>x \<noteq> 0\<close> show ?thesis by auto
    qed
    note 2 = summable_rabs_comparison_test[OF _ ign[OF \<open>summable L\<close>]]
    from 1 have "\ \ i. ?diff (i + ?N) x \ \ (\ i. L (i + ?N))"
      by (metis (lifting) abs_idempotent
          order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF \<open>summable L\<close>]]])
    then have "\\i. ?diff (i + ?N) x\ \ r / 3" (is "?L_part \ r/3")
      using L_estimate by auto

    have "\\n \ (\n?diff n x - f' x0 n\)" ..
    also have "\ < (\n
    proof (rule sum_strict_mono)
      fix n
      assume "n \ {..< ?N}"
      have "\x\ < S" using \\x\ < S\ .
      also have "S \ S'" using \S \ S'\ .
      also have "S' \ ?s n"
        unfolding S'_def
      proof (rule Min_le_iff[THEN iffD2])
        have "?s n \ (?s ` {.. ?s n \ ?s n"
          using \<open>n \<in> {..< ?N}\<close> by auto
        then show "\ a \ (?s ` {.. ?s n"
          by blast
      qed auto
      finally have "\x\ < ?s n" .

      from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF \<open>0 < ?r\<close>,
          unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2]
      have "\x. x \ 0 \ \x\ < ?s n \ \?diff n x - f' x0 n\ < ?r" .
      with \<open>x \<noteq> 0\<close> and \<open>\<bar>x\<bar> < ?s n\<close> show "\<bar>?diff n x - f' x0 n\<bar> < ?r"
        by blast
    qed auto
    also have "\ = of_nat (card {..
      by (rule sum_constant)
    also have "\ = real ?N * ?r"
      by simp
    also have "\ = r/3"
      by (auto simp del: of_nat_Suc)
    finally have "\\n < r / 3" (is "?diff_part < r / 3") .

    from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
    have "\(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)\ =
        \<bar>\<Sum>n. ?diff n x - f' x0 n\<bar>"
      unfolding suminf_diff[OF div_smbl \<open>summable (f' x0)\<close>, symmetric]
      using suminf_divide[OF diff_smbl, symmetric] by auto
    also have "\ \ ?diff_part + \(\n. ?diff (n + ?N) x) - (\ n. f' x0 (n + ?N))\"
      unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"]
      unfolding suminf_diff[OF div_shft_smbl ign[OF \<open>summable (f' x0)\<close>]]
      apply (simp only: add.commute)
      using abs_triangle_ineq by blast
    also have "\ \ ?diff_part + ?L_part + ?f'_part"
      using abs_triangle_ineq4 by auto
    also have "\ < r /3 + r/3 + r/3"
      using \<open>?diff_part < r/3\<close> \<open>?L_part \<le> r/3\<close> and \<open>?f'_part < r/3\<close>
      by (rule add_strict_mono [OF add_less_le_mono])
    finally show ?thesis
      by auto
  qed
  then show "\s > 0. \ x. x \ 0 \ norm (x - 0) < s \
      norm (((\<Sum>n. f (x0 + x) n) - (\<Sum>n. f x0 n)) / x - (\<Sum>n. f' x0 n)) < r"
    using \<open>0 < S\<close> by auto
qed

lemma DERIV_power_series':
  fixes f :: "nat \ real"
  assumes converges: "\x. x \ {-R <..< R} \ summable (\n. f n * real (Suc n) * x^n)"
    and x0_in_I: "x0 \ {-R <..< R}"
    and "0 < R"
  shows "DERIV (\x. (\n. f n * x^(Suc n))) x0 :> (\n. f n * real (Suc n) * x0^n)"
    (is "DERIV (\x. suminf (?f x)) x0 :> suminf (?f' x0)")
proof -
  have for_subinterval: "DERIV (\x. suminf (?f x)) x0 :> suminf (?f' x0)"
    if "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'" for R'
  proof -
    from that have "x0 \ {-R' <..< R'}" and "R' \ {-R <..< R}" and "x0 \ {-R <..< R}"
      by auto
    show ?thesis
    proof (rule DERIV_series')
      show "summable (\ n. \f n * real (Suc n) * R'^n\)"
      proof -
        have "(R' + R) / 2 < R" and "0 < (R' + R) / 2"
          using \<open>0 < R'\<close> \<open>0 < R\<close> \<open>R' < R\<close> by (auto simp: field_simps)
        then have in_Rball: "(R' + R) / 2 \ {-R <..< R}"
          using \<open>R' < R\<close> by auto
        have "norm R' < norm ((R' + R) / 2)"
          using \<open>0 < R'\<close> \<open>0 < R\<close> \<open>R' < R\<close> by (auto simp: field_simps)
        from powser_insidea[OF converges[OF in_Rball] this] show ?thesis
          by auto
      qed
    next
      fix n x y
      assume "x \ {-R' <..< R'}" and "y \ {-R' <..< R'}"
      show "\?f x n - ?f y n\ \ \f n * real (Suc n) * R'^n\ * \x-y\"
      proof -
        have "\f n * x ^ (Suc n) - f n * y ^ (Suc n)\ =
          (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar>"
          unfolding right_diff_distrib[symmetric] diff_power_eq_sum abs_mult
          by auto
        also have "\ \ (\f n\ * \x-y\) * (\real (Suc n)\ * \R' ^ n\)"
        proof (rule mult_left_mono)
          have "\\p \ (\px ^ p * y ^ (n - p)\)"
            by (rule sum_abs)
          also have "\ \ (\p
          proof (rule sum_mono)
            fix p
            assume "p \ {..
            then have "p \ n" by auto
            have "\x^n\ \ R'^n" if "x \ {-R'<..
            proof -
              from that have "\x\ \ R'" by auto
              then show ?thesis
                unfolding power_abs by (rule power_mono) auto
            qed
            from mult_mono[OF this[OF \<open>x \<in> {-R'<..<R'}\<close>, of p] this[OF \<open>y \<in> {-R'<..<R'}\<close>, of "n-p"]]
              and \<open>0 < R'\<close>
            have "\x^p * y^(n - p)\ \ R'^p * R'^(n - p)"
              unfolding abs_mult by auto
            then show "\x^p * y^(n - p)\ \ R'^n"
              unfolding power_add[symmetric] using \<open>p \<le> n\<close> by auto
          qed
          also have "\ = real (Suc n) * R' ^ n"
            unfolding sum_constant card_atLeastLessThan by auto
          finally show "\\p \ \real (Suc n)\ * \R' ^ n\"
            unfolding abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF \<open>0 < R'\<close>]]]
            by linarith
          show "0 \ \f n\ * \x - y\"
            unfolding abs_mult[symmetric] by auto
        qed
        also have "\ = \f n * real (Suc n) * R' ^ n\ * \x - y\"
          unfolding abs_mult mult.assoc[symmetric] by algebra
        finally show ?thesis .
      qed
    next
      show "DERIV (\x. ?f x n) x0 :> ?f' x0 n" for n
        by (auto intro!: derivative_eq_intros simp del: power_Suc)
    next
      fix x
      assume "x \ {-R' <..< R'}"
      then have "R' \ {-R <..< R}" and "norm x < norm R'"
        using assms \<open>R' < R\<close> by auto
      have "summable (\n. f n * x^n)"
      proof (rule summable_comparison_test, intro exI allI impI)
        fix n
        have le: "\f n\ * 1 \ \f n\ * real (Suc n)"
          by (rule mult_left_mono) auto
        show "norm (f n * x^n) \ norm (f n * real (Suc n) * x^n)"
          unfolding real_norm_def abs_mult
          using le mult_right_mono by fastforce
      qed (rule powser_insidea[OF converges[OF \<open>R' \<in> {-R <..< R}\<close>] \<open>norm x < norm R'\<close>])
      from this[THEN summable_mult2[where c=x], simplified mult.assoc, simplified mult.commute]
      show "summable (?f x)" by auto
    next
      show "summable (?f' x0)"
        using converges[OF \<open>x0 \<in> {-R <..< R}\<close>] .
      show "x0 \ {-R' <..< R'}"
        using \<open>x0 \<in> {-R' <..< R'}\<close> .
    qed
  qed
  let ?R = "(R + \x0\) / 2"
  have "\x0\ < ?R"
    using assms by (auto simp: field_simps)
  then have "- ?R < x0"
  proof (cases "x0 < 0")
    case True
    then have "- x0 < ?R"
      using \<open>\<bar>x0\<bar> < ?R\<close> by auto
    then show ?thesis
      unfolding neg_less_iff_less[symmetric, of "- x0"] by auto
  next
    case False
    have "- ?R < 0" using assms by auto
    also have "\ \ x0" using False by auto
    finally show ?thesis .
  qed
  then have "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R"
    using assms by (auto simp: field_simps)
  from for_subinterval[OF this] show ?thesis .
qed

lemma geometric_deriv_sums:
  fixes z :: "'a :: {real_normed_field,banach}"
  assumes "norm z < 1"
  shows   "(\n. of_nat (Suc n) * z ^ n) sums (1 / (1 - z)^2)"
proof -
  have "(\n. diffs (\n. 1) n * z^n) sums (1 / (1 - z)^2)"
  proof (rule termdiffs_sums_strong)
    fix z :: 'a assume "norm z < 1"
    thus "(\n. 1 * z^n) sums (1 / (1 - z))" by (simp add: geometric_sums)
  qed (insert assms, auto intro!: derivative_eq_intros simp: power2_eq_square)
  thus ?thesis unfolding diffs_def by simp
qed

lemma isCont_pochhammer [continuous_intros]: "isCont (\z. pochhammer z n) z"
  for z :: "'a::real_normed_field"
  by (induct n) (auto simp: pochhammer_rec')

lemma continuous_on_pochhammer [continuous_intros]: "continuous_on A (\z. pochhammer z n)"
  for A :: "'a::real_normed_field set"
  by (intro continuous_at_imp_continuous_on ballI isCont_pochhammer)

lemmas continuous_on_pochhammer' [continuous_intros] =
  continuous_on_compose2[OF continuous_on_pochhammer _ subset_UNIV]

subsection \<open>Exponential Function\<close>

definition exp :: "'a \ 'a::{real_normed_algebra_1,banach}"
  where "exp = (\x. \n. x^n /\<^sub>R fact n)"

lemma summable_exp_generic:
  fixes x :: "'a::{real_normed_algebra_1,banach}"
  defines S_def: "S \ \n. x^n /\<^sub>R fact n"
  shows "summable S"
proof -
  have S_Suc: "\n. S (Suc n) = (x * S n) /\<^sub>R (Suc n)"
    unfolding S_def by (simp del: mult_Suc)
  obtain r :: real where r0: "0 < r" and r1: "r < 1"
    using dense [OF zero_less_one] by fast
  obtain N :: nat where N: "norm x < real N * r"
    using ex_less_of_nat_mult r0 by auto
  from r1 show ?thesis
  proof (rule summable_ratio_test [rule_format])
    fix n :: nat
    assume n: "N \ n"
    have "norm x \ real N * r"
      using N by (rule order_less_imp_le)
    also have "real N * r \ real (Suc n) * r"
      using r0 n by (simp add: mult_right_mono)
    finally have "norm x * norm (S n) \ real (Suc n) * r * norm (S n)"
      using norm_ge_zero by (rule mult_right_mono)
    then have "norm (x * S n) \ real (Suc n) * r * norm (S n)"
      by (rule order_trans [OF norm_mult_ineq])
    then have "norm (x * S n) / real (Suc n) \ r * norm (S n)"
      by (simp add: pos_divide_le_eq ac_simps)
    then show "norm (S (Suc n)) \ r * norm (S n)"
      by (simp add: S_Suc inverse_eq_divide)
  qed
qed

lemma summable_norm_exp: "summable (\n. norm (x^n /\<^sub>R fact n))"
  for x :: "'a::{real_normed_algebra_1,banach}"
proof (rule summable_norm_comparison_test [OF exI, rule_format])
  show "summable (\n. norm x^n /\<^sub>R fact n)"
    by (rule summable_exp_generic)
  show "norm (x^n /\<^sub>R fact n) \ norm x^n /\<^sub>R fact n" for n
    by (simp add: norm_power_ineq)
qed

lemma summable_exp: "summable (\n. inverse (fact n) * x^n)"
  for x :: "'a::{real_normed_field,banach}"
  using summable_exp_generic [where x=x]
  by (simp add: scaleR_conv_of_real nonzero_of_real_inverse)

lemma exp_converges: "(\n. x^n /\<^sub>R fact n) sums exp x"
  unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])

lemma exp_fdiffs:
  "diffs (\n. inverse (fact n)) = (\n. inverse (fact n :: 'a::{real_normed_field,banach}))"
  by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
      del: mult_Suc of_nat_Suc)

lemma diffs_of_real: "diffs (\n. of_real (f n)) = (\n. of_real (diffs f n))"
  by (simp add: diffs_def)

lemma DERIV_exp [simp]: "DERIV exp x :> exp x"
  unfolding exp_def scaleR_conv_of_real
proof (rule DERIV_cong)
  have sinv: "summable (\n. of_real (inverse (fact n)) * x ^ n)" for x::'a
    by (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])
  note xx = exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real]
  show "((\x. \n. of_real (inverse (fact n)) * x ^ n) has_field_derivative
        (\<Sum>n. diffs (\<lambda>n. of_real (inverse (fact n))) n * x ^ n))  (at x)"
    by (rule termdiffs [where K="of_real (1 + norm x)"]) (simp_all only: diffs_of_real exp_fdiffs sinv norm_of_real)
  show "(\n. diffs (\n. of_real (inverse (fact n))) n * x ^ n) = (\n. of_real (inverse (fact n)) * x ^ n)"
    by (simp add: diffs_of_real exp_fdiffs)
qed

declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
  and DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]

lemmas has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV]

lemma norm_exp: "norm (exp x) \ exp (norm x)"
proof -
  from summable_norm[OF summable_norm_exp, of x]
  have "norm (exp x) \ (\n. inverse (fact n) * norm (x^n))"
    by (simp add: exp_def)
  also have "\ \ exp (norm x)"
    using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
    by (auto simp: exp_def intro!: suminf_le norm_power_ineq)
  finally show ?thesis .
qed

lemma isCont_exp: "isCont exp x"
  for x :: "'a::{real_normed_field,banach}"
  by (rule DERIV_exp [THEN DERIV_isCont])

lemma isCont_exp' [simp]: "isCont f a \ isCont (\x. exp (f x)) a"
  for f :: "_ \'a::{real_normed_field,banach}"
  by (rule isCont_o2 [OF _ isCont_exp])

lemma tendsto_exp [tendsto_intros]: "(f \ a) F \ ((\x. exp (f x)) \ exp a) F"
  for f:: "_ \'a::{real_normed_field,banach}"
  by (rule isCont_tendsto_compose [OF isCont_exp])

lemma continuous_exp [continuous_intros]: "continuous F f \ continuous F (\x. exp (f x))"
  for f :: "_ \'a::{real_normed_field,banach}"
  unfolding continuous_def by (rule tendsto_exp)

lemma continuous_on_exp [continuous_intros]: "continuous_on s f \ continuous_on s (\x. exp (f x))"
  for f :: "_ \'a::{real_normed_field,banach}"
  unfolding continuous_on_def by (auto intro: tendsto_exp)

subsubsection \<open>Properties of the Exponential Function\<close>

lemma exp_zero [simp]: "exp 0 = 1"
  unfolding exp_def by (simp add: scaleR_conv_of_real)

lemma exp_series_add_commuting:
  fixes x y :: "'a::{real_normed_algebra_1,banach}"
  defines S_def: "S \ \x n. x^n /\<^sub>R fact n"
  assumes comm: "x * y = y * x"
  shows "S (x + y) n = (\i\n. S x i * S y (n - i))"
proof (induct n)
  case 0
  show ?case
    unfolding S_def by simp
next
  case (Suc n)
  have S_Suc: "\x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
    unfolding S_def by (simp del: mult_Suc)
  then have times_S: "\x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
    by simp
  have S_comm: "\n. S x n * y = y * S x n"
    by (simp add: power_commuting_commutes comm S_def)

  have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * (\i\n. S x i * S y (n - i))"
    by (metis Suc.hyps times_S)
  also have "\ = x * (\i\n. S x i * S y (n - i)) + y * (\i\n. S x i * S y (n - i))"
    by (rule distrib_right)
  also have "\ = (\i\n. x * S x i * S y (n - i)) + (\i\n. S x i * y * S y (n - i))"
    by (simp add: sum_distrib_left ac_simps S_comm)
  also have "\ = (\i\n. x * S x i * S y (n - i)) + (\i\n. S x i * (y * S y (n - i)))"
    by (simp add: ac_simps)
  also have "\ = (\i\n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n - i)))
                + (\<Sum>i\<le>n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))"
    by (simp add: times_S Suc_diff_le)
  also have "(\i\n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n - i)))
           = (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n - i)))"
    by (subst sum.atMost_Suc_shift) simp
  also have "(\i\n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))
           = (\<Sum>i\<le>Suc n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))"
    by simp
  also have "(\i\Suc n. real i *\<^sub>R (S x i * S y (Suc n - i)))
           + (\<Sum>i\<le>Suc n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))
           = (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n - i)))"
    by (simp flip: sum.distrib scaleR_add_left of_nat_add)
  also have "\ = real (Suc n) *\<^sub>R (\i\Suc n. S x i * S y (Suc n - i))"
    by (simp only: scaleR_right.sum)
  finally show "S (x + y) (Suc n) = (\i\Suc n. S x i * S y (Suc n - i))"
    by (simp del: sum.cl_ivl_Suc)
qed

lemma exp_add_commuting: "x * y = y * x \ exp (x + y) = exp x * exp y"
  by (simp only: exp_def Cauchy_product summable_norm_exp exp_series_add_commuting)

lemma exp_times_arg_commute: "exp A * A = A * exp A"
  by (simp add: exp_def suminf_mult[symmetric] summable_exp_generic power_commutes suminf_mult2)

lemma exp_add: "exp (x + y) = exp x * exp y"
  for x y :: "'a::{real_normed_field,banach}"
  by (rule exp_add_commuting) (simp add: ac_simps)

lemma exp_double: "exp(2 * z) = exp z ^ 2"
  by (simp add: exp_add_commuting mult_2 power2_eq_square)

lemmas mult_exp_exp = exp_add [symmetric]

lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
  unfolding exp_def
  apply (subst suminf_of_real [OF summable_exp_generic])
  apply (simp add: scaleR_conv_of_real)
  done

lemmas of_real_exp = exp_of_real[symmetric]

corollary exp_in_Reals [simp]: "z \ \ \ exp z \ \"
  by (metis Reals_cases Reals_of_real exp_of_real)

lemma exp_not_eq_zero [simp]: "exp x \ 0"
proof
  have "exp x * exp (- x) = 1"
    by (simp add: exp_add_commuting[symmetric])
  also assume "exp x = 0"
  finally show False by simp
qed

--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.131 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.