# HG changeset patch # User paulson # Date 1574778728 0 # Node ID b4d409c65a769c6210dba0e057edad108ed22883 # Parent c9433e8e314efaafa7d48b1d741b7a522c37a102 Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis. diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Nov 26 08:09:44 2019 +0100 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Nov 26 14:32:08 2019 +0000 @@ -3,13 +3,12 @@ *) section \Complex Analysis Basics\ +text \Definitions of analytic and holomorphic functions, limit theorems, complex differentiation\ theory Complex_Analysis_Basics imports Derivative "HOL-Library.Nonpos_Ints" begin -(* TODO FIXME: A lot of the things in here have nothing to do with complex analysis *) - subsection\<^marker>\tag unimportant\\General lemmas\ lemma nonneg_Reals_cmod_eq_Re: "z \ \\<^sub>\\<^sub>0 \ norm z = Re z" @@ -38,26 +37,6 @@ shows "vector_derivative (\z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))" using assms by (intro vector_derivative_cnj_within) auto -lemma lambda_zero: "(\h::'a::mult_zero. 0) = (*) 0" - by auto - -lemma lambda_one: "(\x::'a::monoid_mult. x) = (*) 1" - by auto - -lemma uniformly_continuous_on_cmul_right [continuous_intros]: - fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" - shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. f x * c)" - using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] . - -lemma uniformly_continuous_on_cmul_left[continuous_intros]: - fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" - assumes "uniformly_continuous_on s f" - shows "uniformly_continuous_on s (\x. c * f x)" -by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right) - -lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm" - by (intro continuous_on_id continuous_on_norm) - lemma shows open_halfspace_Re_lt: "open {z. Re(z) < b}" and open_halfspace_Re_gt: "open {z. Re(z) > b}" @@ -135,7 +114,6 @@ assumes "eventually (\x. norm(f x) \ Re(g x)) F" "(g \ 0) F" shows "(f \ 0) F" by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp - lemma closed_segment_same_Re: assumes "Re a = Re b" shows "closed_segment a b = {z. Re z = Re a \ Im z \ closed_segment (Im a) (Im b)}" @@ -426,20 +404,6 @@ by (rule nonzero_deriv_nonconstant [of f "deriv f \" \ S]) (use assms in \auto simp: holomorphic_derivI\) -subsection\<^marker>\tag unimportant\\Caratheodory characterization\ - -lemma field_differentiable_caratheodory_at: - "f field_differentiable (at z) \ - (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z) g)" - using CARAT_DERIV [of f] - by (simp add: field_differentiable_def has_field_derivative_def) - -lemma field_differentiable_caratheodory_within: - "f field_differentiable (at z within s) \ - (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z within s) g)" - using DERIV_caratheodory_within [of f] - by (simp add: field_differentiable_def has_field_derivative_def) - subsection\Analyticity on a set\ definition\<^marker>\tag important\ analytic_on (infixl "(analytic'_on)" 50) @@ -813,60 +777,6 @@ qed qed - -lemma field_differentiable_series: - fixes f :: "nat \ 'a::{real_normed_field,banach} \ 'a" - assumes "convex S" "open S" - assumes "\n x. x \ S \ (f n has_field_derivative f' n x) (at x)" - assumes "uniformly_convergent_on S (\n x. \i S" "summable (\n. f n x0)" and x: "x \ S" - shows "(\x. \n. f n x) field_differentiable (at x)" -proof - - from assms(4) obtain g' where A: "uniform_limit S (\n x. \iopen S\ have S: "at x within S = at x" by (rule at_within_open) - have "\g. \x\S. (\n. f n x) sums g x \ (g has_field_derivative g' x) (at x within S)" - by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within) - then obtain g where g: "\x. x \ S \ (\n. f n x) sums g x" - "\x. x \ S \ (g has_field_derivative g' x) (at x within S)" by blast - from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)" - by (simp add: has_field_derivative_def S) - have "((\x. \n. f n x) has_derivative (*) (g' x)) (at x)" - by (rule has_derivative_transform_within_open[OF g' \open S\ x]) - (insert g, auto simp: sums_iff) - thus "(\x. \n. f n x) field_differentiable (at x)" unfolding differentiable_def - by (auto simp: summable_def field_differentiable_def has_field_derivative_def) -qed - -subsection\<^marker>\tag unimportant\\Bound theorem\ - -lemma field_differentiable_bound: - fixes S :: "'a::real_normed_field set" - assumes cvs: "convex S" - and df: "\z. z \ S \ (f has_field_derivative f' z) (at z within S)" - and dn: "\z. z \ S \ norm (f' z) \ B" - and "x \ S" "y \ S" - shows "norm(f x - f y) \ B * norm(x - y)" - apply (rule differentiable_bound [OF cvs]) - apply (erule df [unfolded has_field_derivative_def]) - apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms) - done - -subsection\<^marker>\tag unimportant\\Inverse function theorem for complex derivatives\ - -lemma has_field_derivative_inverse_basic: - shows "DERIV f (g y) :> f' \ - f' \ 0 \ - continuous (at y) g \ - open t \ - y \ t \ - (\z. z \ t \ f (g z) = z) - \ DERIV g y :> inverse (f')" - unfolding has_field_derivative_def - apply (rule has_derivative_inverse_basic) - apply (auto simp: bounded_linear_mult_right) - done - subsection\<^marker>\tag unimportant\ \Taylor on Complex Numbers\ lemma sum_Suc_reindex: @@ -1053,92 +963,4 @@ qed -subsection\<^marker>\tag unimportant\ \Polynomal function extremal theorem, from HOL Light\ - -lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*) - fixes c :: "nat \ 'a::real_normed_div_algebra" - assumes "0 < e" - shows "\M. \z. M \ norm(z) \ norm (\i\n. c(i) * z^i) \ e * norm(z) ^ (Suc n)" -proof (induct n) - case 0 with assms - show ?case - apply (rule_tac x="norm (c 0) / e" in exI) - apply (auto simp: field_simps) - done -next - case (Suc n) - obtain M where M: "\z. M \ norm z \ norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" - using Suc assms by blast - show ?case - proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc) - fix z::'a - assume z1: "M \ norm z" and "1 + norm (c (Suc n)) / e \ norm z" - then have z2: "e + norm (c (Suc n)) \ e * norm z" - using assms by (simp add: field_simps) - have "norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" - using M [OF z1] by simp - then have "norm (\i\n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)" - by simp - then have "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)" - by (blast intro: norm_triangle_le elim: ) - also have "... \ (e + norm (c (Suc n))) * norm z ^ Suc n" - by (simp add: norm_power norm_mult algebra_simps) - also have "... \ (e * norm z) * norm z ^ Suc n" - by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power) - finally show "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc (Suc n)" - by simp - qed -qed - -lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*) - fixes c :: "nat \ 'a::real_normed_div_algebra" - assumes k: "c k \ 0" "1\k" and kn: "k\n" - shows "eventually (\z. norm (\i\n. c(i) * z^i) \ B) at_infinity" -using kn -proof (induction n) - case 0 - then show ?case - using k by simp -next - case (Suc m) - let ?even = ?case - show ?even - proof (cases "c (Suc m) = 0") - case True - then show ?even using Suc k - by auto (metis antisym_conv less_eq_Suc_le not_le) - next - case False - then obtain M where M: - "\z. M \ norm z \ norm (\i\m. c i * z^i) \ norm (c (Suc m)) / 2 * norm z ^ Suc m" - using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc - by auto - have "\b. \z. b \ norm z \ B \ norm (\i\Suc m. c i * z^i)" - proof (rule exI [where x="max M (max 1 (\B\ / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc) - fix z::'a - assume z1: "M \ norm z" "1 \ norm z" - and "\B\ * 2 / norm (c (Suc m)) \ norm z" - then have z2: "\B\ \ norm (c (Suc m)) * norm z / 2" - using False by (simp add: field_simps) - have nz: "norm z \ norm z ^ Suc m" - by (metis \1 \ norm z\ One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc) - have *: "\y x. norm (c (Suc m)) * norm z / 2 \ norm y - norm x \ B \ norm (x + y)" - by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2) - have "norm z * norm (c (Suc m)) + 2 * norm (\i\m. c i * z^i) - \ norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m" - using M [of z] Suc z1 by auto - also have "... \ 2 * (norm (c (Suc m)) * norm z ^ Suc m)" - using nz by (simp add: mult_mono del: power_Suc) - finally show "B \ norm ((\i\m. c i * z^i) + c (Suc m) * z ^ Suc m)" - using Suc.IH - apply (auto simp: eventually_at_infinity) - apply (rule *) - apply (simp add: field_simps norm_mult norm_power) - done - qed - then show ?even - by (simp add: eventually_at_infinity) - qed -qed - end diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Analysis/Conformal_Mappings.thy --- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Nov 26 08:09:44 2019 +0100 +++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Nov 26 14:32:08 2019 +0000 @@ -386,8 +386,7 @@ have frne: "frontier (cball \ r) \ {}" using \0 < r\ by auto have contfr: "continuous_on (frontier (cball \ r)) (\z. norm (f z - f \))" - apply (rule continuous_on_compose2 [OF Complex_Analysis_Basics.continuous_on_norm_id]) - using hol frsbU holomorphic_on_imp_continuous_on holomorphic_on_subset by blast+ + by (metis continuous_on_norm continuous_on_subset frsbU hol holomorphic_on_imp_continuous_on) obtain w where "norm (\ - w) = r" and w: "(\z. norm (\ - z) = r \ norm (f w - f \) \ norm(f z - f \))" apply (rule bexE [OF continuous_attains_inf [OF cof frne contfr]]) diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Tue Nov 26 08:09:44 2019 +0100 +++ b/src/HOL/Analysis/Derivative.thy Tue Nov 26 14:32:08 2019 +0000 @@ -937,6 +937,18 @@ finally show ?thesis . qed +lemma field_differentiable_bound: + fixes S :: "'a::real_normed_field set" + assumes cvs: "convex S" + and df: "\z. z \ S \ (f has_field_derivative f' z) (at z within S)" + and dn: "\z. z \ S \ norm (f' z) \ B" + and "x \ S" "y \ S" + shows "norm(f x - f y) \ B * norm(x - y)" + apply (rule differentiable_bound [OF cvs]) + apply (erule df [unfolded has_field_derivative_def]) + apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms) + done + lemma differentiable_bound_segment: fixes f::"'a::real_normed_vector \ 'b::real_normed_vector" @@ -1162,6 +1174,20 @@ qed qed +text\<^marker>\tag unimportant\\Inverse function theorem for complex derivatives\ +lemma has_field_derivative_inverse_basic: + shows "DERIV f (g y) :> f' \ + f' \ 0 \ + continuous (at y) g \ + open t \ + y \ t \ + (\z. z \ t \ f (g z) = z) + \ DERIV g y :> inverse (f')" + unfolding has_field_derivative_def + apply (rule has_derivative_inverse_basic) + apply (auto simp: bounded_linear_mult_right) + done + text \Simply rewrite that based on the domain point x.\ lemma has_derivative_inverse_basic_x: @@ -2175,6 +2201,45 @@ using exp_scaleR_has_vector_derivative_right[of A t] by (simp add: exp_times_scaleR_commute) +lemma field_differentiable_series: + fixes f :: "nat \ 'a::{real_normed_field,banach} \ 'a" + assumes "convex S" "open S" + assumes "\n x. x \ S \ (f n has_field_derivative f' n x) (at x)" + assumes "uniformly_convergent_on S (\n x. \i S" "summable (\n. f n x0)" and x: "x \ S" + shows "(\x. \n. f n x) field_differentiable (at x)" +proof - + from assms(4) obtain g' where A: "uniform_limit S (\n x. \iopen S\ have S: "at x within S = at x" by (rule at_within_open) + have "\g. \x\S. (\n. f n x) sums g x \ (g has_field_derivative g' x) (at x within S)" + by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within) + then obtain g where g: "\x. x \ S \ (\n. f n x) sums g x" + "\x. x \ S \ (g has_field_derivative g' x) (at x within S)" by blast + from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)" + by (simp add: has_field_derivative_def S) + have "((\x. \n. f n x) has_derivative (*) (g' x)) (at x)" + by (rule has_derivative_transform_within_open[OF g' \open S\ x]) + (insert g, auto simp: sums_iff) + thus "(\x. \n. f n x) field_differentiable (at x)" unfolding differentiable_def + by (auto simp: summable_def field_differentiable_def has_field_derivative_def) +qed + +subsubsection\<^marker>\tag unimportant\\Caratheodory characterization\ + +lemma field_differentiable_caratheodory_at: + "f field_differentiable (at z) \ + (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z) g)" + using CARAT_DERIV [of f] + by (simp add: field_differentiable_def has_field_derivative_def) + +lemma field_differentiable_caratheodory_within: + "f field_differentiable (at z within s) \ + (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z within s) g)" + using DERIV_caratheodory_within [of f] + by (simp add: field_differentiable_def has_field_derivative_def) + + subsection \Field derivative\ definition\<^marker>\tag important\ deriv :: "('a \ 'a::real_normed_field) \ 'a \ 'a" where @@ -2236,7 +2301,6 @@ apply (rule vector_derivative_at [OF field_vector_diff_chain_at]) using assms vector_derivative_works by (auto simp: field_differentiable_derivI) - subsection \Relation between convexity and derivative\ (* TODO: Generalise to real vector spaces? *) diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Analysis/Elementary_Normed_Spaces.thy --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Nov 26 08:09:44 2019 +0100 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Nov 26 14:32:08 2019 +0000 @@ -1085,6 +1085,17 @@ unfolding dist_real_def by simp qed +lemma uniformly_continuous_on_cmul_right [continuous_intros]: + fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" + shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. f x * c)" + using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] . + +lemma uniformly_continuous_on_cmul_left[continuous_intros]: + fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" + assumes "uniformly_continuous_on s f" + shows "uniformly_continuous_on s (\x. c * f x)" +by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right) + lemma uniformly_continuous_on_norm[continuous_intros]: fixes f :: "'a :: metric_space \ 'b :: real_normed_vector" assumes "uniformly_continuous_on s f" diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue Nov 26 08:09:44 2019 +0100 +++ b/src/HOL/Limits.thy Tue Nov 26 14:32:08 2019 +0000 @@ -341,6 +341,94 @@ by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) +subsubsection\<^marker>\tag unimportant\ \Polynomal function extremal theorem, from HOL Light\ + +lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*) + fixes c :: "nat \ 'a::real_normed_div_algebra" + assumes "0 < e" + shows "\M. \z. M \ norm(z) \ norm (\i\n. c(i) * z^i) \ e * norm(z) ^ (Suc n)" +proof (induct n) + case 0 with assms + show ?case + apply (rule_tac x="norm (c 0) / e" in exI) + apply (auto simp: field_simps) + done +next + case (Suc n) + obtain M where M: "\z. M \ norm z \ norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" + using Suc assms by blast + show ?case + proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc) + fix z::'a + assume z1: "M \ norm z" and "1 + norm (c (Suc n)) / e \ norm z" + then have z2: "e + norm (c (Suc n)) \ e * norm z" + using assms by (simp add: field_simps) + have "norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" + using M [OF z1] by simp + then have "norm (\i\n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)" + by simp + then have "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)" + by (blast intro: norm_triangle_le elim: ) + also have "... \ (e + norm (c (Suc n))) * norm z ^ Suc n" + by (simp add: norm_power norm_mult algebra_simps) + also have "... \ (e * norm z) * norm z ^ Suc n" + by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power) + finally show "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc (Suc n)" + by simp + qed +qed + +lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*) + fixes c :: "nat \ 'a::real_normed_div_algebra" + assumes k: "c k \ 0" "1\k" and kn: "k\n" + shows "eventually (\z. norm (\i\n. c(i) * z^i) \ B) at_infinity" +using kn +proof (induction n) + case 0 + then show ?case + using k by simp +next + case (Suc m) + let ?even = ?case + show ?even + proof (cases "c (Suc m) = 0") + case True + then show ?even using Suc k + by auto (metis antisym_conv less_eq_Suc_le not_le) + next + case False + then obtain M where M: + "\z. M \ norm z \ norm (\i\m. c i * z^i) \ norm (c (Suc m)) / 2 * norm z ^ Suc m" + using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc + by auto + have "\b. \z. b \ norm z \ B \ norm (\i\Suc m. c i * z^i)" + proof (rule exI [where x="max M (max 1 (\B\ / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc) + fix z::'a + assume z1: "M \ norm z" "1 \ norm z" + and "\B\ * 2 / norm (c (Suc m)) \ norm z" + then have z2: "\B\ \ norm (c (Suc m)) * norm z / 2" + using False by (simp add: field_simps) + have nz: "norm z \ norm z ^ Suc m" + by (metis \1 \ norm z\ One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc) + have *: "\y x. norm (c (Suc m)) * norm z / 2 \ norm y - norm x \ B \ norm (x + y)" + by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2) + have "norm z * norm (c (Suc m)) + 2 * norm (\i\m. c i * z^i) + \ norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m" + using M [of z] Suc z1 by auto + also have "... \ 2 * (norm (c (Suc m)) * norm z ^ Suc m)" + using nz by (simp add: mult_mono del: power_Suc) + finally show "B \ norm ((\i\m. c i * z^i) + c (Suc m) * z ^ Suc m)" + using Suc.IH + apply (auto simp: eventually_at_infinity) + apply (rule *) + apply (simp add: field_simps norm_mult norm_power) + done + qed + then show ?even + by (simp add: eventually_at_infinity) + qed +qed + subsection \Convergence to Zero\ definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" @@ -545,6 +633,9 @@ "continuous_on s f \ continuous_on s (\x. norm (f x))" unfolding continuous_on_def by (auto intro: tendsto_norm) +lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm" + by (intro continuous_on_id continuous_on_norm) + lemma tendsto_norm_zero: "(f \ 0) F \ ((\x. norm (f x)) \ 0) F" by (drule tendsto_norm) simp diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Tue Nov 26 08:09:44 2019 +0100 +++ b/src/HOL/Rings.thy Tue Nov 26 14:32:08 2019 +0000 @@ -128,6 +128,11 @@ end +lemma lambda_zero: "(\h::'a::mult_zero. 0) = (*) 0" + by auto + +lemma lambda_one: "(\x::'a::monoid_mult. x) = (*) 1" + by auto subsection \Abstract divisibility\ diff -r c9433e8e314e -r b4d409c65a76 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Tue Nov 26 08:09:44 2019 +0100 +++ b/src/HOL/Set_Interval.thy Tue Nov 26 14:32:08 2019 +0000 @@ -1944,6 +1944,9 @@ "F g {Suc m..Suc n} = F (\i. g(Suc i)){m..n}" by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) +corollary Suc_reindex_ivl: "m \ n \ F g {m..n} \<^bold>* g (Suc n) = g m \<^bold>* F (\i. g (Suc i)) {m..n}" + by (simp add: assoc atLeast_Suc_atMost flip: shift_bounds_cl_Suc_ivl) + corollary shift_bounds_Suc_ivl: "F g {Suc m..i. g(Suc i)){m..