(* Title: HOL/Analysis/Derivative.thy Author: John Harrison Author: Robert Himmelmann, TU Muenchen (translation from HOL Light); tidied by LCP *) section ‹Multivariate calculus in Euclidean space› theory Derivative imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function begin declare bounded_linear_inner_left [intro] declare has_derivative_bounded_linear[dest] subsection ‹Derivatives› lemma has_derivative_add_const: "(f has_derivative f') net ⟹ ((λx. f x + c) has_derivative f') net" by (intro derivative_eq_intros) auto subsection ‹Derivative with composed bilinear function› text ‹More explicit epsilon-delta forms.› lemma has_derivative_within': "(f has_derivative f')(at x within s) ⟷ bounded_linear f' ∧ (∀e>0. ∃d>0. ∀x'∈s. 0 < norm (x' - x) ∧ norm (x' - x) < d ⟶ norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)" unfolding has_derivative_within Lim_within dist_norm by (simp add: diff_diff_eq) lemma has_derivative_at': "(f has_derivative f') (at x) ⟷ bounded_linear f' ∧ (∀e>0. ∃d>0. ∀x'. 0 < norm (x' - x) ∧ norm (x' - x) < d ⟶ norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)" using has_derivative_within' [of f f' x UNIV] by simp lemma has_derivative_at_withinI: "(f has_derivative f') (at x) ⟹ (f has_derivative f') (at x within s)" unfolding has_derivative_within' has_derivative_at' by blast lemma has_derivative_within_open: "a ∈ S ⟹ open S ⟹ (f has_derivative f') (at a within S) ⟷ (f has_derivative f') (at a)" by (simp only: at_within_interior interior_open) lemma has_derivative_right: fixes f :: "real ⇒ real" and y :: "real" shows "(f has_derivative (( * ) y)) (at x within ({x <..} ∩ I)) ⟷ ((λt. (f x - f t) / (x - t)) ⤏ y) (at x within ({x <..} ∩ I))" proof - have "((λt. (f t - (f x + y * (t - x))) / ¦t - x¦) ⤏ 0) (at x within ({x<..} ∩ I)) ⟷ ((λt. (f t - f x) / (t - x) - y) ⤏ 0) (at x within ({x<..} ∩ I))" by (intro Lim_cong_within) (auto simp add: diff_divide_distrib add_divide_distrib) also have "… ⟷ ((λt. (f t - f x) / (t - x)) ⤏ y) (at x within ({x<..} ∩ I))" by (simp add: Lim_null[symmetric]) also have "… ⟷ ((λt. (f x - f t) / (x - t)) ⤏ y) (at x within ({x<..} ∩ I))" by (intro Lim_cong_within) (simp_all add: field_simps) finally show ?thesis by (simp add: bounded_linear_mult_right has_derivative_within) qed subsubsection ‹Caratheodory characterization› lemma DERIV_caratheodory_within: "(f has_field_derivative l) (at x within S) ⟷ (∃g. (∀z. f z - f x = g z * (z - x)) ∧ continuous (at x within S) g ∧ g x = l)" (is "?lhs = ?rhs") proof assume ?lhs show ?rhs proof (intro exI conjI) let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))" show "∀z. f z - f x = ?g z * (z-x)" by simp show "continuous (at x within S) ?g" using ‹?lhs› by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within) show "?g x = l" by simp qed next assume ?rhs then obtain g where "(∀z. f z - f x = g z * (z-x))" and "continuous (at x within S) g" and "g x = l" by blast thus ?lhs by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within) qed subsection ‹Differentiability› definition differentiable_on :: "('a::real_normed_vector ⇒ 'b::real_normed_vector) ⇒ 'a set ⇒ bool" (infix "differentiable'_on" 50) where "f differentiable_on s ⟷ (∀x∈s. f differentiable (at x within s))" lemma differentiableI: "(f has_derivative f') net ⟹ f differentiable net" unfolding differentiable_def by auto lemma differentiable_onD: "⟦f differentiable_on S; x ∈ S⟧ ⟹ f differentiable (at x within S)" using differentiable_on_def by blast lemma differentiable_at_withinI: "f differentiable (at x) ⟹ f differentiable (at x within s)" unfolding differentiable_def using has_derivative_at_withinI by blast lemma differentiable_at_imp_differentiable_on: "(⋀x. x ∈ s ⟹ f differentiable at x) ⟹ f differentiable_on s" by (metis differentiable_at_withinI differentiable_on_def) corollary differentiable_iff_scaleR: fixes f :: "real ⇒ 'a::real_normed_vector" shows "f differentiable F ⟷ (∃d. (f has_derivative (λx. x *⇩_{R}d)) F)" by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR) lemma differentiable_on_eq_differentiable_at: "open s ⟹ f differentiable_on s ⟷ (∀x∈s. f differentiable at x)" unfolding differentiable_on_def by (metis at_within_interior interior_open) lemma differentiable_transform_within: assumes "f differentiable (at x within s)" and "0 < d" and "x ∈ s" and "⋀x'. ⟦x'∈s; dist x' x < d⟧ ⟹ f x' = g x'" shows "g differentiable (at x within s)" using assms has_derivative_transform_within unfolding differentiable_def by blast lemma differentiable_on_ident [simp, derivative_intros]: "(λx. x) differentiable_on S" by (simp add: differentiable_at_imp_differentiable_on) lemma differentiable_on_id [simp, derivative_intros]: "id differentiable_on S" by (simp add: id_def) lemma differentiable_on_const [simp, derivative_intros]: "(λz. c) differentiable_on S" by (simp add: differentiable_on_def) lemma differentiable_on_mult [simp, derivative_intros]: fixes f :: "'M::real_normed_vector ⇒ 'a::real_normed_algebra" shows "⟦f differentiable_on S; g differentiable_on S⟧ ⟹ (λz. f z * g z) differentiable_on S" unfolding differentiable_on_def differentiable_def using differentiable_def differentiable_mult by blast lemma differentiable_on_compose: "⟦g differentiable_on S; f differentiable_on (g ` S)⟧ ⟹ (λx. f (g x)) differentiable_on S" by (simp add: differentiable_in_compose differentiable_on_def) lemma bounded_linear_imp_differentiable_on: "bounded_linear f ⟹ f differentiable_on S" by (simp add: differentiable_on_def bounded_linear_imp_differentiable) lemma linear_imp_differentiable_on: fixes f :: "'a::euclidean_space ⇒ 'b::real_normed_vector" shows "linear f ⟹ f differentiable_on S" by (simp add: differentiable_on_def linear_imp_differentiable) lemma differentiable_on_minus [simp, derivative_intros]: "f differentiable_on S ⟹ (λz. -(f z)) differentiable_on S" by (simp add: differentiable_on_def) lemma differentiable_on_add [simp, derivative_intros]: "⟦f differentiable_on S; g differentiable_on S⟧ ⟹ (λz. f z + g z) differentiable_on S" by (simp add: differentiable_on_def) lemma differentiable_on_diff [simp, derivative_intros]: "⟦f differentiable_on S; g differentiable_on S⟧ ⟹ (λz. f z - g z) differentiable_on S" by (simp add: differentiable_on_def) lemma differentiable_on_inverse [simp, derivative_intros]: fixes f :: "'a :: real_normed_vector ⇒ 'b :: real_normed_field" shows "f differentiable_on S ⟹ (⋀x. x ∈ S ⟹ f x ≠ 0) ⟹ (λx. inverse (f x)) differentiable_on S" by (simp add: differentiable_on_def) lemma differentiable_on_scaleR [derivative_intros, simp]: "⟦f differentiable_on S; g differentiable_on S⟧ ⟹ (λx. f x *⇩_{R}g x) differentiable_on S" unfolding differentiable_on_def by (blast intro: differentiable_scaleR) lemma has_derivative_sqnorm_at [derivative_intros, simp]: "((λx. (norm x)⇧^{2}) has_derivative (λx. 2 *⇩_{R}(a ∙ x))) (at a)" using bounded_bilinear.FDERIV [of "(∙)" id id a _ id id] by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner) lemma differentiable_sqnorm_at [derivative_intros, simp]: fixes a :: "'a :: {real_normed_vector,real_inner}" shows "(λx. (norm x)⇧^{2}) differentiable (at a)" by (force simp add: differentiable_def intro: has_derivative_sqnorm_at) lemma differentiable_on_sqnorm [derivative_intros, simp]: fixes S :: "'a :: {real_normed_vector,real_inner} set" shows "(λx. (norm x)⇧^{2}) differentiable_on S" by (simp add: differentiable_at_imp_differentiable_on) lemma differentiable_norm_at [derivative_intros, simp]: fixes a :: "'a :: {real_normed_vector,real_inner}" shows "a ≠ 0 ⟹ norm differentiable (at a)" using differentiableI has_derivative_norm by blast lemma differentiable_on_norm [derivative_intros, simp]: fixes S :: "'a :: {real_normed_vector,real_inner} set" shows "0 ∉ S ⟹ norm differentiable_on S" by (metis differentiable_at_imp_differentiable_on differentiable_norm_at) subsection ‹Frechet derivative and Jacobian matrix› definition "frechet_derivative f net = (SOME f'. (f has_derivative f') net)" lemma frechet_derivative_works: "f differentiable net ⟷ (f has_derivative (frechet_derivative f net)) net" unfolding frechet_derivative_def differentiable_def unfolding some_eq_ex[of "λ f' . (f has_derivative f') net"] .. lemma linear_frechet_derivative: "f differentiable net ⟹ linear (frechet_derivative f net)" unfolding frechet_derivative_works has_derivative_def by (auto intro: bounded_linear.linear) subsection ‹Differentiability implies continuity› lemma differentiable_imp_continuous_within: "f differentiable (at x within s) ⟹ continuous (at x within s) f" by (auto simp: differentiable_def intro: has_derivative_continuous) lemma differentiable_imp_continuous_on: "f differentiable_on s ⟹ continuous_on s f" unfolding differentiable_on_def continuous_on_eq_continuous_within using differentiable_imp_continuous_within by blast lemma differentiable_on_subset: "f differentiable_on t ⟹ s ⊆ t ⟹ f differentiable_on s" unfolding differentiable_on_def using differentiable_within_subset by blast lemma differentiable_on_empty: "f differentiable_on {}" unfolding differentiable_on_def by auto lemma has_derivative_continuous_on: "(⋀x. x ∈ s ⟹ (f has_derivative f' x) (at x within s)) ⟹ continuous_on s f" by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def) text ‹Results about neighborhoods filter.› lemma eventually_nhds_metric_le: "eventually P (nhds a) = (∃d>0. ∀x. dist x a ≤ d ⟶ P x)" unfolding eventually_nhds_metric by (safe, rule_tac x="d / 2" in exI, auto) lemma le_nhds: "F ≤ nhds a ⟷ (∀S. open S ∧ a ∈ S ⟶ eventually (λx. x ∈ S) F)" unfolding le_filter_def eventually_nhds by (fast elim: eventually_mono) lemma le_nhds_metric: "F ≤ nhds a ⟷ (∀e>0. eventually (λx. dist x a < e) F)" unfolding le_filter_def eventually_nhds_metric by (fast elim: eventually_mono) lemma le_nhds_metric_le: "F ≤ nhds a ⟷ (∀e>0. eventually (λx. dist x a ≤ e) F)" unfolding le_filter_def eventually_nhds_metric_le by (fast elim: eventually_mono) text ‹Several results are easier using a "multiplied-out" variant. (I got this idea from Dieudonne's proof of the chain rule).› lemma has_derivative_within_alt: "(f has_derivative f') (at x within s) ⟷ bounded_linear f' ∧ (∀e>0. ∃d>0. ∀y∈s. norm(y - x) < d ⟶ norm (f y - f x - f' (y - x)) ≤ e * norm (y - x))" unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap eventually_at dist_norm diff_diff_eq by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq) lemma has_derivative_within_alt2: "(f has_derivative f') (at x within s) ⟷ bounded_linear f' ∧ (∀e>0. eventually (λy. norm (f y - f x - f' (y - x)) ≤ e * norm (y - x)) (at x within s))" unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap eventually_at dist_norm diff_diff_eq by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq) lemma has_derivative_at_alt: "(f has_derivative f') (at x) ⟷ bounded_linear f' ∧ (∀e>0. ∃d>0. ∀y. norm(y - x) < d ⟶ norm (f y - f x - f'(y - x)) ≤ e * norm (y - x))" using has_derivative_within_alt[where s=UNIV] by simp subsection ‹The chain rule› lemma diff_chain_within[derivative_intros]: assumes "(f has_derivative f') (at x within s)" and "(g has_derivative g') (at (f x) within (f ` s))" shows "((g ∘ f) has_derivative (g' ∘ f'))(at x within s)" using has_derivative_in_compose[OF assms] by (simp add: comp_def) lemma diff_chain_at[derivative_intros]: "(f has_derivative f') (at x) ⟹ (g has_derivative g') (at (f x)) ⟹ ((g ∘ f) has_derivative (g' ∘ f')) (at x)" using has_derivative_compose[of f f' x UNIV g g'] by (simp add: comp_def) lemma has_vector_derivative_within_open: "a ∈ S ⟹ open S ⟹ (f has_vector_derivative f') (at a within S) ⟷ (f has_vector_derivative f') (at a)" by (simp only: at_within_interior interior_open) lemma field_vector_diff_chain_within: assumes Df: "(f has_vector_derivative f') (at x within S)" and Dg: "(g has_field_derivative g') (at (f x) within f ` S)" shows "((g ∘ f) has_vector_derivative (f' * g')) (at x within S)" using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg [unfolded has_field_derivative_def]] by (auto simp: o_def mult.commute has_vector_derivative_def) lemma vector_derivative_diff_chain_within: assumes Df: "(f has_vector_derivative f') (at x within S)" and Dg: "(g has_derivative g') (at (f x) within f`S)" shows "((g ∘ f) has_vector_derivative (g' f')) (at x within S)" using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg] linear.scaleR[OF has_derivative_linear[OF Dg]] unfolding has_vector_derivative_def o_def by (auto simp: o_def mult.commute has_vector_derivative_def) subsection ‹Composition rules stated just for differentiability› lemma differentiable_chain_at: "f differentiable (at x) ⟹ g differentiable (at (f x)) ⟹ (g ∘ f) differentiable (at x)" unfolding differentiable_def by (meson diff_chain_at) lemma differentiable_chain_within: "f differentiable (at x within S) ⟹ g differentiable (at(f x) within (f ` S)) ⟹ (g ∘ f) differentiable (at x within S)" unfolding differentiable_def by (meson diff_chain_within) subsection ‹Uniqueness of derivative› text ‹ The general result is a bit messy because we need approachability of the limit point from any direction. But OK for nontrivial intervals etc. › lemma frechet_derivative_unique_within: fixes f :: "'a::euclidean_space ⇒ 'b::real_normed_vector" assumes 1: "(f has_derivative f') (at x within S)" and 2: "(f has_derivative f'') (at x within S)" and S: "⋀i e. ⟦i∈Basis; e>0⟧ ⟹ ∃d. 0 < ¦d¦ ∧ ¦d¦ < e ∧ (x + d *⇩_{R}i) ∈ S" shows "f' = f''" proof - note as = assms(1,2)[unfolded has_derivative_def] then interpret f': bounded_linear f' by auto from as interpret f'': bounded_linear f'' by auto have "x islimpt S" unfolding islimpt_approachable proof (intro allI impI) fix e :: real assume "e > 0" obtain d where "0 < ¦d¦" and "¦d¦ < e" and "x + d *⇩_{R}(SOME i. i ∈ Basis) ∈ S" using assms(3) SOME_Basis ‹e>0› by blast then show "∃x'∈S. x' ≠ x ∧ dist x' x < e" by (rule_tac x="x + d *⇩_{R}(SOME i. i ∈ Basis)" in bexI) (auto simp: dist_norm SOME_Basis nonzero_Basis) qed then have *: "netlimit (at x within S) = x" by (simp add: Lim_ident_at trivial_limit_within) show ?thesis proof (rule linear_eq_stdbasis) show "linear f'" "linear f''" unfolding linear_conv_bounded_linear using as by auto next fix i :: 'a assume i: "i ∈ Basis" define e where "e = norm (f' i - f'' i)" show "f' i = f'' i" proof (rule ccontr) assume "f' i ≠ f'' i" then have "e > 0" unfolding e_def by auto obtain d where d: "0 < d" "(⋀y. y∈S ⟶ 0 < dist y x ∧ dist y x < d ⟶ dist ((f y - f x - f' (y - x)) /⇩_{R}norm (y - x) - (f y - f x - f'' (y - x)) /⇩_{R}norm (y - x)) (0 - 0) < e)" using tendsto_diff [OF as(1,2)[THEN conjunct2]] unfolding * Lim_within using ‹e>0› by blast obtain c where c: "0 < ¦c¦" "¦c¦ < d ∧ x + c *⇩_{R}i ∈ S" using assms(3) i d(1) by blast have *: "norm (- ((1 / ¦c¦) *⇩_{R}f' (c *⇩_{R}i)) + (1 / ¦c¦) *⇩_{R}f'' (c *⇩_{R}i)) = norm ((1 / ¦c¦) *⇩_{R}(- (f' (c *⇩_{R}i)) + f'' (c *⇩_{R}i)))" unfolding scaleR_right_distrib by auto also have "… = norm ((1 / ¦c¦) *⇩_{R}(c *⇩_{R}(- (f' i) + f'' i)))" unfolding f'.scaleR f''.scaleR unfolding scaleR_right_distrib scaleR_minus_right by auto also have "… = e" unfolding e_def using c(1) using norm_minus_cancel[of "f' i - f'' i"] by auto finally show False using c using d(2)[of "x + c *⇩_{R}i"] unfolding dist_norm unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib using i by (auto simp: inverse_eq_divide) qed qed qed lemma frechet_derivative_unique_within_closed_interval: fixes f::"'a::euclidean_space ⇒ 'b::real_normed_vector" assumes ab: "⋀i. i∈Basis ⟹ a∙i < b∙i" and x: "x ∈ cbox a b" and "(f has_derivative f' ) (at x within cbox a b)" and "(f has_derivative f'') (at x within cbox a b)" shows "f' = f''" proof (rule frechet_derivative_unique_within) fix e :: real fix i :: 'a assume "e > 0" and i: "i ∈ Basis" then show "∃d. 0 < ¦d¦ ∧ ¦d¦ < e ∧ x + d *⇩_{R}i ∈ cbox a b" proof (cases "x∙i = a∙i") case True with ab[of i] ‹e>0› x i show ?thesis by (rule_tac x="(min (b∙i - a∙i) e) / 2" in exI) (auto simp add: mem_box field_simps inner_simps inner_Basis) next case False moreover have "a ∙ i < x ∙ i" using False i mem_box(2) x by force moreover { have "a ∙ i * 2 + min (x ∙ i - a ∙ i) e ≤ a∙i *2 + x∙i - a∙i" by auto also have "… = a∙i + x∙i" by auto also have "… ≤ 2 * (x∙i)" using ‹a ∙ i < x ∙ i› by auto finally have "a ∙ i * 2 + min (x ∙ i - a ∙ i) e ≤ x ∙ i * 2" by auto } moreover have "min (x ∙ i - a ∙ i) e ≥ 0" by (simp add: ‹0 < e› ‹a ∙ i < x ∙ i› less_eq_real_def) then have "x ∙ i * 2 ≤ b ∙ i * 2 + min (x ∙ i - a ∙ i) e" using i mem_box(2) x by force ultimately show ?thesis using ab[of i] ‹e>0› x i by (rule_tac x="- (min (x∙i - a∙i) e) / 2" in exI) (auto simp add: mem_box field_simps inner_simps inner_Basis) qed qed (use assms in auto) lemma frechet_derivative_unique_within_open_interval: fixes f::"'a::euclidean_space ⇒ 'b::real_normed_vector" assumes x: "x ∈ box a b" and f: "(f has_derivative f' ) (at x within box a b)" "(f has_derivative f'') (at x within box a b)" shows "f' = f''" proof - have "at x within box a b = at x" by (metis x at_within_interior interior_open open_box) with f show "f' = f''" by (simp add: has_derivative_unique) qed lemma frechet_derivative_at: "(f has_derivative f') (at x) ⟹ f' = frechet_derivative f (at x)" using differentiable_def frechet_derivative_works has_derivative_unique by blast lemma frechet_derivative_within_cbox: fixes f :: "'a::euclidean_space ⇒ 'b::real_normed_vector" assumes "⋀i. i∈Basis ⟹ a∙i < b∙i" and "x ∈ cbox a b" and "(f has_derivative f') (at x within cbox a b)" shows "frechet_derivative f (at x within cbox a b) = f'" using assms by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works) subsection ‹The traditional Rolle theorem in one dimension› text ‹Derivatives of local minima and maxima are zero.› lemma has_derivative_local_min: fixes f :: "'a::real_normed_vector ⇒ real" assumes deriv: "(f has_derivative f') (at x)" assumes min: "eventually (λy. f x ≤ f y) (at x)" shows "f' = (λh. 0)" proof fix h :: 'a interpret f': bounded_linear f' using deriv by (rule has_derivative_bounded_linear) show "f' h = 0" proof (cases "h = 0") case False from min obtain d where d1: "0 < d" and d2: "∀y∈ball x d. f x ≤ f y" unfolding eventually_at by (force simp: dist_commute) have "FDERIV (λr. x + r *⇩_{R}h) 0 :> (λr. r *⇩_{R}h)" by (intro derivative_eq_intros) auto then have "FDERIV (λr. f (x + r *⇩_{R}h)) 0 :> (λk. f' (k *⇩_{R}h))" by (rule has_derivative_compose, simp add: deriv) then have "DERIV (λr. f (x + r *⇩_{R}h)) 0 :> f' h" unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs) moreover have "0 < d / norm h" using d1 and ‹h ≠ 0› by simp moreover have "∀y. ¦0 - y¦ < d / norm h ⟶ f (x + 0 *⇩_{R}h) ≤ f (x + y *⇩_{R}h)" using ‹h ≠ 0› by (auto simp add: d2 dist_norm pos_less_divide_eq) ultimately show "f' h = 0" by (rule DERIV_local_min) qed simp qed lemma has_derivative_local_max: fixes f :: "'a::real_normed_vector ⇒ real" assumes "(f has_derivative f') (at x)" assumes "eventually (λy. f y ≤ f x) (at x)" shows "f' = (λh. 0)" using has_derivative_local_min [of "λx. - f x" "λh. - f' h" "x"] using assms unfolding fun_eq_iff by simp lemma differential_zero_maxmin: fixes f::"'a::real_normed_vector ⇒ real" assumes "x ∈ S" and "open S" and deriv: "(f has_derivative f') (at x)" and mono: "(∀y∈S. f y ≤ f x) ∨ (∀y∈S. f x ≤ f y)" shows "f' = (λv. 0)" using mono proof assume "∀y∈S. f y ≤ f x" with ‹x ∈ S› and ‹open S› have "eventually (λy. f y ≤ f x) (at x)" unfolding eventually_at_topological by auto with deriv show ?thesis by (rule has_derivative_local_max) next assume "∀y∈S. f x ≤ f y" with ‹x ∈ S› and ‹open S› have "eventually (λy. f x ≤ f y) (at x)" unfolding eventually_at_topological by auto with deriv show ?thesis by (rule has_derivative_local_min) qed lemma differential_zero_maxmin_component: (* TODO: delete? *) fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes k: "k ∈ Basis" and ball: "0 < e" "(∀y ∈ ball x e. (f y)∙k ≤ (f x)∙k) ∨ (∀y∈ball x e. (f x)∙k ≤ (f y)∙k)" and diff: "f differentiable (at x)" shows "(∑j∈Basis. (frechet_derivative f (at x) j ∙ k) *⇩_{R}j) = (0::'a)" (is "?D k = 0") proof - let ?f' = "frechet_derivative f (at x)" have "x ∈ ball x e" using ‹0 < e› by simp moreover have "open (ball x e)" by simp moreover have "((λx. f x ∙ k) has_derivative (λh. ?f' h ∙ k)) (at x)" using bounded_linear_inner_left diff[unfolded frechet_derivative_works] by (rule bounded_linear.has_derivative) ultimately have "(λh. frechet_derivative f (at x) h ∙ k) = (λv. 0)" using ball(2) by (rule differential_zero_maxmin) then show ?thesis unfolding fun_eq_iff by simp qed theorem Rolle: fixes f :: "real ⇒ real" assumes "a < b" and fab: "f a = f b" and contf: "continuous_on {a..b} f" and derf: "⋀x. ⟦a < x; x < b⟧ ⟹ (f has_derivative f' x) (at x)" shows "∃x∈{a <..< b}. f' x = (λv. 0)" proof - have "∃x∈box a b. (∀y∈box a b. f x ≤ f y) ∨ (∀y∈box a b. f y ≤ f x)" proof - have "(a + b) / 2 ∈ {a..b}" using assms(1) by auto then have *: "{a..b} ≠ {}" by auto obtain d where d: "d ∈cbox a b" "∀y∈cbox a b. f y ≤ f d" using continuous_attains_sup[OF compact_Icc * contf] by auto obtain c where c: "c ∈ cbox a b" "∀y∈cbox a b. f c ≤ f y" using continuous_attains_inf[OF compact_Icc * contf] by auto show ?thesis proof (cases "d ∈ box a b ∨ c ∈ box a b") case True then show ?thesis by (metis c(2) d(2) box_subset_cbox subset_iff) next define e where "e = (a + b) /2" case False then have "f d = f c" using d c fab by auto with c d have "⋀x. x ∈ {a..b} ⟹ f x = f d" by force then show ?thesis by (rule_tac x=e in bexI) (auto simp: e_def ‹a < b›) qed qed then obtain x where x: "x ∈ {a <..< b}" "(∀y∈{a <..< b}. f x ≤ f y) ∨ (∀y∈{a <..< b}. f y ≤ f x)" by auto then have "f' x = (λv. 0)" apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"]) using assms apply auto done then show ?thesis by (metis x(1)) qed subsection ‹One-dimensional mean value theorem› lemma mvt: fixes f :: "real ⇒ real" assumes "a < b" and contf: "continuous_on {a..b} f" and derf: "⋀x. ⟦a < x; x < b⟧ ⟹ (f has_derivative f' x) (at x)" shows "∃x∈{a<..<b}. f b - f a = (f' x) (b - a)" proof - have "∃x∈{a <..< b}. (λxa. f' x xa - (f b - f a) / (b - a) * xa) = (λv. 0)" proof (intro Rolle[OF ‹a < b›, of "λx. f x - (f b - f a) / (b - a) * x"] ballI) fix x assume x: "a < x" "x < b" show "((λx. f x - (f b - f a) / (b - a) * x) has_derivative (λxa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)" by (intro derivative_intros derf[OF x]) qed (use assms in ‹auto intro!: continuous_intros simp: field_simps›) then obtain x where "x ∈ {a <..< b}" "(λxa. f' x xa - (f b - f a) / (b - a) * xa) = (λv. 0)" .. then show ?thesis by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0 zero_less_mult_iff nonzero_mult_div_cancel_right not_real_square_gt_zero times_divide_eq_left) qed lemma mvt_simple: fixes f :: "real ⇒ real" assumes "a < b" and derf: "⋀x. ⟦a ≤ x; x ≤ b⟧ ⟹ (f has_derivative f' x) (at x within {a..b})" shows "∃x∈{a<..<b}. f b - f a = f' x (b - a)" proof (rule mvt) have "f differentiable_on {a..b}" using derf unfolding differentiable_on_def differentiable_def by force then show "continuous_on {a..b} f" by (rule differentiable_imp_continuous_on) show "(f has_derivative f' x) (at x)" if "a < x" "x < b" for x by (metis at_within_Icc_at derf leI order.asym that) qed (rule assms) lemma mvt_very_simple: fixes f :: "real ⇒ real" assumes "a ≤ b" and derf: "⋀x. ⟦a ≤ x; x ≤ b⟧ ⟹ (f has_derivative f' x) (at x within {a..b})" shows "∃x∈{a..b}. f b - f a = f' x (b - a)" proof (cases "a = b") interpret bounded_linear "f' b" using assms(2) assms(1) by auto case True then show ?thesis by force next case False then show ?thesis using mvt_simple[OF _ derf] by (metis ‹a ≤ b› atLeastAtMost_iff dual_order.order_iff_strict greaterThanLessThan_iff) qed text ‹A nice generalization (see Havin's proof of 5.19 from Rudin's book).› lemma mvt_general: fixes f :: "real ⇒ 'a::real_inner" assumes "a < b" and contf: "continuous_on {a..b} f" and derf: "⋀x. ⟦a < x; x < b⟧ ⟹ (f has_derivative f' x) (at x)" shows "∃x∈{a<..<b}. norm (f b - f a) ≤ norm (f' x (b - a))" proof - have "∃x∈{a<..<b}. (f b - f a) ∙ f b - (f b - f a) ∙ f a = (f b - f a) ∙ f' x (b - a)" apply (rule mvt [OF ‹a < b›]) apply (intro continuous_intros contf) using derf apply (blast intro: has_derivative_inner_right) done then obtain x where x: "x ∈ {a<..<b}" "(f b - f a) ∙ f b - (f b - f a) ∙ f a = (f b - f a) ∙ f' x (b - a)" .. show ?thesis proof (cases "f a = f b") case False have "norm (f b - f a) * norm (f b - f a) = (norm (f b - f a))⇧^{2}" by (simp add: power2_eq_square) also have "… = (f b - f a) ∙ (f b - f a)" unfolding power2_norm_eq_inner .. also have "… = (f b - f a) ∙ f' x (b - a)" using x(2) by (simp only: inner_diff_right) also have "… ≤ norm (f b - f a) * norm (f' x (b - a))" by (rule norm_cauchy_schwarz) finally show ?thesis using False x(1) by (auto simp add: mult_left_cancel) next case True then show ?thesis using ‹a < b› by (rule_tac x="(a + b) /2" in bexI) auto qed qed subsection ‹More general bound theorems› proposition differentiable_bound_general: fixes f :: "real ⇒ 'a::real_normed_vector" assumes "a < b" and f_cont: "continuous_on {a..b} f" and phi_cont: "continuous_on {a..b} φ" and f': "⋀x. a < x ⟹ x < b ⟹ (f has_vector_derivative f' x) (at x)" and phi': "⋀x. a < x ⟹ x < b ⟹ (φ has_vector_derivative φ' x) (at x)" and bnd: "⋀x. a < x ⟹ x < b ⟹ norm (f' x) ≤ φ' x" shows "norm (f b - f a) ≤ φ b - φ a" proof - { fix x assume x: "a < x" "x < b" have "0 ≤ norm (f' x)" by simp also have "… ≤ φ' x" using x by (auto intro!: bnd) finally have "0 ≤ φ' x" . } note phi'_nonneg = this note f_tendsto = assms(2)[simplified continuous_on_def, rule_format] note phi_tendsto = assms(3)[simplified continuous_on_def, rule_format] { fix e::real assume "e > 0" define e2 where "e2 = e / 2" with ‹e > 0› have "e2 > 0" by simp let ?le = "λx1. norm (f x1 - f a) ≤ φ x1 - φ a + e * (x1 - a) + e" define A where "A = {x2. a ≤ x2 ∧ x2 ≤ b ∧ (∀x1∈{a ..< x2}. ?le x1)}" have A_subset: "A ⊆ {a..b}" by (auto simp: A_def) { fix x2 assume a: "a ≤ x2" "x2 ≤ b" and le: "∀x1∈{a..<x2}. ?le x1" have "?le x2" using ‹e > 0› proof cases assume "x2 ≠ a" with a have "a < x2" by simp have "at x2 within {a <..<x2}≠ bot" using ‹a < x2› by (auto simp: trivial_limit_within islimpt_in_closure) moreover have "((λx1. (φ x1 - φ a) + e * (x1 - a) + e) ⤏ (φ x2 - φ a) + e * (x2 - a) + e) (at x2 within {a <..<x2})" "((λx1. norm (f x1 - f a)) ⤏ norm (f x2 - f a)) (at x2 within {a <..<x2})" using a by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto intro: tendsto_within_subset[where S="{a..b}"]) moreover have "eventually (λx. x > a) (at x2 within {a <..<x2})" by (auto simp: eventually_at_filter) hence "eventually ?le (at x2 within {a <..<x2})" unfolding eventually_at_filter by eventually_elim (insert le, auto) ultimately show ?thesis by (rule tendsto_le) qed simp } note le_cont = this have "a ∈ A" using assms by (auto simp: A_def) hence [simp]: "A ≠ {}" by auto have A_ivl: "⋀x1 x2. x2 ∈ A ⟹ x1 ∈ {a ..x2} ⟹ x1 ∈ A" by (simp add: A_def) have [simp]: "bdd_above A" by (auto simp: A_def) define y where "y = Sup A" have "y ≤ b" unfolding y_def by (simp add: cSup_le_iff) (simp add: A_def) have leI: "⋀x x1. a ≤ x1 ⟹ x ∈ A ⟹ x1 < x ⟹ ?le x1" by (auto simp: A_def intro!: le_cont) have y_all_le: "∀x1∈{a..<y}. ?le x1" by (auto simp: y_def less_cSup_iff leI) have "a ≤ y" by (metis ‹a ∈ A› ‹bdd_above A› cSup_upper y_def) have "y ∈ A" using y_all_le ‹a ≤ y› ‹y ≤ b› by (auto simp: A_def) hence "A = {a .. y}" using A_subset by (auto simp: subset_iff y_def cSup_upper intro: A_ivl) from le_cont[OF ‹a ≤ y› ‹y ≤ b› y_all_le] have le_y: "?le y" . have "y = b" proof (cases "a = y") case True with ‹a < b› have "y < b" by simp with ‹a = y› f_cont phi_cont ‹e2 > 0› have 1: "∀⇩_{F}x in at y within {y..b}. dist (f x) (f y) < e2" and 2: "∀⇩_{F}x in at y within {y..b}. dist (φ x) (φ y) < e2" by (auto simp: continuous_on_def tendsto_iff) have 3: "eventually (λx. y < x) (at y within {y..b})" by (auto simp: eventually_at_filter) have 4: "eventually (λx::real. x < b) (at y within {y..b})" using _ ‹y < b› by (rule order_tendstoD) (auto intro!: tendsto_eq_intros) from 1 2 3 4 have eventually_le: "eventually (λx. ?le x) (at y within {y .. b})" proof eventually_elim case (elim x1) have "norm (f x1 - f a) = norm (f x1 - f y)" by (simp add: ‹a = y›) also have "norm (f x1 - f y) ≤ e2" using elim ‹a = y› by (auto simp : dist_norm intro!: less_imp_le) also have "… ≤ e2 + (φ x1 - φ a + e2 + e * (x1 - a))" using ‹0 < e› elim by (intro add_increasing2[OF add_nonneg_nonneg order.refl]) (auto simp: ‹a = y› dist_norm intro!: mult_nonneg_nonneg) also have "… = φ x1 - φ a + e * (x1 - a) + e" by (simp add: e2_def) finally show "?le x1" . qed from this[unfolded eventually_at_topological] ‹?le y› obtain S where S: "open S" "y ∈ S" "⋀x. x∈S ⟹ x ∈ {y..b} ⟹ ?le x" by metis from ‹open S› obtain d where d: "⋀x. dist x y < d ⟹ x ∈ S" "d > 0" by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ ‹y ∈ S›]) define d' where "d' = min b (y + (d/2))" have "d' ∈ A" unfolding A_def proof safe show "a ≤ d'" using ‹a = y› ‹0 < d› ‹y < b› by (simp add: d'_def) show "d' ≤ b" by (simp add: d'_def) fix x1 assume "x1 ∈ {a..<d'}" hence "x1 ∈ S" "x1 ∈ {y..b}" by (auto simp: ‹a = y› d'_def dist_real_def intro!: d ) thus "?le x1" by (rule S) qed hence "d' ≤ y" unfolding y_def by (rule cSup_upper) simp then show "y = b" using ‹d > 0› ‹y < b› by (simp add: d'_def) next case False with ‹a ≤ y› have "a < y" by simp show "y = b" proof (rule ccontr) assume "y ≠ b" hence "y < b" using ‹y ≤ b› by simp let ?F = "at y within {y..<b}" from f' phi' have "(f has_vector_derivative f' y) ?F" and "(φ has_vector_derivative φ' y) ?F" using ‹a < y› ‹y < b› by (auto simp add: at_within_open[of _ "{a<..<b}"] has_vector_derivative_def intro!: has_derivative_subset[where s="{a<..<b}" and t="{y..<b}"]) hence "∀⇩_{F}x1 in ?F. norm (f x1 - f y - (x1 - y) *⇩_{R}f' y) ≤ e2 * ¦x1 - y¦" "∀⇩_{F}x1 in ?F. norm (φ x1 - φ y - (x1 - y) *⇩_{R}φ' y) ≤ e2 * ¦x1 - y¦" using ‹e2 > 0› by (auto simp: has_derivative_within_alt2 has_vector_derivative_def) moreover have "∀⇩_{F}x1 in ?F. y ≤ x1" "∀⇩_{F}x1 in ?F. x1 < b" by (auto simp: eventually_at_filter) ultimately have "∀⇩_{F}x1 in ?F. norm (f x1 - f y) ≤ (φ x1 - φ y) + e * ¦x1 - y¦" (is "∀⇩_{F}x1 in ?F. ?le' x1") proof eventually_elim case (elim x1) from norm_triangle_ineq2[THEN order_trans, OF elim(1)] have "norm (f x1 - f y) ≤ norm (f' y) * ¦x1 - y¦ + e2 * ¦x1 - y¦" by (simp add: ac_simps) also have "norm (f' y) ≤ φ' y" using bnd ‹a < y› ‹y < b› by simp also have "φ' y * ¦x1 - y¦ ≤ φ x1 - φ y + e2 * ¦x1 - y¦" using elim by (simp add: ac_simps) finally have "norm (f x1 - f y) ≤ φ x1 - φ y + e2 * ¦x1 - y¦ + e2 * ¦x1 - y¦" by (auto simp: mult_right_mono) thus ?case by (simp add: e2_def) qed moreover have "?le' y" by simp ultimately obtain S where S: "open S" "y ∈ S" "⋀x. x∈S ⟹ x ∈ {y..<b} ⟹ ?le' x" unfolding eventually_at_topological by metis from ‹open S› obtain d where d: "⋀x. dist x y < d ⟹ x ∈ S" "d > 0" by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ ‹y ∈ S›]) define d' where "d' = min ((y + b)/2) (y + (d/2))" have "d' ∈ A" unfolding A_def proof safe show "a ≤ d'" using ‹a < y› ‹0 < d› ‹y < b› by (simp add: d'_def) show "d' ≤ b" using ‹y < b› by (simp add: d'_def min_def) fix x1 assume x1: "x1 ∈ {a..<d'}" show "?le x1" proof (cases "x1 < y") case True then show ?thesis using ‹y ∈ A› local.leI x1 by auto next case False hence x1': "x1 ∈ S" "x1 ∈ {y..<b}" using x1 by (auto simp: d'_def dist_real_def intro!: d) have "norm (f x1 - f a) ≤ norm (f x1 - f y) + norm (f y - f a)" by (rule order_trans[OF _ norm_triangle_ineq]) simp also note S(3)[OF x1'] also note le_y finally show "?le x1" using False by (auto simp: algebra_simps) qed qed hence "d' ≤ y" unfolding y_def by (rule cSup_upper) simp thus False using ‹d > 0› ‹y < b› by (simp add: d'_def min_def split: if_split_asm) qed qed with le_y have "norm (f b - f a) ≤ φ b - φ a + e * (b - a + 1)" by (simp add: algebra_simps) } note * = this show ?thesis proof (rule field_le_epsilon) fix e::real assume "e > 0" then show "norm (f b - f a) ≤ φ b - φ a + e" using *[of "e / (b - a + 1)"] ‹a < b› by simp qed qed lemma differentiable_bound: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "convex S" and derf: "⋀x. x∈S ⟹ (f has_derivative f' x) (at x within S)" and B: "⋀x. x ∈ S ⟹ onorm (f' x) ≤ B" and x: "x ∈ S" and y: "y ∈ S" shows "norm (f x - f y) ≤ B * norm (x - y)" proof - let ?p = "λu. x + u *⇩_{R}(y - x)" let ?φ = "λh. h * B * norm (x - y)" have *: "x + u *⇩_{R}(y - x) ∈ S" if "u ∈ {0..1}" for u proof - have "u *⇩_{R}y = u *⇩_{R}(y - x) + u *⇩_{R}x" by (simp add: scale_right_diff_distrib) then show "x + u *⇩_{R}(y - x) ∈ S" using that ‹convex S› unfolding convex_alt by (metis (no_types) atLeastAtMost_iff linordered_field_class.sign_simps(2) pth_c(3) scaleR_collapse x y) qed have "⋀z. z ∈ (λu. x + u *⇩_{R}(y - x)) ` {0..1} ⟹ (f has_derivative f' z) (at z within (λu. x + u *⇩_{R}(y - x)) ` {0..1})" by (auto intro: * has_derivative_within_subset [OF derf]) then have "continuous_on (?p ` {0..1}) f" unfolding continuous_on_eq_continuous_within by (meson has_derivative_continuous) with * have 1: "continuous_on {0 .. 1} (f ∘ ?p)" by (intro continuous_intros)+ { fix u::real assume u: "u ∈{0 <..< 1}" let ?u = "?p u" interpret linear "(f' ?u)" using u by (auto intro!: has_derivative_linear derf *) have "(f ∘ ?p has_derivative (f' ?u) ∘ (λu. 0 + u *⇩_{R}(y - x))) (at u within box 0 1)" by (intro derivative_intros has_derivative_within_subset [OF derf]) (use u * in auto) hence "((f ∘ ?p) has_vector_derivative f' ?u (y - x)) (at u)" by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan] scaleR has_vector_derivative_def o_def) } note 2 = this have 3: "continuous_on {0..1} ?φ" by (rule continuous_intros)+ have 4: "(?φ has_vector_derivative B * norm (x - y)) (at u)" for u by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros) { fix u::real assume u: "u ∈{0 <..< 1}" let ?u = "?p u" interpret bounded_linear "(f' ?u)" using u by (auto intro!: has_derivative_bounded_linear derf *) have "norm (f' ?u (y - x)) ≤ onorm (f' ?u) * norm (y - x)" by (rule onorm) (rule bounded_linear) also have "onorm (f' ?u) ≤ B" using u by (auto intro!: assms(3)[rule_format] *) finally have "norm ((f' ?u) (y - x)) ≤ B * norm (x - y)" by (simp add: mult_right_mono norm_minus_commute) } note 5 = this have "norm (f x - f y) = norm ((f ∘ (λu. x + u *⇩_{R}(y - x))) 1 - (f ∘ (λu. x + u *⇩_{R}(y - x))) 0)" by (auto simp add: norm_minus_commute) also from differentiable_bound_general[OF zero_less_one 1, OF 3 2 4 5] have "norm ((f ∘ ?p) 1 - (f ∘ ?p) 0) ≤ B * norm (x - y)" by simp finally show ?thesis . qed lemma differentiable_bound_segment: fixes f::"'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "⋀t. t ∈ {0..1} ⟹ x0 + t *⇩_{R}a ∈ G" assumes f': "⋀x. x ∈ G ⟹ (f has_derivative f' x) (at x within G)" assumes B: "⋀x. x ∈ {0..1} ⟹ onorm (f' (x0 + x *⇩_{R}a)) ≤ B" shows "norm (f (x0 + a) - f x0) ≤ norm a * B" proof - let ?G = "(λx. x0 + x *⇩_{R}a) ` {0..1}" have "?G = (+) x0 ` (λx. x *⇩_{R}a) ` {0..1}" by auto also have "convex …" by (intro convex_translation convex_scaled convex_real_interval) finally have "convex ?G" . moreover have "?G ⊆ G" "x0 ∈ ?G" "x0 + a ∈ ?G" using assms by (auto intro: image_eqI[where x=1]) ultimately show ?thesis using has_derivative_subset[OF f' ‹?G ⊆ G›] B differentiable_bound[of "(λx. x0 + x *⇩_{R}a) ` {0..1}" f f' B "x0 + a" x0] by (force simp: ac_simps) qed lemma differentiable_bound_linearization: fixes f::"'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes S: "⋀t. t ∈ {0..1} ⟹ a + t *⇩_{R}(b - a) ∈ S" assumes f'[derivative_intros]: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)" assumes B: "⋀x. x ∈ S ⟹ onorm (f' x - f' x0) ≤ B" assumes "x0 ∈ S" shows "norm (f b - f a - f' x0 (b - a)) ≤ norm (b - a) * B" proof - define g where [abs_def]: "g x = f x - f' x0 x" for x have g: "⋀x. x ∈ S ⟹ (g has_derivative (λi. f' x i - f' x0 i)) (at x within S)" unfolding g_def using assms by (auto intro!: derivative_eq_intros bounded_linear.has_derivative[OF has_derivative_bounded_linear, OF f']) from B have "∀x∈{0..1}. onorm (λi. f' (a + x *⇩_{R}(b - a)) i - f' x0 i) ≤ B" using assms by (auto simp: fun_diff_def) with differentiable_bound_segment[OF S g] ‹x0 ∈ S› show ?thesis by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']]) qed lemma vector_differentiable_bound_linearization: fixes f::"real ⇒ 'b::real_normed_vector" assumes f': "⋀x. x ∈ S ⟹ (f has_vector_derivative f' x) (at x within S)" assumes "closed_segment a b ⊆ S" assumes B: "⋀x. x ∈ S ⟹ norm (f' x - f' x0) ≤ B" assumes "x0 ∈ S" shows "norm (f b - f a - (b - a) *⇩_{R}f' x0) ≤ norm (b - a) * B" using assms by (intro differentiable_bound_linearization[of a b S f "λx h. h *⇩_{R}f' x" x0 B]) (force simp: closed_segment_real_eq has_vector_derivative_def scaleR_diff_right[symmetric] mult.commute[of B] intro!: onorm_le mult_left_mono)+ text ‹In particular.› lemma has_derivative_zero_constant: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "convex s" and "⋀x. x ∈ s ⟹ (f has_derivative (λh. 0)) (at x within s)" shows "∃c. ∀x∈s. f x = c" proof - { fix x y assume "x ∈ s" "y ∈ s" then have "norm (f x - f y) ≤ 0 * norm (x - y)" using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero) then have "f x = f y" by simp } then show ?thesis by metis qed lemma has_field_derivative_zero_constant: assumes "convex s" "⋀x. x ∈ s ⟹ (f has_field_derivative 0) (at x within s)" shows "∃c. ∀x∈s. f (x) = (c :: 'a :: real_normed_field)" proof (rule has_derivative_zero_constant) have A: "( * ) 0 = (λ_. 0 :: 'a)" by (intro ext) simp fix x assume "x ∈ s" thus "(f has_derivative (λh. 0)) (at x within s)" using assms(2)[of x] by (simp add: has_field_derivative_def A) qed fact lemma has_vector_derivative_zero_constant: assumes "convex s" assumes "⋀x. x ∈ s ⟹ (f has_vector_derivative 0) (at x within s)" obtains c where "⋀x. x ∈ s ⟹ f x = c" using has_derivative_zero_constant[of s f] assms by (auto simp: has_vector_derivative_def) lemma has_derivative_zero_unique: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "convex s" and "⋀x. x ∈ s ⟹ (f has_derivative (λh. 0)) (at x within s)" and "x ∈ s" "y ∈ s" shows "f x = f y" using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force lemma has_derivative_zero_unique_connected: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "open s" "connected s" assumes f: "⋀x. x ∈ s ⟹ (f has_derivative (λx. 0)) (at x)" assumes "x ∈ s" "y ∈ s" shows "f x = f y" proof (rule connected_local_const[where f=f, OF ‹connected s› ‹x∈s› ‹y∈s›]) show "∀a∈s. eventually (λb. f a = f b) (at a within s)" proof fix a assume "a ∈ s" with ‹open s› obtain e where "0 < e" "ball a e ⊆ s" by (rule openE) then have "∃c. ∀x∈ball a e. f x = c" by (intro has_derivative_zero_constant) (auto simp: at_within_open[OF _ open_ball] f convex_ball) with ‹0<e› have "∀x∈ball a e. f a = f x" by auto then show "eventually (λb. f a = f b) (at a within s)" using ‹0<e› unfolding eventually_at_topological by (intro exI[of _ "ball a e"]) auto qed qed subsection ‹Differentiability of inverse function (most basic form)› lemma has_derivative_inverse_basic: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes derf: "(f has_derivative f') (at (g y))" and ling': "bounded_linear g'" and "g' ∘ f' = id" and contg: "continuous (at y) g" and "open T" and "y ∈ T" and fg: "⋀z. z ∈ T ⟹ f (g z) = z" shows "(g has_derivative g') (at y)" proof - interpret f': bounded_linear f' using assms unfolding has_derivative_def by auto interpret g': bounded_linear g' using assms by auto obtain C where C: "0 < C" "⋀x. norm (g' x) ≤ norm x * C" using bounded_linear.pos_bounded[OF assms(2)] by blast have lem1: "∀e>0. ∃d>0. ∀z. norm (z - y) < d ⟶ norm (g z - g y - g'(z - y)) ≤ e * norm (g z - g y)" proof (intro allI impI) fix e :: real assume "e > 0" with C(1) have *: "e / C > 0" by auto obtain d0 where "0 < d0" and d0: "⋀u. norm (u - g y) < d0 ⟹ norm (f u - f (g y) - f' (u - g y)) ≤ e / C * norm (u - g y)" using derf * unfolding has_derivative_at_alt by blast obtain d1 where "0 < d1" and d1: "⋀x. ⟦0 < dist x y; dist x y < d1⟧ ⟹ dist (g x) (g y) < d0" using contg ‹0 < d0› unfolding continuous_at Lim_at by blast obtain d2 where "0 < d2" and d2: "⋀u. dist u y < d2 ⟹ u ∈ T" using ‹open T› ‹y ∈ T› unfolding open_dist by blast obtain d where d: "0 < d" "d < d1" "d < d2" using field_lbound_gt_zero[OF ‹0 < d1› ‹0 < d2›] by blast show "∃d>0. ∀z. norm (z - y) < d ⟶ norm (g z - g y - g' (z - y)) ≤ e * norm (g z - g y)" proof (intro exI allI impI conjI) fix z assume as: "norm (z - y) < d" then have "z ∈ T" using d2 d unfolding dist_norm by auto have "norm (g z - g y - g' (z - y)) ≤ norm (g' (f (g z) - y - f' (g z - g y)))" unfolding g'.diff f'.diff unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] fg[OF ‹z∈T›] by (simp add: norm_minus_commute) also have "… ≤ norm (f (g z) - y - f' (g z - g y)) * C" by (rule C(2)) also have "… ≤ (e / C) * norm (g z - g y) * C" proof - have "norm (g z - g y) < d0" by (metis as cancel_comm_monoid_add_class.diff_cancel d(2) ‹0 < d0› d1 diff_gt_0_iff_gt diff_strict_mono dist_norm dist_self zero_less_dist_iff) then show ?thesis by (metis C(1) ‹y ∈ T› d0 fg real_mult_le_cancel_iff1) qed also have "… ≤ e * norm (g z - g y)" using C by (auto simp add: field_simps) finally show "norm (g z - g y - g' (z - y)) ≤ e * norm (g z - g y)" by simp qed (use d in auto) qed have *: "(0::real) < 1 / 2" by auto obtain d where "0 < d" and d: "⋀z. norm (z - y) < d ⟹ norm (g z - g y - g' (z - y)) ≤ 1/2 * norm (g z - g y)" using lem1 * by blast define B where "B = C * 2" have "B > 0" unfolding B_def using C by auto have lem2: "norm (g z - g y) ≤ B * norm (z - y)" if z: "norm(z - y) < d" for z proof - have "norm (g z - g y) ≤ norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))" by (rule norm_triangle_sub) also have "… ≤ norm (g' (z - y)) + 1 / 2 * norm (g z - g y)" by (rule add_left_mono) (use d z in auto) also have "… ≤ norm (z - y) * C + 1 / 2 * norm (g z - g y)" by (rule add_right_mono) (use C in auto) finally show "norm (g z - g y) ≤ B * norm (z - y)" unfolding B_def by (auto simp add: field_simps) qed show ?thesis unfolding has_derivative_at_alt proof (intro conjI assms allI impI) fix e :: real assume "e > 0" then have *: "e / B > 0" by (metis ‹B > 0› divide_pos_pos) obtain d' where "0 < d'" and d': "⋀z. norm (z - y) < d' ⟹ norm (g z - g y - g' (z - y)) ≤ e / B * norm (g z - g y)" using lem1 * by blast obtain k where k: "0 < k" "k < d" "k < d'" using field_lbound_gt_zero[OF ‹0 < d› ‹0 < d'›] by blast show "∃d>0. ∀ya. norm (ya - y) < d ⟶ norm (g ya - g y - g' (ya - y)) ≤ e * norm (ya - y)" proof (intro exI allI impI conjI) fix z assume as: "norm (z - y) < k" then have "norm (g z - g y - g' (z - y)) ≤ e / B * norm(g z - g y)" using d' k by auto also have "… ≤ e * norm (z - y)" unfolding times_divide_eq_left pos_divide_le_eq[OF ‹B>0›] using lem2[of z] k as ‹e > 0› by (auto simp add: field_simps) finally show "norm (g z - g y - g' (z - y)) ≤ e * norm (z - y)" by simp qed (use k in auto) qed qed text ‹Simply rewrite that based on the domain point x.› lemma has_derivative_inverse_basic_x: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "(f has_derivative f') (at x)" and "bounded_linear g'" and "g' ∘ f' = id" and "continuous (at (f x)) g" and "g (f x) = x" and "open T" and "f x ∈ T" and "⋀y. y ∈ T ⟹ f (g y) = y" shows "(g has_derivative g') (at (f x))" by (rule has_derivative_inverse_basic) (use assms in auto) text ‹This is the version in Dieudonne', assuming continuity of f and g.› lemma has_derivative_inverse_dieudonne: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "open S" and "open (f ` S)" and "continuous_on S f" and "continuous_on (f ` S) g" and "⋀x. x ∈ S ⟹ g (f x) = x" and "x ∈ S" and "(f has_derivative f') (at x)" and "bounded_linear g'" and "g' ∘ f' = id" shows "(g has_derivative g') (at (f x))" apply (rule has_derivative_inverse_basic_x[OF assms(7-9) _ _ assms(2)]) using assms(3-6) unfolding continuous_on_eq_continuous_at[OF assms(1)] continuous_on_eq_continuous_at[OF assms(2)] apply auto done text ‹Here's the simplest way of not assuming much about g.› lemma has_derivative_inverse: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "compact S" and "x ∈ S" and fx: "f x ∈ interior (f ` S)" and "continuous_on S f" and gf: "⋀y. y ∈ S ⟹ g (f y) = y" and "(f has_derivative f') (at x)" and "bounded_linear g'" and "g' ∘ f' = id" shows "(g has_derivative g') (at (f x))" proof - have *: "⋀y. y ∈ interior (f ` S) ⟹ f (g y) = y" by (metis gf image_iff interior_subset subsetCE) show ?thesis apply (rule has_derivative_inverse_basic_x[OF assms(6-8), where T = "interior (f ` S)"]) apply (rule continuous_on_interior[OF _ fx]) apply (rule continuous_on_inv) apply (simp_all add: assms *) done qed subsection ‹Proving surjectivity via Brouwer fixpoint theorem› lemma brouwer_surjective: fixes f :: "'n::euclidean_space ⇒ 'n" assumes "compact T" and "convex T" and "T ≠ {}" and "continuous_on T f" and "⋀x y. ⟦x∈S; y∈T⟧ ⟹ x + (y - f y) ∈ T" and "x ∈ S" shows "∃y∈T. f y = x" proof - have *: "⋀x y. f y = x ⟷ x + (y - f y) = y" by (auto simp add: algebra_simps) show ?thesis unfolding * apply (rule brouwer[OF assms(1-3), of "λy. x + (y - f y)"]) apply (intro continuous_intros) using assms apply auto done qed lemma brouwer_surjective_cball: fixes f :: "'n::euclidean_space ⇒ 'n" assumes "continuous_on (cball a e) f" and "e > 0" and "x ∈ S" and "⋀x y. ⟦x∈S; y∈cball a e⟧ ⟹ x + (y - f y) ∈ cball a e" shows "∃y∈cball a e. f y = x" apply (rule brouwer_surjective) apply (rule compact_cball convex_cball)+ unfolding cball_eq_empty using assms apply auto done text ‹See Sussmann: "Multidifferential calculus", Theorem 2.1.1› lemma sussmann_open_mapping: fixes f :: "'a::real_normed_vector ⇒ 'b::euclidean_space" assumes "open S" and contf: "continuous_on S f" and "x ∈ S" and derf: "(f has_derivative f') (at x)" and "bounded_linear g'" "f' ∘ g' = id" and "T ⊆ S" and x: "x ∈ interior T" shows "f x ∈ interior (f ` T)" proof - interpret f': bounded_linear f' using assms unfolding has_derivative_def by auto interpret g': bounded_linear g' using assms by auto obtain B where B: "0 < B" "∀x. norm (g' x) ≤ norm x * B" using bounded_linear.pos_bounded[OF assms(5)] by blast hence *: "1 / (2 * B) > 0" by auto obtain e0 where e0: "0 < e0" "∀y. norm (y - x) < e0 ⟶ norm (f y - f x - f' (y - x)) ≤ 1 / (2 * B) * norm (y - x)" using derf unfolding has_derivative_at_alt using * by blast obtain e1 where e1: "0 < e1" "cball x e1 ⊆ T" using mem_interior_cball x by blast have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B" using field_lbound_gt_zero[OF *] by blast have lem: "∃y∈cball (f x) e. f (x + g' (y - f x)) = z" if "z∈cball (f x) (e / 2)" for z proof (rule brouwer_surjective_cball) have z: "z ∈ S" if as: "y ∈cball (f x) e" "z = x + (g' y - g' (f x))" for y z proof- have "dist x z = norm (g' (f x) - g' y)" unfolding as(2) and dist_norm by auto also have "… ≤ norm (f x - y) * B" by (metis B(2) g'.diff) also have "… ≤ e * B" by (metis B(1) dist_norm mem_cball real_mult_le_cancel_iff1 that(1)) also have "… ≤ e1" using B(1) e(3) pos_less_divide_eq by fastforce finally have "z ∈ cball x e1" by force then show "z ∈ S" using e1 assms(7) by auto qed show "continuous_on (cball (f x) e) (λy. f (x + g' (y - f x)))" unfolding g'.diff proof (rule continuous_on_compose2 [OF _ _ order_refl, of _ _ f]) show "continuous_on ((λy. x + (g' y - g' (f x))) ` cball (f x) e) f" by (rule continuous_on_subset[OF contf]) (use z in blast) show "continuous_on (cball (f x) e) (λy. x + (g' y - g' (f x)))" by (intro continuous_intros linear_continuous_on[OF ‹bounded_linear g'›]) qed next fix y z assume y: "y ∈ cball (f x) (e / 2)" and z: "z ∈ cball (f x) e" have "norm (g' (z - f x)) ≤ norm (z - f x) * B" using B by auto also have "… ≤ e * B" by (metis B(1) z dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1) also have "… < e0" using B(1) e(2) pos_less_divide_eq by blast finally have *: "norm (x + g' (z - f x) - x) < e0" by auto have **: "f x + f' (x + g' (z - f x) - x) = z" using assms(6)[unfolded o_def id_def,THEN cong] by auto have "norm (f x - (y + (z - f (x + g' (z - f x))))) ≤ norm (f (x + g' (z - f x)) - z) + norm (f x - y)" using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by (auto simp add: algebra_simps) also have "… ≤ 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0(2)[rule_format, OF *] by (simp only: algebra_simps **) auto also have "… ≤ 1 / (B * 2) * norm (g' (z - f x)) + e/2" using y by (auto simp: dist_norm) also have "… ≤ 1 / (B * 2) * B * norm (z - f x) + e/2" using * B by (auto simp add: field_simps) also have "… ≤ 1 / 2 * norm (z - f x) + e/2" by auto also have "… ≤ e/2 + e/2" using B(1) ‹norm (z - f x) * B ≤ e * B› by auto finally show "y + (z - f (x + g' (z - f x))) ∈ cball (f x) e" by (auto simp: dist_norm) qed (use e that in auto) show ?thesis unfolding mem_interior proof (intro exI conjI subsetI) fix y assume "y ∈ ball (f x) (e / 2)" then have *: "y ∈ cball (f x) (e / 2)" by auto obtain z where z: "z ∈ cball (f x) e" "f (x + g' (z - f x)) = y" using lem * by blast then have "norm (g' (z - f x)) ≤ norm (z - f x) * B" using B by (auto simp add: field_simps) also have "… ≤ e * B" by (metis B(1) dist_norm mem_cball norm_minus_commute real_mult_le_cancel_iff1 z(1)) also have "… ≤ e1" using e B unfolding less_divide_eq by auto finally have "x + g'(z - f x) ∈ T" by (metis add_diff_cancel diff_diff_add dist_norm e1(2) mem_cball norm_minus_commute subset_eq) then show "y ∈ f ` T" using z by auto qed (use e in auto) qed text ‹Hence the following eccentric variant of the inverse function theorem. This has no continuity assumptions, but we do need the inverse function. We could put ‹f' ∘ g = I› but this happens to fit with the minimal linear algebra theory I've set up so far.› lemma has_derivative_inverse_strong: fixes f :: "'n::euclidean_space ⇒ 'n" assumes "open S" and "x ∈ S" and contf: "continuous_on S f" and gf: "⋀x. x ∈ S ⟹ g (f x) = x" and derf: "(f has_derivative f') (at x)" and id: "f' ∘ g' = id" shows "(g has_derivative g') (at (f x))" proof - have linf: "bounded_linear f'" using derf unfolding has_derivative_def by auto then have ling: "bounded_linear g'" unfolding linear_conv_bounded_linear[symmetric] using id right_inverse_linear by blast moreover have "g' ∘ f' = id" using id linf ling unfolding linear_conv_bounded_linear[symmetric] using linear_inverse_left by auto moreover have *: "⋀T. ⟦T ⊆ S; x ∈ interior T⟧ ⟹ f x ∈ interior (f ` T)" apply (rule sussmann_open_mapping) apply (rule assms ling)+ apply auto done have "continuous (at (f x)) g" unfolding continuous_at Lim_at proof (rule, rule) fix e :: real assume "e > 0" then have "f x ∈ interior (f ` (ball x e ∩ S))" using *[rule_format,of "ball x e ∩ S"] ‹x ∈ S› by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)]) then obtain d where d: "0 < d" "ball (f x) d ⊆ f ` (ball x e ∩ S)" unfolding mem_interior by blast show "∃d>0. ∀y. 0 < dist y (f x) ∧ dist y (f x) < d ⟶ dist (g y) (g (f x)) < e" proof (intro exI allI impI conjI) fix y assume "0 < dist y (f x) ∧ dist y (f x) < d" then have "g y ∈ g ` f ` (ball x e ∩ S)" by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff) then show "dist (g y) (g (f x)) < e" using gf[OF ‹x ∈ S›] by (simp add: assms(4) dist_commute image_iff) qed (use d in auto) qed moreover have "f x ∈ interior (f ` S)" apply (rule sussmann_open_mapping) apply (rule assms ling)+ using interior_open[OF assms(1)] and ‹x ∈ S› apply auto done moreover have "f (g y) = y" if "y ∈ interior (f ` S)" for y by (metis gf imageE interiorE set_mp that) ultimately show ?thesis using assms by (metis has_derivative_inverse_basic_x open_interior) qed text ‹A rewrite based on the other domain.› lemma has_derivative_inverse_strong_x: fixes f :: "'a::euclidean_space ⇒ 'a" assumes "open S" and "g y ∈ S" and "continuous_on S f" and "⋀x. x ∈ S ⟹ g (f x) = x" and "(f has_derivative f') (at (g y))" and "f' ∘ g' = id" and "f (g y) = y" shows "(g has_derivative g') (at y)" using has_derivative_inverse_strong[OF assms(1-6)] unfolding assms(7) by simp text ‹On a region.› lemma has_derivative_inverse_on: fixes f :: "'n::euclidean_space ⇒ 'n" assumes "open S" and derf: "⋀x. x ∈ S ⟹ (f has_derivative f'(x)) (at x)" and "⋀x. x ∈ S ⟹ g (f x) = x" and "f' x ∘ g' x = id" and "x ∈ S" shows "(g has_derivative g'(x)) (at (f x))" proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f]) show "continuous_on S f" unfolding continuous_on_eq_continuous_at[OF ‹open S›] using derf has_derivative_continuous by blast qed (use assms in auto) text ‹Invertible derivative continous at a point implies local injectivity. It's only for this we need continuity of the derivative, except of course if we want the fact that the inverse derivative is also continuous. So if we know for some other reason that the inverse function exists, it's OK.› proposition has_derivative_locally_injective: fixes f :: "'n::euclidean_space ⇒ 'm::euclidean_space" assumes "a ∈ S" and "open S" and bling: "bounded_linear g'" and "g' ∘ f' a = id" and derf: "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x)" and "⋀e. e > 0 ⟹ ∃d>0. ∀x. dist a x < d ⟶ onorm (λv. f' x v - f' a v) < e" obtains r where "r > 0" "ball a r ⊆ S" "inj_on f (ball a r)" proof - interpret bounded_linear g' using assms by auto note f'g' = assms(4)[unfolded id_def o_def,THEN cong] have "g' (f' a (∑Basis)) = (∑Basis)" "(∑Basis) ≠ (0::'n)" using f'g' by auto then have *: "0 < onorm g'" unfolding onorm_pos_lt[OF assms(3)] by fastforce define k where "k = 1 / onorm g' / 2" have *: "k > 0" unfolding k_def using * by auto obtain d1 where d1: "0 < d1" "⋀x. dist a x < d1 ⟹ onorm (λv. f' x v - f' a v) < k" using assms(6) * by blast from ‹open S› obtain d2 where "d2 > 0" "ball a d2 ⊆ S" using ‹a∈S› .. obtain d2 where d2: "0 < d2" "ball a d2 ⊆ S" using ‹0 < d2› ‹ball a d2 ⊆ S› by blast obtain d where d: "0 < d" "d < d1" "d < d2" using field_lbound_gt_zero[OF d1(1) d2(1)] by blast show ?thesis proof show "0 < d" by (fact d) show "ball a d ⊆ S" using ‹d < d2› ‹ball a d2 ⊆ S› by auto show "inj_on f (ball a d)" unfolding inj_on_def proof (intro strip) fix x y assume as: "x ∈ ball a d" "y ∈ ball a d" "f x = f y" define ph where [abs_def]: "ph w = w - g' (f w - f x)" for w have ph':"ph = g' ∘ (λw. f' a w - (f w - f x))" unfolding ph_def o_def by (simp add: diff f'g') have "norm (ph x - ph y) ≤ (1 / 2) * norm (x - y)" proof (rule differentiable_bound[OF convex_ball _ _ as(1-2)]) fix u assume u: "u ∈ ball a d" then have "u ∈ S" using d d2 by auto have *: "(λv. v - g' (f' u v)) = g' ∘ (λw. f' a w - f' u w)" unfolding o_def and diff using f'g' by auto have blin: "bounded_linear (f' a)" using ‹a ∈ S› derf by blast show "(ph has_derivative (λv. v - g' (f' u v))) (at u within ball a d)" unfolding ph' * comp_def by (rule ‹u ∈ S› derivative_eq_intros has_derivative_at_withinI [OF derf] bounded_linear.has_derivative [OF blin] bounded_linear.has_derivative [OF bling] |simp)+ have **: "bounded_linear (λx. f' u x - f' a x)" "bounded_linear (λx. f' a x - f' u x)" using ‹u ∈ S› blin bounded_linear_sub derf by auto then have "onorm (λv. v - g' (f' u v)) ≤ onorm g' * onorm (λw. f' a w - f' u w)" by (simp add: "*" bounded_linear_axioms onorm_compose) also have "… ≤ onorm g' * k" apply (rule mult_left_mono) using d1(2)[of u] using onorm_neg[where f="λx. f' u x - f' a x"] d u onorm_pos_le[OF bling] apply (auto simp: algebra_simps) done also have "… ≤ 1 / 2" unfolding k_def by auto finally show "onorm (λv. v - g' (f' u v)) ≤ 1 / 2" . qed moreover have "norm (ph y - ph x) = norm (y - x)" by (simp add: as(3) ph_def) ultimately show "x = y" unfolding norm_minus_commute by auto qed qed qed subsection ‹Uniformly convergent sequence of derivatives› lemma has_derivative_sequence_lipschitz_lemma: fixes f :: "nat ⇒ 'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "convex S" and derf: "⋀n x. x ∈ S ⟹ ((f n) has_derivative (f' n x)) (at x within S)" and nle: "⋀n x h. ⟦n≥N; x ∈ S⟧ ⟹ norm (f' n x h - g' x h) ≤ e * norm h" and "0 ≤ e" shows "∀m≥N. ∀n≥N. ∀x∈S. ∀y∈S. norm ((f m x - f n x) - (f m y - f n y)) ≤ 2 * e * norm (x - y)" proof clarify fix m n x y assume as: "N ≤ m" "N ≤ n" "x ∈ S" "y ∈ S" show "norm ((f m x - f n x) - (f m y - f n y)) ≤ 2 * e * norm (x - y)" proof (rule differentiable_bound[where f'="λx h. f' m x h - f' n x h", OF ‹convex S› _ _ as(3-4)]) fix x assume "x ∈ S" show "((λa. f m a - f n a) has_derivative (λh. f' m x h - f' n x h)) (at x within S)" by (rule derivative_intros derf ‹x∈S›)+ show "onorm (λh. f' m x h - f' n x h) ≤ 2 * e" proof (rule onorm_bound) fix h have "norm (f' m x h - f' n x h) ≤ norm (f' m x h - g' x h) + norm (f' n x h - g' x h)" using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] by (auto simp add: algebra_simps norm_minus_commute) also have "… ≤ e * norm h + e * norm h" using nle[OF ‹N ≤ m› ‹x ∈ S›, of h] nle[OF ‹N ≤ n› ‹x ∈ S›, of h] by (auto simp add: field_simps) finally show "norm (f' m x h - f' n x h) ≤ 2 * e * norm h" by auto qed (simp add: ‹0 ≤ e›) qed qed lemma has_derivative_sequence_Lipschitz: fixes f :: "nat ⇒ 'a::real_normed_vector ⇒ 'b::real_normed_vector" assumes "convex S" and "⋀n x. x ∈ S ⟹ ((f n) has_derivative (f' n x)) (at x within S)" and nle: "⋀e. e > 0 ⟹ ∀⇩_{F}n in sequentially. ∀x∈S. ∀h. norm (f' n x h - g' x h) ≤ e * norm h" and "e > 0" shows "∃N. ∀m≥N. ∀n≥N. ∀x∈S. ∀y∈S. norm ((f m x - f n x) - (f m y - f n y)) ≤ e * norm (x - y)" proof - have *: "2 * (e/2) = e" using ‹e > 0› by auto obtain N where "∀n≥N. ∀x∈S. ∀h. norm (f' n x h - g' x h) ≤ (e/2) * norm h" using nle ‹e > 0› unfolding eventually_sequentially by (metis less_divide_eq_numeral1(1) mult_zero_left) then show "∃N. ∀m≥N. ∀n≥N. ∀x∈S. ∀y∈S. norm (f m x - f n x - (f m y - f n y)) ≤ e * norm (x - y)" apply (rule_tac x=N in exI) apply (rule has_derivative_sequence_lipschitz_lemma[where e="e/2", unfolded *]) using assms ‹e > 0› apply auto done qed lemma has_derivative_sequence: fixes f :: "nat ⇒ 'a::real_normed_vector ⇒ 'b::banach" assumes "convex S" and derf: "⋀n x. x ∈ S ⟹ ((f n) has_derivative (f' n x)) (at x within S)" and nle: "⋀e. e > 0 ⟹ ∀⇩_{F}n in sequentially. ∀x∈S. ∀h. norm (f' n x h - g' x h) ≤ e * norm h" and "x0 ∈ S" and lim: "((λn. f n x0) ⤏ l) sequentially" shows "∃g. ∀x∈S. (λn. f n x) ⇢ g x ∧ (g has_derivative g'(x)) (at x within S)" proof - have lem1: "⋀e. e > 0 ⟹ ∃N. ∀m≥N. ∀n≥N. ∀x∈S. ∀y∈S. norm ((f m x - f n x) - (f m y - f n y)) ≤ e * norm (x - y)" using assms(1,2,3) by (rule has_derivative_sequence_Lipschitz) have "∃g. ∀x∈S. ((λn. f n x) ⤏ g x) sequentially" proof (intro ballI bchoice) fix x assume "x ∈ S" show "∃y. (λn. f n x) ⇢ y" unfolding convergent_eq_Cauchy proof (cases "x = x0") case True then show "Cauchy (λn. f n x)" using LIMSEQ_imp_Cauchy[OF lim] by auto next case False show "Cauchy (λn. f n x)" unfolding Cauchy_def proof (intro allI impI) fix e :: real assume "e > 0" hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto obtain M where M: "∀m≥M. ∀n≥M. dist (f m x0) (f n x0) < e / 2" using LIMSEQ_imp_Cauchy[OF lim] * unfolding Cauchy_def by blast obtain N where N: "∀m≥N. ∀n≥N. ∀u∈S. ∀y∈S. norm (f m u - f n u - (f m y - f n y)) ≤ e / 2 / norm (x - x0) * norm (u - y)" using lem1 *(2) by blast show "∃M. ∀m≥M. ∀n≥M. dist (f m x) (f n x) < e" proof (intro exI allI impI) fix m n assume as: "max M N ≤m" "max M N≤n" have "dist (f m x) (f n x) ≤ norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))" unfolding dist_norm by (rule norm_triangle_sub) also have "… ≤ norm (f m x0 - f n x0) + e / 2" using N ‹x∈S› ‹x0∈S› as False by fastforce also have "… < e / 2 + e / 2" by (rule add_strict_right_mono) (use as M in ‹auto simp: dist_norm›) finally show "dist (f m x) (f n x) < e" by auto qed qed qed qed then obtain g where g: "∀x∈S. (λn. f n x) ⇢ g x" .. have lem2: "∃N. ∀n≥N. ∀x∈S. ∀y∈S. norm ((f n x - f n y) - (g x - g y)) ≤ e * norm (x - y)" if "e > 0" for e proof - obtain N where N: "∀m≥N. ∀n≥N. ∀x∈S. ∀y∈S. norm (f m x - f n x - (f m y - f n y)) ≤ e * norm (x - y)" using lem1 ‹e > 0› by blast show "∃N. ∀n≥N. ∀x∈S. ∀y∈S. norm (f n x - f n y - (g x - g y)) ≤ e * norm (x - y)" proof (intro exI ballI allI impI) fix n x y assume as: "N ≤ n" "x ∈ S" "y ∈ S" have "((λm. norm (f n x - f n y - (f m x - f m y))) ⤏ norm (f n x - f n y - (g x - g y))) sequentially" by (intro tendsto_intros g[rule_format] as) moreover have "eventually (λm. norm (f n x - f n y - (f m x - f m y)) ≤ e * norm (x - y)) sequentially" unfolding eventually_sequentially proof (intro exI allI impI) fix m assume "N ≤ m" then show "norm (f n x - f n y - (f m x - f m y)) ≤ e * norm (x - y)" using N as by (auto simp add: algebra_simps) qed ultimately show "norm (f n x - f n y - (g x - g y)) ≤ e * norm (x - y)" by (simp add: tendsto_upperbound) qed qed have "∀x∈S. ((λn. f n x) ⤏ g x) sequentially ∧ (g has_derivative g' x) (at x within S)" unfolding has_derivative_within_alt2 proof (intro ballI conjI allI impI) fix x assume "x ∈ S" then show "(λn. f n x) ⇢ g x" by (simp add: g) have tog': "(λn. f' n x u) ⇢ g' x u" for u unfolding filterlim_def le_nhds_metric_le eventually_filtermap dist_norm proof (intro allI impI) fix e :: real assume "e > 0" show "eventually (λn. norm (f' n x u - g' x u) ≤ e) sequentially" proof (cases "u = 0") case True have "eventually (λn. norm (f' n x u - g' x u) ≤ e * norm u) sequentially" using nle ‹0 < e› ‹x ∈ S› by (fast elim: eventually_mono) then show ?thesis using ‹u = 0› ‹0 < e› by (auto elim: eventually_mono) next case False with ‹0 < e› have "0 < e / norm u" by simp then have "eventually (λn. norm (f' n x u - g' x u) ≤ e / norm u * norm u) sequentially" using nle ‹x ∈ S› by (fast elim: eventually_mono) then show ?thesis using ‹u ≠ 0› by simp qed qed show "bounded_linear (g' x)" proof fix x' y z :: 'a fix c :: real note lin = assms(2)[rule_format,OF ‹x∈S›,THEN has_derivative_bounded_linear] show "g' x (c *⇩_{R}x') = c *⇩_{R}g' x x'" apply (rule tendsto_unique[OF trivial_limit_sequentially tog']) unfolding lin[THEN bounded_linear.linear, THEN linear_cmul] apply (intro tendsto_intros tog') done show "g' x (y + z) = g' x y + g' x z" apply (rule tendsto_unique[OF trivial_limit_sequentially tog']) unfolding lin[THEN bounded_linear.linear, THEN linear_add] apply (rule tendsto_add) apply (rule tog')+ done obtain N where N: "∀h. norm (f' N x h - g' x h) ≤ 1 * norm h" using nle ‹x ∈ S› unfolding eventually_sequentially by (fast intro: zero_less_one) have "bounded_linear (f' N x)" using derf ‹x ∈ S› by fast from bounded_linear.bounded [OF this] obtain K where K: "∀h. norm (f' N x h) ≤ norm h * K" .. { fix h have "norm (g' x h) = norm (f' N x h - (f' N x h - g' x h))" by simp also have "… ≤ norm (f' N x h) + norm (f' N x h - g' x h)" by (rule norm_triangle_ineq4) also have "… ≤ norm h * K + 1 * norm h" using N K by (fast intro: add_mono) finally have "norm (g' x h) ≤ norm h * (K + 1)" by (simp add: ring_distribs) } then show "∃K. ∀h. norm (g' x h) ≤ norm h * K" by fast qed show "eventually (λy. norm (g y - g x - g' x (y - x)) ≤ e * norm (y - x)) (at x within S)" if "e > 0" for e proof - have *: "e / 3 > 0" using that by auto obtain N1 where N1: "∀n≥N1. ∀x∈S. ∀h. norm (f' n x h - g' x h) ≤ e / 3 * norm h" using nle * unfolding eventually_sequentially by blast obtain N2 where N2[rule_format]: "∀n≥N2. ∀x∈S. ∀y∈S. norm (f n x - f n y - (g x - g y)) ≤ e / 3 * norm (x - y)" using lem2 * by blast let ?N = "max N1 N2" have "eventually (λy. norm (f ?N y - f ?N x - f' ?N x (y - x)) ≤ e / 3 * norm (y - x)) (at x within S)" using derf[unfolded has_derivative_within_alt2] and ‹x ∈ S› and * by fast moreover have "eventually (λy. y ∈ S) (at x within S)" unfolding eventually_at by (fast intro: zero_less_one) ultimately show "∀⇩_{F}y in at x within S. norm (g y - g x - g' x (y - x)) ≤ e * norm (y - x)" proof (rule eventually_elim2) fix y assume "y ∈ S" assume "norm (f ?N y - f ?N x - f' ?N x (y - x)) ≤ e / 3 * norm (y - x)" moreover have "norm (g y - g x - (f ?N y - f ?N x)) ≤ e / 3 * norm (y - x)" using N2[OF _ ‹y ∈ S› ‹x ∈ S›] by (simp add: norm_minus_commute) ultimately have "norm (g y - g x - f' ?N x (y - x)) ≤ 2 * e / 3 * norm (y - x)" using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"] by (auto simp add: algebra_simps) moreover have " norm (f' ?N x (y - x) - g' x (y - x)) ≤ e / 3 * norm (y - x)" using N1 ‹x ∈ S› by auto ultimately show "norm (g y - g x - g' x (y - x)) ≤ e * norm (y - x)" using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by (auto simp add: algebra_simps) qed qed qed then show ?thesis by fast qed text ‹Can choose to line up antiderivatives if we want.› lemma has_antiderivative_sequence: fixes f :: "nat ⇒ 'a::real_normed_vector ⇒ 'b::banach" assumes "convex S" and der: "⋀n x. x ∈ S ⟹ ((f n) has_derivative (f' n x)) (at x within S)" and no: "⋀e. e > 0 ⟹ ∀⇩_{F}n in sequentially. ∀x∈S. ∀h. norm (f' n x h - g' x h) ≤ e * norm h" shows "∃g. ∀x∈S. (g has_derivative g' x) (at x within S)" proof (cases "S = {}") case False then obtain a where "a ∈ S" by auto have *: "⋀P Q. ∃g. ∀x∈S. P g x ∧ Q g x ⟹ ∃g. ∀x∈S. Q g x" by auto show ?thesis apply (rule *) apply (rule has_derivative_sequence [OF ‹convex S› _ no, of "λn x. f n x + (f 0 a - f n a)"]) apply (metis assms(2) has_derivative_add_const) using ‹a ∈ S› apply auto done qed auto lemma has_antiderivative_limit: fixes g' :: "'a::real_normed_vector ⇒ 'a ⇒ 'b::banach" assumes "convex S" and "⋀e. e>0 ⟹ ∃f f'. ∀x∈S. (f has_derivative (f' x)) (at x within S) ∧ (∀h. norm (f' x h - g' x h) ≤ e * norm h)" shows "∃g. ∀x∈S. (g has_derivative g' x) (at x within S)" proof - have *: "∀n. ∃f f'. ∀x∈S. (f has_derivative (f' x)) (at x within S) ∧ (∀h. norm(f' x h - g' x h) ≤ inverse (real (Suc n)) * norm h)" by (simp add: assms(2)) obtain f where *: "⋀x. ∃f'. ∀xa∈S. (f x has_derivative f' xa) (at xa within S) ∧ (∀h. norm (f' xa h - g' xa h) ≤ inverse (real (Suc x)) * norm h)" using * by metis obtain f' where f': "⋀x. ∀z∈S. (f x has_derivative f' x z) (at z within S) ∧ (∀h. norm (f' x z h - g' z h) ≤ inverse (real (Suc x)) * norm h)" using * by metis show ?thesis proof (rule has_antiderivative_sequence[OF ‹convex S›, of f f']) fix e :: real assume "e > 0" obtain N where N: "inverse (real (Suc N)) < e" using reals_Archimedean[OF ‹e>0›] .. show "∀⇩_{F}n in sequentially. ∀x∈S. ∀h. norm (f' n x h - g' x h) ≤ e * norm h" unfolding eventually_sequentially proof (intro exI allI ballI impI) fix n x h assume n: "N ≤ n" and x: "x ∈ S" have *: "inverse (real (Suc n)) ≤ e" apply (rule order_trans[OF _ N[THEN less_imp_le]]) using n apply (auto simp add: field_simps) done show "norm (f' n x h - g' x h) ≤ e * norm h" by (meson "*" mult_right_mono norm_ge_zero order.trans x f') qed qed (use f' in auto) qed subsection ‹Differentiation of a series› lemma has_derivative_series: fixes f :: "nat ⇒ 'a::real_normed_vector ⇒ 'b::banach" assumes "convex S" and "⋀n x. x ∈ S ⟹ ((f n) has_derivative (f' n x)) (at x within S)" and "⋀e. e>0 ⟹ ∀⇩_{F}n in sequentially. ∀x∈S. ∀h. norm (sum (λi. f' i x h) {..<n} - g' x h) ≤ e * norm h" and "x ∈ S" and "(λn. f n x) sums l" shows "∃g. ∀x∈S. (λn. f n x) sums (g x) ∧ (g has_derivative g' x) (at x within S)" unfolding sums_def apply (rule has_derivative_sequence[OF assms(1) _ assms(3)]) apply (metis assms(2) has_derivative_sum) using assms(4-5) unfolding sums_def apply auto done lemma has_field_derivative_series: fixes f :: "nat ⇒ ('a :: {real_normed_field,banach}) ⇒ 'a" assumes "convex S" assumes "⋀n x. x ∈ S ⟹ (f n has_field_derivative f' n x) (at x within S)" assumes "uniform_limit S (λn x. ∑i<n. f' i x) g' sequentially" assumes "x0 ∈ S" "summable (λn. f n x0)" shows "∃g. ∀x∈S. (λn. f n x) sums g x ∧ (g has_field_derivative g' x) (at x within S)" unfolding has_field_derivative_def proof (rule has_derivative_series) show "∀⇩_{F}n in sequentially. ∀x∈S. ∀h. norm ((∑i<n. f' i x * h) - g' x * h) ≤ e * norm h" if "e > 0" for e unfolding eventually_sequentially proof - from that assms(3) obtain N where N: "⋀n x. n ≥ N ⟹ x ∈ S ⟹ norm ((∑i<n. f' i x) - g' x) < e" unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast { fix n :: nat and x h :: 'a assume nx: "n ≥ N" "x ∈ S" have "norm ((∑i<n. f' i x * h) - g' x * h) = norm ((∑i<n. f' i x) - g' x) * norm h" by (simp add: norm_mult [symmetric] ring_distribs sum_distrib_right) also from N[OF nx] have "norm ((∑i<n. f' i x) - g' x) ≤ e" by simp hence "norm ((∑i<n. f' i x) - g' x) * norm h ≤ e * norm h" by (intro mult_right_mono) simp_all finally have "norm ((∑i<n. f' i x * h) - g' x * h) ≤ e * norm h" . } thus "∃N. ∀n≥N. ∀x∈S. ∀h. norm ((∑i<n. f' i x * h) - g' x * h) ≤ e * norm h" by blast qed qed (use assms in ‹auto simp: has_field_derivative_def›) lemma has_field_derivative_series': fixes f :: "nat ⇒ ('a :: {real_normed_field,banach}) ⇒ 'a" assumes "convex S" assumes "⋀n x. x ∈ S ⟹ (f n has_field_derivative f' n x) (at x within S)" assumes "uniformly_convergent_on S (λn x. ∑i<n. f' i x)" assumes "x0 ∈ S" "summable (λn. f n x0)" "x ∈ interior S" shows "summable (λn. f n x)" "((λx. ∑n. f n x) has_field_derivative (∑n. f' n x)) (at x)" proof - from ‹x ∈ interior S› have "x ∈ S" using interior_subset by blast define g' where [abs_def]: "g' x = (∑i. f' i x)" for x from assms(3) have "uniform_limit S (λn x. ∑i<n. f' i x) g' sequentially" by (simp add: uniformly_convergent_uniform_limit_iff suminf_eq_lim g'_def) from has_field_derivative_series[OF assms(1,2) this assms(4,5)] 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(1)[OF ‹x ∈ S›] show "summable (λn. f n x)" by (simp add: sums_iff) from g(2)[OF ‹x ∈ S›] ‹x ∈ interior S› have "(g has_field_derivative g' x) (at x)" by (simp add: at_within_interior[of x S]) also have "(g has_field_derivative g' x) (at x) ⟷ ((λx. ∑n. f n x) has_field_derivative g' x) (at x)" using eventually_nhds_in_nhd[OF ‹x ∈ interior S›] interior_subset[of S] g(1) by (intro DERIV_cong_ev) (auto elim!: eventually_mono simp: sums_iff) finally show "((λx. ∑n. f n x) has_field_derivative g' x) (at x)" . qed lemma 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<n. f' i x)" assumes "x0 ∈ S" "summable (λn. f n x0)" and x: "x ∈ S" shows "summable (λn. f n x)" and "(λx. ∑n. f n x) differentiable (at x)" proof - from assms(4) obtain g' where A: "uniform_limit S (λn x. ∑i<n. f' i x) g' sequentially" unfolding uniformly_convergent_on_def by blast from x and ‹open 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[OF x] show "summable (λn. f n x)" by (auto simp: summable_def) 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) differentiable (at x)" unfolding differentiable_def by (auto simp: summable_def differentiable_def has_field_derivative_def) qed lemma 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<n. f' i x)" assumes "x0 ∈ S" "summable (λn. f n x0)" shows "(λx. ∑n. f n x) differentiable (at x0)" using differentiable_series[OF assms, of x0] ‹x0 ∈ S› by blast+ text ‹Considering derivative @{typ "real ⇒ 'b::real_normed_vector"} as a vector.› definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)" lemma vector_derivative_unique_within: assumes not_bot: "at x within S ≠ bot" and f': "(f has_vector_derivative f') (at x within S)" and f'': "(f has_vector_derivative f'') (at x within S)" shows "f' = f''" proof - have "(λx. x *⇩_{R}f') = (λx. x *⇩_{R}f'')" proof (rule frechet_derivative_unique_within, simp_all) show "∃d. d ≠ 0 ∧ ¦d¦ < e ∧ x + d ∈ S" if "0 < e" for e proof - from that obtain x' where "x' ∈ S" "x' ≠ x" "¦x' - x¦ < e" using islimpt_approachable_real[of x S] not_bot by (auto simp add: trivial_limit_within) then show ?thesis using eq_iff_diff_eq_0 by fastforce qed qed (use f' f'' in ‹auto simp: has_vector_derivative_def›) then show ?thesis unfolding fun_eq_iff by (metis scaleR_one) qed lemma vector_derivative_unique_at: "(f has_vector_derivative f') (at x) ⟹ (f has_vector_derivative f'') (at x) ⟹ f' = f''" by (rule vector_derivative_unique_within) auto lemma differentiableI_vector: "(f has_vector_derivative y) F ⟹ f differentiable F" by (auto simp: differentiable_def has_vector_derivative_def) lemma vector_derivative_works: "f differentiable net ⟷ (f has_vector_derivative (vector_derivative f net)) net" (is "?l = ?r") proof assume ?l obtain f' where f': "(f has_derivative f') net" using ‹?l› unfolding differentiable_def .. then interpret bounded_linear f' by auto show ?r unfolding vector_derivative_def has_vector_derivative_def by (rule someI[of _ "f' 1"]) (simp add: scaleR[symmetric] f') qed (auto simp: vector_derivative_def has_vector_derivative_def differentiable_def) lemma vector_derivative_within: assumes not_bot: "at x within S ≠ bot" and y: "(f has_vector_derivative y) (at x within S)" shows "vector_derivative f (at x within S) = y" using y by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y]) (auto simp: differentiable_def has_vector_derivative_def) lemma frechet_derivative_eq_vector_derivative: assumes "f differentiable (at x)" shows "(frechet_derivative f (at x)) = (λr. r *⇩_{R}vector_derivative f (at x))" using assms by (auto simp: differentiable_iff_scaleR vector_derivative_def has_vector_derivative_def intro: someI frechet_derivative_at [symmetric]) lemma has_real_derivative: fixes f :: "real ⇒ real" assumes "(f has_derivative f') F" obtains c where "(f has_real_derivative c) F" proof - obtain c where "f' = (λx. x * c)" by (metis assms has_derivative_bounded_linear real_bounded_linear) then show ?thesis by (metis assms that has_field_derivative_def mult_commute_abs) qed lemma has_real_derivative_iff: fixes f :: "real ⇒ real" shows "(∃c. (f has_real_derivative c) F) = (∃D. (f has_derivative D) F)" by (metis has_field_derivative_def has_real_derivative) lemma has_vector_derivative_cong_ev: assumes *: "eventually (λx. x ∈ S ⟶ f x = g x) (nhds x)" "f x = g x" shows "(f has_vector_derivative f') (at x within S) = (g has_vector_derivative f') (at x within S)" unfolding has_vector_derivative_def has_derivative_def using * apply (cases "at x within S ≠ bot") apply (intro refl conj_cong filterlim_cong) apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono) done definition deriv :: "('a ⇒ 'a::real_normed_field) ⇒ 'a ⇒ 'a" where "deriv f x ≡ SOME D. DERIV f x :> D" lemma DERIV_imp_deriv: "DERIV f x :> f' ⟹ deriv f x = f'" unfolding deriv_def by (metis some_equality DERIV_unique) lemma DERIV_deriv_iff_has_field_derivative: "DERIV f x :> deriv f x ⟷ (∃f'. (f has_field_derivative f') (at x))" by (auto simp: has_field_derivative_def DERIV_imp_deriv) lemma DERIV_deriv_iff_real_differentiable: fixes x :: real shows "DERIV f x :> deriv f x ⟷ f differentiable at x" unfolding differentiable_def by (metis DERIV_imp_deriv has_real_derivative_iff) lemma deriv_cong_ev: assumes "eventually (λx. f x = g x) (nhds x)" "x = y" shows "deriv f x = deriv g y" proof - have "(λD. (f has_field_derivative D) (at x)) = (λD. (g has_field_derivative D) (at y))" by (intro ext DERIV_cong_ev refl assms) thus ?thesis by (simp add: deriv_def assms) qed lemma higher_deriv_cong_ev: assumes "eventually (λx. f x = g x) (nhds x)" "x = y" shows "(deriv ^^ n) f x = (deriv ^^ n) g y" proof - from assms(1) have "eventually (λx. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)" proof (induction n arbitrary: f g) case (Suc n) from Suc.prems have "eventually (λy. eventually (λz. f z = g z) (nhds y)) (nhds x)" by (simp add: eventually_eventually) hence "eventually (λx. deriv f x = deriv g x) (nhds x)" by eventually_elim (rule deriv_cong_ev, simp_all) thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps) qed auto from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp qed lemma real_derivative_chain: fixes x :: real shows "f differentiable at x ⟹ g differentiable at (f x) ⟹ deriv (g o f) x = deriv g (f x) * deriv f x" by (metis DERIV_deriv_iff_real_differentiable DERIV_chain DERIV_imp_deriv) lemma field_derivative_eq_vector_derivative: "(deriv f x) = vector_derivative f (at x)" by (simp add: mult.commute deriv_def vector_derivative_def has_vector_derivative_def has_field_derivative_def) lemma islimpt_closure_open: fixes s :: "'a::perfect_space set" assumes "open s" and t: "t = closure s" "x ∈ t" shows "x islimpt t" proof cases assume "x ∈ s" { fix T assume "x ∈ T" "open T" then have "open (s ∩ T)" using ‹open s› by auto then have "s ∩ T ≠ {x}" using not_open_singleton[of x] by auto with ‹x ∈ T› ‹x ∈ s› have "∃y∈t. y ∈ T ∧ y ≠ x" using closure_subset[of s] by (auto simp: t) } then show ?thesis by (auto intro!: islimptI) next assume "x ∉ s" with t show ?thesis unfolding t closure_def by (auto intro: islimpt_subset) qed lemma vector_derivative_unique_within_closed_interval: assumes ab: "a < b" "x ∈ cbox a b" assumes D: "(f has_vector_derivative f') (at x within cbox a b)" "(f has_vector_derivative f'') (at x within cbox a b)" shows "f' = f''" using ab by (intro vector_derivative_unique_within[OF _ D]) (auto simp: trivial_limit_within intro!: islimpt_closure_open[where s="{a <..< b}"]) lemma vector_derivative_at: "(f has_vector_derivative f') (at x) ⟹ vector_derivative f (at x) = f'" by (intro vector_derivative_within at_neq_bot) lemma has_vector_derivative_id_at [simp]: "vector_derivative (λx. x) (at a) = 1" by (simp add: vector_derivative_at) lemma vector_derivative_minus_at [simp]: "f differentiable at a ⟹ vector_derivative (λx. - f x) (at a) = - vector_derivative f (at a)" by (simp add: vector_derivative_at has_vector_derivative_minus vector_derivative_works [symmetric]) lemma vector_derivative_add_at [simp]: "⟦f differentiable at a; g differentiable at a⟧ ⟹ vector_derivative (λx. f x + g x) (at a) = vector_derivative f (at a) + vector_derivative g (at a)" by (simp add: vector_derivative_at has_vector_derivative_add vector_derivative_works [symmetric]) lemma vector_derivative_diff_at [simp]: "⟦f differentiable at a; g differentiable at a⟧ ⟹ vector_derivative (λx. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)" by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric]) lemma vector_derivative_mult_at [simp]: fixes f g :: "real ⇒ 'a :: real_normed_algebra" shows "⟦f differentiable at a; g differentiable at a⟧ ⟹ vector_derivative (λx. f x * g x) (at a) = f a * vector_derivative g (at a) + vector_derivative f (at a) * g a" by (simp add: vector_derivative_at has_vector_derivative_mult vector_derivative_works [symmetric]) lemma vector_derivative_scaleR_at [simp]: "⟦f differentiable at a; g differentiable at a⟧ ⟹ vector_derivative (λx. f x *⇩_{R}g x) (at a) = f a *⇩_{R}vector_derivative g (at a) + vector_derivative f (at a) *⇩_{R}g a" apply (rule vector_derivative_at) apply (rule has_vector_derivative_scaleR) apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs) done lemma vector_derivative_within_cbox: assumes ab: "a < b" "x ∈ cbox a b" assumes f: "(f has_vector_derivative f') (at x within cbox a b)" shows "vector_derivative f (at x within cbox a b) = f'" by (intro vector_derivative_unique_within_closed_interval[OF ab _ f] vector_derivative_works[THEN iffD1] differentiableI_vector) fact lemma vector_derivative_within_closed_interval: fixes f::"real ⇒ 'a::euclidean_space" assumes "a < b" and "x ∈ {a..b}" assumes "(f has_vector_derivative f') (at x within {a..b})" shows "vector_derivative f (at x within {a..b}) = f'" using assms vector_derivative_within_cbox by fastforce lemma has_vector_derivative_within_subset: "(f has_vector_derivative f') (at x within S) ⟹ T ⊆ S ⟹ (f has_vector_derivative f') (at x within T)" by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset) lemma has_vector_derivative_at_within: "(f has_vector_derivative f') (at x) ⟹ (f has_vector_derivative f') (at x within S)" unfolding has_vector_derivative_def by (rule has_derivative_at_withinI) lemma has_vector_derivative_weaken: fixes x D and f g S T assumes f: "(f has_vector_derivative D) (at x within T)" and "x ∈ S" "S ⊆ T" and "⋀x. x ∈ S ⟹ f x = g x" shows "(g has_vector_derivative D) (at x within S)" proof - have "(f has_vector_derivative D) (at x within S) ⟷ (g has_vector_derivative D) (at x within S)" unfolding has_vector_derivative_def has_derivative_iff_norm using assms by (intro conj_cong Lim_cong_within refl) auto then show ?thesis using has_vector_derivative_within_subset[OF f ‹S ⊆ T›] by simp qed lemma has_vector_derivative_transform_within: assumes "(f has_vector_derivative f') (at x within S)" and "0 < d" and "x ∈ S" and "⋀x'. ⟦x'∈S; dist x' x < d⟧ ⟹ f x' = g x'" shows "(g has_vector_derivative f') (at x within S)" using assms unfolding has_vector_derivative_def by (rule has_derivative_transform_within) lemma has_vector_derivative_transform_within_open: assumes "(f has_vector_derivative f') (at x)" and "open S" and "x ∈ S" and "⋀y. y∈S ⟹ f y = g y" shows "(g has_vector_derivative f') (at x)" using assms unfolding has_vector_derivative_def by (rule has_derivative_transform_within_open) lemma has_vector_derivative_transform: assumes "x ∈ S" "⋀x. x ∈ S ⟹ g x = f x" assumes f': "(f has_vector_derivative f') (at x within S)" shows "(g has_vector_derivative f') (at x within S)" using assms unfolding has_vector_derivative_def by (rule has_derivative_transform) lemma vector_diff_chain_at: assumes "(f has_vector_derivative f') (at x)" and "(g has_vector_derivative g') (at (f x))" shows "((g ∘ f) has_vector_derivative (f' *⇩_{R}g')) (at x)" using assms has_vector_derivative_at_within has_vector_derivative_def vector_derivative_diff_chain_within by blast lemma vector_diff_chain_within: assumes "(f has_vector_derivative f') (at x within s)" and "(g has_vector_derivative g') (at (f x) within f ` s)" shows "((g ∘ f) has_vector_derivative (f' *⇩_{R}g')) (at x within s)" using assms has_vector_derivative_def vector_derivative_diff_chain_within by blast lemma vector_derivative_const_at [simp]: "vector_derivative (λx. c) (at a) = 0" by (simp add: vector_derivative_at) lemma vector_derivative_at_within_ivl: "(f has_vector_derivative f') (at x) ⟹ a ≤ x ⟹ x ≤ b ⟹ a<b ⟹ vector_derivative f (at x within {a..b}) = f'" using has_vector_derivative_at_within vector_derivative_within_cbox by fastforce lemma vector_derivative_chain_at: assumes "f differentiable at x" "(g differentiable at (f x))" shows "vector_derivative (g ∘ f) (at x) = vector_derivative f (at x) *⇩_{R}vector_derivative g (at (f x))" by (metis vector_diff_chain_at vector_derivative_at vector_derivative_works assms) lemma field_vector_diff_chain_at: (*thanks to Wenda Li*) assumes Df: "(f has_vector_derivative f') (at x)" and Dg: "(g has_field_derivative g') (at (f x))" shows "((g ∘ f) has_vector_derivative (f' * g')) (at x)" using diff_chain_at[OF Df[unfolded has_vector_derivative_def] Dg [unfolded has_field_derivative_def]] by (auto simp: o_def mult.commute has_vector_derivative_def) lemma vector_derivative_chain_within: assumes "at x within S ≠ bot" "f differentiable (at x within S)" "(g has_derivative g') (at (f x) within f ` S)" shows "vector_derivative (g ∘ f) (at x within S) = g' (vector_derivative f (at x within S)) " apply (rule vector_derivative_within [OF ‹at x within S ≠ bot›]) apply (rule vector_derivative_diff_chain_within) using assms(2-3) vector_derivative_works by auto subsection‹The notion of being field differentiable› definition field_differentiable :: "['a ⇒ 'a::real_normed_field, 'a filter] ⇒ bool" (infixr "(field'_differentiable)" 50) where "f field_differentiable F ≡ ∃f'. (f has_field_derivative f') F" lemma field_differentiable_imp_differentiable: "f field_differentiable F ⟹ f differentiable F" unfolding field_differentiable_def differentiable_def using has_field_derivative_imp_has_derivative by auto lemma field_differentiable_derivI: "f field_differentiable (at x) ⟹ (f has_field_derivative deriv f x) (at x)" by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative) lemma field_differentiable_imp_continuous_at: "f field_differentiable (at x within S) ⟹ continuous (at x within S) f" by (metis DERIV_continuous field_differentiable_def) lemma field_differentiable_within_subset: "⟦f field_differentiable (at x within S); T ⊆ S⟧ ⟹ f field_differentiable (at x within T)" by (metis DERIV_subset field_differentiable_def) lemma field_differentiable_at_within: "⟦f field_differentiable (at x)⟧ ⟹ f field_differentiable (at x within S)" unfolding field_differentiable_def by (metis DERIV_subset top_greatest) lemma field_differentiable_linear [simp,derivative_intros]: "(( * ) c) field_differentiable F" unfolding field_differentiable_def has_field_derivative_def mult_commute_abs by (force intro: has_derivative_mult_right) lemma field_differentiable_const [simp,derivative_intros]: "(λz. c) field_differentiable F" unfolding field_differentiable_def has_field_derivative_def using DERIV_const has_field_derivative_imp_has_derivative by blast lemma field_differentiable_ident [simp,derivative_intros]: "(λz. z) field_differentiable F" unfolding field_differentiable_def has_field_derivative_def using DERIV_ident has_field_derivative_def by blast lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F" unfolding id_def by (rule field_differentiable_ident) lemma field_differentiable_minus [derivative_intros]: "f field_differentiable F ⟹ (λz. - (f z)) field_differentiable F" unfolding field_differentiable_def by (metis field_differentiable_minus) lemma field_differentiable_add [derivative_intros]: assumes "f field_differentiable F" "g field_differentiable F" shows "(λz. f z + g z) field_differentiable F" using assms unfolding field_differentiable_def by (metis field_differentiable_add) lemma field_differentiable_add_const [simp,derivative_intros]: "(+) c field_differentiable F" by (simp add: field_differentiable_add) lemma field_differentiable_sum [derivative_intros]: "(⋀i. i ∈ I ⟹ (f i) field_differentiable F) ⟹ (λz. ∑i∈I. f i z) field_differentiable F" by (induct I rule: infinite_finite_induct) (auto intro: field_differentiable_add field_differentiable_const) lemma field_differentiable_diff [derivative_intros]: assumes "f field_differentiable F" "g field_differentiable F" shows "(λz. f z - g z) field_differentiable F" using assms unfolding field_differentiable_def by (metis field_differentiable_diff) lemma field_differentiable_inverse [derivative_intros]: assumes "f field_differentiable (at a within S)" "f a ≠ 0" shows "(λz. inverse (f z)) field_differentiable (at a within S)" using assms unfolding field_differentiable_def by (metis DERIV_inverse_fun) lemma field_differentiable_mult [derivative_intros]: assumes "f field_differentiable (at a within S)" "g field_differentiable (at a within S)" shows "(λz. f z * g z) field_differentiable (at a within S)" using assms unfolding field_differentiable_def by (metis DERIV_mult [of f _ a S g]) lemma field_differentiable_divide [derivative_intros]: assumes "f field_differentiable (at a within S)" "g field_differentiable (at a within S)" "g a ≠ 0" shows "(λz. f z / g z) field_differentiable (at a within S)" using assms unfolding field_differentiable_def by (metis DERIV_divide [of f _ a S g]) lemma field_differentiable_power [derivative_intros]: assumes "f field_differentiable (at a within S)" shows "(λz. f z ^ n) field_differentiable (at a within S)" using assms unfolding field_differentiable_def by (metis DERIV_power) lemma field_differentiable_transform_within: "0 < d ⟹ x ∈ S ⟹ (⋀x'. x' ∈ S ⟹ dist x' x < d ⟹ f x' = g x') ⟹ f field_differentiable (at x within S) ⟹ g field_differentiable (at x within S)" unfolding field_differentiable_def has_field_derivative_def by (blast intro: has_derivative_transform_within) lemma field_differentiable_compose_within: assumes "f field_differentiable (at a within S)" "g field_differentiable (at (f a) within f`S)" shows "(g o f) field_differentiable (at a within S)" using assms unfolding field_differentiable_def by (metis DERIV_image_chain) lemma field_differentiable_compose: "f field_differentiable at z ⟹ g field_differentiable at (f z) ⟹ (g o f) field_differentiable at z" by (metis field_differentiable_at_within field_differentiable_compose_within) lemma field_differentiable_within_open: "⟦a ∈ S; open S⟧ ⟹ f field_differentiable at a within S ⟷ f field_differentiable at a" unfolding field_differentiable_def by (metis at_within_open) lemma vector_derivative_chain_at_general: assumes "f differentiable at x" "g field_differentiable at (f x)" shows "vector_derivative (g ∘ f) (at x) = vector_derivative f (at x) * deriv g (f x)" apply (rule vector_derivative_at [OF field_vector_diff_chain_at]) using assms vector_derivative_works by (auto simp: field_differentiable_derivI) lemma exp_scaleR_has_vector_derivative_right: "((λt. exp (t *⇩_{R}A)) has_vector_derivative exp (t *⇩_{R}A) * A) (at t within T)" unfolding has_vector_derivative_def proof (rule has_derivativeI) let ?F = "at t within (T ∩ {t - 1 <..< t + 1})" have *: "at t within T = ?F" by (rule at_within_nhd[where S="{t - 1 <..< t + 1}"]) auto let ?e = "λi x. (inverse (1 + real i) * inverse (fact i) * (x - t) ^ i) *⇩_{R}(A * A ^ i)" have "∀⇩_{F}n in sequentially. ∀x∈T ∩ {t - 1<..<t + 1}. norm (?e n x) ≤ norm (A ^ (n + 1) /⇩_{R}fact (n + 1))" by (auto simp: divide_simps power_abs intro!: mult_left_le_one_le power_le_one eventuallyI) then have "uniform_limit (T ∩ {t - 1<..<t + 1}) (λn x. ∑i<n. ?e i x) (λx. ∑i. ?e i x) sequentially" by (rule weierstrass_m_test_ev) (intro summable_ignore_initial_segment summable_norm_exp) moreover have "∀⇩_{F}x in sequentially. x > 0" by (metis eventually_gt_at_top) then have "∀⇩_{F}n in sequentially. ((λx. ∑i<n. ?e i x) ⤏ A) ?F" by eventually_elim (auto intro!: tendsto_eq_intros simp: power_0_left if_distrib if_distribR sum.delta cong: if_cong) ultimately have [tendsto_intros]: "((λx. ∑i. ?e i x) ⤏ A) ?F" by (auto intro!: swap_uniform_limit[where f="λn x. ∑i < n. ?e i x" and F = sequentially]) have [tendsto_intros]: "((λx. if x = t then 0 else 1) ⤏ 1) ?F" by (rule Lim_eventually) (simp add: eventually_at_filter) have "((λy. ((y - t) / abs (y - t)) *⇩_{R}((∑n. ?e n y) - A)) ⤏ 0) (at t within T)" unfolding * by (rule tendsto_norm_zero_cancel) (auto intro!: tendsto_eq_intros) moreover have "∀⇩_{F}x in at t within T. x ≠ t" by (simp add: eventually_at_filter) then have "∀⇩_{F}x in at t within T. ((x - t) / ¦x - t¦) *⇩_{R}((∑n. ?e n x) - A) = (exp ((x - t) *⇩_{R}A) - 1 - (x - t) *⇩_{R}A) /⇩_{R}norm (x - t)" proof eventually_elim case (elim x) have "(exp ((x - t) *⇩_{R}A) - 1 - (x - t) *⇩_{R}A) /⇩_{R}norm (x - t) = ((∑n. (x - t) *⇩_{R}?e n x) - (x - t) *⇩_{R}A) /⇩_{R}norm (x - t)" unfolding exp_first_term by (simp add: ac_simps) also have "summable (λn. ?e n x)" proof - from elim have "?e n x = (((x - t) *⇩_{R}A) ^ (n + 1)) /⇩_{R}fact (n + 1) /⇩_{R}(x - t)" for n by simp then show ?thesis by (auto simp only: intro!: summable_scaleR_right summable_ignore_initial_segment summable_exp_generic) qed then have "(∑n. (x - t) *⇩_{R}?e n x) = (x - t) *⇩_{R}(∑n. ?e n x)" by (rule suminf_scaleR_right[symmetric]) also have "(… - (x - t) *⇩_{R}A) /⇩_{R}norm (x - t) = (x - t) *⇩_{R}((∑n. ?e n x) - A) /⇩_{R}norm (x - t)" by (simp add: algebra_simps) finally show ?case by (simp add: divide_simps) qed ultimately have "((λy. (exp ((y - t) *⇩_{R}A) - 1 - (y - t) *⇩_{R}A) /⇩_{R}norm (y - t)) ⤏ 0) (at t within T)" by (rule Lim_transform_eventually[rotated]) from tendsto_mult_right_zero[OF this, where c="exp (t *⇩_{R}A)"] show "((λy. (exp (y *⇩_{R}A) - exp (t *⇩_{R}A) - (y - t) *⇩_{R}(exp (t *⇩_{R}A) * A)) /⇩_{R}norm (y - t)) ⤏ 0) (at t within T)" by (rule Lim_transform_eventually[rotated]) (auto simp: algebra_simps divide_simps exp_add_commuting[symmetric]) qed (rule bounded_linear_scaleR_left) lemma exp_times_scaleR_commute: "exp (t *⇩_{R}A) * A = A * exp (t *⇩_{R}A)" using exp_times_arg_commute[symmetric, of "t *⇩_{R}A"] by (auto simp: algebra_simps) lemma exp_scaleR_has_vector_derivative_left: "((λt. exp (t *⇩_{R}A)) has_vector_derivative A * exp (t *⇩_{R}A)) (at t)" using exp_scaleR_has_vector_derivative_right[of A t] by (simp add: exp_times_scaleR_commute) subsection ‹Relation between convexity and derivative› (* TODO: Generalise to real vector spaces? *) lemma convex_on_imp_above_tangent: assumes convex: "convex_on A f" and connected: "connected A" assumes c: "c ∈ interior A" and x : "x ∈ A" assumes deriv: "(f has_field_derivative f') (at c within A)" shows "f x - f c ≥ f' * (x - c)" proof (cases x c rule: linorder_cases) assume xc: "x > c" let ?A' = "interior A ∩ {c<..}" from c have "c ∈ interior A ∩ closure {c<..}" by auto also have "… ⊆ closure (interior A ∩ {c<..})" by (intro open_Int_closure_subset) auto finally have "at c within ?A' ≠ bot" by (subst at_within_eq_bot_iff) auto moreover from deriv have "((λy. (f y - f c) / (y - c)) ⤏ f') (at c within ?A')" unfolding has_field_derivative_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le) moreover from eventually_at_right_real[OF xc] have "eventually (λy. (f y - f c) / (y - c) ≤ (f x - f c) / (x - c)) (at_right c)" proof eventually_elim fix y assume y: "y ∈ {c<..<x}" with convex connected x c have "f y ≤ (f x - f c) / (x - c) * (y - c) + f c" using interior_subset[of A] by (intro convex_onD_Icc' convex_on_subset[OF convex] connected_contains_Icc) auto hence "f y - f c ≤ (f x - f c) / (x - c) * (y - c)" by simp thus "(f y - f c) / (y - c) ≤ (f x - f c) / (x - c)" using y xc by (simp add: divide_simps) qed hence "eventually (λy. (f y - f c) / (y - c) ≤ (f x - f c) / (x - c)) (at c within ?A')" by (blast intro: filter_leD at_le) ultimately have "f' ≤ (f x - f c) / (x - c)" by (simp add: tendsto_upperbound) thus ?thesis using xc by (simp add: field_simps) next assume xc: "x < c" let ?A' = "interior A ∩ {..<c}" from c have "c ∈ interior A ∩ closure {..<c}" by auto also have "… ⊆ closure (interior A ∩ {..<c})" by (intro open_Int_closure_subset) auto finally have "at c within ?A' ≠ bot" by (subst at_within_eq_bot_iff) auto moreover from deriv have "((λy. (f y - f c) / (y - c)) ⤏ f') (at c within ?A')" unfolding has_field_derivative_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le) moreover from eventually_at_left_real[OF xc] have "eventually (λy. (f y - f c) / (y - c) ≥ (f x - f c) / (x - c)) (at_left c)" proof eventually_elim fix y assume y: "y ∈ {x<..<c}" with convex connected x c have "f y ≤ (f x - f c) / (c - x) * (c - y) + f c" using interior_subset[of A] by (intro convex_onD_Icc'' convex_on_subset[OF convex] connected_contains_Icc) auto hence "f y - f c ≤ (f x - f c) * ((c - y) / (c - x))" by simp also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps) finally show "(f y - f c) / (y - c) ≥ (f x - f c) / (x - c)" using y xc by (simp add: divide_simps) qed hence "eventually (λy. (f y - f c) / (y - c) ≥ (f x - f c) / (x - c)) (at c within ?A')" by (blast intro: filter_leD at_le) ultimately have "f' ≥ (f x - f c) / (x - c)" by (simp add: tendsto_lowerbound) thus ?thesis using xc by (simp add: field_simps) qed simp_all subsection ‹Partial derivatives› lemma eventually_at_Pair_within_TimesI1: fixes x::"'a::metric_space" assumes "∀⇩_{F}x' in at x within X. P x'" assumes "P x" shows "∀⇩_{F}(x', y') in at (x, y) within X × Y. P x'" proof - from assms[unfolded eventually_at_topological] obtain S where S: "open S" "x ∈ S" "⋀x'. x' ∈ X ⟹ x' ∈ S ⟹ P x'" by metis show "∀⇩_{F}(x', y') in at (x, y) within X × Y. P x'" unfolding eventually_at_topological by (auto intro!: exI[where x="S × UNIV"] S open_Times) qed lemma eventually_at_Pair_within_TimesI2: fixes x::"'a::metric_space" assumes "∀⇩_{F}y' in at y within Y. P y'" "P y" shows "∀⇩_{F}(x', y') in at (x, y) within X × Y. P y'" proof - from assms[unfolded eventually_at_topological] obtain S where S: "open S" "y ∈ S" "⋀y'. y' ∈ Y ⟹ y' ∈ S ⟹ P y'" by metis show "∀⇩_{F}(x', y') in at (x, y) within X × Y. P y'" unfolding eventually_at_topological by (auto intro!: exI[where x="UNIV × S"] S open_Times) qed lemma has_derivative_partialsI: fixes f::"'a::real_normed_vector ⇒ 'b::real_normed_vector ⇒ 'c::real_normed_vector" assumes fx: "((λx. f x y) has_derivative fx) (at x within X)" assumes fy: "⋀x y. x ∈ X ⟹ y ∈ Y ⟹ ((λy. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)" assumes fy_cont[unfolded continuous_within]: "continuous (at (x, y) within X × Y) (λ(x, y). fy x y)" assumes "y ∈ Y" "convex Y" shows "((λ(x, y). f x y) has_derivative (λ(tx, ty). fx tx + fy x y ty)) (at (x, y) within X × Y)" proof (safe intro!: has_derivativeI tendstoI, goal_cases) case (2 e') interpret fx: bounded_linear "fx" using fx by (rule has_derivative_bounded_linear) define e where "e = e' / 9" have "e > 0" using ‹e' > 0› by (simp add: e_def) from fy_cont[THEN tendstoD, OF ‹e > 0›] have "∀⇩_{F}(x', y') in at (x, y) within X × Y. dist (fy x' y') (fy x y) < e" by (auto simp: split_beta') from this[unfolded eventually_at] obtain d' where "d' > 0" "⋀x' y'. x' ∈ X ⟹ y' ∈ Y ⟹ (x', y') ≠ (x, y) ⟹ dist (x', y') (x, y) < d' ⟹ dist (fy x' y') (fy x y) < e" by auto then have d': "x' ∈ X ⟹ y' ∈ Y ⟹ dist (x', y') (x, y) < d' ⟹ dist (fy x' y') (fy x y) < e" for x' y' using ‹0 < e› by (cases "(x', y') = (x, y)") auto define d where "d = d' / sqrt 2" have "d > 0" using ‹0 < d'› by (simp add: d_def) have d: "x' ∈ X ⟹ y' ∈ Y ⟹ dist x' x < d ⟹ dist y' y < d ⟹ dist (fy x' y') (fy x y) < e" for x' y' by (auto simp: dist_prod_def d_def intro!: d' real_sqrt_sum_squares_less) let ?S = "ball y d ∩ Y" have "convex ?S" by (auto intro!: convex_Int ‹convex Y›) { fix x'::'a and y'::'b assume x': "x' ∈ X" and y': "y' ∈ Y" assume dx': "dist x' x < d" and dy': "dist y' y < d" have "norm (fy x' y' - fy x' y) ≤ dist (fy x' y') (fy x y) + dist (fy x' y) (fy x y)" by norm also have "dist (fy x' y') (fy x y) < e" by (rule d; fact) also have "dist (fy x' y) (fy x y) < e" by (auto intro!: d simp: dist_prod_def x' ‹d > 0› ‹y ∈ Y› dx') finally have "norm (fy x' y' - fy x' y) < e + e" by arith then have "onorm (blinfun_apply (fy x' y') - blinfun_apply (fy x' y)) < e + e" by (auto simp: norm_blinfun.rep_eq blinfun.diff_left[abs_def] fun_diff_def) } note onorm = this have ev_mem: "∀⇩_{F}(x', y') in at (x, y) within X × Y. (x', y') ∈ X × Y" using ‹y ∈ Y› by (auto simp: eventually_at intro!: zero_less_one) moreover have ev_dist: "∀⇩_{F}xy in at (x, y) within X × Y. dist xy (x, y) < d" if "d > 0" for d using eventually_at_ball[OF that] by (rule eventually_elim2) (auto simp: dist_commute mem_ball intro!: eventually_True) note ev_dist[OF ‹0 < d›] ultimately have "∀⇩_{F}(x', y') in at (x, y) within X × Y. norm (f x' y' - f x' y - (fy x' y) (y' - y)) ≤ norm (y' - y) * (e + e)" proof (eventually_elim, safe) fix x' y' assume "x' ∈ X" and y': "y' ∈ Y" assume dist: "dist (x', y') (x, y) < d" then have dx: "dist x' x < d" and dy: "dist y' y < d" unfolding dist_prod_def fst_conv snd_conv atomize_conj by (metis le_less_trans real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2) { fix t::real assume "t ∈ {0 .. 1}" then have "y + t *⇩_{R}(y' - y) ∈ closed_segment y y'" by (auto simp: closed_segment_def algebra_simps intro!: exI[where x=t]) also have "… ⊆ ball y d ∩ Y" using ‹y ∈ Y› ‹0 < d› dy y' by (intro ‹convex ?S›[unfolded convex_contains_segment, rule_format, of y y']) (auto simp: dist_commute) finally have "y + t *⇩_{R}(y' - y) ∈ ?S" . } note seg = this have "⋀x. x ∈ ball y d ∩ Y ⟹ onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) ≤ e + e" by (safe intro!: onorm less_imp_le ‹x' ∈ X› dx) (auto simp: dist_commute ‹0 < d› ‹y ∈ Y›) with seg has_derivative_within_subset[OF assms(2)[OF ‹x' ∈ X›]] show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) ≤ norm (y' - y) * (e + e)" by (rule differentiable_bound_linearization[where S="?S"]) (auto intro!: ‹0 < d› ‹y ∈ Y›) qed moreover let ?le = "λx'. norm (f x' y - f x y - (fx) (x' - x)) ≤ norm (x' - x) * e" from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF ‹0 < e›] have "∀⇩_{F}x' in at x within X. ?le x'" by eventually_elim (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm) then have "∀⇩_{F}(x', y') in at (x, y) within X × Y. ?le x'" by (rule eventually_at_Pair_within_TimesI1) (simp add: blinfun.bilinear_simps) moreover have "∀⇩_{F}(x', y') in at (x, y) within X × Y. norm ((x', y') - (x, y)) ≠ 0" unfolding norm_eq_zero right_minus_eq by (auto simp: eventually_at intro!: zero_less_one) moreover from fy_cont[THEN tendstoD, OF ‹0 < e›] have "∀⇩_{F}x' in at x within X. norm (fy x' y - fy x y) < e" unfolding eventually_at using ‹y ∈ Y› by (auto simp: dist_prod_def dist_norm) then have "∀⇩_{F}(x', y') in at (x, y) within X × Y. norm (fy x' y - fy x y) < e" by (rule eventually_at_Pair_within_TimesI1) (simp add: blinfun.bilinear_simps ‹0 < e›) ultimately have "∀⇩_{F}(x', y') in at (x, y) within X × Y. norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /⇩_{R}norm ((x', y') - (x, y))) < e'" apply eventually_elim proof safe fix x' y' have "norm (f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) ≤ norm (f x' y' - f x' y - fy x' y (y' - y)) + norm (fy x y (y' - y) - fy x' y (y' - y)) + norm (f x' y - f x y - fx (x' - x))" by norm also assume nz: "norm ((x', y') - (x, y)) ≠ 0" and nfy: "norm (fy x' y - fy x y) < e" assume "norm (f x' y' - f x' y - blinfun_apply (fy x' y) (y' - y)) ≤ norm (y' - y) * (e + e)" also assume "norm (f x' y - f x y - (fx) (x' - x)) ≤ norm (x' - x) * e" also have "norm ((fy x y) (y' - y) - (fy x' y) (y' - y)) ≤ norm ((fy x y) - (fy x' y)) * norm (y' - y)" by (auto simp: blinfun.bilinear_simps[symmetric] intro!: norm_blinfun) also have "… ≤ (e + e) * norm (y' - y)" using ‹e > 0› nfy by (auto simp: norm_minus_commute intro!: mult_right_mono) also have "norm (x' - x) * e ≤ norm (x' - x) * (e + e)" using ‹0 < e› by simp also have "norm (y' - y) * (e + e) + (e + e) * norm (y' - y) + norm (x' - x) * (e + e) ≤ (norm (y' - y) + norm (x' - x)) * (4 * e)" using ‹e > 0› by (simp add: algebra_simps) also have "… ≤ 2 * norm ((x', y') - (x, y)) * (4 * e)" using ‹0 < e› real_sqrt_sum_squares_ge1[of "norm (x' - x)" "norm (y' - y)"] real_sqrt_sum_squares_ge2[of "norm (y' - y)" "norm (x' - x)"] by (auto intro!: mult_right_mono simp: norm_prod_def simp del: real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2) also have "… ≤ norm ((x', y') - (x, y)) * (8 * e)" by simp also have "… < norm ((x', y') - (x, y)) * e'" using ‹0 < e'› nz by (auto simp: e_def) finally show "norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /⇩_{R}norm ((x', y') - (x, y))) < e'" by (auto simp: divide_simps dist_norm mult.commute) qed then show ?case by eventually_elim (auto simp: dist_norm field_simps) next from has_derivative_bounded_linear[OF fx] obtain fxb where "fx = blinfun_apply fxb" by (metis bounded_linear_Blinfun_apply) then show "bounded_linear (λ(tx, ty). fx tx + blinfun_apply (fy x y) ty)" by (auto intro!: bounded_linear_intros simp: split_beta') qed subsection ‹Differentiable case distinction› lemma has_derivative_within_If_eq: "((λx. if P x then f x else g x) has_derivative f') (at x within S) = (bounded_linear f' ∧ ((λy.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/⇩_{R}norm (y - x) else (g y - ((if P x then f x else g x) + f' (y - x)))/⇩_{R}norm (y - x))) ⤏ 0) (at x within S))" (is "_ = (_ ∧ (?if ⤏ 0) _)") proof - have "(λy. (1 / norm (y - x)) *⇩_{R}((if P y then f y else g y) - ((if P x then f x else g x) + f' (y - x)))) = ?if" by (auto simp: inverse_eq_divide) thus ?thesis by (auto simp: has_derivative_within) qed lemma has_derivative_If_within_closures: assumes f': "x ∈ S ∪ (closure S ∩ closure T) ⟹ (f has_derivative f' x) (at x within S ∪ (closure S ∩ closure T))" assumes g': "x ∈ T ∪ (closure S ∩ closure T) ⟹ (g has_derivative g' x) (at x within T ∪ (closure S ∩ closure T))" assumes connect: "x ∈ closure S ⟹ x ∈ closure T ⟹ f x = g x" assumes connect': "x ∈ closure S ⟹ x ∈ closure T ⟹ f' x = g' x" assumes x_in: "x ∈ S ∪ T" shows "((λx. if x ∈ S then f x else g x) has_derivative (if x ∈ S then f' x else g' x)) (at x within (S ∪ T))" proof - from f' x_in interpret f': bounded_linear "if x ∈ S then f' x else (λx. 0)" by (auto simp add: has_derivative_within) from g' interpret g': bounded_linear "if x ∈ T then g' x else (λx. 0)" by (auto simp add: has_derivative_within) have bl: "bounded_linear (if x ∈ S then f' x else g' x)" using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in by (unfold_locales; force) show ?thesis using f' g' closure_subset[of T] closure_subset[of S] unfolding has_derivative_within_If_eq by (intro conjI bl tendsto_If_within_closures x_in) (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp) qed lemma has_vector_derivative_If_within_closures: assumes x_in: "x ∈ S ∪ T" assumes "u = S ∪ T" assumes f': "x ∈ S ∪ (closure S ∩ closure T) ⟹ (f has_vector_derivative f' x) (at x within S ∪ (closure S ∩ closure T))" assumes g': "x ∈ T ∪ (closure S ∩ closure T) ⟹ (g has_vector_derivative g' x) (at x within T ∪ (closure S ∩ closure T))" assumes connect: "x ∈ closure S ⟹ x ∈ closure T ⟹ f x = g x" assumes connect': "x ∈ closure S ⟹ x ∈ closure T ⟹ f' x = g' x" shows "((λx. if x ∈ S then f x else g x) has_vector_derivative (if x ∈ S then f' x else g' x)) (at x within u)" unfolding has_vector_derivative_def assms using x_in apply (intro has_derivative_If_within_closures[where ?f' = "λx a. a *⇩_{R}f' x" and ?g' = "λx a. a *⇩_{R}g' x", THEN has_derivative_eq_rhs]) subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption) subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption) by (auto simp: assms) end