--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat Aug 04 01:03:39 2018 +0200
@@ -1341,6 +1341,29 @@
lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0"
using has_contour_integral_trivial contour_integral_unique by blast
+lemma differentiable_linepath [intro]: "linepath a b differentiable at x within A"
+ by (auto simp: linepath_def)
+
+lemma bounded_linear_linepath:
+ assumes "bounded_linear f"
+ shows "f (linepath a b x) = linepath (f a) (f b) x"
+proof -
+ interpret f: bounded_linear f by fact
+ show ?thesis by (simp add: linepath_def f.add f.scale)
+qed
+
+lemma bounded_linear_linepath':
+ assumes "bounded_linear f"
+ shows "f \<circ> linepath a b = linepath (f a) (f b)"
+ using bounded_linear_linepath[OF assms] by (simp add: fun_eq_iff)
+
+lemma cnj_linepath: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x"
+ by (simp add: linepath_def)
+
+lemma cnj_linepath': "cnj \<circ> linepath a b = linepath (cnj a) (cnj b)"
+ by (simp add: linepath_def fun_eq_iff)
+
+
subsection\<open>Relation to subpath construction\<close>
@@ -1501,6 +1524,62 @@
"contour_integral g f = integral {0..1} (\<lambda>x. f (g x) * vector_derivative g (at x))"
by (simp add: contour_integral_def integral_def has_contour_integral contour_integrable_on)
+lemma contour_integral_cong:
+ assumes "g = g'" "\<And>x. x \<in> path_image g \<Longrightarrow> f x = f' x"
+ shows "contour_integral g f = contour_integral g' f'"
+ unfolding contour_integral_integral using assms
+ by (intro integral_cong) (auto simp: path_image_def)
+
+
+text \<open>Contour integral along a segment on the real axis\<close>
+
+lemma has_contour_integral_linepath_Reals_iff:
+ fixes a b :: complex and f :: "complex \<Rightarrow> complex"
+ assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
+ shows "(f has_contour_integral I) (linepath a b) \<longleftrightarrow>
+ ((\<lambda>x. f (of_real x)) has_integral I) {Re a..Re b}"
+proof -
+ from assms have [simp]: "of_real (Re a) = a" "of_real (Re b) = b"
+ by (simp_all add: complex_eq_iff)
+ from assms have "a \<noteq> b" by auto
+ have "((\<lambda>x. f (of_real x)) has_integral I) (cbox (Re a) (Re b)) \<longleftrightarrow>
+ ((\<lambda>x. f (a + b * of_real x - a * of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}"
+ by (subst has_integral_affinity_iff [of "Re b - Re a" _ "Re a", symmetric])
+ (insert assms, simp_all add: field_simps scaleR_conv_of_real)
+ also have "(\<lambda>x. f (a + b * of_real x - a * of_real x)) =
+ (\<lambda>x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))"
+ using \<open>a \<noteq> b\<close> by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real)
+ also have "(\<dots> has_integral I /\<^sub>R (Re b - Re a)) {0..1} \<longleftrightarrow>
+ ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms
+ by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps)
+ also have "\<dots> \<longleftrightarrow> (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def
+ by (intro has_integral_cong) (simp add: vector_derivative_linepath_within)
+ finally show ?thesis by simp
+qed
+
+lemma contour_integrable_linepath_Reals_iff:
+ fixes a b :: complex and f :: "complex \<Rightarrow> complex"
+ assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
+ shows "(f contour_integrable_on linepath a b) \<longleftrightarrow>
+ (\<lambda>x. f (of_real x)) integrable_on {Re a..Re b}"
+ using has_contour_integral_linepath_Reals_iff[OF assms, of f]
+ by (auto simp: contour_integrable_on_def integrable_on_def)
+
+lemma contour_integral_linepath_Reals_eq:
+ fixes a b :: complex and f :: "complex \<Rightarrow> complex"
+ assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
+ shows "contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (of_real x))"
+proof (cases "f contour_integrable_on linepath a b")
+ case True
+ thus ?thesis using has_contour_integral_linepath_Reals_iff[OF assms, of f]
+ using has_contour_integral_integral has_contour_integral_unique by blast
+next
+ case False
+ thus ?thesis using contour_integrable_linepath_Reals_iff[OF assms, of f]
+ by (simp add: not_integrable_contour_integral not_integrable_integral)
+qed
+
+
text\<open>Cauchy's theorem where there's a primitive\<close>
@@ -4875,6 +4954,10 @@
apply (rule derivative_eq_intros | simp)+
done
+corollary differentiable_part_circlepath:
+ "part_circlepath c r a b differentiable at x within A"
+ using has_vector_derivative_part_circlepath[of c r a b x A] differentiableI_vector by blast
+
corollary vector_derivative_part_circlepath:
"vector_derivative (part_circlepath z r s t) (at x) =
\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)"
@@ -4923,6 +5006,17 @@
by (fastforce simp add: path_image_def part_circlepath_def)
qed
+proposition path_image_part_circlepath':
+ "path_image (part_circlepath z r s t) = (\<lambda>x. z + r * cis x) ` closed_segment s t"
+proof -
+ have "path_image (part_circlepath z r s t) =
+ (\<lambda>x. z + r * exp(\<i> * of_real x)) ` linepath s t ` {0..1}"
+ by (simp add: image_image path_image_def part_circlepath_def)
+ also have "linepath s t ` {0..1} = closed_segment s t"
+ by (rule linepath_image_01)
+ finally show ?thesis by (simp add: cis_conv_exp)
+qed
+
corollary path_image_part_circlepath_subset:
"\<lbrakk>s \<le> t; 0 \<le> r\<rbrakk> \<Longrightarrow> path_image(part_circlepath z r s t) \<subseteq> sphere z r"
by (auto simp: path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)
@@ -4937,6 +5031,106 @@
by (simp add: dist_norm norm_minus_commute)
qed
+corollary path_image_part_circlepath_subset':
+ assumes "r \<ge> 0"
+ shows "path_image (part_circlepath z r s t) \<subseteq> sphere z r"
+proof (cases "s \<le> t")
+ case True
+ thus ?thesis using path_image_part_circlepath_subset[of s t r z] assms by simp
+next
+ case False
+ thus ?thesis using path_image_part_circlepath_subset[of t s r z] assms
+ by (subst reversepath_part_circlepath [symmetric], subst path_image_reversepath) simp_all
+qed
+
+lemma part_circlepath_cnj: "cnj (part_circlepath c r a b x) = part_circlepath (cnj c) r (-a) (-b) x"
+ by (simp add: part_circlepath_def exp_cnj linepath_def algebra_simps)
+
+lemma contour_integral_bound_part_circlepath:
+ assumes "f contour_integrable_on part_circlepath c r a b"
+ assumes "B \<ge> 0" "r \<ge> 0" "\<And>x. x \<in> path_image (part_circlepath c r a b) \<Longrightarrow> norm (f x) \<le> B"
+ shows "norm (contour_integral (part_circlepath c r a b) f) \<le> B * r * \<bar>b - a\<bar>"
+proof -
+ let ?I = "integral {0..1} (\<lambda>x. f (part_circlepath c r a b x) * \<i> * of_real (r * (b - a)) *
+ exp (\<i> * linepath a b x))"
+ have "norm ?I \<le> integral {0..1} (\<lambda>x::real. B * 1 * (r * \<bar>b - a\<bar>) * 1)"
+ proof (rule integral_norm_bound_integral, goal_cases)
+ case 1
+ with assms(1) show ?case
+ by (simp add: contour_integrable_on vector_derivative_part_circlepath mult_ac)
+ next
+ case (3 x)
+ with assms(2-) show ?case unfolding norm_mult norm_of_real abs_mult
+ by (intro mult_mono) (auto simp: path_image_def)
+ qed auto
+ also have "?I = contour_integral (part_circlepath c r a b) f"
+ by (simp add: contour_integral_integral vector_derivative_part_circlepath mult_ac)
+ finally show ?thesis by simp
+qed
+
+lemma has_contour_integral_part_circlepath_iff:
+ assumes "a < b"
+ shows "(f has_contour_integral I) (part_circlepath c r a b) \<longleftrightarrow>
+ ((\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) has_integral I) {a..b}"
+proof -
+ have "(f has_contour_integral I) (part_circlepath c r a b) \<longleftrightarrow>
+ ((\<lambda>x. f (part_circlepath c r a b x) * vector_derivative (part_circlepath c r a b)
+ (at x within {0..1})) has_integral I) {0..1}"
+ unfolding has_contour_integral_def ..
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (part_circlepath c r a b x) * r * (b - a) * \<i> *
+ cis (linepath a b x)) has_integral I) {0..1}"
+ by (intro has_integral_cong, subst vector_derivative_part_circlepath01)
+ (simp_all add: cis_conv_exp)
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (c + r * exp (\<i> * linepath (of_real a) (of_real b) x)) *
+ r * \<i> * exp (\<i> * linepath (of_real a) (of_real b) x) *
+ vector_derivative (linepath (of_real a) (of_real b))
+ (at x within {0..1})) has_integral I) {0..1}"
+ by (intro has_integral_cong, subst vector_derivative_linepath_within)
+ (auto simp: part_circlepath_def cis_conv_exp of_real_linepath [symmetric])
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>z. f (c + r * exp (\<i> * z)) * r * \<i> * exp (\<i> * z)) has_contour_integral I)
+ (linepath (of_real a) (of_real b))"
+ by (simp add: has_contour_integral_def)
+ also have "\<dots> \<longleftrightarrow> ((\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) has_integral I) {a..b}" using assms
+ by (subst has_contour_integral_linepath_Reals_iff) (simp_all add: cis_conv_exp)
+ finally show ?thesis .
+qed
+
+lemma contour_integrable_part_circlepath_iff:
+ assumes "a < b"
+ shows "f contour_integrable_on (part_circlepath c r a b) \<longleftrightarrow>
+ (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
+ using assms by (auto simp: contour_integrable_on_def integrable_on_def
+ has_contour_integral_part_circlepath_iff)
+
+lemma contour_integral_part_circlepath_eq:
+ assumes "a < b"
+ shows "contour_integral (part_circlepath c r a b) f =
+ integral {a..b} (\<lambda>t. f (c + r * cis t) * r * \<i> * cis t)"
+proof (cases "f contour_integrable_on part_circlepath c r a b")
+ case True
+ hence "(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
+ using assms by (simp add: contour_integrable_part_circlepath_iff)
+ with True show ?thesis
+ using has_contour_integral_part_circlepath_iff[OF assms]
+ contour_integral_unique has_integral_integrable_integral by blast
+next
+ case False
+ hence "\<not>(\<lambda>t. f (c + r * cis t) * r * \<i> * cis t) integrable_on {a..b}"
+ using assms by (simp add: contour_integrable_part_circlepath_iff)
+ with False show ?thesis
+ by (simp add: not_integrable_contour_integral not_integrable_integral)
+qed
+
+lemma contour_integral_part_circlepath_reverse:
+ "contour_integral (part_circlepath c r a b) f = -contour_integral (part_circlepath c r b a) f"
+ by (subst reversepath_part_circlepath [symmetric], subst contour_integral_reversepath) simp_all
+
+lemma contour_integral_part_circlepath_reverse':
+ "b < a \<Longrightarrow> contour_integral (part_circlepath c r a b) f =
+ -contour_integral (part_circlepath c r b a) f"
+ by (rule contour_integral_part_circlepath_reverse)
+
+
proposition finite_bounded_log: "finite {z::complex. norm z \<le> b \<and> exp z = w}"
proof (cases "w = 0")
case True then show ?thesis by auto
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Sat Aug 04 01:03:39 2018 +0200
@@ -41,6 +41,24 @@
lemma linear_cnj: "linear cnj"
using bounded_linear.linear[OF bounded_linear_cnj] .
+lemma vector_derivative_cnj_within:
+ assumes "at x within A \<noteq> bot" and "f differentiable at x within A"
+ shows "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) =
+ cnj (vector_derivative f (at x within A))" (is "_ = cnj ?D")
+proof -
+ let ?D = "vector_derivative f (at x within A)"
+ from assms have "(f has_vector_derivative ?D) (at x within A)"
+ by (subst (asm) vector_derivative_works)
+ hence "((\<lambda>x. cnj (f x)) has_vector_derivative cnj ?D) (at x within A)"
+ by (rule has_vector_derivative_cnj)
+ thus ?thesis using assms by (auto dest: vector_derivative_within)
+qed
+
+lemma vector_derivative_cnj:
+ assumes "f differentiable at x"
+ shows "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
+ using assms by (intro vector_derivative_cnj_within) auto
+
lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
by auto
@@ -286,6 +304,35 @@
"f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
by (metis holomorphic_on_compose holomorphic_on_subset)
+lemma holomorphic_on_balls_imp_entire:
+ assumes "\<not>bdd_above A" "\<And>r. r \<in> A \<Longrightarrow> f holomorphic_on ball c r"
+ shows "f holomorphic_on B"
+proof (rule holomorphic_on_subset)
+ show "f holomorphic_on UNIV" unfolding holomorphic_on_def
+ proof
+ fix z :: complex
+ from \<open>\<not>bdd_above A\<close> obtain r where r: "r \<in> A" "r > norm (z - c)"
+ by (meson bdd_aboveI not_le)
+ with assms(2) have "f holomorphic_on ball c r" by blast
+ moreover from r have "z \<in> ball c r" by (auto simp: dist_norm norm_minus_commute)
+ ultimately show "f field_differentiable at z"
+ by (auto simp: holomorphic_on_def at_within_open[of _ "ball c r"])
+ qed
+qed auto
+
+lemma holomorphic_on_balls_imp_entire':
+ assumes "\<And>r. r > 0 \<Longrightarrow> f holomorphic_on ball c r"
+ shows "f holomorphic_on B"
+proof (rule holomorphic_on_balls_imp_entire)
+ {
+ fix M :: real
+ have "\<exists>x. x > max M 0" by (intro gt_ex)
+ hence "\<exists>x>0. x > M" by auto
+ }
+ thus "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
+ by (auto simp: not_le)
+qed (insert assms, auto)
+
lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
by (metis field_differentiable_minus holomorphic_on_def)
--- a/src/HOL/Analysis/Complex_Transcendental.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sat Aug 04 01:03:39 2018 +0200
@@ -176,6 +176,16 @@
lemma holomorphic_on_cos: "cos holomorphic_on S"
by (simp add: field_differentiable_within_cos holomorphic_on_def)
+lemma holomorphic_on_sin' [holomorphic_intros]:
+ assumes "f holomorphic_on A"
+ shows "(\<lambda>x. sin (f x)) holomorphic_on A"
+ using holomorphic_on_compose[OF assms holomorphic_on_sin] by (simp add: o_def)
+
+lemma holomorphic_on_cos' [holomorphic_intros]:
+ assumes "f holomorphic_on A"
+ shows "(\<lambda>x. cos (f x)) holomorphic_on A"
+ using holomorphic_on_compose[OF assms holomorphic_on_cos] by (simp add: o_def)
+
subsection\<open>Get a nice real/imaginary separation in Euler's formula\<close>
lemma Euler: "exp(z) = of_real(exp(Re z)) *
@@ -1308,6 +1318,11 @@
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 holomorphic_on_Ln' [holomorphic_intros]:
+ "(\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> f holomorphic_on A \<Longrightarrow> (\<lambda>z. Ln (f z)) holomorphic_on A"
+ using holomorphic_on_compose_gen[OF _ holomorphic_on_Ln, of f A "- \<real>\<^sub>\<le>\<^sub>0"]
+ by (auto simp: o_def)
+
lemma tendsto_Ln [tendsto_intros]:
fixes L F
assumes "(f \<longlongrightarrow> L) F" "L \<notin> \<real>\<^sub>\<le>\<^sub>0"
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Aug 04 01:03:39 2018 +0200
@@ -4612,6 +4612,93 @@
unfolding absolutely_integrable_restrict_UNIV .
qed
+lemma uniform_limit_set_lebesgue_integral_at_top:
+ fixes f :: "'a \<Rightarrow> real \<Rightarrow> 'b::{banach, second_countable_topology}"
+ and g :: "real \<Rightarrow> real"
+ assumes bound: "\<And>x y. x \<in> A \<Longrightarrow> y \<ge> a \<Longrightarrow> norm (f x y) \<le> g y"
+ assumes integrable: "set_integrable M {a..} g"
+ assumes measurable: "\<And>x. x \<in> A \<Longrightarrow> set_borel_measurable M {a..} (f x)"
+ assumes "sets borel \<subseteq> sets M"
+ shows "uniform_limit A (\<lambda>b x. LINT y:{a..b}|M. f x y) (\<lambda>x. LINT y:{a..}|M. f x y) at_top"
+proof (cases "A = {}")
+ case False
+ then obtain x where x: "x \<in> A" by auto
+ have g_nonneg: "g y \<ge> 0" if "y \<ge> a" for y
+ proof -
+ have "0 \<le> norm (f x y)" by simp
+ also have "\<dots> \<le> g y" using bound[OF x that] by simp
+ finally show ?thesis .
+ qed
+
+ have integrable': "set_integrable M {a..} (\<lambda>y. f x y)" if "x \<in> A" for x
+ unfolding set_integrable_def
+ proof (rule Bochner_Integration.integrable_bound)
+ show "integrable M (\<lambda>x. indicator {a..} x * g x)"
+ using integrable by (simp add: set_integrable_def)
+ show "(\<lambda>y. indicat_real {a..} y *\<^sub>R f x y) \<in> borel_measurable M" using measurable[OF that]
+ by (simp add: set_borel_measurable_def)
+ show "AE y in M. norm (indicat_real {a..} y *\<^sub>R f x y) \<le> norm (indicat_real {a..} y * g y)"
+ using bound[OF that] by (intro AE_I2) (auto simp: indicator_def g_nonneg)
+ qed
+
+ show ?thesis
+ proof (rule uniform_limitI)
+ fix e :: real assume e: "e > 0"
+ have sets [intro]: "A \<in> sets M" if "A \<in> sets borel" for A
+ using that assms by blast
+
+ have "((\<lambda>b. LINT y:{a..b}|M. g y) \<longlongrightarrow> (LINT y:{a..}|M. g y)) at_top"
+ by (intro tendsto_set_lebesgue_integral_at_top assms sets) auto
+ with e obtain b0 :: real where b0: "\<forall>b\<ge>b0. \<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
+ by (auto simp: tendsto_iff eventually_at_top_linorder dist_real_def abs_minus_commute)
+ define b where "b = max a b0"
+ have "a \<le> b" by (simp add: b_def)
+ from b0 have "\<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
+ by (auto simp: b_def)
+ also have "{a..} = {a..b} \<union> {b<..}" by (auto simp: b_def)
+ also have "\<bar>(LINT y:\<dots>|M. g y) - (LINT y:{a..b}|M. g y)\<bar> = \<bar>(LINT y:{b<..}|M. g y)\<bar>"
+ using \<open>a \<le> b\<close> by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable])
+ also have "(LINT y:{b<..}|M. g y) \<ge> 0"
+ using g_nonneg \<open>a \<le> b\<close> unfolding set_lebesgue_integral_def
+ by (intro Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
+ hence "\<bar>(LINT y:{b<..}|M. g y)\<bar> = (LINT y:{b<..}|M. g y)" by simp
+ finally have less: "(LINT y:{b<..}|M. g y) < e" .
+
+ have "eventually (\<lambda>b. b \<ge> b0) at_top" by (rule eventually_ge_at_top)
+ moreover have "eventually (\<lambda>b. b \<ge> a) at_top" by (rule eventually_ge_at_top)
+ ultimately show "eventually (\<lambda>b. \<forall>x\<in>A.
+ dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e) at_top"
+ proof eventually_elim
+ case (elim b)
+ show ?case
+ proof
+ fix x assume x: "x \<in> A"
+ have "dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) =
+ norm ((LINT y:{a..}|M. f x y) - (LINT y:{a..b}|M. f x y))"
+ by (simp add: dist_norm norm_minus_commute)
+ also have "{a..} = {a..b} \<union> {b<..}" using elim by auto
+ also have "(LINT y:\<dots>|M. f x y) - (LINT y:{a..b}|M. f x y) = (LINT y:{b<..}|M. f x y)"
+ using elim x
+ by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable'])
+ also have "norm \<dots> \<le> (LINT y:{b<..}|M. norm (f x y))" using elim x
+ by (intro set_integral_norm_bound set_integrable_subset[OF integrable']) auto
+ also have "\<dots> \<le> (LINT y:{b<..}|M. g y)" using elim x bound g_nonneg
+ by (intro set_integral_mono set_integrable_norm set_integrable_subset[OF integrable']
+ set_integrable_subset[OF integrable]) auto
+ also have "(LINT y:{b<..}|M. g y) \<ge> 0"
+ using g_nonneg \<open>a \<le> b\<close> unfolding set_lebesgue_integral_def
+ by (intro Bochner_Integration.integral_nonneg) (auto simp: indicator_def)
+ hence "(LINT y:{b<..}|M. g y) = \<bar>(LINT y:{b<..}|M. g y)\<bar>" by simp
+ also have "\<dots> = \<bar>(LINT y:{a..b} \<union> {b<..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar>"
+ using elim by (subst set_integral_Un) (auto intro!: set_integrable_subset[OF integrable])
+ also have "{a..b} \<union> {b<..} = {a..}" using elim by auto
+ also have "\<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
+ using b0 elim by blast
+ finally show "dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e" .
+ qed
+ qed
+ qed
+qed auto
--- a/src/HOL/Analysis/FPS_Convergence.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Sat Aug 04 01:03:39 2018 +0200
@@ -193,6 +193,24 @@
by (subst analytic_on_open) auto
qed
+lemma continuous_eval_fps [continuous_intros]:
+ fixes z :: "'a::{real_normed_field,banach}"
+ assumes "norm z < fps_conv_radius F"
+ shows "continuous (at z within A) (eval_fps F)"
+proof -
+ from ereal_dense2[OF assms] obtain K :: real where K: "norm z < K" "K < fps_conv_radius F"
+ by auto
+ have "0 \<le> norm z" by simp
+ also have "norm z < K" by fact
+ finally have "K > 0" .
+ from K and \<open>K > 0\<close> have "summable (\<lambda>n. fps_nth F n * of_real K ^ n)"
+ by (intro summable_fps) auto
+ from this have "isCont (eval_fps F) z" unfolding eval_fps_def
+ by (rule isCont_powser) (use K in auto)
+ thus "continuous (at z within A) (eval_fps F)"
+ by (simp add: continuous_at_imp_continuous_within)
+qed
+
subsection%unimportant \<open>Lower bounds on radius of convergence\<close>
@@ -831,6 +849,20 @@
ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def)
qed
+lemma has_fps_expansion_imp_continuous:
+ fixes F :: "'a::{real_normed_field,banach} fps"
+ assumes "f has_fps_expansion F"
+ shows "continuous (at 0 within A) f"
+proof -
+ from assms have "isCont (eval_fps F) 0"
+ by (intro continuous_eval_fps) (auto simp: has_fps_expansion_def zero_ereal_def)
+ also have "?this \<longleftrightarrow> isCont f 0" using assms
+ by (intro isCont_cong) (auto simp: has_fps_expansion_def)
+ finally have "isCont f 0" .
+ thus "continuous (at 0 within A) f"
+ by (simp add: continuous_at_imp_continuous_within)
+qed
+
lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]:
"(\<lambda>_. c) has_fps_expansion fps_const c"
by (auto simp: has_fps_expansion_def)
--- a/src/HOL/Analysis/Gamma_Function.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Sat Aug 04 01:03:39 2018 +0200
@@ -1457,6 +1457,15 @@
lemma holomorphic_rGamma [holomorphic_intros]: "rGamma holomorphic_on A"
unfolding holomorphic_on_def by (auto intro!: field_differentiable_rGamma)
+lemma holomorphic_rGamma' [holomorphic_intros]:
+ assumes "f holomorphic_on A"
+ shows "(\<lambda>x. rGamma (f x)) holomorphic_on A"
+proof -
+ have "rGamma \<circ> f holomorphic_on A" using assms
+ by (intro holomorphic_on_compose assms holomorphic_rGamma)
+ thus ?thesis by (simp only: o_def)
+qed
+
lemma analytic_rGamma: "rGamma analytic_on A"
unfolding analytic_on_def by (auto intro!: exI[of _ 1] holomorphic_rGamma)
@@ -1467,6 +1476,15 @@
lemma holomorphic_Gamma [holomorphic_intros]: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma holomorphic_on A"
unfolding holomorphic_on_def by (auto intro!: field_differentiable_Gamma)
+lemma holomorphic_Gamma' [holomorphic_intros]:
+ assumes "f holomorphic_on A" and "\<And>x. x \<in> A \<Longrightarrow> f x \<notin> \<int>\<^sub>\<le>\<^sub>0"
+ shows "(\<lambda>x. Gamma (f x)) holomorphic_on A"
+proof -
+ have "Gamma \<circ> f holomorphic_on A" using assms
+ by (intro holomorphic_on_compose assms holomorphic_Gamma) auto
+ thus ?thesis by (simp only: o_def)
+qed
+
lemma analytic_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
(auto intro!: holomorphic_Gamma)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Aug 04 01:03:39 2018 +0200
@@ -687,6 +687,17 @@
apply (simp_all add: integrable_integral integrable_linear has_integral_linear )
done
+lemma integrable_on_cnj_iff:
+ "(\<lambda>x. cnj (f x)) integrable_on A \<longleftrightarrow> f integrable_on A"
+ using integrable_linear[OF _ bounded_linear_cnj, of f A]
+ integrable_linear[OF _ bounded_linear_cnj, of "cnj \<circ> f" A]
+ by (auto simp: o_def)
+
+lemma integral_cnj: "cnj (integral A f) = integral A (\<lambda>x. cnj (f x))"
+ by (cases "f integrable_on A")
+ (simp_all add: integral_linear[OF _ bounded_linear_cnj, symmetric]
+ o_def integrable_on_cnj_iff not_integrable_integral)
+
lemma integral_component_eq[simp]:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes "f integrable_on S"
@@ -3440,6 +3451,64 @@
lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified]
+lemma integrable_on_affinity:
+ assumes "m \<noteq> 0" "f integrable_on (cbox a b)"
+ shows "(\<lambda>x. f (m *\<^sub>R x + c)) integrable_on ((\<lambda>x. (1 / m) *\<^sub>R x - ((1 / m) *\<^sub>R c)) ` cbox a b)"
+proof -
+ from assms obtain I where "(f has_integral I) (cbox a b)"
+ by (auto simp: integrable_on_def)
+ from has_integral_affinity[OF this assms(1), of c] show ?thesis
+ by (auto simp: integrable_on_def)
+qed
+
+lemma has_integral_cmul_iff:
+ assumes "c \<noteq> 0"
+ shows "((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R I)) A \<longleftrightarrow> (f has_integral I) A"
+ using assms has_integral_cmul[of f I A c]
+ has_integral_cmul[of "\<lambda>x. c *\<^sub>R f x" "c *\<^sub>R I" A "inverse c"] by (auto simp: field_simps)
+
+lemma has_integral_affinity':
+ fixes a :: "'a::euclidean_space"
+ assumes "(f has_integral i) (cbox a b)" and "m > 0"
+ shows "((\<lambda>x. f(m *\<^sub>R x + c)) has_integral (i /\<^sub>R m ^ DIM('a)))
+ (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m))"
+proof (cases "cbox a b = {}")
+ case True
+ hence "(cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) = {}"
+ using \<open>m > 0\<close> unfolding box_eq_empty by (auto simp: algebra_simps)
+ with True and assms show ?thesis by simp
+next
+ case False
+ have "((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (1 / \<bar>m\<bar> ^ DIM('a)) *\<^sub>R i)
+ ((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b)"
+ using assms by (intro has_integral_affinity) auto
+ also have "((\<lambda>x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox a b) =
+ ((\<lambda>x. - ((1 / m) *\<^sub>R c) + x) ` (\<lambda>x. (1 / m) *\<^sub>R x) ` cbox a b)"
+ by (simp add: image_image algebra_simps)
+ also have "(\<lambda>x. (1 / m) *\<^sub>R x) ` cbox a b = cbox ((1 / m) *\<^sub>R a) ((1 / m) *\<^sub>R b)" using \<open>m > 0\<close> False
+ by (subst image_smult_cbox) simp_all
+ also have "(\<lambda>x. - ((1 / m) *\<^sub>R c) + x) ` \<dots> = cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)"
+ by (subst cbox_translation [symmetric]) (simp add: field_simps vector_add_divide_simps)
+ finally show ?thesis using \<open>m > 0\<close> by (simp add: field_simps)
+qed
+
+lemma has_integral_affinity_iff:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: real_normed_vector"
+ assumes "m > 0"
+ shows "((\<lambda>x. f (m *\<^sub>R x + c)) has_integral (I /\<^sub>R m ^ DIM('a)))
+ (cbox ((a - c) /\<^sub>R m) ((b - c) /\<^sub>R m)) \<longleftrightarrow>
+ (f has_integral I) (cbox a b)" (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ from has_integral_affinity'[OF this, of "1 / m" "-c /\<^sub>R m"] and \<open>m > 0\<close>
+ show ?rhs by (simp add: field_simps vector_add_divide_simps)
+next
+ assume ?rhs
+ from has_integral_affinity'[OF this, of m c] and \<open>m > 0\<close>
+ show ?lhs by simp
+qed
+
+
subsection \<open>Special case of stretching coordinate axes separately\<close>
lemma has_integral_stretch:
--- a/src/HOL/Analysis/Path_Connected.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Sat Aug 04 01:03:39 2018 +0200
@@ -1177,6 +1177,21 @@
unfolding pathfinish_def linepath_def
by auto
+lemma linepath_inner: "linepath a b x \<bullet> v = linepath (a \<bullet> v) (b \<bullet> v) x"
+ by (simp add: linepath_def algebra_simps)
+
+lemma Re_linepath': "Re (linepath a b x) = linepath (Re a) (Re b) x"
+ by (simp add: linepath_def)
+
+lemma Im_linepath': "Im (linepath a b x) = linepath (Im a) (Im b) x"
+ by (simp add: linepath_def)
+
+lemma linepath_0': "linepath a b 0 = a"
+ by (simp add: linepath_def)
+
+lemma linepath_1': "linepath a b 1 = b"
+ by (simp add: linepath_def)
+
lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
unfolding linepath_def
by (intro continuous_intros)
@@ -1200,6 +1215,9 @@
lemma linepath_0 [simp]: "linepath 0 b x = x *\<^sub>R b"
by (simp add: linepath_def)
+lemma linepath_cnj: "cnj (linepath a b x) = linepath (cnj a) (cnj b) x"
+ by (simp add: linepath_def)
+
lemma arc_linepath:
assumes "a \<noteq> b" shows [simp]: "arc (linepath a b)"
proof -
--- a/src/HOL/Analysis/Set_Integral.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Sat Aug 04 01:03:39 2018 +0200
@@ -54,6 +54,15 @@
by (auto simp add: indicator_def)
*)
+lemma set_integrable_cong:
+ assumes "M = M'" "A = A'" "\<And>x. x \<in> A \<Longrightarrow> f x = f' x"
+ shows "set_integrable M A f = set_integrable M' A' f'"
+proof -
+ have "(\<lambda>x. indicator A x *\<^sub>R f x) = (\<lambda>x. indicator A' x *\<^sub>R f' x)"
+ using assms by (auto simp: indicator_def)
+ thus ?thesis by (simp add: set_integrable_def assms)
+qed
+
lemma set_borel_measurable_sets:
fixes f :: "_ \<Rightarrow> _::real_normed_vector"
assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
@@ -925,4 +934,127 @@
then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n])
qed (auto simp add: assms Limsup_bounded)
+lemma tendsto_set_lebesgue_integral_at_right:
+ fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
+ assumes "a < b" and sets: "\<And>a'. a' \<in> {a<..b} \<Longrightarrow> {a'..b} \<in> sets M"
+ and "set_integrable M {a<..b} f"
+ shows "((\<lambda>a'. set_lebesgue_integral M {a'..b} f) \<longlongrightarrow>
+ set_lebesgue_integral M {a<..b} f) (at_right a)"
+proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
+ case (1 S)
+ have eq: "(\<Union>n. {S n..b}) = {a<..b}"
+ proof safe
+ fix x n assume "x \<in> {S n..b}"
+ with 1(1,2)[of n] show "x \<in> {a<..b}" by auto
+ next
+ fix x assume "x \<in> {a<..b}"
+ with order_tendstoD[OF \<open>S \<longlonglongrightarrow> a\<close>, of x] show "x \<in> (\<Union>n. {S n..b})"
+ by (force simp: eventually_at_top_linorder dest: less_imp_le)
+ qed
+ have "(\<lambda>n. set_lebesgue_integral M {S n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {S n..b}) f"
+ by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
+ with eq show ?case by simp
+qed
+
+
+text \<open>
+ The next lemmas relate convergence of integrals over an interval to
+ improper integrals.
+\<close>
+lemma tendsto_set_lebesgue_integral_at_left:
+ fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
+ assumes "a < b" and sets: "\<And>b'. b' \<in> {a..<b} \<Longrightarrow> {a..b'} \<in> sets M"
+ and "set_integrable M {a..<b} f"
+ shows "((\<lambda>b'. set_lebesgue_integral M {a..b'} f) \<longlongrightarrow>
+ set_lebesgue_integral M {a..<b} f) (at_left b)"
+proof (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
+ case (1 S)
+ have eq: "(\<Union>n. {a..S n}) = {a..<b}"
+ proof safe
+ fix x n assume "x \<in> {a..S n}"
+ with 1(1,2)[of n] show "x \<in> {a..<b}" by auto
+ next
+ fix x assume "x \<in> {a..<b}"
+ with order_tendstoD[OF \<open>S \<longlonglongrightarrow> b\<close>, of x] show "x \<in> (\<Union>n. {a..S n})"
+ by (force simp: eventually_at_top_linorder dest: less_imp_le)
+ qed
+ have "(\<lambda>n. set_lebesgue_integral M {a..S n} f) \<longlonglongrightarrow> set_lebesgue_integral M (\<Union>n. {a..S n}) f"
+ by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le)
+ with eq show ?case by simp
+qed
+
+lemma tendsto_set_lebesgue_integral_at_top:
+ fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+ assumes sets: "\<And>b. b \<ge> a \<Longrightarrow> {a..b} \<in> sets M"
+ and int: "set_integrable M {a..} f"
+ shows "((\<lambda>b. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {a..} f) at_top"
+proof (rule tendsto_at_topI_sequentially)
+ fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
+ show "(\<lambda>n. set_lebesgue_integral M {a..X n} f) \<longlonglongrightarrow> set_lebesgue_integral M {a..} f"
+ unfolding set_lebesgue_integral_def
+ proof (rule integral_dominated_convergence)
+ show "integrable M (\<lambda>x. indicat_real {a..} x *\<^sub>R norm (f x))"
+ using integrable_norm[OF int[unfolded set_integrable_def]] by simp
+ show "AE x in M. (\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
+ proof
+ fix x
+ from \<open>filterlim X at_top sequentially\<close>
+ have "eventually (\<lambda>n. x \<le> X n) sequentially"
+ unfolding filterlim_at_top_ge[where c=x] by auto
+ then show "(\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
+ by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+ qed
+ fix n show "AE x in M. norm (indicator {a..X n} x *\<^sub>R f x) \<le>
+ indicator {a..} x *\<^sub>R norm (f x)"
+ by (auto split: split_indicator)
+ next
+ from int show "(\<lambda>x. indicat_real {a..} x *\<^sub>R f x) \<in> borel_measurable M"
+ by (simp add: set_integrable_def)
+ next
+ fix n :: nat
+ from sets have "{a..X n} \<in> sets M" by (cases "X n \<ge> a") auto
+ with int have "set_integrable M {a..X n} f"
+ by (rule set_integrable_subset) auto
+ thus "(\<lambda>x. indicat_real {a..X n} x *\<^sub>R f x) \<in> borel_measurable M"
+ by (simp add: set_integrable_def)
+ qed
+qed
+
+lemma tendsto_set_lebesgue_integral_at_bot:
+ fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+ assumes sets: "\<And>a. a \<le> b \<Longrightarrow> {a..b} \<in> sets M"
+ and int: "set_integrable M {..b} f"
+ shows "((\<lambda>a. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {..b} f) at_bot"
+proof (rule tendsto_at_botI_sequentially)
+ fix X :: "nat \<Rightarrow> real" assume "filterlim X at_bot sequentially"
+ show "(\<lambda>n. set_lebesgue_integral M {X n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {..b} f"
+ unfolding set_lebesgue_integral_def
+ proof (rule integral_dominated_convergence)
+ show "integrable M (\<lambda>x. indicat_real {..b} x *\<^sub>R norm (f x))"
+ using integrable_norm[OF int[unfolded set_integrable_def]] by simp
+ show "AE x in M. (\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
+ proof
+ fix x
+ from \<open>filterlim X at_bot sequentially\<close>
+ have "eventually (\<lambda>n. x \<ge> X n) sequentially"
+ unfolding filterlim_at_bot_le[where c=x] by auto
+ then show "(\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
+ by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+ qed
+ fix n show "AE x in M. norm (indicator {X n..b} x *\<^sub>R f x) \<le>
+ indicator {..b} x *\<^sub>R norm (f x)"
+ by (auto split: split_indicator)
+ next
+ from int show "(\<lambda>x. indicat_real {..b} x *\<^sub>R f x) \<in> borel_measurable M"
+ by (simp add: set_integrable_def)
+ next
+ fix n :: nat
+ from sets have "{X n..b} \<in> sets M" by (cases "X n \<le> b") auto
+ with int have "set_integrable M {X n..b} f"
+ by (rule set_integrable_subset) auto
+ thus "(\<lambda>x. indicat_real {X n..b} x *\<^sub>R f x) \<in> borel_measurable M"
+ by (simp add: set_integrable_def)
+ qed
+qed
+
end
--- a/src/HOL/Archimedean_Field.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Archimedean_Field.thy Sat Aug 04 01:03:39 2018 +0200
@@ -707,6 +707,9 @@
lemma frac_of_int [simp]: "frac (of_int z) = 0"
by (simp add: frac_def)
+lemma frac_frac [simp]: "frac (frac x) = frac x"
+ by (simp add: frac_def)
+
lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
proof -
have "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
@@ -743,6 +746,14 @@
apply (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
done
+lemma frac_in_Ints_iff [simp]: "frac x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
+proof safe
+ assume "frac x \<in> \<int>"
+ hence "of_int \<lfloor>x\<rfloor> + frac x \<in> \<int>" by auto
+ also have "of_int \<lfloor>x\<rfloor> + frac x = x" by (simp add: frac_def)
+ finally show "x \<in> \<int>" .
+qed (auto simp: frac_def)
+
subsection \<open>Rounding to the nearest integer\<close>
--- a/src/HOL/Complex.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Complex.thy Sat Aug 04 01:03:39 2018 +0200
@@ -623,6 +623,27 @@
lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
by (simp add: sums_def lim_cnj cnj_sum [symmetric] del: cnj_sum)
+lemma differentiable_cnj_iff:
+ "(\<lambda>z. cnj (f z)) differentiable at x within A \<longleftrightarrow> f differentiable at x within A"
+proof
+ assume "(\<lambda>z. cnj (f z)) differentiable at x within A"
+ then obtain D where "((\<lambda>z. cnj (f z)) has_derivative D) (at x within A)"
+ by (auto simp: differentiable_def)
+ from has_derivative_cnj[OF this] show "f differentiable at x within A"
+ by (auto simp: differentiable_def)
+next
+ assume "f differentiable at x within A"
+ then obtain D where "(f has_derivative D) (at x within A)"
+ by (auto simp: differentiable_def)
+ from has_derivative_cnj[OF this] show "(\<lambda>z. cnj (f z)) differentiable at x within A"
+ by (auto simp: differentiable_def)
+qed
+
+lemma has_vector_derivative_cnj [derivative_intros]:
+ assumes "(f has_vector_derivative f') (at z within A)"
+ shows "((\<lambda>z. cnj (f z)) has_vector_derivative cnj f') (at z within A)"
+ using assms by (auto simp: has_vector_derivative_complex_iff intro: derivative_intros)
+
subsection \<open>Basic Lemmas\<close>
@@ -778,9 +799,15 @@
lemma sgn_cis [simp]: "sgn (cis a) = cis a"
by (simp add: sgn_div_norm)
+lemma cis_2pi [simp]: "cis (2 * pi) = 1"
+ by (simp add: cis.ctr complex_eq_iff)
+
lemma cis_neq_zero [simp]: "cis a \<noteq> 0"
by (metis norm_cis norm_zero zero_neq_one)
+lemma cis_cnj: "cnj (cis t) = cis (-t)"
+ by (simp add: complex_eq_iff)
+
lemma cis_mult: "cis a * cis b = cis (a + b)"
by (simp add: complex_eq_iff cos_add sin_add)
@@ -802,6 +829,15 @@
lemma cis_pi [simp]: "cis pi = -1"
by (simp add: complex_eq_iff)
+lemma cis_pi_half[simp]: "cis (pi / 2) = \<i>"
+ by (simp add: cis.ctr complex_eq_iff)
+
+lemma cis_minus_pi_half[simp]: "cis (-(pi / 2)) = -\<i>"
+ by (simp add: cis.ctr complex_eq_iff)
+
+lemma cis_multiple_2pi[simp]: "n \<in> \<int> \<Longrightarrow> cis (2 * pi * n) = 1"
+ by (auto elim!: Ints_cases simp: cis.ctr one_complex.ctr)
+
subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>
@@ -847,6 +883,11 @@
subsubsection \<open>Complex exponential\<close>
+lemma exp_Reals_eq:
+ assumes "z \<in> \<real>"
+ shows "exp z = of_real (exp (Re z))"
+ using assms by (auto elim!: Reals_cases simp: exp_of_real)
+
lemma cis_conv_exp: "cis b = exp (\<i> * b)"
proof -
have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
@@ -901,6 +942,10 @@
lemma exp_two_pi_i' [simp]: "exp (\<i> * (of_real pi * 2)) = 1"
by (metis exp_two_pi_i mult.commute)
+lemma continuous_on_cis [continuous_intros]:
+ "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. cis (f x))"
+ by (auto simp: cis_conv_exp intro!: continuous_intros)
+
subsubsection \<open>Complex argument\<close>
--- a/src/HOL/Int.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Int.thy Sat Aug 04 01:03:39 2018 +0200
@@ -892,6 +892,9 @@
apply (rule of_int_minus [symmetric])
done
+lemma minus_in_Ints_iff: "-x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
+ using Ints_minus[of x] Ints_minus[of "-x"] by auto
+
lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
apply (auto simp add: Ints_def)
apply (rule range_eqI)
--- a/src/HOL/Limits.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Limits.thy Sat Aug 04 01:03:39 2018 +0200
@@ -1316,6 +1316,16 @@
and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
by auto
+lemma tendsto_at_botI_sequentially:
+ fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
+ assumes *: "\<And>X. filterlim X at_bot sequentially \<Longrightarrow> (\<lambda>n. f (X n)) \<longlonglongrightarrow> y"
+ shows "(f \<longlongrightarrow> y) at_bot"
+ unfolding filterlim_at_bot_mirror
+proof (rule tendsto_at_topI_sequentially)
+ fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
+ thus "(\<lambda>n. f (-X n)) \<longlonglongrightarrow> y" by (intro *) (auto simp: filterlim_uminus_at_top)
+qed
+
lemma filterlim_at_infinity_imp_filterlim_at_top:
assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
assumes "eventually (\<lambda>x. f x > 0) F"
--- a/src/HOL/Real_Vector_Spaces.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Aug 04 01:03:39 2018 +0200
@@ -1012,6 +1012,9 @@
lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
using dist_triangle2 [of x y a] by (simp add: dist_commute)
+lemma abs_dist_diff_le: "\<bar>dist a b - dist b c\<bar> \<le> dist a c"
+ using dist_triangle3[of b c a] dist_triangle2[of a b c] by simp
+
lemma dist_pos_lt: "x \<noteq> y \<Longrightarrow> 0 < dist x y"
by (simp add: zero_less_dist_iff)
--- a/src/HOL/Series.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Series.thy Sat Aug 04 01:03:39 2018 +0200
@@ -703,6 +703,27 @@
qed
qed
+lemma summable_Cauchy':
+ fixes f :: "nat \<Rightarrow> 'a :: banach"
+ assumes "eventually (\<lambda>m. \<forall>n\<ge>m. norm (sum f {m..<n}) \<le> g m) sequentially"
+ assumes "filterlim g (nhds 0) sequentially"
+ shows "summable f"
+proof (subst summable_Cauchy, intro allI impI, goal_cases)
+ case (1 e)
+ from order_tendstoD(2)[OF assms(2) this] and assms(1)
+ have "eventually (\<lambda>m. \<forall>n. norm (sum f {m..<n}) < e) at_top"
+ proof eventually_elim
+ case (elim m)
+ show ?case
+ proof
+ fix n
+ from elim show "norm (sum f {m..<n}) < e"
+ by (cases "n \<ge> m") auto
+ qed
+ qed
+ thus ?case by (auto simp: eventually_at_top_linorder)
+qed
+
context
fixes f :: "nat \<Rightarrow> 'a::banach"
begin
--- a/src/HOL/Topological_Spaces.thy Sat Aug 04 00:19:23 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy Sat Aug 04 01:03:39 2018 +0200
@@ -2131,6 +2131,9 @@
lemma isCont_def: "isCont f a \<longleftrightarrow> f \<midarrow>a\<rightarrow> f a"
by (rule continuous_at)
+lemma isContD: "isCont f x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x"
+ by (simp add: isCont_def)
+
lemma isCont_cong:
assumes "eventually (\<lambda>x. f x = g x) (nhds x)"
shows "isCont f x \<longleftrightarrow> isCont g x"