--- 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)
--- 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"
--- 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>
--- 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]
--- 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"
--- 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