moved in some material from Euler-MacLaurin
authorpaulson <lp15@cam.ac.uk>
Mon Jan 08 17:11:25 2018 +0000 (16 months ago)
changeset 673712d9cf74943e1
parent 67370 86aa6e2abee1
child 67383 aacea75450b4
moved in some material from Euler-MacLaurin
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Uniform_Limit.thy
src/HOL/Limits.thy
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Jan 07 22:18:59 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Jan 08 17:11:25 2018 +0000
     1.3 @@ -401,6 +401,16 @@
     1.4    finally show \<dots> .
     1.5  qed (insert assms, auto)
     1.6  
     1.7 +lemma leibniz_rule_holomorphic:
     1.8 +  fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex"
     1.9 +  assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
    1.10 +  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
    1.11 +  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
    1.12 +  assumes "convex U"
    1.13 +  shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U"
    1.14 +  using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
    1.15 +  by (auto simp: holomorphic_on_def)
    1.16 +
    1.17  lemma DERIV_deriv_iff_field_differentiable:
    1.18    "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
    1.19    unfolding field_differentiable_def by (metis DERIV_imp_deriv)
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Jan 07 22:18:59 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jan 08 17:11:25 2018 +0000
     2.3 @@ -1217,7 +1217,7 @@
     2.4    using field_differentiable_def has_field_derivative_Ln by blast
     2.5  
     2.6  lemma field_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
     2.7 -         \<Longrightarrow> Ln field_differentiable (at z within s)"
     2.8 +         \<Longrightarrow> Ln field_differentiable (at z within S)"
     2.9    using field_differentiable_at_Ln field_differentiable_within_subset by blast
    2.10  
    2.11  lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
    2.12 @@ -1227,15 +1227,34 @@
    2.13     "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
    2.14    by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
    2.15  
    2.16 -lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) Ln"
    2.17 +lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Ln"
    2.18    using continuous_at_Ln continuous_at_imp_continuous_within by blast
    2.19  
    2.20 -lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s Ln"
    2.21 +lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S Ln"
    2.22    by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
    2.23  
    2.24 -lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
    2.25 +lemma continuous_on_Ln' [continuous_intros]: 
    2.26 +  "continuous_on S f \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S (\<lambda>x. Ln (f x))"
    2.27 +  by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto
    2.28 +
    2.29 +lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on S"
    2.30    by (simp add: field_differentiable_within_Ln holomorphic_on_def)
    2.31  
    2.32 +lemma tendsto_Ln [tendsto_intros]:
    2.33 +  fixes L F
    2.34 +  assumes "(f \<longlongrightarrow> L) F" "L \<notin> \<real>\<^sub>\<le>\<^sub>0"
    2.35 +  shows   "((\<lambda>x. Ln (f x)) \<longlongrightarrow> Ln L) F"
    2.36 +proof -
    2.37 +  have "nhds L \<ge> filtermap f F"
    2.38 +    using assms(1) by (simp add: filterlim_def)
    2.39 +  moreover have "\<forall>\<^sub>F y in nhds L. y \<in> - \<real>\<^sub>\<le>\<^sub>0"
    2.40 +    using eventually_nhds_in_open[of "- \<real>\<^sub>\<le>\<^sub>0" L] assms by (auto simp: open_Compl)
    2.41 +  ultimately have "\<forall>\<^sub>F y in filtermap f F. y \<in> - \<real>\<^sub>\<le>\<^sub>0" by (rule filter_leD)
    2.42 +  moreover have "continuous_on (-\<real>\<^sub>\<le>\<^sub>0) Ln" by (rule continuous_on_Ln) auto
    2.43 +  ultimately show ?thesis using continuous_on_tendsto_compose[of "- \<real>\<^sub>\<le>\<^sub>0" Ln f L F] assms
    2.44 +    by (simp add: eventually_filtermap)
    2.45 +qed
    2.46 +
    2.47  lemma divide_ln_mono:
    2.48    fixes x y::real
    2.49    assumes "3 \<le> x" "x \<le> y"
     3.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Jan 07 22:18:59 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Jan 08 17:11:25 2018 +0000
     3.3 @@ -6078,6 +6078,86 @@
     3.4    using assms
     3.5    by auto
     3.6  
     3.7 +
     3.8 +lemma uniformly_convergent_improper_integral:
     3.9 +  fixes f :: "'b \<Rightarrow> real \<Rightarrow> 'a :: {banach}"
    3.10 +  assumes deriv: "\<And>x. x \<ge> a \<Longrightarrow> (G has_field_derivative g x) (at x within {a..})"
    3.11 +  assumes integrable: "\<And>a' b x. x \<in> A \<Longrightarrow> a' \<ge> a \<Longrightarrow> b \<ge> a' \<Longrightarrow> f x integrable_on {a'..b}"
    3.12 +  assumes G: "convergent G"
    3.13 +  assumes le: "\<And>y x. y \<in> A \<Longrightarrow> x \<ge> a \<Longrightarrow> norm (f y x) \<le> g x"
    3.14 +  shows   "uniformly_convergent_on A (\<lambda>b x. integral {a..b} (f x))"
    3.15 +proof (intro Cauchy_uniformly_convergent uniformly_Cauchy_onI', goal_cases)
    3.16 +  case (1 \<epsilon>)
    3.17 +  from G have "Cauchy G"
    3.18 +    by (auto intro!: convergent_Cauchy)
    3.19 +  with 1 obtain M where M: "dist (G (real m)) (G (real n)) < \<epsilon>" if "m \<ge> M" "n \<ge> M" for m n
    3.20 +    by (force simp: Cauchy_def)
    3.21 +  define M' where "M' = max (nat \<lceil>a\<rceil>) M"
    3.22 +
    3.23 +  show ?case
    3.24 +  proof (rule exI[of _ M'], safe, goal_cases)
    3.25 +    case (1 x m n)
    3.26 +    have M': "M' \<ge> a" "M' \<ge> M" unfolding M'_def by linarith+
    3.27 +    have int_g: "(g has_integral (G (real n) - G (real m))) {real m..real n}"
    3.28 +      using 1 M' by (intro fundamental_theorem_of_calculus) 
    3.29 +                    (auto simp: has_field_derivative_iff_has_vector_derivative [symmetric] 
    3.30 +                          intro!: DERIV_subset[OF deriv])
    3.31 +    have int_f: "f x integrable_on {a'..real n}" if "a' \<ge> a" for a'
    3.32 +      using that 1 by (cases "a' \<le> real n") (auto intro: integrable)
    3.33 +
    3.34 +    have "dist (integral {a..real m} (f x)) (integral {a..real n} (f x)) =
    3.35 +            norm (integral {a..real n} (f x) - integral {a..real m} (f x))"
    3.36 +      by (simp add: dist_norm norm_minus_commute)
    3.37 +    also have "integral {a..real m} (f x) + integral {real m..real n} (f x) = 
    3.38 +                 integral {a..real n} (f x)"
    3.39 +      using M' and 1 by (intro integral_combine int_f) auto
    3.40 +    hence "integral {a..real n} (f x) - integral {a..real m} (f x) = 
    3.41 +             integral {real m..real n} (f x)"
    3.42 +      by (simp add: algebra_simps)
    3.43 +    also have "norm \<dots> \<le> integral {real m..real n} g"
    3.44 +      using le 1 M' int_f int_g by (intro integral_norm_bound_integral) auto 
    3.45 +    also from int_g have "integral {real m..real n} g = G (real n) - G (real m)"
    3.46 +      by (simp add: has_integral_iff)
    3.47 +    also have "\<dots> \<le> dist (G m) (G n)" 
    3.48 +      by (simp add: dist_norm)
    3.49 +    also from 1 and M' have "\<dots> < \<epsilon>"
    3.50 +      by (intro M) auto
    3.51 +    finally show ?case .
    3.52 +  qed
    3.53 +qed
    3.54 +
    3.55 +lemma uniformly_convergent_improper_integral':
    3.56 +  fixes f :: "'b \<Rightarrow> real \<Rightarrow> 'a :: {banach, real_normed_algebra}"
    3.57 +  assumes deriv: "\<And>x. x \<ge> a \<Longrightarrow> (G has_field_derivative g x) (at x within {a..})"
    3.58 +  assumes integrable: "\<And>a' b x. x \<in> A \<Longrightarrow> a' \<ge> a \<Longrightarrow> b \<ge> a' \<Longrightarrow> f x integrable_on {a'..b}"
    3.59 +  assumes G: "convergent G"
    3.60 +  assumes le: "eventually (\<lambda>x. \<forall>y\<in>A. norm (f y x) \<le> g x) at_top"
    3.61 +  shows   "uniformly_convergent_on A (\<lambda>b x. integral {a..b} (f x))"
    3.62 +proof -
    3.63 +  from le obtain a'' where le: "\<And>y x. y \<in> A \<Longrightarrow> x \<ge> a'' \<Longrightarrow> norm (f y x) \<le> g x"
    3.64 +    by (auto simp: eventually_at_top_linorder)
    3.65 +  define a' where "a' = max a a''"
    3.66 +
    3.67 +  have "uniformly_convergent_on A (\<lambda>b x. integral {a'..real b} (f x))"
    3.68 +  proof (rule uniformly_convergent_improper_integral)
    3.69 +    fix t assume t: "t \<ge> a'"
    3.70 +    hence "(G has_field_derivative g t) (at t within {a..})"
    3.71 +      by (intro deriv) (auto simp: a'_def)
    3.72 +    moreover have "{a'..} \<subseteq> {a..}" unfolding a'_def by auto
    3.73 +    ultimately show "(G has_field_derivative g t) (at t within {a'..})"
    3.74 +      by (rule DERIV_subset)
    3.75 +  qed (insert le, auto simp: a'_def intro: integrable G)
    3.76 +  hence "uniformly_convergent_on A (\<lambda>b x. integral {a..a'} (f x) + integral {a'..real b} (f x))" 
    3.77 +    (is ?P) by (intro uniformly_convergent_add) auto
    3.78 +  also have "eventually (\<lambda>x. \<forall>y\<in>A. integral {a..a'} (f y) + integral {a'..x} (f y) =
    3.79 +                   integral {a..x} (f y)) sequentially"
    3.80 +    by (intro eventually_mono [OF eventually_ge_at_top[of "nat \<lceil>a'\<rceil>"]] ballI integral_combine)
    3.81 +       (auto simp: a'_def intro: integrable)
    3.82 +  hence "?P \<longleftrightarrow> ?thesis"
    3.83 +    by (intro uniformly_convergent_cong) simp_all
    3.84 +  finally show ?thesis .
    3.85 +qed
    3.86 +
    3.87  subsection \<open>differentiation under the integral sign\<close>
    3.88  
    3.89  lemma integral_continuous_on_param:
    3.90 @@ -6283,6 +6363,15 @@
    3.91      done
    3.92  qed
    3.93  
    3.94 +lemma leibniz_rule_field_differentiable:
    3.95 +  fixes f::"'a::{real_normed_field, banach} \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'a"
    3.96 +  assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
    3.97 +  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
    3.98 +  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
    3.99 +  assumes "x0 \<in> U" "convex U"
   3.100 +  shows "(\<lambda>x. integral (cbox a b) (f x)) field_differentiable at x0 within U"
   3.101 +  using leibniz_rule_field_derivative[OF assms] by (auto simp: field_differentiable_def)
   3.102 +
   3.103  
   3.104  subsection \<open>Exchange uniform limit and integral\<close>
   3.105  
     4.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Jan 07 22:18:59 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Mon Jan 08 17:11:25 2018 +0000
     4.3 @@ -108,8 +108,7 @@
     4.4      using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
     4.5  qed
     4.6  
     4.7 -lemma
     4.8 -  tendsto_uniform_limitI:
     4.9 +lemma tendsto_uniform_limitI:
    4.10    assumes "uniform_limit S f l F"
    4.11    assumes "x \<in> S"
    4.12    shows "((\<lambda>y. f y x) \<longlongrightarrow> l x) F"
    4.13 @@ -184,6 +183,12 @@
    4.14    shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
    4.15    using assms by (intro uniform_limit_cong always_eventually) blast+
    4.16  
    4.17 +lemma uniformly_convergent_cong:
    4.18 +  assumes "eventually (\<lambda>x. \<forall>y\<in>A. f x y = g x y) sequentially" "A = B"
    4.19 +  shows "uniformly_convergent_on A f \<longleftrightarrow> uniformly_convergent_on B g"
    4.20 +  unfolding uniformly_convergent_on_def assms(2) [symmetric]
    4.21 +  by (intro iff_exI uniform_limit_cong eventually_mono [OF assms(1)]) auto
    4.22 +
    4.23  lemma uniformly_convergent_uniform_limit_iff:
    4.24    "uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
    4.25  proof
    4.26 @@ -203,6 +208,10 @@
    4.27  lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
    4.28    by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
    4.29  
    4.30 +lemma uniformly_convergent_on_const [simp,intro]:
    4.31 +  "uniformly_convergent_on A (\<lambda>_. c)"
    4.32 +  by (auto simp: uniformly_convergent_on_def uniform_limit_iff intro!: exI[of _ c])
    4.33 +
    4.34  text\<open>Cauchy-type criteria for uniform convergence.\<close>
    4.35  
    4.36  lemma Cauchy_uniformly_convergent:
    4.37 @@ -402,6 +411,17 @@
    4.38      by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
    4.39  qed
    4.40  
    4.41 +lemma (in bounded_linear) uniformly_convergent_on:
    4.42 +  assumes "uniformly_convergent_on A g"
    4.43 +  shows   "uniformly_convergent_on A (\<lambda>x y. f (g x y))"
    4.44 +proof -
    4.45 +  from assms obtain l where "uniform_limit A g l sequentially"
    4.46 +    unfolding uniformly_convergent_on_def by blast
    4.47 +  hence "uniform_limit A (\<lambda>x y. f (g x y)) (\<lambda>x. f (l x)) sequentially"
    4.48 +    by (rule uniform_limit)
    4.49 +  thus ?thesis unfolding uniformly_convergent_on_def by blast
    4.50 +qed
    4.51 +
    4.52  lemmas bounded_linear_uniform_limit_intros[uniform_limit_intros] =
    4.53    bounded_linear.uniform_limit[OF bounded_linear_Im]
    4.54    bounded_linear.uniform_limit[OF bounded_linear_Re]
     5.1 --- a/src/HOL/Limits.thy	Sun Jan 07 22:18:59 2018 +0100
     5.2 +++ b/src/HOL/Limits.thy	Mon Jan 08 17:11:25 2018 +0000
     5.3 @@ -1081,6 +1081,77 @@
     5.4    qed
     5.5  qed force
     5.6  
     5.7 +lemma filterlim_at_infinity_imp_norm_at_top:
     5.8 +  fixes F
     5.9 +  assumes "filterlim f at_infinity F"
    5.10 +  shows   "filterlim (\<lambda>x. norm (f x)) at_top F"
    5.11 +proof -
    5.12 +  {
    5.13 +    fix r :: real 
    5.14 +    have "\<forall>\<^sub>F x in F. r \<le> norm (f x)" using filterlim_at_infinity[of 0 f F] assms 
    5.15 +      by (cases "r > 0") 
    5.16 +         (auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero])
    5.17 +  }
    5.18 +  thus ?thesis by (auto simp: filterlim_at_top)
    5.19 +qed
    5.20 +  
    5.21 +lemma filterlim_norm_at_top_imp_at_infinity:
    5.22 +  fixes F
    5.23 +  assumes "filterlim (\<lambda>x. norm (f x)) at_top F"
    5.24 +  shows   "filterlim f at_infinity F"
    5.25 +  using filterlim_at_infinity[of 0 f F] assms by (auto simp: filterlim_at_top)
    5.26 +
    5.27 +lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity"
    5.28 +  by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident)
    5.29 +
    5.30 +lemma eventually_not_equal_at_infinity:
    5.31 +  "eventually (\<lambda>x. x \<noteq> (a :: 'a :: {real_normed_vector})) at_infinity"
    5.32 +proof -
    5.33 +  from filterlim_norm_at_top[where 'a = 'a]
    5.34 +    have "\<forall>\<^sub>F x in at_infinity. norm a < norm (x::'a)" by (auto simp: filterlim_at_top_dense)
    5.35 +  thus ?thesis by eventually_elim auto
    5.36 +qed
    5.37 +
    5.38 +lemma filterlim_int_of_nat_at_topD:
    5.39 +  fixes F
    5.40 +  assumes "filterlim (\<lambda>x. f (int x)) F at_top"
    5.41 +  shows   "filterlim f F at_top"
    5.42 +proof -
    5.43 +  have "filterlim (\<lambda>x. f (int (nat x))) F at_top"
    5.44 +    by (rule filterlim_compose[OF assms filterlim_nat_sequentially])
    5.45 +  also have "?this \<longleftrightarrow> filterlim f F at_top"
    5.46 +    by (intro filterlim_cong refl eventually_mono [OF eventually_ge_at_top[of "0::int"]]) auto
    5.47 +  finally show ?thesis .
    5.48 +qed
    5.49 +
    5.50 +lemma filterlim_int_sequentially [tendsto_intros]:
    5.51 +  "filterlim int at_top sequentially"
    5.52 +  unfolding filterlim_at_top
    5.53 +proof
    5.54 +  fix C :: int
    5.55 +  show "eventually (\<lambda>n. int n \<ge> C) at_top"
    5.56 +    using eventually_ge_at_top[of "nat \<lceil>C\<rceil>"] by eventually_elim linarith
    5.57 +qed
    5.58 +
    5.59 +lemma filterlim_real_of_int_at_top [tendsto_intros]:
    5.60 +  "filterlim real_of_int at_top at_top"
    5.61 +  unfolding filterlim_at_top
    5.62 +proof
    5.63 +  fix C :: real
    5.64 +  show "eventually (\<lambda>n. real_of_int n \<ge> C) at_top"
    5.65 +    using eventually_ge_at_top[of "\<lceil>C\<rceil>"] by eventually_elim linarith
    5.66 +qed
    5.67 +
    5.68 +lemma filterlim_abs_real: "filterlim (abs::real \<Rightarrow> real) at_top at_top"
    5.69 +proof (subst filterlim_cong[OF refl refl])
    5.70 +  from eventually_ge_at_top[of "0::real"] show "eventually (\<lambda>x::real. \<bar>x\<bar> = x) at_top"
    5.71 +    by eventually_elim simp
    5.72 +qed (simp_all add: filterlim_ident)
    5.73 +
    5.74 +lemma filterlim_of_real_at_infinity [tendsto_intros]:
    5.75 +  "filterlim (of_real :: real \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity at_top"
    5.76 +  by (intro filterlim_norm_at_top_imp_at_infinity) (auto simp: filterlim_abs_real)
    5.77 +    
    5.78  lemma not_tendsto_and_filterlim_at_infinity:
    5.79    fixes c :: "'a::real_normed_vector"
    5.80    assumes "F \<noteq> bot"
    5.81 @@ -1534,6 +1605,14 @@
    5.82    shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot"
    5.83    using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot)
    5.84  
    5.85 +lemma filterlim_power_at_infinity [tendsto_intros]:
    5.86 +  fixes F and f :: "'a \<Rightarrow> 'b :: real_normed_div_algebra"
    5.87 +  assumes "filterlim f at_infinity F" "n > 0"
    5.88 +  shows   "filterlim (\<lambda>x. f x ^ n) at_infinity F"
    5.89 +  by (rule filterlim_norm_at_top_imp_at_infinity)
    5.90 +     (auto simp: norm_power intro!: filterlim_pow_at_top assms 
    5.91 +           intro: filterlim_at_infinity_imp_norm_at_top)
    5.92 +
    5.93  lemma filterlim_tendsto_add_at_top:
    5.94    assumes f: "(f \<longlongrightarrow> c) F"
    5.95      and g: "LIM x F. g x :> at_top"
     6.1 --- a/src/HOL/Parity.thy	Sun Jan 07 22:18:59 2018 +0100
     6.2 +++ b/src/HOL/Parity.thy	Mon Jan 08 17:11:25 2018 +0000
     6.3 @@ -483,6 +483,9 @@
     6.4  lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
     6.5    by (cases "even (n + k)") auto
     6.6  
     6.7 +lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)"
     6.8 +  by (induct n) auto
     6.9 +
    6.10  end
    6.11  
    6.12  context linordered_idom