--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Jun 03 18:23:29 2018 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Jun 03 18:23:38 2018 +0200
@@ -40,9 +40,7 @@
lemmas swap_apply1 = swap_apply(1)
lemmas swap_apply2 = swap_apply(2)
-lemmas lessThan_empty_iff = Iio_eq_empty_iff_nat
lemmas Zero_notin_Suc = zero_notin_Suc_image
-lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
lemma pointwise_minimal_pointwise_maximal:
fixes s :: "(nat \<Rightarrow> nat) set"
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Jun 03 18:23:29 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Jun 03 18:23:38 2018 +0200
@@ -3370,7 +3370,7 @@
fix e::real
assume e: "e>0"
obtain p where p: "polynomial_function p \<and>
- pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and> (\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < min e (d / 2))"
+ pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and> (\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < min e (d/2))"
using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "min e (d/2)"] d \<open>0<e\<close> by auto
have "(\<lambda>w. 1 / (w - z)) holomorphic_on UNIV - {z}"
by (auto simp: intro!: holomorphic_intros)
@@ -4650,17 +4650,19 @@
have lpa: "linked_paths atends g p"
by (metis (mono_tags, lifting) N01(1) ksf linked_paths_def pathfinish_def pathstart_def psf)
show ?case
- apply (rule_tac x="min d1 d2" in exI)
- apply (simp add: \<open>0 < d1\<close> \<open>0 < d2\<close>, clarify)
- apply (rule_tac s="contour_integral p f" in trans)
- using pk_le N01(1) ksf pathfinish_def pathstart_def
- apply (force intro!: vpp d1 simp add: linked_paths_def psf ksf)
- using pk_le N01 apply (force intro!: vpp d2 lpa simp add: linked_paths_def psf ksf)
- done
+ proof (intro exI; safe)
+ fix j
+ assume "valid_path j" "linked_paths atends g j"
+ and "\<forall>u\<in>{0..1}. cmod (j u - k (real (Suc n) / real N, u)) < min d1 d2"
+ then have "contour_integral j f = contour_integral p f"
+ using pk_le N01(1) ksf by (force intro!: vpp d1 simp add: linked_paths_def psf)
+ also have "... = contour_integral g f"
+ using pk_le by (force intro!: vpp d2 lpa)
+ finally show "contour_integral j f = contour_integral g f" .
+ qed (simp add: \<open>0 < d1\<close> \<open>0 < d2\<close>)
qed
then obtain d where "0 < d"
- "\<And>j. valid_path j \<and> (\<forall>u \<in> {0..1}. norm(j u - k (1,u)) < d) \<and>
- linked_paths atends g j
+ "\<And>j. valid_path j \<and> (\<forall>u \<in> {0..1}. norm(j u - k (1,u)) < d) \<and> linked_paths atends g j
\<Longrightarrow> contour_integral j f = contour_integral g f"
using \<open>N>0\<close> by auto
then have "linked_paths atends g h \<Longrightarrow> contour_integral h f = contour_integral g f"
@@ -4726,15 +4728,14 @@
and hq_less: "\<forall>t\<in>{0..1}. cmod (h t - q t) < e"
and paq: "contour_integral q (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number h z"
using winding_number [OF \<open>path h\<close> pah \<open>0 < e\<close>] unfolding winding_number_prop_def by blast
- have gp: "homotopic_paths (- {z}) g p"
+ have "homotopic_paths (- {z}) g p"
by (simp add: d p valid_path_imp_path norm_minus_commute gp_less)
- have hq: "homotopic_paths (- {z}) h q"
+ moreover have "homotopic_paths (- {z}) h q"
by (simp add: e q valid_path_imp_path norm_minus_commute hq_less)
- have "contour_integral p (\<lambda>w. 1/(w - z)) = contour_integral q (\<lambda>w. 1/(w - z))"
- apply (rule Cauchy_theorem_homotopic_paths [of "-{z}"])
- apply (blast intro: homotopic_paths_trans homotopic_paths_sym gp hq assms)
- apply (auto intro!: holomorphic_intros simp: p q)
- done
+ ultimately have "homotopic_paths (- {z}) p q"
+ by (blast intro: homotopic_paths_trans homotopic_paths_sym assms)
+ then have "contour_integral p (\<lambda>w. 1/(w - z)) = contour_integral q (\<lambda>w. 1/(w - z))"
+ by (rule Cauchy_theorem_homotopic_paths) (auto intro!: holomorphic_intros simp: p q)
then show ?thesis
by (simp add: pap paq)
qed
@@ -4792,16 +4793,13 @@
by (blast intro: sym homotopic_loops_linear winding_number_homotopic_loops)
lemma winding_number_nearby_paths_eq:
- "\<lbrakk>path g; path h;
- pathstart h = pathstart g; pathfinish h = pathfinish g;
+ "\<lbrakk>path g; path h; pathstart h = pathstart g; pathfinish h = pathfinish g;
\<And>t. t \<in> {0..1} \<Longrightarrow> norm(h t - g t) < norm(g t - z)\<rbrakk>
\<Longrightarrow> winding_number h z = winding_number g z"
by (metis segment_bound(2) norm_minus_commute not_le winding_number_paths_linear_eq)
lemma winding_number_nearby_loops_eq:
- "\<lbrakk>path g; path h;
- pathfinish g = pathstart g;
- pathfinish h = pathstart h;
+ "\<lbrakk>path g; path h; pathfinish g = pathstart g; pathfinish h = pathstart h;
\<And>t. t \<in> {0..1} \<Longrightarrow> norm(h t - g t) < norm(g t - z)\<rbrakk>
\<Longrightarrow> winding_number h z = winding_number g z"
by (metis segment_bound(2) norm_minus_commute not_le winding_number_loops_linear_eq)
@@ -4968,12 +4966,7 @@
have **: "((\<lambda>x. if (part_circlepath z r s t x) \<in> k then 0
else f(part_circlepath z r s t x) *
vector_derivative (part_circlepath z r s t) (at x)) has_integral i) {0..1}"
- apply (rule has_integral_spike
- [where f = "\<lambda>x. f(part_circlepath z r s t x) * vector_derivative (part_circlepath z r s t) (at x)"])
- apply (rule negligible_finite [OF fin01])
- using fi has_contour_integral
- apply auto
- done
+ by (rule has_integral_spike [OF negligible_finite [OF fin01]]) (use fi has_contour_integral in auto)
have *: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1; part_circlepath z r s t x \<notin> k\<rbrakk> \<Longrightarrow> cmod (f (part_circlepath z r s t x)) \<le> B"
by (auto intro!: B [unfolded path_image_def image_def, simplified])
show ?thesis
@@ -5023,9 +5016,8 @@
proof (cases "r = 0 \<or> s = t")
case True
then show ?thesis
- apply (rule disjE)
- apply (force simp: part_circlepath_def simple_path_def intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+
- done
+ unfolding part_circlepath_def simple_path_def
+ by (rule disjE) (force intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+
next
case False then have "r \<noteq> 0" "s \<noteq> t" by auto
have *: "\<And>x y z s t. \<i>*((1 - x) * s + x * t) = \<i>*(((1 - y) * s + y * t)) + z \<longleftrightarrow> \<i>*(x - y) * (t - s) = z"
@@ -5033,28 +5025,29 @@
have abs01: "\<And>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1
\<Longrightarrow> (x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0 \<longleftrightarrow> \<bar>x - y\<bar> \<in> {0,1})"
by auto
- have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P \<bar>x - y\<bar>) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
- by force
have **: "\<And>x y. (\<exists>n. (complex_of_real x - of_real y) * (of_real t - of_real s) = 2 * (of_int n * of_real pi)) \<longleftrightarrow>
(\<exists>n. \<bar>x - y\<bar> * (t - s) = 2 * (of_int n * pi))"
by (force simp: algebra_simps abs_if dest: arg_cong [where f=Re] arg_cong [where f=complex_of_real]
intro: exI [where x = "-n" for n])
- have 1: "\<forall>x. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> (\<exists>n. x * (t - s) = 2 * (real_of_int n * pi)) \<longrightarrow> x = 0 \<or> x = 1 \<Longrightarrow> \<bar>s - t\<bar> \<le> 2 * pi"
- apply (rule ccontr)
- apply (drule_tac x="2*pi / \<bar>t - s\<bar>" in spec)
- using False
- apply (simp add: abs_minus_commute divide_simps)
- apply (frule_tac x=1 in spec)
- apply (drule_tac x="-1" in spec, simp)
- done
+ have 1: "\<bar>s - t\<bar> \<le> 2 * pi"
+ if "\<And>x. 0 \<le> x \<and> x \<le> 1 \<Longrightarrow> (\<exists>n. x * (t - s) = 2 * (real_of_int n * pi)) \<longrightarrow> x = 0 \<or> x = 1"
+ proof (rule ccontr)
+ assume "\<not> \<bar>s - t\<bar> \<le> 2 * pi"
+ then have *: "\<And>n. t - s \<noteq> of_int n * \<bar>s - t\<bar>"
+ using False that [of "2*pi / \<bar>t - s\<bar>"] by (simp add: abs_minus_commute divide_simps)
+ show False
+ using * [of 1] * [of "-1"] by auto
+ qed
have 2: "\<bar>s - t\<bar> = \<bar>2 * (real_of_int n * pi) / x\<bar>" if "x \<noteq> 0" "x * (t - s) = 2 * (real_of_int n * pi)" for x n
proof -
have "t-s = 2 * (real_of_int n * pi)/x"
using that by (simp add: field_simps)
then show ?thesis by (metis abs_minus_commute)
qed
+ have abs_away: "\<And>P. (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. P \<bar>x - y\<bar>) \<longleftrightarrow> (\<forall>x::real. 0 \<le> x \<and> x \<le> 1 \<longrightarrow> P x)"
+ by force
show ?thesis using False
- apply (simp add: simple_path_def path_part_circlepath)
+ apply (simp add: simple_path_def)
apply (simp add: part_circlepath_def linepath_def exp_eq * ** abs01 del: Set.insert_iff)
apply (subst abs_away)
apply (auto simp: 1)
@@ -5068,22 +5061,20 @@
shows "arc (part_circlepath z r s t)"
proof -
have *: "x = y" if eq: "\<i> * (linepath s t x) = \<i> * (linepath s t y) + 2 * of_int n * complex_of_real pi * \<i>"
- and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
- proof -
- have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
- by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_div_cancel_left eq)
- then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
- by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
- then have st: "x \<noteq> y \<Longrightarrow> (s-t) = (of_int n * (pi * 2) / (y-x))"
- by (force simp: field_simps)
- show ?thesis
- apply (rule ccontr)
- using assms x y
- apply (simp add: st abs_mult field_simps)
- using st
- apply (auto simp: dest: of_int_lessD)
- done
- qed
+ and x: "x \<in> {0..1}" and y: "y \<in> {0..1}" for x y n
+ proof (rule ccontr)
+ assume "x \<noteq> y"
+ have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
+ by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_div_cancel_left eq)
+ then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
+ by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
+ with \<open>x \<noteq> y\<close> have st: "s-t = (of_int n * (pi * 2) / (y-x))"
+ by (force simp: field_simps)
+ have "\<bar>real_of_int n\<bar> < \<bar>y - x\<bar>"
+ using assms \<open>x \<noteq> y\<close> by (simp add: st abs_mult field_simps)
+ then show False
+ using assms x y st by (auto dest: of_int_lessD)
+ qed
show ?thesis
using assms
apply (simp add: arc_def)
@@ -5219,14 +5210,16 @@
by (simp add: sphere_def dist_norm norm_minus_commute)
proposition contour_integral_circlepath:
- "0 < r \<Longrightarrow> contour_integral (circlepath z r) (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i>"
- apply (rule contour_integral_unique)
- apply (simp add: has_contour_integral_def)
- apply (subst has_integral_cong)
- apply (simp add: vector_derivative_circlepath01)
- using has_integral_const_real [of _ 0 1]
- apply (force simp: circlepath)
- done
+ assumes "r > 0"
+ shows "contour_integral (circlepath z r) (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i>"
+proof (rule contour_integral_unique)
+ show "((\<lambda>w. 1 / (w - z)) has_contour_integral 2 * complex_of_real pi * \<i>) (circlepath z r)"
+ unfolding has_contour_integral_def using assms
+ apply (subst has_integral_cong)
+ apply (simp add: vector_derivative_circlepath01)
+ using has_integral_const_real [of _ 0 1] apply (force simp: circlepath)
+ done
+qed
lemma winding_number_circlepath_centre: "0 < r \<Longrightarrow> winding_number (circlepath z r) z = 1"
apply (rule winding_number_unique_loop)
@@ -5250,10 +5243,12 @@
have disjo: "cball z r' \<inter> sphere z r = {}"
using \<open>r' < r\<close> by (force simp: cball_def sphere_def)
have "winding_number(circlepath z r) w = winding_number(circlepath z r) z"
- apply (rule winding_number_around_inside [where s = "cball z r'"])
- apply (simp_all add: disjo order.strict_implies_order winding_number_circlepath_centre)
- apply (simp_all add: False r'_def dist_norm norm_minus_commute)
- done
+ proof (rule winding_number_around_inside [where s = "cball z r'"])
+ show "winding_number (circlepath z r) z \<noteq> 0"
+ by (simp add: winding_number_circlepath_centre)
+ show "cball z r' \<inter> path_image (circlepath z r) = {}"
+ by (simp add: disjo less_eq_real_def)
+ qed (auto simp: r'_def dist_norm norm_minus_commute)
also have "\<dots> = 1"
by (simp add: winding_number_circlepath_centre)
finally show ?thesis .
@@ -5263,7 +5258,7 @@
text\<open> Hence the Cauchy formula for points inside a circle.\<close>
theorem Cauchy_integral_circlepath:
- assumes "continuous_on (cball z r) f" "f holomorphic_on (ball z r)" "norm(w - z) < r"
+ assumes contf: "continuous_on (cball z r) f" and holf: "f holomorphic_on (ball z r)" and wz: "norm(w - z) < r"
shows "((\<lambda>u. f u/(u - w)) has_contour_integral (2 * of_real pi * \<i> * f w))
(circlepath z r)"
proof -
@@ -5271,12 +5266,15 @@
using assms le_less_trans norm_ge_zero by blast
have "((\<lambda>u. f u / (u - w)) has_contour_integral (2 * pi) * \<i> * winding_number (circlepath z r) w * f w)
(circlepath z r)"
- apply (rule Cauchy_integral_formula_weak [where s = "cball z r" and k = "{}"])
- using assms \<open>r > 0\<close>
- apply (simp_all add: dist_norm norm_minus_commute)
- apply (metis at_within_interior dist_norm holomorphic_on_def interior_ball mem_ball norm_minus_commute)
- apply (simp add: cball_def sphere_def dist_norm, clarify, simp)
- by (metis dist_commute dist_norm less_irrefl)
+ proof (rule Cauchy_integral_formula_weak [where s = "cball z r" and k = "{}"])
+ show "\<And>x. x \<in> interior (cball z r) - {} \<Longrightarrow>
+ f field_differentiable at x"
+ using holf holomorphic_on_imp_differentiable_at by auto
+ have "w \<notin> sphere z r"
+ by simp (metis dist_commute dist_norm not_le order_refl wz)
+ then show "path_image (circlepath z r) \<subseteq> cball z r - {w}"
+ using \<open>r > 0\<close> by (auto simp add: cball_def sphere_def)
+ qed (use wz in \<open>simp_all add: dist_norm norm_minus_commute contf\<close>)
then show ?thesis
by (simp add: winding_number_circlepath assms)
qed
@@ -5330,20 +5328,18 @@
have Ble: "B * e / (\<bar>B\<bar> + 1) \<le> e"
using \<open>0 \<le> B\<close> \<open>0 < e\<close> by (simp add: divide_simps)
have "\<exists>h. (\<forall>x\<in>{0..1}. cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - h x) \<le> e) \<and> h integrable_on {0..1}"
- apply (rule_tac x="\<lambda>x. f (a::'a) (\<gamma> x) * vector_derivative \<gamma> (at x)" in exI)
- apply (intro inta conjI ballI)
- apply (rule order_trans [OF _ Ble])
- apply (frule noleB)
- apply (frule fga)
- using \<open>0 \<le> B\<close> \<open>0 < e\<close>
- apply (simp add: norm_mult left_diff_distrib [symmetric] norm_minus_commute divide_simps)
- apply (drule (1) mult_mono [OF less_imp_le])
- apply (simp_all add: mult_ac)
- done
+ proof (intro exI conjI ballI)
+ show "cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - f a (\<gamma> x) * vector_derivative \<gamma> (at x)) \<le> e"
+ if "x \<in> {0..1}" for x
+ apply (rule order_trans [OF _ Ble])
+ using noleB [OF that] fga [OF that] \<open>0 \<le> B\<close> \<open>0 < e\<close>
+ apply (simp add: norm_mult left_diff_distrib [symmetric] norm_minus_commute divide_simps)
+ apply (fastforce simp: mult_ac dest: mult_mono [OF less_imp_le])
+ done
+ qed (rule inta)
}
then show lintg: "l contour_integrable_on \<gamma>"
- apply (simp add: contour_integrable_on)
- by (metis (mono_tags, lifting)integrable_uniform_limit_real)
+ unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real)
{ fix e::real
define B' where "B' = B + 1"
have B': "B' > 0" "B' > B" using \<open>0 \<le> B\<close> by (auto simp: B'_def)
@@ -5363,13 +5359,17 @@
then show ?thesis
by (simp add: left_diff_distrib [symmetric] norm_mult)
qed
+ have le_e: "\<And>x. \<lbrakk>\<forall>xa\<in>{0..1}. 2 * cmod (f x (\<gamma> xa) - l (\<gamma> xa)) < e / B'; f x contour_integrable_on \<gamma>\<rbrakk>
+ \<Longrightarrow> cmod (integral {0..1}
+ (\<lambda>u. f x (\<gamma> u) * vector_derivative \<gamma> (at u) - l (\<gamma> u) * vector_derivative \<gamma> (at u))) < e"
+ apply (rule le_less_trans [OF integral_norm_bound_integral ie])
+ apply (simp add: lintg integrable_diff contour_integrable_on [symmetric])
+ apply (blast intro: *)+
+ done
have "\<forall>\<^sub>F x in F. dist (contour_integral \<gamma> (f x)) (contour_integral \<gamma> l) < e"
apply (rule eventually_mono [OF eventually_conj [OF ev_no' ev_fint]])
apply (simp add: dist_norm contour_integrable_on path_image_def contour_integral_integral)
- apply (simp add: lintg integral_diff [symmetric] contour_integrable_on [symmetric], clarify)
- apply (rule le_less_trans [OF integral_norm_bound_integral ie])
- apply (simp add: lintg integrable_diff contour_integrable_on [symmetric])
- apply (blast intro: *)+
+ apply (simp add: lintg integral_diff [symmetric] contour_integrable_on [symmetric] le_e)
done
}
then show "((\<lambda>n. contour_integral \<gamma> (f n)) \<longlongrightarrow> contour_integral \<gamma> l) F"
@@ -5404,14 +5404,16 @@
using open_contains_ball by blast
have [simp]: "\<And>n. cmod (1 + of_nat n) = 1 + of_nat n"
by (metis norm_of_nat of_nat_Suc)
+ have cint: "\<And>x. \<lbrakk>x \<noteq> w; cmod (x - w) < d\<rbrakk>
+ \<Longrightarrow> (\<lambda>z. (f' z / (z - x) ^ k - f' z / (z - w) ^ k) / (x * k - w * k)) contour_integrable_on \<gamma>"
+ apply (rule contour_integrable_div [OF contour_integrable_diff])
+ using int w d
+ by (force simp: dist_norm norm_minus_commute intro!: has_contour_integral_integrable)+
have 1: "\<forall>\<^sub>F n in at w. (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k)
contour_integrable_on \<gamma>"
- apply (simp add: eventually_at)
+ unfolding eventually_at
apply (rule_tac x=d in exI)
- apply (simp add: \<open>d > 0\<close> dist_norm field_simps, clarify)
- apply (rule contour_integrable_div [OF contour_integrable_diff])
- using int w d
- apply (force simp: dist_norm norm_minus_commute intro!: has_contour_integral_integrable)+
+ apply (simp add: \<open>d > 0\<close> dist_norm field_simps cint)
done
have bim_g: "bounded (image f' (path_image \<gamma>))"
by (simp add: compact_imp_bounded compact_continuous_image compact_valid_path_image assms)
@@ -5424,7 +5426,7 @@
proof -
have *: "cmod ((inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k) - inverse (x - w) ^ Suc k) < e"
if x: "x \<in> path_image \<gamma>" and "u \<noteq> w" and uwd: "cmod (u - w) < d/2"
- and uw_less: "cmod (u - w) < e * (d / 2) ^ (k+2) / (1 + real k)"
+ and uw_less: "cmod (u - w) < e * (d/2) ^ (k+2) / (1 + real k)"
for u x
proof -
define ff where [abs_def]:
@@ -5434,8 +5436,8 @@
else (k * of_real(Suc k)) / (x - w)^(k + 2))" for n :: nat and w
have km1: "\<And>z::complex. z \<noteq> 0 \<Longrightarrow> z ^ (k - Suc 0) = z ^ k / z"
by (simp add: field_simps) (metis Suc_pred \<open>k \<noteq> 0\<close> neq0_conv power_Suc)
- have ff1: "(ff i has_field_derivative ff (Suc i) z) (at z within ball w (d / 2))"
- if "z \<in> ball w (d / 2)" "i \<le> 1" for i z
+ have ff1: "(ff i has_field_derivative ff (Suc i) z) (at z within ball w (d/2))"
+ if "z \<in> ball w (d/2)" "i \<le> 1" for i z
proof -
have "z \<notin> path_image \<gamma>"
using \<open>x \<in> path_image \<gamma>\<close> d that ball_divide_subset_numeral by blast
@@ -5452,22 +5454,18 @@
qed
{ fix a::real and b::real assume ab: "a > 0" "b > 0"
then have "k * (1 + real k) * (1 / a) \<le> k * (1 + real k) * (4 / b) \<longleftrightarrow> b \<le> 4 * a"
- apply (subst mult_le_cancel_left_pos)
- using \<open>k \<noteq> 0\<close>
- apply (auto simp: divide_simps)
- done
+ by (subst mult_le_cancel_left_pos) (use \<open>k \<noteq> 0\<close> in \<open>auto simp: divide_simps\<close>)
with ab have "real k * (1 + real k) / a \<le> (real k * 4 + real k * real k * 4) / b \<longleftrightarrow> b \<le> 4 * a"
by (simp add: field_simps)
} note canc = this
- have ff2: "cmod (ff (Suc 1) v) \<le> real (k * (k + 1)) / (d / 2) ^ (k + 2)"
- if "v \<in> ball w (d / 2)" for v
+ have ff2: "cmod (ff (Suc 1) v) \<le> real (k * (k + 1)) / (d/2) ^ (k + 2)"
+ if "v \<in> ball w (d/2)" for v
proof -
+ have lessd: "\<And>z. cmod (\<gamma> z - v) < d/2 \<Longrightarrow> cmod (w - \<gamma> z) < d"
+ by (metis that norm_minus_commute norm_triangle_half_r dist_norm mem_ball)
have "d/2 \<le> cmod (x - v)" using d x that
- apply (simp add: dist_norm path_image_def ball_def not_less [symmetric] del: divide_const_simps, clarify)
- apply (drule subsetD)
- prefer 2 apply blast
- apply (metis norm_minus_commute norm_triangle_half_r CollectI)
- done
+ using lessd d x
+ by (auto simp add: dist_norm path_image_def ball_def not_less [symmetric] del: divide_const_simps)
then have "d \<le> cmod (x - v) * 2"
by (simp add: divide_simps)
then have dpow_le: "d ^ (k+2) \<le> (cmod (x - v) * 2) ^ (k+2)"
@@ -5475,24 +5473,22 @@
have "x \<noteq> v" using that
using \<open>x \<in> path_image \<gamma>\<close> ball_divide_subset_numeral d by fastforce
then show ?thesis
- using \<open>d > 0\<close>
- apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc)
- using dpow_le
- apply (simp add: algebra_simps divide_simps mult_less_0_iff)
+ using \<open>d > 0\<close> apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc)
+ using dpow_le apply (simp add: algebra_simps divide_simps mult_less_0_iff)
done
qed
- have ub: "u \<in> ball w (d / 2)"
+ have ub: "u \<in> ball w (d/2)"
using uwd by (simp add: dist_commute dist_norm)
have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
- \<le> (real k * 4 + real k * real k * 4) * (cmod (u - w) * cmod (u - w)) / (d * (d * (d / 2) ^ k))"
+ \<le> (real k * 4 + real k * real k * 4) * (cmod (u - w) * cmod (u - w)) / (d * (d * (d/2) ^ k))"
using complex_taylor [OF _ ff1 ff2 _ ub, of w, simplified]
by (simp add: ff_def \<open>0 < d\<close>)
then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
- \<le> (cmod (u - w) * real k) * (1 + real k) * cmod (u - w) / (d / 2) ^ (k+2)"
+ \<le> (cmod (u - w) * real k) * (1 + real k) * cmod (u - w) / (d/2) ^ (k+2)"
by (simp add: field_simps)
then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
/ (cmod (u - w) * real k)
- \<le> (1 + real k) * cmod (u - w) / (d / 2) ^ (k+2)"
+ \<le> (1 + real k) * cmod (u - w) / (d/2) ^ (k+2)"
using \<open>k \<noteq> 0\<close> \<open>u \<noteq> w\<close> by (simp add: mult_ac zero_less_mult_iff pos_divide_le_eq)
also have "\<dots> < e"
using uw_less \<open>0 < d\<close> by (simp add: mult_ac divide_simps)
@@ -5503,7 +5499,7 @@
using uwd \<open>0 < d\<close> x d by (force simp: dist_norm ball_def norm_minus_commute)
show ?thesis
apply (rule le_less_trans [OF _ e])
- using \<open>k \<noteq> 0\<close> \<open>x \<noteq> u\<close> \<open>u \<noteq> w\<close>
+ using \<open>k \<noteq> 0\<close> \<open>x \<noteq> u\<close> \<open>u \<noteq> w\<close>
apply (simp add: field_simps norm_divide [symmetric])
done
qed
@@ -5538,8 +5534,7 @@
inverse (\<gamma> x - w) * inverse (\<gamma> x - w) ^ k)"
by (simp add: norm_mult)
also have "\<dots> < cmod (f' (\<gamma> x)) * (e/C)"
- apply (rule mult_strict_left_mono [OF ec])
- using False by simp
+ using False mult_strict_left_mono [OF ec] by force
also have "\<dots> \<le> e" using C
by (metis False \<open>0 < e\<close> frac_le less_eq_real_def mult.commute pos_le_divide_eq x zero_less_norm_iff)
finally show ?thesis .
@@ -5557,13 +5552,17 @@
by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
have **: "contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k)) =
(f u - f w) / (u - w) / k"
- if "dist u w < d" for u
- apply (rule contour_integral_unique)
- apply (simp add: diff_divide_distrib algebra_simps)
- apply (rule has_contour_integral_diff; rule has_contour_integral_div; simp add: field_simps; rule int)
- apply (metis contra_subsetD d dist_commute mem_ball that)
- apply (rule w)
- done
+ if "dist u w < d" for u
+ proof -
+ have u: "u \<in> s - path_image \<gamma>"
+ by (metis subsetD d dist_commute mem_ball that)
+ show ?thesis
+ apply (rule contour_integral_unique)
+ apply (simp add: diff_divide_distrib algebra_simps)
+ apply (intro has_contour_integral_diff has_contour_integral_div)
+ using u w apply (simp_all add: field_simps int)
+ done
+ qed
show ?thes2
apply (simp add: has_field_derivative_iff del: power_Suc)
apply (rule Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close> ])
@@ -5628,14 +5627,14 @@
subsection\<open>Existence of all higher derivatives\<close>
proposition derivative_is_holomorphic:
- assumes "open s"
- and fder: "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z)"
- shows "f' holomorphic_on s"
+ assumes "open S"
+ and fder: "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative f' z) (at z)"
+ shows "f' holomorphic_on S"
proof -
- have *: "\<exists>h. (f' has_field_derivative h) (at z)" if "z \<in> s" for z
+ have *: "\<exists>h. (f' has_field_derivative h) (at z)" if "z \<in> S" for z
proof -
- obtain r where "r > 0" and r: "cball z r \<subseteq> s"
- using open_contains_cball \<open>z \<in> s\<close> \<open>open s\<close> by blast
+ obtain r where "r > 0" and r: "cball z r \<subseteq> S"
+ using open_contains_cball \<open>z \<in> S\<close> \<open>open S\<close> by blast
then have holf_cball: "f holomorphic_on cball z r"
apply (simp add: holomorphic_on_def)
using field_differentiable_at_within field_differentiable_def fder by blast
@@ -5673,38 +5672,38 @@
done
qed
show ?thesis
- by (simp add: holomorphic_on_open [OF \<open>open s\<close>] *)
+ by (simp add: holomorphic_on_open [OF \<open>open S\<close>] *)
qed
lemma holomorphic_deriv [holomorphic_intros]:
- "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
+ "\<lbrakk>f holomorphic_on S; open S\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on S"
by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
-lemma analytic_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
+lemma analytic_deriv [analytic_intros]: "f analytic_on S \<Longrightarrow> (deriv f) analytic_on S"
using analytic_on_holomorphic holomorphic_deriv by auto
-lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on s"
+lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on S; open S\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on S"
by (induction n) (auto simp: holomorphic_deriv)
-lemma analytic_higher_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
+lemma analytic_higher_deriv [analytic_intros]: "f analytic_on S \<Longrightarrow> (deriv ^^ n) f analytic_on S"
unfolding analytic_on_def using holomorphic_higher_deriv by blast
lemma has_field_derivative_higher_deriv:
- "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk>
+ "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
\<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
by (metis (no_types, hide_lams) DERIV_deriv_iff_field_differentiable at_within_open comp_apply
funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
lemma valid_path_compose_holomorphic:
- assumes "valid_path g" and holo:"f holomorphic_on s" and "open s" "path_image g \<subseteq> s"
+ assumes "valid_path g" and holo:"f holomorphic_on S" and "open S" "path_image g \<subseteq> S"
shows "valid_path (f \<circ> g)"
proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
fix x assume "x \<in> path_image g"
then show "f field_differentiable at x"
using analytic_on_imp_differentiable_at analytic_on_open assms holo by blast
next
- have "deriv f holomorphic_on s"
- using holomorphic_deriv holo \<open>open s\<close> by auto
+ have "deriv f holomorphic_on S"
+ using holomorphic_deriv holo \<open>open S\<close> by auto
then show "continuous_on (path_image g) (deriv f)"
using assms(4) holomorphic_on_imp_continuous_on holomorphic_on_subset by auto
qed
@@ -5713,15 +5712,15 @@
subsection\<open>Morera's theorem\<close>
lemma Morera_local_triangle_ball:
- assumes "\<And>z. z \<in> s
+ assumes "\<And>z. z \<in> S
\<Longrightarrow> \<exists>e a. 0 < e \<and> z \<in> ball a e \<and> continuous_on (ball a e) f \<and>
(\<forall>b c. closed_segment b c \<subseteq> ball a e
\<longrightarrow> contour_integral (linepath a b) f +
contour_integral (linepath b c) f +
contour_integral (linepath c a) f = 0)"
- shows "f analytic_on s"
+ shows "f analytic_on S"
proof -
- { fix z assume "z \<in> s"
+ { fix z assume "z \<in> S"
with assms obtain e a where
"0 < e" and z: "z \<in> ball a e" and contf: "continuous_on (ball a e) f"
and 0: "\<And>b c. closed_segment b c \<subseteq> ball a e
@@ -5733,29 +5732,31 @@
have sb_ball: "ball z (e - dist a z) \<subseteq> ball a e"
by (simp add: dist_commute ball_subset_ball_iff)
have "\<exists>e>0. f holomorphic_on ball z e"
- apply (rule_tac x="e - dist a z" in exI)
- apply (simp add: az)
- apply (rule holomorphic_on_subset [OF _ sb_ball])
- apply (rule derivative_is_holomorphic[OF open_ball])
- apply (rule triangle_contour_integrals_starlike_primitive [OF contf _ open_ball, of a])
- apply (simp_all add: 0 \<open>0 < e\<close>)
- apply (meson \<open>0 < e\<close> centre_in_ball convex_ball convex_contains_segment mem_ball)
- done
+ proof (intro exI conjI)
+ have sub_ball: "\<And>y. dist a y < e \<Longrightarrow> closed_segment a y \<subseteq> ball a e"
+ by (meson \<open>0 < e\<close> centre_in_ball convex_ball convex_contains_segment mem_ball)
+ show "f holomorphic_on ball z (e - dist a z)"
+ apply (rule holomorphic_on_subset [OF _ sb_ball])
+ apply (rule derivative_is_holomorphic[OF open_ball])
+ apply (rule triangle_contour_integrals_starlike_primitive [OF contf _ open_ball, of a])
+ apply (simp_all add: 0 \<open>0 < e\<close> sub_ball)
+ done
+ qed (simp add: az)
}
then show ?thesis
by (simp add: analytic_on_def)
qed
lemma Morera_local_triangle:
- assumes "\<And>z. z \<in> s
+ assumes "\<And>z. z \<in> S
\<Longrightarrow> \<exists>t. open t \<and> z \<in> t \<and> continuous_on t f \<and>
(\<forall>a b c. convex hull {a,b,c} \<subseteq> t
\<longrightarrow> contour_integral (linepath a b) f +
contour_integral (linepath b c) f +
contour_integral (linepath c a) f = 0)"
- shows "f analytic_on s"
+ shows "f analytic_on S"
proof -
- { fix z assume "z \<in> s"
+ { fix z assume "z \<in> S"
with assms obtain t where
"open t" and z: "z \<in> t" and contf: "continuous_on t f"
and 0: "\<And>a b c. convex hull {a,b,c} \<subseteq> t
@@ -5767,29 +5768,27 @@
using open_contains_ball by blast
have [simp]: "continuous_on (ball z e) f" using contf
using continuous_on_subset e by blast
- have "\<exists>e a. 0 < e \<and>
- z \<in> ball a e \<and>
- continuous_on (ball a e) f \<and>
- (\<forall>b c. closed_segment b c \<subseteq> ball a e \<longrightarrow>
- contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0)"
- apply (rule_tac x=e in exI)
- apply (rule_tac x=z in exI)
- apply (simp add: \<open>e > 0\<close>, clarify)
- apply (rule 0)
- apply (meson z \<open>0 < e\<close> centre_in_ball closed_segment_subset convex_ball dual_order.trans e starlike_convex_subset)
- done
+ have eq0: "\<And>b c. closed_segment b c \<subseteq> ball z e \<Longrightarrow>
+ contour_integral (linepath z b) f +
+ contour_integral (linepath b c) f +
+ contour_integral (linepath c z) f = 0"
+ by (meson 0 z \<open>0 < e\<close> centre_in_ball closed_segment_subset convex_ball dual_order.trans e starlike_convex_subset)
+ have "\<exists>e a. 0 < e \<and> z \<in> ball a e \<and> continuous_on (ball a e) f \<and>
+ (\<forall>b c. closed_segment b c \<subseteq> ball a e \<longrightarrow>
+ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0)"
+ using \<open>e > 0\<close> eq0 by force
}
then show ?thesis
by (simp add: Morera_local_triangle_ball)
qed
proposition Morera_triangle:
- "\<lbrakk>continuous_on s f; open s;
- \<And>a b c. convex hull {a,b,c} \<subseteq> s
+ "\<lbrakk>continuous_on S f; open S;
+ \<And>a b c. convex hull {a,b,c} \<subseteq> S
\<longrightarrow> contour_integral (linepath a b) f +
contour_integral (linepath b c) f +
contour_integral (linepath c a) f = 0\<rbrakk>
- \<Longrightarrow> f analytic_on s"
+ \<Longrightarrow> f analytic_on S"
using Morera_local_triangle by blast
@@ -5798,10 +5797,10 @@
lemma higher_deriv_linear [simp]:
"(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
- by (induction n) (auto simp: deriv_const deriv_linear)
+ by (induction n) auto
lemma higher_deriv_const [simp]: "(deriv ^^ n) (\<lambda>w. c) = (\<lambda>w. if n=0 then c else 0)"
- by (induction n) (auto simp: deriv_const)
+ by (induction n) auto
lemma higher_deriv_ident [simp]:
"(deriv ^^ n) (\<lambda>w. w) z = (if n = 0 then z else if n = 1 then 1 else 0)"
@@ -5820,7 +5819,7 @@
by (metis DERIV_chain comp_funpow comp_id funpow_swap1 mult.right_neutral)
proposition higher_deriv_uminus:
- assumes "f holomorphic_on s" "open s" and z: "z \<in> s"
+ assumes "f holomorphic_on S" "open S" and z: "z \<in> S"
shows "(deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
using z
proof (induction n arbitrary: z)
@@ -5829,18 +5828,18 @@
case (Suc n z)
have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
using Suc.prems assms has_field_derivative_higher_deriv by auto
- show ?case
- apply simp
- apply (rule DERIV_imp_deriv)
+ have "((deriv ^^ n) (\<lambda>w. - f w) has_field_derivative - deriv ((deriv ^^ n) f) z) (at z)"
apply (rule DERIV_transform_within_open [of "\<lambda>w. -((deriv ^^ n) f w)"])
- apply (rule derivative_eq_intros | rule * refl assms Suc)+
- apply (simp add: Suc)
+ apply (rule derivative_eq_intros | rule * refl assms)+
+ apply (auto simp add: Suc)
done
+ then show ?case
+ by (simp add: DERIV_imp_deriv)
qed
proposition higher_deriv_add:
fixes z::complex
- assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
+ assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \<in> S"
shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
using z
proof (induction n arbitrary: z)
@@ -5850,18 +5849,19 @@
have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
"((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
using Suc.prems assms has_field_derivative_higher_deriv by auto
- show ?case
- apply simp
- apply (rule DERIV_imp_deriv)
+ have "((deriv ^^ n) (\<lambda>w. f w + g w) has_field_derivative
+ deriv ((deriv ^^ n) f) z + deriv ((deriv ^^ n) g) z) (at z)"
apply (rule DERIV_transform_within_open [of "\<lambda>w. (deriv ^^ n) f w + (deriv ^^ n) g w"])
- apply (rule derivative_eq_intros | rule * refl assms Suc)+
- apply (simp add: Suc)
+ apply (rule derivative_eq_intros | rule * refl assms)+
+ apply (auto simp add: Suc)
done
+ then show ?case
+ by (simp add: DERIV_imp_deriv)
qed
corollary higher_deriv_diff:
fixes z::complex
- assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
+ assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \<in> S"
shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
apply (simp only: Groups.group_add_class.diff_conv_add_uminus higher_deriv_add)
apply (subst higher_deriv_add)
@@ -5874,7 +5874,7 @@
proposition higher_deriv_mult:
fixes z::complex
- assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
+ assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \<in> S"
shows "(deriv ^^ n) (\<lambda>w. f w * g w) z =
(\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
using z
@@ -5892,23 +5892,26 @@
apply (subst (4) sum_Suc_reindex)
apply (auto simp: algebra_simps Suc_diff_le intro: sum.cong)
done
- show ?case
- apply (simp only: funpow.simps o_apply)
- apply (rule DERIV_imp_deriv)
+ have "((deriv ^^ n) (\<lambda>w. f w * g w) has_field_derivative
+ (\<Sum>i = 0..Suc n. (Suc n choose i) * (deriv ^^ i) f z * (deriv ^^ (Suc n - i)) g z))
+ (at z)"
apply (rule DERIV_transform_within_open
- [of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
- apply (simp add: algebra_simps)
- apply (rule DERIV_cong [OF DERIV_sum])
- apply (rule DERIV_cmult)
- apply (auto intro: DERIV_mult * sumeq \<open>open s\<close> Suc.prems Suc.IH [symmetric])
+ [of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
+ apply (simp add: algebra_simps)
+ apply (rule DERIV_cong [OF DERIV_sum])
+ apply (rule DERIV_cmult)
+ apply (auto intro: DERIV_mult * sumeq \<open>open S\<close> Suc.prems Suc.IH [symmetric])
done
+ then show ?case
+ unfolding funpow.simps o_apply
+ by (simp add: DERIV_imp_deriv)
qed
proposition higher_deriv_transform_within_open:
fixes z::complex
- assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
- and fg: "\<And>w. w \<in> s \<Longrightarrow> f w = g w"
+ assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \<in> S"
+ and fg: "\<And>w. w \<in> S \<Longrightarrow> f w = g w"
shows "(deriv ^^ i) f z = (deriv ^^ i) g z"
using z
by (induction i arbitrary: z)
@@ -5916,45 +5919,41 @@
proposition higher_deriv_compose_linear:
fixes z::complex
- assumes f: "f holomorphic_on t" and s: "open s" and t: "open t" and z: "z \<in> s"
- and fg: "\<And>w. w \<in> s \<Longrightarrow> u * w \<in> t"
+ assumes f: "f holomorphic_on T" and S: "open S" and T: "open T" and z: "z \<in> S"
+ and fg: "\<And>w. w \<in> S \<Longrightarrow> u * w \<in> T"
shows "(deriv ^^ n) (\<lambda>w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)"
using z
proof (induction n arbitrary: z)
case 0 then show ?case by simp
next
case (Suc n z)
- have holo0: "f holomorphic_on ( *) u ` s"
+ have holo0: "f holomorphic_on ( *) u ` S"
by (meson fg f holomorphic_on_subset image_subset_iff)
- have holo1: "(\<lambda>w. f (u * w)) holomorphic_on s"
+ have holo2: "(deriv ^^ n) f holomorphic_on ( * ) u ` S"
+ by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
+ have holo3: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on S"
+ by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros)
+ have holo1: "(\<lambda>w. f (u * w)) holomorphic_on S"
apply (rule holomorphic_on_compose [where g=f, unfolded o_def])
apply (rule holo0 holomorphic_intros)+
done
- have holo2: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on s"
- apply (rule holomorphic_intros)+
- apply (rule holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def])
- apply (rule holomorphic_intros)
- apply (rule holomorphic_on_subset [where s=t])
- apply (rule holomorphic_intros assms)+
- apply (blast intro: fg)
- done
have "deriv ((deriv ^^ n) (\<lambda>w. f (u * w))) z = deriv (\<lambda>z. u^n * (deriv ^^ n) f (u*z)) z"
- apply (rule complex_derivative_transform_within_open [OF _ holo2 s Suc.prems])
- apply (rule holomorphic_higher_deriv [OF holo1 s])
+ apply (rule complex_derivative_transform_within_open [OF _ holo3 S Suc.prems])
+ apply (rule holomorphic_higher_deriv [OF holo1 S])
apply (simp add: Suc.IH)
done
also have "\<dots> = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z)) z"
apply (rule deriv_cmult)
apply (rule analytic_on_imp_differentiable_at [OF _ Suc.prems])
- apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and T=t, unfolded o_def])
+ apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and T=T, unfolded o_def])
apply (simp add: analytic_on_linear)
- apply (simp add: analytic_on_open f holomorphic_higher_deriv t)
+ apply (simp add: analytic_on_open f holomorphic_higher_deriv T)
apply (blast intro: fg)
done
also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "( *) u", unfolded o_def])
apply (rule derivative_intros)
- using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
+ using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv T apply blast
apply (simp add: deriv_linear)
done
finally show ?case
@@ -6002,26 +6001,26 @@
proposition no_isolated_singularity:
fixes z::complex
- assumes f: "continuous_on s f" and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
- shows "f holomorphic_on s"
+ assumes f: "continuous_on S f" and holf: "f holomorphic_on (S - K)" and S: "open S" and K: "finite K"
+ shows "f holomorphic_on S"
proof -
{ fix z
- assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f field_differentiable at x"
+ assume "z \<in> S" and cdf: "\<And>x. x\<in>S - K \<Longrightarrow> f field_differentiable at x"
have "f field_differentiable at z"
- proof (cases "z \<in> k")
- case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
+ proof (cases "z \<in> K")
+ case False then show ?thesis by (blast intro: cdf \<open>z \<in> S\<close>)
next
case True
- with finite_set_avoid [OF k, of z]
- obtain d where "d>0" and d: "\<And>x. \<lbrakk>x\<in>k; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
+ with finite_set_avoid [OF K, of z]
+ obtain d where "d>0" and d: "\<And>x. \<lbrakk>x\<in>K; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
by blast
- obtain e where "e>0" and e: "ball z e \<subseteq> s"
- using s \<open>z \<in> s\<close> by (force simp: open_contains_ball)
+ obtain e where "e>0" and e: "ball z e \<subseteq> S"
+ using S \<open>z \<in> S\<close> by (force simp: open_contains_ball)
have fde: "continuous_on (ball z (min d e)) f"
by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
obtain g where "\<And>w. w \<in> ball z (min d e) \<Longrightarrow> (g has_field_derivative f w) (at w within ball z (min d e))"
apply (rule contour_integral_convex_primitive [OF convex_ball fde])
- apply (rule Cauchy_theorem_triangle_cofinite [OF _ k])
+ apply (rule Cauchy_theorem_triangle_cofinite [OF _ K])
apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset)
apply (rule cdf)
apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset
@@ -6034,43 +6033,43 @@
by (metis open_ball \<open>0 < d\<close> \<open>0 < e\<close> at_within_open centre_in_ball min_less_iff_conj)
qed
}
- with holf s k show ?thesis
+ with holf S K show ?thesis
by (simp add: holomorphic_on_open open_Diff finite_imp_closed field_differentiable_def [symmetric])
qed
lemma no_isolated_singularity':
fixes z::complex
- assumes f: "\<And>z. z \<in> k \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within s)"
- and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
- shows "f holomorphic_on s"
+ assumes f: "\<And>z. z \<in> K \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within S)"
+ and holf: "f holomorphic_on (S - K)" and S: "open S" and K: "finite K"
+ shows "f holomorphic_on S"
proof (rule no_isolated_singularity[OF _ assms(2-)])
- show "continuous_on s f" unfolding continuous_on_def
+ show "continuous_on S f" unfolding continuous_on_def
proof
- fix z assume z: "z \<in> s"
- show "(f \<longlongrightarrow> f z) (at z within s)"
- proof (cases "z \<in> k")
+ fix z assume z: "z \<in> S"
+ show "(f \<longlongrightarrow> f z) (at z within S)"
+ proof (cases "z \<in> K")
case False
- from holf have "continuous_on (s - k) f"
+ from holf have "continuous_on (S - K) f"
by (rule holomorphic_on_imp_continuous_on)
- with z False have "(f \<longlongrightarrow> f z) (at z within (s - k))"
+ with z False have "(f \<longlongrightarrow> f z) (at z within (S - K))"
by (simp add: continuous_on_def)
- also from z k s False have "at z within (s - k) = at z within s"
+ also from z K S False have "at z within (S - K) = at z within S"
by (subst (1 2) at_within_open) (auto intro: finite_imp_closed)
- finally show "(f \<longlongrightarrow> f z) (at z within s)" .
+ finally show "(f \<longlongrightarrow> f z) (at z within S)" .
qed (insert assms z, simp_all)
qed
qed
proposition Cauchy_integral_formula_convex:
- assumes s: "convex s" and k: "finite k" and contf: "continuous_on s f"
- and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
- and z: "z \<in> interior s" and vpg: "valid_path \<gamma>"
- and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+ assumes S: "convex S" and K: "finite K" and contf: "continuous_on S f"
+ and fcd: "(\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x)"
+ and z: "z \<in> interior S" and vpg: "valid_path \<gamma>"
+ and pasz: "path_image \<gamma> \<subseteq> S - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
- apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
+ apply (rule Cauchy_integral_formula_weak [OF S finite.emptyI contf])
apply (simp add: holomorphic_on_open [symmetric] field_differentiable_def)
- using no_isolated_singularity [where s = "interior s"]
- apply (metis k contf fcd holomorphic_on_open field_differentiable_def continuous_on_subset
+ using no_isolated_singularity [where S = "interior S"]
+ apply (metis K contf fcd holomorphic_on_open field_differentiable_def continuous_on_subset
has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
using assms
apply auto
@@ -7330,7 +7329,7 @@
done
show ?thesis
unfolding d_def
- apply (rule no_isolated_singularity [OF * _ u, where k = "{w}"])
+ apply (rule no_isolated_singularity [OF * _ u, where K = "{w}"])
apply (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
done
qed
--- a/src/HOL/Analysis/Conformal_Mappings.thy Sun Jun 03 18:23:29 2018 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Sun Jun 03 18:23:38 2018 +0200
@@ -2489,7 +2489,7 @@
finally have **: "g \<midarrow>z\<rightarrow> g z" .
have g_holo: "g holomorphic_on s"
- by (rule no_isolated_singularity'[where k = "{z}"])
+ by (rule no_isolated_singularity'[where K = "{z}"])
(insert assms * **, simp_all add: at_within_open_NO_MATCH)
from s and this have "residue (\<lambda>w. g w / (w - z)) z = g z"
by (rule residue_simple)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Jun 03 18:23:29 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Jun 03 18:23:38 2018 +0200
@@ -3925,55 +3925,42 @@
subsection \<open>Stronger form with finite number of exceptional points\<close>
lemma fundamental_theorem_of_calculus_interior_strong:
- fixes f :: "real \<Rightarrow> 'a::banach"
- assumes "finite s"
- and "a \<le> b"
- and "continuous_on {a..b} f"
- and "\<forall>x\<in>{a <..< b} - s. (f has_vector_derivative f'(x)) (at x)"
- shows "(f' has_integral (f b - f a)) {a..b}"
+ fixes f :: "real \<Rightarrow> 'a::banach"
+ assumes "finite S"
+ and "a \<le> b" "\<And>x. x \<in> {a <..< b} - S \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
+ and "continuous_on {a .. b} f"
+ shows "(f' has_integral (f b - f a)) {a .. b}"
using assms
-proof (induct "card s" arbitrary: s a b)
- case 0
+proof (induction arbitrary: a b)
+case empty
then show ?case
- by (force simp add: intro: fundamental_theorem_of_calculus_interior)
+ using fundamental_theorem_of_calculus_interior by force
next
- case (Suc n)
- then obtain c s' where cs: "s = insert c s'" and n: "n = card s'"
- by (metis card_eq_SucD)
- then have "finite s'"
- using \<open>finite s\<close> by force
+case (insert x S)
show ?case
- proof (cases "c \<in> box a b")
- case False
- with \<open>finite s'\<close> show ?thesis
- using cs n Suc
- by (metis Diff_iff box_real(1) insert_iff)
+ proof (cases "x \<in> {a<..<b}")
+ case False then show ?thesis
+ using insert by blast
next
- let ?P = "\<lambda>i j. \<forall>x\<in>{i <..< j} - s'. (f has_vector_derivative f' x) (at x)"
- case True
- then have "a \<le> c" "c \<le> b"
- by (auto simp: mem_box)
- moreover have "?P a c" "?P c b"
- using Suc.prems(4) True \<open>a \<le> c\<close> cs(1) by auto
- moreover have "continuous_on {a..c} f" "continuous_on {c..b} f"
- using \<open>continuous_on {a..b} f\<close> \<open>a \<le> c\<close> \<open>c \<le> b\<close> continuous_on_subset by fastforce+
- ultimately have "(f' has_integral f c - f a + (f b - f c)) {a..b}"
- using Suc.hyps(1) \<open>finite s'\<close> \<open>n = card s'\<close> by (blast intro: has_integral_combine)
- then show ?thesis
- by auto
+ case True then have "a < x" "x < b"
+ by auto
+ have "(f' has_integral f x - f a) {a..x}" "(f' has_integral f b - f x) {x..b}"
+ using \<open>continuous_on {a..b} f\<close> \<open>a < x\<close> \<open>x < b\<close> continuous_on_subset by (force simp: intro!: insert)+
+ then have "(f' has_integral f x - f a + (f b - f x)) {a..b}"
+ using \<open>a < x\<close> \<open>x < b\<close> has_integral_combine less_imp_le by blast
+ then show ?thesis
+ by simp
qed
qed
corollary fundamental_theorem_of_calculus_strong:
fixes f :: "real \<Rightarrow> 'a::banach"
- assumes "finite s"
+ assumes "finite S"
and "a \<le> b"
+ and vec: "\<And>x. x \<in> {a..b} - S \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
and "continuous_on {a..b} f"
- and vec: "\<forall>x\<in>{a..b} - s. (f has_vector_derivative f'(x)) (at x)"
shows "(f' has_integral (f b - f a)) {a..b}"
- apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
- using vec apply (auto simp: mem_box)
- done
+ by (rule fundamental_theorem_of_calculus_interior_strong [OF \<open>finite S\<close>]) (force simp: assms)+
proposition indefinite_integral_continuous_left:
fixes f:: "real \<Rightarrow> 'a::banach"
@@ -7242,7 +7229,6 @@
define f where "f = (\<lambda>k x. if x \<in> {inverse (of_nat (Suc k))..c} then x powr a else 0)"
define F where "F = (\<lambda>k. if inverse (of_nat (Suc k)) \<le> c then
c powr (a+1)/(a+1) - inverse (real (Suc k)) powr (a+1)/(a+1) else 0)"
-
{
fix k :: nat
have "(f k has_integral F k) {0..c}"
@@ -7448,8 +7434,8 @@
lemma integrable_on_subinterval:
fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
- assumes "f integrable_on s" "{a..b} \<subseteq> s"
+ assumes "f integrable_on S" "{a..b} \<subseteq> S"
shows "f integrable_on {a..b}"
- using integrable_on_subcbox[of f s a b] assms by (simp add: cbox_interval)
+ using integrable_on_subcbox[of f S a b] assms by (simp add: cbox_interval)
end
--- a/src/HOL/Analysis/Infinite_Products.thy Sun Jun 03 18:23:29 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Sun Jun 03 18:23:38 2018 +0200
@@ -50,21 +50,21 @@
by (rule tendsto_eq_intros refl | simp)+
qed auto
-definition gen_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"
- where "gen_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
+definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"
+ where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
- where "f has_prod p \<equiv> gen_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> gen_has_prod f (Suc i) q)"
+ where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)"
definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
- "convergent_prod f \<equiv> \<exists>M p. gen_has_prod f M p"
+ "convergent_prod f \<equiv> \<exists>M p. raw_has_prod f M p"
definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
(binder "\<Prod>" 10)
where "prodinf f = (THE p. f has_prod p)"
-lemmas prod_defs = gen_has_prod_def has_prod_def convergent_prod_def prodinf_def
+lemmas prod_defs = raw_has_prod_def has_prod_def convergent_prod_def prodinf_def
lemma has_prod_subst[trans]: "f = g \<Longrightarrow> g has_prod z \<Longrightarrow> f has_prod z"
by simp
@@ -72,34 +72,39 @@
lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c"
by presburger
-lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0"
- by (simp add: gen_has_prod_def)
+lemma raw_has_prod_nonzero [simp]: "\<not> raw_has_prod f M 0"
+ by (simp add: raw_has_prod_def)
-lemma gen_has_prod_eq_0:
- fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
- assumes p: "gen_has_prod f m p" and i: "f i = 0" "i \<ge> m"
+lemma raw_has_prod_eq_0:
+ fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
+ assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \<ge> m"
shows "p = 0"
proof -
have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n
- by (metis i that atMost_atLeast0 atMost_iff diff_add finite_atLeastAtMost prod_zero_iff)
+ proof -
+ have "\<exists>k\<le>n. f (k + m) = 0"
+ using i that by auto
+ then show ?thesis
+ by auto
+ qed
have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)
with p show ?thesis
- unfolding gen_has_prod_def
+ unfolding raw_has_prod_def
using LIMSEQ_unique by blast
qed
-lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. gen_has_prod f (Suc i) p))"
+lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. raw_has_prod f (Suc i) p))"
by (simp add: has_prod_def)
lemma has_prod_unique2:
- fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+ fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
assumes "f has_prod a" "f has_prod b" shows "a = b"
using assms
- by (auto simp: has_prod_def gen_has_prod_eq_0) (meson gen_has_prod_def sequentially_bot tendsto_unique)
+ by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique)
lemma has_prod_unique:
- fixes f :: "nat \<Rightarrow> 'a :: {idom,t2_space}"
+ fixes f :: "nat \<Rightarrow> 'a :: {semidom,t2_space}"
shows "f has_prod s \<Longrightarrow> s = prodinf f"
by (simp add: has_prod_unique2 prodinf_def the_equality)
@@ -378,42 +383,55 @@
shows "abs_convergent_prod f"
using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)
-lemma convergent_prod_ignore_initial_segment:
- fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}"
- assumes "convergent_prod f"
- shows "convergent_prod (\<lambda>n. f (n + m))"
+lemma raw_has_prod_ignore_initial_segment:
+ fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
+ assumes "raw_has_prod f M p" "N \<ge> M"
+ obtains q where "raw_has_prod f N q"
proof -
- from assms obtain M L
- where L: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> L" "L \<noteq> 0" and nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0"
- by (auto simp: convergent_prod_altdef)
- define C where "C = (\<Prod>k<m. f (k + M))"
+ have p: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> p" and "p \<noteq> 0"
+ using assms by (auto simp: raw_has_prod_def)
+ then have nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0"
+ using assms by (auto simp: raw_has_prod_eq_0)
+ define C where "C = (\<Prod>k<N-M. f (k + M))"
from nz have [simp]: "C \<noteq> 0"
by (auto simp: C_def)
- from L(1) have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) \<longlonglongrightarrow> L"
+ from p have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) \<longlonglongrightarrow> p"
by (rule LIMSEQ_ignore_initial_segment)
- also have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)))"
+ also have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)))"
proof (rule ext, goal_cases)
case (1 n)
- have "{..n+m} = {..<m} \<union> {m..n+m}" by auto
- also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=m..n+m. f (k + M))"
+ have "{..n+(N-M)} = {..<(N-M)} \<union> {(N-M)..n+(N-M)}" by auto
+ also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=(N-M)..n+(N-M). f (k + M))"
unfolding C_def by (rule prod.union_disjoint) auto
- also have "(\<Prod>k=m..n+m. f (k + M)) = (\<Prod>k\<le>n. f (k + m + M))"
- by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + m" "\<lambda>k. k - m"]) auto
- finally show ?case by (simp add: add_ac)
+ also have "(\<Prod>k=(N-M)..n+(N-M). f (k + M)) = (\<Prod>k\<le>n. f (k + (N-M) + M))"
+ by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + (N-M)" "\<lambda>k. k - (N-M)"]) auto
+ finally show ?case
+ using \<open>N \<ge> M\<close> by (simp add: add_ac)
qed
- finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)) / C) \<longlonglongrightarrow> L / C"
+ finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)) / C) \<longlonglongrightarrow> p / C"
by (intro tendsto_divide tendsto_const) auto
- hence "(\<lambda>n. \<Prod>k\<le>n. f (k + M + m)) \<longlonglongrightarrow> L / C" by simp
- moreover from \<open>L \<noteq> 0\<close> have "L / C \<noteq> 0" by simp
- ultimately show ?thesis
- unfolding prod_defs by blast
+ hence "(\<lambda>n. \<Prod>k\<le>n. f (k + N)) \<longlonglongrightarrow> p / C" by simp
+ moreover from \<open>p \<noteq> 0\<close> have "p / C \<noteq> 0" by simp
+ ultimately show ?thesis
+ using raw_has_prod_def that by blast
qed
+corollary convergent_prod_ignore_initial_segment:
+ fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
+ assumes "convergent_prod f"
+ shows "convergent_prod (\<lambda>n. f (n + m))"
+ using assms
+ unfolding convergent_prod_def
+ apply clarify
+ apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment)
+ apply (auto simp add: raw_has_prod_def add_ac)
+ done
+
corollary convergent_prod_ignore_nonzero_segment:
fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0"
- shows "\<exists>p. gen_has_prod f M p"
+ shows "\<exists>p. raw_has_prod f M p"
using convergent_prod_ignore_initial_segment [OF f]
by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))
@@ -551,13 +569,13 @@
with L show ?thesis by (auto simp: prod_defs)
qed
-lemma gen_has_prod_cases:
+lemma raw_has_prod_cases:
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
- assumes "gen_has_prod f M p"
- obtains i where "i<M" "f i = 0" | p where "gen_has_prod f 0 p"
+ assumes "raw_has_prod f M p"
+ obtains i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p"
proof -
have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
- using assms unfolding gen_has_prod_def by blast+
+ using assms unfolding raw_has_prod_def by blast+
then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p"
by (metis tendsto_mult_left)
moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n
@@ -572,8 +590,8 @@
qed
ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"
by (auto intro: LIMSEQ_offset [where k=M])
- then have "gen_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0"
- using \<open>p \<noteq> 0\<close> assms that by (auto simp: gen_has_prod_def)
+ then have "raw_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0"
+ using \<open>p \<noteq> 0\<close> assms that by (auto simp: raw_has_prod_def)
then show thesis
using that by blast
qed
@@ -581,8 +599,8 @@
corollary convergent_prod_offset_0:
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
- shows "\<exists>p. gen_has_prod f 0 p"
- using assms convergent_prod_def gen_has_prod_cases by blast
+ shows "\<exists>p. raw_has_prod f 0 p"
+ using assms convergent_prod_def raw_has_prod_cases by blast
lemma prodinf_eq_lim:
fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
@@ -648,7 +666,7 @@
qed
lemma has_prod_finite:
- fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+ fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
assumes [simp]: "finite N"
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
shows "f has_prod (\<Prod>n\<in>N. f n)"
@@ -668,7 +686,7 @@
moreover have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f N"
by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right)
ultimately show ?thesis
- by (simp add: gen_has_prod_def has_prod_def)
+ by (simp add: raw_has_prod_def has_prod_def)
next
case False
then obtain k where "k \<in> N" "f k = 0"
@@ -692,8 +710,8 @@
(use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
finally show ?thesis .
qed
- have q: "gen_has_prod f (Suc (Max ?Z)) ?q"
- proof (simp add: gen_has_prod_def)
+ have q: "raw_has_prod f (Suc (Max ?Z)) ?q"
+ proof (simp add: raw_has_prod_def)
show "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + Max ?Z))) \<longlonglongrightarrow> ?q"
by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq)
qed
@@ -709,17 +727,20 @@
qed
corollary has_prod_0:
- fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+ fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}"
assumes "\<And>n. f n = 1"
shows "f has_prod 1"
by (simp add: assms has_prod_cong)
+lemma prodinf_zero[simp]: "prodinf (\<lambda>n. 1::'a::real_normed_field) = 1"
+ using has_prod_unique by force
+
lemma convergent_prod_finite:
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
assumes "finite N" "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
shows "convergent_prod f"
proof -
- have "\<exists>n p. gen_has_prod f n p"
+ have "\<exists>n p. raw_has_prod f n p"
using assms has_prod_def has_prod_finite by blast
then show ?thesis
by (simp add: convergent_prod_def)
@@ -759,12 +780,12 @@
assumes "convergent_prod f"
shows "\<exists>p. f has_prod p"
proof -
- obtain M p where p: "gen_has_prod f M p"
+ obtain M p where p: "raw_has_prod f M p"
using assms convergent_prod_def by blast
then have "p \<noteq> 0"
- using gen_has_prod_nonzero by blast
+ using raw_has_prod_nonzero by blast
with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i
- using gen_has_prod_eq_0 that by blast
+ using raw_has_prod_eq_0 that by blast
define C where "C = (\<Prod>n<M. f n)"
show ?thesis
proof (cases "\<forall>n\<le>M. f n \<noteq> 0")
@@ -781,7 +802,7 @@
by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)
have "f i \<noteq> 0" if "i > ?N" for i
by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)
- then have "\<exists>p. gen_has_prod f (Suc ?N) p"
+ then have "\<exists>p. raw_has_prod f (Suc ?N) p"
using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)
then show ?thesis
unfolding has_prod_def using 0 by blast
@@ -796,7 +817,7 @@
lemma convergent_prod_LIMSEQ:
shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f"
by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent
- convergent_prod_to_zero_iff gen_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)
+ convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)
lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
proof
@@ -818,4 +839,494 @@
end
+subsection \<open>Infinite products on ordered, topological monoids\<close>
+
+lemma LIMSEQ_prod_0:
+ fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"
+ assumes "f i = 0"
+ shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
+proof (subst tendsto_cong)
+ show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0"
+ proof
+ show "prod f {..n} = 0" if "n \<ge> i" for n
+ using that assms by auto
+ qed
+qed auto
+
+lemma LIMSEQ_prod_nonneg:
+ fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
+ assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a"
+ shows "a \<ge> 0"
+ by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])
+
+
+context
+ fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
+begin
+
+lemma has_prod_le:
+ assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n"
+ shows "a \<le> b"
+proof (cases "a=0 \<or> b=0")
+ case True
+ then show ?thesis
+ proof
+ assume [simp]: "a=0"
+ have "b \<ge> 0"
+ proof (rule LIMSEQ_prod_nonneg)
+ show "(\<lambda>n. prod g {..n}) \<longlonglongrightarrow> b"
+ using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0)
+ qed (use le order_trans in auto)
+ then show ?thesis
+ by auto
+ next
+ assume [simp]: "b=0"
+ then obtain i where "g i = 0"
+ using g by (auto simp: prod_defs)
+ then have "f i = 0"
+ using antisym le by force
+ then have "a=0"
+ using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique)
+ then show ?thesis
+ by auto
+ qed
+next
+ case False
+ then show ?thesis
+ using assms
+ unfolding has_prod_def raw_has_prod_def
+ by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono)
+qed
+
+lemma prodinf_le:
+ assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n"
+ shows "prodinf f \<le> prodinf g"
+ using has_prod_le [OF assms] has_prod_unique f g by blast
+
end
+
+
+lemma prod_le_prodinf:
+ fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}"
+ assumes "f has_prod a" "\<And>i. 0 \<le> f i" "\<And>i. i\<ge>n \<Longrightarrow> 1 \<le> f i"
+ shows "prod f {..<n} \<le> prodinf f"
+ by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto)
+
+lemma prodinf_nonneg:
+ fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}"
+ assumes "f has_prod a" "\<And>i. 1 \<le> f i"
+ shows "1 \<le> prodinf f"
+ using prod_le_prodinf[of f a 0] assms
+ by (metis order_trans prod_ge_1 zero_le_one)
+
+lemma prodinf_le_const:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes "convergent_prod f" "\<And>n. prod f {..<n} \<le> x"
+ shows "prodinf f \<le> x"
+ by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2)
+
+lemma prodinf_eq_one_iff:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes f: "convergent_prod f" and ge1: "\<And>n. 1 \<le> f n"
+ shows "prodinf f = 1 \<longleftrightarrow> (\<forall>n. f n = 1)"
+proof
+ assume "prodinf f = 1"
+ then have "(\<lambda>n. \<Prod>i<n. f i) \<longlonglongrightarrow> 1"
+ using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost)
+ then have "\<And>i. (\<Prod>n\<in>{i}. f n) \<le> 1"
+ proof (rule LIMSEQ_le_const)
+ have "1 \<le> prod f n" for n
+ by (simp add: ge1 prod_ge_1)
+ have "prod f {..<n} = 1" for n
+ by (metis \<open>\<And>n. 1 \<le> prod f n\<close> \<open>prodinf f = 1\<close> antisym f convergent_prod_has_prod ge1 order_trans prod_le_prodinf zero_le_one)
+ then have "(\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" if "n \<ge> Suc i" for i n
+ by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod_lessThan_Suc)
+ then show "\<exists>N. \<forall>n\<ge>N. (\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" for i
+ by blast
+ qed
+ with ge1 show "\<forall>n. f n = 1"
+ by (auto intro!: antisym)
+qed (metis prodinf_zero fun_eq_iff)
+
+lemma prodinf_pos_iff:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes "convergent_prod f" "\<And>n. 1 \<le> f n"
+ shows "1 < prodinf f \<longleftrightarrow> (\<exists>i. 1 < f i)"
+ using prod_le_prodinf[of f 1] prodinf_eq_one_iff
+ by (metis convergent_prod_has_prod assms less_le prodinf_nonneg)
+
+lemma less_1_prodinf2:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes "convergent_prod f" "\<And>n. 1 \<le> f n" "1 < f i"
+ shows "1 < prodinf f"
+proof -
+ have "1 < (\<Prod>n<Suc i. f n)"
+ using assms by (intro less_1_prod2[where i=i]) auto
+ also have "\<dots> \<le> prodinf f"
+ by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \<open>blast+\<close>)
+ finally show ?thesis .
+qed
+
+lemma less_1_prodinf:
+ fixes f :: "nat \<Rightarrow> real"
+ shows "\<lbrakk>convergent_prod f; \<And>n. 1 < f n\<rbrakk> \<Longrightarrow> 1 < prodinf f"
+ by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le)
+
+lemma prodinf_nonzero:
+ fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
+ assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
+ shows "prodinf f \<noteq> 0"
+ by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def)
+
+lemma less_0_prodinf:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes f: "convergent_prod f" and 0: "\<And>i. f i > 0"
+ shows "0 < prodinf f"
+proof -
+ have "prodinf f \<noteq> 0"
+ by (metis assms less_irrefl prodinf_nonzero)
+ moreover have "0 < (\<Prod>n<i. f n)" for i
+ by (simp add: 0 prod_pos)
+ then have "prodinf f \<ge> 0"
+ using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast
+ ultimately show ?thesis
+ by auto
+qed
+
+lemma prod_less_prodinf2:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 \<le> f m" and 0: "\<And>m. 0 < f m" and i: "n \<le> i" "1 < f i"
+ shows "prod f {..<n} < prodinf f"
+proof -
+ have "prod f {..<n} \<le> prod f {..<i}"
+ by (rule prod_mono2) (use assms less_le in auto)
+ then have "prod f {..<n} < f i * prod f {..<i}"
+ using mult_less_le_imp_less[of 1 "f i" "prod f {..<n}" "prod f {..<i}"] assms
+ by (simp add: prod_pos)
+ moreover have "prod f {..<Suc i} \<le> prodinf f"
+ using prod_le_prodinf[of f _ "Suc i"]
+ by (meson "0" "1" Suc_leD convergent_prod_has_prod f \<open>n \<le> i\<close> le_trans less_eq_real_def)
+ ultimately show ?thesis
+ by (metis le_less_trans mult.commute not_le prod_lessThan_Suc)
+qed
+
+lemma prod_less_prodinf:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 < f m" and 0: "\<And>m. 0 < f m"
+ shows "prod f {..<n} < prodinf f"
+ by (meson "0" "1" f le_less prod_less_prodinf2)
+
+lemma raw_has_prodI_bounded:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes pos: "\<And>n. 1 \<le> f n"
+ and le: "\<And>n. (\<Prod>i<n. f i) \<le> x"
+ shows "\<exists>p. raw_has_prod f 0 p"
+ unfolding raw_has_prod_def add_0_right
+proof (rule exI LIMSEQ_incseq_SUP conjI)+
+ show "bdd_above (range (\<lambda>n. prod f {..n}))"
+ by (metis bdd_aboveI2 le lessThan_Suc_atMost)
+ then have "(SUP i. prod f {..i}) > 0"
+ by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one)
+ then show "(SUP i. prod f {..i}) \<noteq> 0"
+ by auto
+ show "incseq (\<lambda>n. prod f {..n})"
+ using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2)
+qed
+
+lemma convergent_prodI_nonneg_bounded:
+ fixes f :: "nat \<Rightarrow> real"
+ assumes "\<And>n. 1 \<le> f n" "\<And>n. (\<Prod>i<n. f i) \<le> x"
+ shows "convergent_prod f"
+ using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast
+
+
+subsection \<open>Infinite products on topological monoids\<close>
+
+context
+ fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}"
+begin
+
+lemma raw_has_prod_mult: "\<lbrakk>raw_has_prod f M a; raw_has_prod g M b\<rbrakk> \<Longrightarrow> raw_has_prod (\<lambda>n. f n * g n) M (a * b)"
+ by (force simp add: prod.distrib tendsto_mult raw_has_prod_def)
+
+lemma has_prod_mult_nz: "\<lbrakk>f has_prod a; g has_prod b; a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. f n * g n) has_prod (a * b)"
+ by (simp add: raw_has_prod_mult has_prod_def)
+
+end
+
+
+context
+ fixes f g :: "nat \<Rightarrow> 'a::real_normed_field"
+begin
+
+lemma has_prod_mult:
+ assumes f: "f has_prod a" and g: "g has_prod b"
+ shows "(\<lambda>n. f n * g n) has_prod (a * b)"
+ using f [unfolded has_prod_def]
+proof (elim disjE exE conjE)
+ assume f0: "raw_has_prod f 0 a"
+ show ?thesis
+ using g [unfolded has_prod_def]
+ proof (elim disjE exE conjE)
+ assume g0: "raw_has_prod g 0 b"
+ with f0 show ?thesis
+ by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def)
+ next
+ fix j q
+ assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"
+ obtain p where p: "raw_has_prod f (Suc j) p"
+ using f0 raw_has_prod_ignore_initial_segment by blast
+ then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc j))"
+ using q raw_has_prod_mult by blast
+ then show ?thesis
+ using \<open>b = 0\<close> \<open>g j = 0\<close> has_prod_0_iff by fastforce
+ qed
+next
+ fix i p
+ assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p"
+ show ?thesis
+ using g [unfolded has_prod_def]
+ proof (elim disjE exE conjE)
+ assume g0: "raw_has_prod g 0 b"
+ obtain q where q: "raw_has_prod g (Suc i) q"
+ using g0 raw_has_prod_ignore_initial_segment by blast
+ then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc i))"
+ using raw_has_prod_mult p by blast
+ then show ?thesis
+ using \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff by fastforce
+ next
+ fix j q
+ assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"
+ obtain p' where p': "raw_has_prod f (Suc (max i j)) p'"
+ by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p)
+ moreover
+ obtain q' where q': "raw_has_prod g (Suc (max i j)) q'"
+ by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q)
+ ultimately show ?thesis
+ using \<open>b = 0\<close> by (simp add: has_prod_def) (metis \<open>f i = 0\<close> \<open>g j = 0\<close> raw_has_prod_mult max_def)
+ qed
+qed
+
+lemma convergent_prod_mult:
+ assumes f: "convergent_prod f" and g: "convergent_prod g"
+ shows "convergent_prod (\<lambda>n. f n * g n)"
+ unfolding convergent_prod_def
+proof -
+ obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q"
+ using convergent_prod_def f g by blast+
+ then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'"
+ by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2)
+ then show "\<exists>M p. raw_has_prod (\<lambda>n. f n * g n) M p"
+ using raw_has_prod_mult by blast
+qed
+
+lemma prodinf_mult: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f * prodinf g = (\<Prod>n. f n * g n)"
+ by (intro has_prod_unique has_prod_mult convergent_prod_has_prod)
+
+end
+
+context
+ fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_field"
+ and I :: "'i set"
+begin
+
+lemma has_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> (f i) has_prod (x i)) \<Longrightarrow> (\<lambda>n. \<Prod>i\<in>I. f i n) has_prod (\<Prod>i\<in>I. x i)"
+ by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult)
+
+lemma prodinf_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> (\<Prod>n. \<Prod>i\<in>I. f i n) = (\<Prod>i\<in>I. \<Prod>n. f i n)"
+ using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp
+
+lemma convergent_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> convergent_prod (\<lambda>n. \<Prod>i\<in>I. f i n)"
+ using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force
+
+end
+
+subsection \<open>Infinite summability on real normed vector spaces\<close>
+
+context
+ fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
+begin
+
+lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"
+proof -
+ have "raw_has_prod f M (a * f M) \<longleftrightarrow> (\<lambda>i. \<Prod>j\<le>Suc i. f (j+M)) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
+ by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def)
+ also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
+ by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod_atLeast1_atMost_eq lessThan_Suc_atMost)
+ also have "\<dots> \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"
+ proof safe
+ assume tends: "(\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M" and 0: "a * f M \<noteq> 0"
+ with tendsto_divide[OF tends tendsto_const, of "f M"]
+ show "raw_has_prod (\<lambda>n. f (Suc n)) M a"
+ by (simp add: raw_has_prod_def)
+ qed (auto intro: tendsto_mult_right simp: raw_has_prod_def)
+ finally show ?thesis .
+qed
+
+lemma has_prod_Suc_iff:
+ assumes "f 0 \<noteq> 0" shows "(\<lambda>n. f (Suc n)) has_prod a \<longleftrightarrow> f has_prod (a * f 0)"
+proof (cases "a = 0")
+ case True
+ then show ?thesis
+ proof (simp add: has_prod_def, safe)
+ fix i x
+ assume "f (Suc i) = 0" and "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) x"
+ then obtain y where "raw_has_prod f (Suc (Suc i)) y"
+ by (metis (no_types) raw_has_prod_eq_0 Suc_n_not_le_n raw_has_prod_Suc_iff raw_has_prod_ignore_initial_segment raw_has_prod_nonzero linear)
+ then show "\<exists>i. f i = 0 \<and> Ex (raw_has_prod f (Suc i))"
+ using \<open>f (Suc i) = 0\<close> by blast
+ next
+ fix i x
+ assume "f i = 0" and x: "raw_has_prod f (Suc i) x"
+ then obtain j where j: "i = Suc j"
+ by (metis assms not0_implies_Suc)
+ moreover have "\<exists> y. raw_has_prod (\<lambda>n. f (Suc n)) i y"
+ using x by (auto simp: raw_has_prod_def)
+ then show "\<exists>i. f (Suc i) = 0 \<and> Ex (raw_has_prod (\<lambda>n. f (Suc n)) (Suc i))"
+ using \<open>f i = 0\<close> j by blast
+ qed
+next
+ case False
+ then show ?thesis
+ by (auto simp: has_prod_def raw_has_prod_Suc_iff assms)
+qed
+
+lemma convergent_prod_Suc_iff:
+ assumes "\<And>k. f k \<noteq> 0" shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f"
+proof
+ assume "convergent_prod f"
+ then have "f has_prod prodinf f"
+ by (rule convergent_prod_has_prod)
+ moreover have "prodinf f \<noteq> 0"
+ by (simp add: \<open>convergent_prod f\<close> assms prodinf_nonzero)
+ ultimately have "(\<lambda>n. f (Suc n)) has_prod (prodinf f * inverse (f 0))"
+ by (simp add: has_prod_Suc_iff inverse_eq_divide assms)
+ then show "convergent_prod (\<lambda>n. f (Suc n))"
+ using has_prod_iff by blast
+next
+ assume "convergent_prod (\<lambda>n. f (Suc n))"
+ then show "convergent_prod f"
+ using assms convergent_prod_def raw_has_prod_Suc_iff by blast
+qed
+
+lemma raw_has_prod_inverse:
+ assumes "raw_has_prod f M a" shows "raw_has_prod (\<lambda>n. inverse (f n)) M (inverse a)"
+ using assms unfolding raw_has_prod_def by (auto dest: tendsto_inverse simp: prod_inversef [symmetric])
+
+lemma has_prod_inverse:
+ assumes "f has_prod a" shows "(\<lambda>n. inverse (f n)) has_prod (inverse a)"
+using assms raw_has_prod_inverse unfolding has_prod_def by auto
+
+lemma convergent_prod_inverse:
+ assumes "convergent_prod f"
+ shows "convergent_prod (\<lambda>n. inverse (f n))"
+ using assms unfolding convergent_prod_def by (blast intro: raw_has_prod_inverse elim: )
+
+end
+
+context (* Separate contexts are necessary to allow general use of the results above, here. *)
+ fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
+begin
+
+lemma raw_has_prod_Suc_iff': "raw_has_prod f M a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M (a / f M) \<and> f M \<noteq> 0"
+ by (metis raw_has_prod_eq_0 add.commute add.left_neutral raw_has_prod_Suc_iff raw_has_prod_nonzero le_add1 nonzero_mult_div_cancel_right times_divide_eq_left)
+
+lemma has_prod_divide: "f has_prod a \<Longrightarrow> g has_prod b \<Longrightarrow> (\<lambda>n. f n / g n) has_prod (a / b)"
+ unfolding divide_inverse by (intro has_prod_inverse has_prod_mult)
+
+lemma convergent_prod_divide:
+ assumes f: "convergent_prod f" and g: "convergent_prod g"
+ shows "convergent_prod (\<lambda>n. f n / g n)"
+ using f g has_prod_divide has_prod_iff by blast
+
+lemma prodinf_divide: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f / prodinf g = (\<Prod>n. f n / g n)"
+ by (intro has_prod_unique has_prod_divide convergent_prod_has_prod)
+
+lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)"
+ by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod)
+
+lemma has_prod_iff_shift:
+ assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
+ shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))"
+ using assms
+proof (induct n arbitrary: a)
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ then have "(\<lambda>i. f (Suc i + n)) has_prod a \<longleftrightarrow> (\<lambda>i. f (i + n)) has_prod (a * f n)"
+ by (subst has_prod_Suc_iff) auto
+ with Suc show ?case
+ by (simp add: ac_simps)
+qed
+
+corollary has_prod_iff_shift':
+ assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
+ shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> f has_prod a"
+ by (simp add: assms has_prod_iff_shift)
+
+lemma has_prod_one_iff_shift:
+ assumes "\<And>i. i < n \<Longrightarrow> f i = 1"
+ shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a"
+ by (simp add: assms has_prod_iff_shift)
+
+lemma convergent_prod_iff_shift:
+ shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f"
+ apply safe
+ using convergent_prod_offset apply blast
+ using convergent_prod_ignore_initial_segment convergent_prod_def by blast
+
+lemma has_prod_split_initial_segment:
+ assumes "f has_prod a" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
+ shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i))"
+ using assms has_prod_iff_shift' by blast
+
+lemma prodinf_divide_initial_segment:
+ assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
+ shows "(\<Prod>i. f (i + n)) = (\<Prod>i. f i) / (\<Prod>i<n. f i)"
+ by (rule has_prod_unique[symmetric]) (auto simp: assms has_prod_iff_shift)
+
+lemma prodinf_split_initial_segment:
+ assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
+ shows "prodinf f = (\<Prod>i. f (i + n)) * (\<Prod>i<n. f i)"
+ by (auto simp add: assms prodinf_divide_initial_segment)
+
+lemma prodinf_split_head:
+ assumes "convergent_prod f" "f 0 \<noteq> 0"
+ shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0"
+ using prodinf_split_initial_segment[of 1] assms by simp
+
+end
+
+context (* Separate contexts are necessary to allow general use of the results above, here. *)
+ fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
+begin
+
+lemma convergent_prod_inverse_iff: "convergent_prod (\<lambda>n. inverse (f n)) \<longleftrightarrow> convergent_prod f"
+ by (auto dest: convergent_prod_inverse)
+
+lemma convergent_prod_const_iff:
+ fixes c :: "'a :: {real_normed_field}"
+ shows "convergent_prod (\<lambda>_. c) \<longleftrightarrow> c = 1"
+proof
+ assume "convergent_prod (\<lambda>_. c)"
+ then show "c = 1"
+ using convergent_prod_imp_LIMSEQ LIMSEQ_unique by blast
+next
+ assume "c = 1"
+ then show "convergent_prod (\<lambda>_. c)"
+ by auto
+qed
+
+lemma has_prod_power: "f has_prod a \<Longrightarrow> (\<lambda>i. f i ^ n) has_prod (a ^ n)"
+ by (induction n) (auto simp: has_prod_mult)
+
+lemma convergent_prod_power: "convergent_prod f \<Longrightarrow> convergent_prod (\<lambda>i. f i ^ n)"
+ by (induction n) (auto simp: convergent_prod_mult)
+
+lemma prodinf_power: "convergent_prod f \<Longrightarrow> prodinf (\<lambda>i. f i ^ n) = prodinf f ^ n"
+ by (metis has_prod_unique convergent_prod_imp_has_prod has_prod_power)
+
+end
+
+end
--- a/src/HOL/Groups_Big.thy Sun Jun 03 18:23:29 2018 +0200
+++ b/src/HOL/Groups_Big.thy Sun Jun 03 18:23:38 2018 +0200
@@ -1302,17 +1302,20 @@
by simp
qed
-lemma (in linordered_semidom) prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
+context linordered_semidom
+begin
+
+lemma prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
by (induct A rule: infinite_finite_induct) simp_all
-lemma (in linordered_semidom) prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
+lemma prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
by (induct A rule: infinite_finite_induct) simp_all
-lemma (in linordered_semidom) prod_mono:
+lemma prod_mono:
"(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i) \<Longrightarrow> prod f A \<le> prod g A"
by (induct A rule: infinite_finite_induct) (force intro!: prod_nonneg mult_mono)+
-lemma (in linordered_semidom) prod_mono_strict:
+lemma prod_mono_strict:
assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
shows "prod f A < prod g A"
using assms
@@ -1324,6 +1327,42 @@
then show ?case by (force intro: mult_strict_mono' prod_nonneg)
qed
+end
+
+lemma prod_mono2:
+ fixes f :: "'a \<Rightarrow> 'b :: linordered_idom"
+ assumes fin: "finite B"
+ and sub: "A \<subseteq> B"
+ and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 1 \<le> f b"
+ and A: "\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a"
+ shows "prod f A \<le> prod f B"
+proof -
+ have "prod f A \<le> prod f A * prod f (B-A)"
+ by (metis prod_ge_1 A mult_le_cancel_left1 nn not_less prod_nonneg)
+ also from fin finite_subset[OF sub fin] have "\<dots> = prod f (A \<union> (B-A))"
+ by (simp add: prod.union_disjoint del: Un_Diff_cancel)
+ also from sub have "A \<union> (B-A) = B" by blast
+ finally show ?thesis .
+qed
+
+lemma less_1_prod:
+ fixes f :: "'a \<Rightarrow> 'b::linordered_idom"
+ shows "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 1 < f i) \<Longrightarrow> 1 < prod f I"
+ by (induct I rule: finite_ne_induct) (auto intro: less_1_mult)
+
+lemma less_1_prod2:
+ fixes f :: "'a \<Rightarrow> 'b::linordered_idom"
+ assumes I: "finite I" "i \<in> I" "1 < f i" "\<And>i. i \<in> I \<Longrightarrow> 1 \<le> f i"
+ shows "1 < prod f I"
+proof -
+ have "1 < f i * prod f (I - {i})"
+ using assms
+ by (meson DiffD1 leI less_1_mult less_le_trans mult_le_cancel_left1 prod_ge_1)
+ also have "\<dots> = prod f I"
+ using assms by (simp add: prod.remove)
+ finally show ?thesis .
+qed
+
lemma (in linordered_field) abs_prod: "\<bar>prod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
--- a/src/HOL/Set_Interval.thy Sun Jun 03 18:23:29 2018 +0200
+++ b/src/HOL/Set_Interval.thy Sun Jun 03 18:23:38 2018 +0200
@@ -507,7 +507,7 @@
lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot"
by (auto simp: set_eq_iff not_less le_bot)
-lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
+lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
by (simp add: Iio_eq_empty_iff bot_nat_def)
lemma mono_image_least:
@@ -709,7 +709,7 @@
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k"
by (simp add: lessThan_def atMost_def less_Suc_eq_le)
-lemma Iic_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
+lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
unfolding lessThan_Suc_atMost[symmetric] lessThan_Suc_eq_insert_0[of "Suc n"] ..
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
@@ -803,7 +803,7 @@
lemma atLeast0_atMost_Suc_eq_insert_0:
"{0..Suc n} = insert 0 (Suc ` {0..n})"
- by (simp add: atLeast0AtMost Iic_Suc_eq_insert_0)
+ by (simp add: atLeast0AtMost atMost_Suc_eq_insert_0)
subsubsection \<open>Intervals of nats with @{term Suc}\<close>
@@ -2408,6 +2408,16 @@
"\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..n}"
"\<Prod>i<n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..<n}"
+lemma prod_atLeast1_atMost_eq:
+ "prod f {Suc 0..n} = (\<Prod>k<n. f (Suc k))"
+proof -
+ have "prod f {Suc 0..n} = prod f (Suc ` {..<n})"
+ by (simp add: image_Suc_lessThan)
+ also have "\<dots> = (\<Prod>k<n. f (Suc k))"
+ by (simp add: prod.reindex)
+ finally show ?thesis .
+qed
+
lemma prod_int_plus_eq: "prod int {i..i+j} = \<Prod>{int i..int (i+j)}"
by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
@@ -2441,7 +2451,7 @@
"prod f {Suc m..<Suc n} = prod (%i. f(Suc i)){m..<n}"
by (simp add:prod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
-lemma prod_lessThan_Suc: "prod f {..<Suc n} = prod f {..<n} * f n"
+lemma prod_lessThan_Suc [simp]: "prod f {..<Suc n} = prod f {..<n} * f n"
by (simp add: lessThan_Suc mult.commute)
lemma prod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
--- a/src/HOL/Topological_Spaces.thy Sun Jun 03 18:23:29 2018 +0200
+++ b/src/HOL/Topological_Spaces.thy Sun Jun 03 18:23:38 2018 +0200
@@ -1353,6 +1353,12 @@
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+lemma LIMSEQ_lessThan_iff_atMost:
+ shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
+ apply (subst LIMSEQ_Suc_iff [symmetric])
+ apply (simp only: lessThan_Suc_atMost)
+ done
+
lemma LIMSEQ_unique: "X \<longlonglongrightarrow> a \<Longrightarrow> X \<longlonglongrightarrow> b \<Longrightarrow> a = b"
for a b :: "'a::t2_space"
using trivial_limit_sequentially by (rule tendsto_unique)