# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1515431485 0
# Node ID 2d9cf74943e14bf732909f21006ff74563248ffc
# Parent  86aa6e2abee15f911ec164bce5f405cf26e9c86c
moved in some material from Euler-MacLaurin

diff -r 86aa6e2abee1 -r 2d9cf74943e1 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Jan 07 22:18:59 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Jan 08 17:11:25 2018 +0000
@@ -401,6 +401,16 @@
   finally show \<dots> .
 qed (insert assms, auto)
 
+lemma leibniz_rule_holomorphic:
+  fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex"
+  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)"
+  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
+  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
+  assumes "convex U"
+  shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U"
+  using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
+  by (auto simp: holomorphic_on_def)
+
 lemma DERIV_deriv_iff_field_differentiable:
   "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
   unfolding field_differentiable_def by (metis DERIV_imp_deriv)
diff -r 86aa6e2abee1 -r 2d9cf74943e1 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Jan 07 22:18:59 2018 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jan 08 17:11:25 2018 +0000
@@ -1217,7 +1217,7 @@
   using field_differentiable_def has_field_derivative_Ln by blast
 
 lemma field_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
-         \<Longrightarrow> Ln field_differentiable (at z within s)"
+         \<Longrightarrow> Ln field_differentiable (at z within S)"
   using field_differentiable_at_Ln field_differentiable_within_subset by blast
 
 lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
@@ -1227,15 +1227,34 @@
    "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
   by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
 
-lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) Ln"
+lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Ln"
   using continuous_at_Ln continuous_at_imp_continuous_within by blast
 
-lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s Ln"
+lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S Ln"
   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
 
-lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
+lemma continuous_on_Ln' [continuous_intros]: 
+  "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))"
+  by (rule continuous_on_compose2[OF continuous_on_Ln, of "UNIV - nonpos_Reals" S f]) auto
+
+lemma holomorphic_on_Ln [holomorphic_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on S"
   by (simp add: field_differentiable_within_Ln holomorphic_on_def)
 
+lemma tendsto_Ln [tendsto_intros]:
+  fixes L F
+  assumes "(f \<longlongrightarrow> L) F" "L \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  shows   "((\<lambda>x. Ln (f x)) \<longlongrightarrow> Ln L) F"
+proof -
+  have "nhds L \<ge> filtermap f F"
+    using assms(1) by (simp add: filterlim_def)
+  moreover have "\<forall>\<^sub>F y in nhds L. y \<in> - \<real>\<^sub>\<le>\<^sub>0"
+    using eventually_nhds_in_open[of "- \<real>\<^sub>\<le>\<^sub>0" L] assms by (auto simp: open_Compl)
+  ultimately have "\<forall>\<^sub>F y in filtermap f F. y \<in> - \<real>\<^sub>\<le>\<^sub>0" by (rule filter_leD)
+  moreover have "continuous_on (-\<real>\<^sub>\<le>\<^sub>0) Ln" by (rule continuous_on_Ln) auto
+  ultimately show ?thesis using continuous_on_tendsto_compose[of "- \<real>\<^sub>\<le>\<^sub>0" Ln f L F] assms
+    by (simp add: eventually_filtermap)
+qed
+
 lemma divide_ln_mono:
   fixes x y::real
   assumes "3 \<le> x" "x \<le> y"
diff -r 86aa6e2abee1 -r 2d9cf74943e1 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Jan 07 22:18:59 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Jan 08 17:11:25 2018 +0000
@@ -6078,6 +6078,86 @@
   using assms
   by auto
 
+
+lemma uniformly_convergent_improper_integral:
+  fixes f :: "'b \<Rightarrow> real \<Rightarrow> 'a :: {banach}"
+  assumes deriv: "\<And>x. x \<ge> a \<Longrightarrow> (G has_field_derivative g x) (at x within {a..})"
+  assumes integrable: "\<And>a' b x. x \<in> A \<Longrightarrow> a' \<ge> a \<Longrightarrow> b \<ge> a' \<Longrightarrow> f x integrable_on {a'..b}"
+  assumes G: "convergent G"
+  assumes le: "\<And>y x. y \<in> A \<Longrightarrow> x \<ge> a \<Longrightarrow> norm (f y x) \<le> g x"
+  shows   "uniformly_convergent_on A (\<lambda>b x. integral {a..b} (f x))"
+proof (intro Cauchy_uniformly_convergent uniformly_Cauchy_onI', goal_cases)
+  case (1 \<epsilon>)
+  from G have "Cauchy G"
+    by (auto intro!: convergent_Cauchy)
+  with 1 obtain M where M: "dist (G (real m)) (G (real n)) < \<epsilon>" if "m \<ge> M" "n \<ge> M" for m n
+    by (force simp: Cauchy_def)
+  define M' where "M' = max (nat \<lceil>a\<rceil>) M"
+
+  show ?case
+  proof (rule exI[of _ M'], safe, goal_cases)
+    case (1 x m n)
+    have M': "M' \<ge> a" "M' \<ge> M" unfolding M'_def by linarith+
+    have int_g: "(g has_integral (G (real n) - G (real m))) {real m..real n}"
+      using 1 M' by (intro fundamental_theorem_of_calculus) 
+                    (auto simp: has_field_derivative_iff_has_vector_derivative [symmetric] 
+                          intro!: DERIV_subset[OF deriv])
+    have int_f: "f x integrable_on {a'..real n}" if "a' \<ge> a" for a'
+      using that 1 by (cases "a' \<le> real n") (auto intro: integrable)
+
+    have "dist (integral {a..real m} (f x)) (integral {a..real n} (f x)) =
+            norm (integral {a..real n} (f x) - integral {a..real m} (f x))"
+      by (simp add: dist_norm norm_minus_commute)
+    also have "integral {a..real m} (f x) + integral {real m..real n} (f x) = 
+                 integral {a..real n} (f x)"
+      using M' and 1 by (intro integral_combine int_f) auto
+    hence "integral {a..real n} (f x) - integral {a..real m} (f x) = 
+             integral {real m..real n} (f x)"
+      by (simp add: algebra_simps)
+    also have "norm \<dots> \<le> integral {real m..real n} g"
+      using le 1 M' int_f int_g by (intro integral_norm_bound_integral) auto 
+    also from int_g have "integral {real m..real n} g = G (real n) - G (real m)"
+      by (simp add: has_integral_iff)
+    also have "\<dots> \<le> dist (G m) (G n)" 
+      by (simp add: dist_norm)
+    also from 1 and M' have "\<dots> < \<epsilon>"
+      by (intro M) auto
+    finally show ?case .
+  qed
+qed
+
+lemma uniformly_convergent_improper_integral':
+  fixes f :: "'b \<Rightarrow> real \<Rightarrow> 'a :: {banach, real_normed_algebra}"
+  assumes deriv: "\<And>x. x \<ge> a \<Longrightarrow> (G has_field_derivative g x) (at x within {a..})"
+  assumes integrable: "\<And>a' b x. x \<in> A \<Longrightarrow> a' \<ge> a \<Longrightarrow> b \<ge> a' \<Longrightarrow> f x integrable_on {a'..b}"
+  assumes G: "convergent G"
+  assumes le: "eventually (\<lambda>x. \<forall>y\<in>A. norm (f y x) \<le> g x) at_top"
+  shows   "uniformly_convergent_on A (\<lambda>b x. integral {a..b} (f x))"
+proof -
+  from le obtain a'' where le: "\<And>y x. y \<in> A \<Longrightarrow> x \<ge> a'' \<Longrightarrow> norm (f y x) \<le> g x"
+    by (auto simp: eventually_at_top_linorder)
+  define a' where "a' = max a a''"
+
+  have "uniformly_convergent_on A (\<lambda>b x. integral {a'..real b} (f x))"
+  proof (rule uniformly_convergent_improper_integral)
+    fix t assume t: "t \<ge> a'"
+    hence "(G has_field_derivative g t) (at t within {a..})"
+      by (intro deriv) (auto simp: a'_def)
+    moreover have "{a'..} \<subseteq> {a..}" unfolding a'_def by auto
+    ultimately show "(G has_field_derivative g t) (at t within {a'..})"
+      by (rule DERIV_subset)
+  qed (insert le, auto simp: a'_def intro: integrable G)
+  hence "uniformly_convergent_on A (\<lambda>b x. integral {a..a'} (f x) + integral {a'..real b} (f x))" 
+    (is ?P) by (intro uniformly_convergent_add) auto
+  also have "eventually (\<lambda>x. \<forall>y\<in>A. integral {a..a'} (f y) + integral {a'..x} (f y) =
+                   integral {a..x} (f y)) sequentially"
+    by (intro eventually_mono [OF eventually_ge_at_top[of "nat \<lceil>a'\<rceil>"]] ballI integral_combine)
+       (auto simp: a'_def intro: integrable)
+  hence "?P \<longleftrightarrow> ?thesis"
+    by (intro uniformly_convergent_cong) simp_all
+  finally show ?thesis .
+qed
+
 subsection \<open>differentiation under the integral sign\<close>
 
 lemma integral_continuous_on_param:
@@ -6283,6 +6363,15 @@
     done
 qed
 
+lemma leibniz_rule_field_differentiable:
+  fixes f::"'a::{real_normed_field, banach} \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'a"
+  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)"
+  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
+  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
+  assumes "x0 \<in> U" "convex U"
+  shows "(\<lambda>x. integral (cbox a b) (f x)) field_differentiable at x0 within U"
+  using leibniz_rule_field_derivative[OF assms] by (auto simp: field_differentiable_def)
+
 
 subsection \<open>Exchange uniform limit and integral\<close>
 
diff -r 86aa6e2abee1 -r 2d9cf74943e1 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Jan 07 22:18:59 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Mon Jan 08 17:11:25 2018 +0000
@@ -108,8 +108,7 @@
     using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
 qed
 
-lemma
-  tendsto_uniform_limitI:
+lemma tendsto_uniform_limitI:
   assumes "uniform_limit S f l F"
   assumes "x \<in> S"
   shows "((\<lambda>y. f y x) \<longlongrightarrow> l x) F"
@@ -184,6 +183,12 @@
   shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
   using assms by (intro uniform_limit_cong always_eventually) blast+
 
+lemma uniformly_convergent_cong:
+  assumes "eventually (\<lambda>x. \<forall>y\<in>A. f x y = g x y) sequentially" "A = B"
+  shows "uniformly_convergent_on A f \<longleftrightarrow> uniformly_convergent_on B g"
+  unfolding uniformly_convergent_on_def assms(2) [symmetric]
+  by (intro iff_exI uniform_limit_cong eventually_mono [OF assms(1)]) auto
+
 lemma uniformly_convergent_uniform_limit_iff:
   "uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
 proof
@@ -203,6 +208,10 @@
 lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
   by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
 
+lemma uniformly_convergent_on_const [simp,intro]:
+  "uniformly_convergent_on A (\<lambda>_. c)"
+  by (auto simp: uniformly_convergent_on_def uniform_limit_iff intro!: exI[of _ c])
+
 text\<open>Cauchy-type criteria for uniform convergence.\<close>
 
 lemma Cauchy_uniformly_convergent:
@@ -402,6 +411,17 @@
     by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
 qed
 
+lemma (in bounded_linear) uniformly_convergent_on:
+  assumes "uniformly_convergent_on A g"
+  shows   "uniformly_convergent_on A (\<lambda>x y. f (g x y))"
+proof -
+  from assms obtain l where "uniform_limit A g l sequentially"
+    unfolding uniformly_convergent_on_def by blast
+  hence "uniform_limit A (\<lambda>x y. f (g x y)) (\<lambda>x. f (l x)) sequentially"
+    by (rule uniform_limit)
+  thus ?thesis unfolding uniformly_convergent_on_def by blast
+qed
+
 lemmas bounded_linear_uniform_limit_intros[uniform_limit_intros] =
   bounded_linear.uniform_limit[OF bounded_linear_Im]
   bounded_linear.uniform_limit[OF bounded_linear_Re]
diff -r 86aa6e2abee1 -r 2d9cf74943e1 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sun Jan 07 22:18:59 2018 +0100
+++ b/src/HOL/Limits.thy	Mon Jan 08 17:11:25 2018 +0000
@@ -1081,6 +1081,77 @@
   qed
 qed force
 
+lemma filterlim_at_infinity_imp_norm_at_top:
+  fixes F
+  assumes "filterlim f at_infinity F"
+  shows   "filterlim (\<lambda>x. norm (f x)) at_top F"
+proof -
+  {
+    fix r :: real 
+    have "\<forall>\<^sub>F x in F. r \<le> norm (f x)" using filterlim_at_infinity[of 0 f F] assms 
+      by (cases "r > 0") 
+         (auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero])
+  }
+  thus ?thesis by (auto simp: filterlim_at_top)
+qed
+  
+lemma filterlim_norm_at_top_imp_at_infinity:
+  fixes F
+  assumes "filterlim (\<lambda>x. norm (f x)) at_top F"
+  shows   "filterlim f at_infinity F"
+  using filterlim_at_infinity[of 0 f F] assms by (auto simp: filterlim_at_top)
+
+lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity"
+  by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident)
+
+lemma eventually_not_equal_at_infinity:
+  "eventually (\<lambda>x. x \<noteq> (a :: 'a :: {real_normed_vector})) at_infinity"
+proof -
+  from filterlim_norm_at_top[where 'a = 'a]
+    have "\<forall>\<^sub>F x in at_infinity. norm a < norm (x::'a)" by (auto simp: filterlim_at_top_dense)
+  thus ?thesis by eventually_elim auto
+qed
+
+lemma filterlim_int_of_nat_at_topD:
+  fixes F
+  assumes "filterlim (\<lambda>x. f (int x)) F at_top"
+  shows   "filterlim f F at_top"
+proof -
+  have "filterlim (\<lambda>x. f (int (nat x))) F at_top"
+    by (rule filterlim_compose[OF assms filterlim_nat_sequentially])
+  also have "?this \<longleftrightarrow> filterlim f F at_top"
+    by (intro filterlim_cong refl eventually_mono [OF eventually_ge_at_top[of "0::int"]]) auto
+  finally show ?thesis .
+qed
+
+lemma filterlim_int_sequentially [tendsto_intros]:
+  "filterlim int at_top sequentially"
+  unfolding filterlim_at_top
+proof
+  fix C :: int
+  show "eventually (\<lambda>n. int n \<ge> C) at_top"
+    using eventually_ge_at_top[of "nat \<lceil>C\<rceil>"] by eventually_elim linarith
+qed
+
+lemma filterlim_real_of_int_at_top [tendsto_intros]:
+  "filterlim real_of_int at_top at_top"
+  unfolding filterlim_at_top
+proof
+  fix C :: real
+  show "eventually (\<lambda>n. real_of_int n \<ge> C) at_top"
+    using eventually_ge_at_top[of "\<lceil>C\<rceil>"] by eventually_elim linarith
+qed
+
+lemma filterlim_abs_real: "filterlim (abs::real \<Rightarrow> real) at_top at_top"
+proof (subst filterlim_cong[OF refl refl])
+  from eventually_ge_at_top[of "0::real"] show "eventually (\<lambda>x::real. \<bar>x\<bar> = x) at_top"
+    by eventually_elim simp
+qed (simp_all add: filterlim_ident)
+
+lemma filterlim_of_real_at_infinity [tendsto_intros]:
+  "filterlim (of_real :: real \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity at_top"
+  by (intro filterlim_norm_at_top_imp_at_infinity) (auto simp: filterlim_abs_real)
+    
 lemma not_tendsto_and_filterlim_at_infinity:
   fixes c :: "'a::real_normed_vector"
   assumes "F \<noteq> bot"
@@ -1534,6 +1605,14 @@
   shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot"
   using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot)
 
+lemma filterlim_power_at_infinity [tendsto_intros]:
+  fixes F and f :: "'a \<Rightarrow> 'b :: real_normed_div_algebra"
+  assumes "filterlim f at_infinity F" "n > 0"
+  shows   "filterlim (\<lambda>x. f x ^ n) at_infinity F"
+  by (rule filterlim_norm_at_top_imp_at_infinity)
+     (auto simp: norm_power intro!: filterlim_pow_at_top assms 
+           intro: filterlim_at_infinity_imp_norm_at_top)
+
 lemma filterlim_tendsto_add_at_top:
   assumes f: "(f \<longlongrightarrow> c) F"
     and g: "LIM x F. g x :> at_top"
diff -r 86aa6e2abee1 -r 2d9cf74943e1 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Jan 07 22:18:59 2018 +0100
+++ b/src/HOL/Parity.thy	Mon Jan 08 17:11:25 2018 +0000
@@ -483,6 +483,9 @@
 lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)"
   by (cases "even (n + k)") auto
 
+lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)"
+  by (induct n) auto
+
 end
 
 context linordered_idom