section ‹Multivariate calculus in Euclidean space›
theory Derivative
imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
begin
lemma onorm_inner_left:
assumes "bounded_linear r"
shows "onorm (λx. r x ∙ f) ≤ onorm r * norm f"
proof (rule onorm_bound)
fix x
have "norm (r x ∙ f) ≤ norm (r x) * norm f"
by (simp add: Cauchy_Schwarz_ineq2)
also have "… ≤ onorm r * norm x * norm f"
by (intro mult_right_mono onorm assms norm_ge_zero)
finally show "norm (r x ∙ f) ≤ onorm r * norm f * norm x"
by (simp add: ac_simps)
qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)
lemma onorm_inner_right:
assumes "bounded_linear r"
shows "onorm (λx. f ∙ r x) ≤ norm f * onorm r"
apply (subst inner_commute)
apply (rule onorm_inner_left[OF assms, THEN order_trans])
apply simp
done
declare has_derivative_bounded_linear[dest]
subsection ‹Derivatives›
subsubsection ‹Combining theorems.›
lemmas has_derivative_id = has_derivative_ident
lemmas has_derivative_neg = has_derivative_minus
lemmas has_derivative_sub = has_derivative_diff
lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
lemmas inner_right_has_derivative = has_derivative_inner_right
lemmas inner_left_has_derivative = has_derivative_inner_left
lemmas mult_right_has_derivative = has_derivative_mult_right
lemmas mult_left_has_derivative = has_derivative_mult_left
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.›
lemma has_derivative_bilinear_within:
assumes "(f has_derivative f') (at x within s)"
and "(g has_derivative g') (at x within s)"
and "bounded_bilinear h"
shows "((λx. h (f x) (g x)) has_derivative (λd. h (f x) (g' d) + h (f' d) (g x))) (at x within s)"
using bounded_bilinear.FDERIV[OF assms(3,1,2)] .
lemma has_derivative_bilinear_at:
assumes "(f has_derivative f') (at x)"
and "(g has_derivative g') (at x)"
and "bounded_bilinear h"
shows "((λx. h (f x) (g x)) has_derivative (λd. h (f x) (g' d) + h (f' d) (g x))) (at x)"
using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
text ‹These are the only cases we'll care about, probably.›
lemma has_derivative_within: "(f has_derivative f') (at x within s) ⟷
bounded_linear f' ∧ ((λy. (1 / norm(y - x)) *⇩R (f y - (f x + f' (y - x)))) ⤏ 0) (at x within s)"
unfolding has_derivative_def Lim
by (auto simp add: netlimit_within field_simps)
lemma has_derivative_at: "(f has_derivative f') (at x) ⟷
bounded_linear f' ∧ ((λy. (1 / (norm(y - x))) *⇩R (f y - (f x + f' (y - x)))) ⤏ 0) (at x)"
using has_derivative_within [of f f' x UNIV]
by simp
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
unfolding diff_0_right
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_within:
"(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 (op * 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_within_iff:
"(f has_field_derivative D) (at a within s) ⟷ ((λz. (f z - f a) / (z - a)) ⤏ D) (at a within s)"
proof -
have 1: "⋀w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
by (metis divide_diff_eq_iff eq_iff_diff_eq_0 mult.commute)
show ?thesis
apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
apply (simp add: LIM_zero_iff [where l = D, symmetric])
apply (simp add: Lim_within dist_norm)
apply (simp add: nonzero_norm_divide [symmetric])
apply (simp add: 1 diff_diff_eq ac_simps)
done
qed
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 DERIV_within_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 DERIV_within_iff cong: Lim_cong_within)
qed
subsubsection ‹Limit transformation for derivatives›
lemma has_derivative_transform_within:
assumes "(f has_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_derivative f') (at x within s)"
using assms
unfolding has_derivative_within
by (force simp add: intro: Lim_transform_within)
lemma has_derivative_transform_within_open:
assumes "(f has_derivative f') (at x)"
and "open s"
and "x ∈ s"
and "⋀x. x∈s ⟹ f x = g x"
shows "(g has_derivative f') (at x)"
using assms unfolding has_derivative_at
by (force simp add: intro: Lim_transform_within_open)
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_within
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_within_open:
assumes "a ∈ s"
and "open s"
shows "f differentiable (at a within s) ⟷ f differentiable (at a)"
using assms
by (simp only: at_within_interior interior_open)
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
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
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)
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 "(f has_derivative f') (at x within s)"
and "(f has_derivative f'') (at x within s)"
and "∀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 (rule, rule)
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"
apply (rule_tac x="x + d *⇩R (SOME i. i ∈ Basis)" in bexI)
unfolding dist_norm
apply (auto simp: SOME_Basis nonzero_Basis)
done
qed
then have *: "netlimit (at x within s) = x"
apply (auto intro!: netlimit_within)
by (metis trivial_limit_within)
show ?thesis
apply (rule linear_eq_stdbasis)
unfolding linear_conv_bounded_linear
apply (rule as(1,2)[THEN conjunct1])+
proof (rule, rule ccontr)
fix i :: 'a
assume i: "i ∈ Basis"
def e ≡ "norm (f' i - f'' i)"
assume "f' i ≠ f'' i"
then have "e > 0"
unfolding e_def by auto
obtain d where d:
"0 < d"
"(⋀xa. xa∈s ⟶ 0 < dist xa x ∧ dist xa x < d ⟶
dist ((f xa - f x - f' (xa - x)) /⇩R norm (xa - x) -
(f xa - f x - f'' (xa - x)) /⇩R norm (xa - 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
lemma frechet_derivative_unique_at:
"(f has_derivative f') (at x) ⟹ (f has_derivative f'') (at x) ⟹ f' = f''"
by (rule has_derivative_unique)
lemma frechet_derivative_unique_within_closed_interval:
fixes f::"'a::euclidean_space ⇒ 'b::real_normed_vector"
assumes "∀i∈Basis. a∙i < b∙i"
and "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''"
apply(rule frechet_derivative_unique_within)
apply(rule assms(3,4))+
proof (rule, rule, rule)
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
then show ?thesis
apply (rule_tac x="(min (b∙i - a∙i) e) / 2" in exI)
using assms(1)[THEN bspec[where x=i]] and ‹e>0› and assms(2)
unfolding mem_box
using i
apply (auto simp add: field_simps inner_simps inner_Basis)
done
next
note * = assms(2)[unfolded mem_box, THEN bspec, OF i]
case False
moreover have "a ∙ i < x ∙ i"
using False * by auto
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 * 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"
using * and ‹e>0› by auto
then have "x ∙ i * 2 ≤ b ∙ i * 2 + min (x ∙ i - a ∙ i) e"
using * by auto
ultimately show ?thesis
apply (rule_tac x="- (min (x∙i - a∙i) e) / 2" in exI)
using assms(1)[THEN bspec, OF i] and ‹e>0› and assms(2)
unfolding mem_box
using i
apply (auto simp add: field_simps inner_simps inner_Basis)
done
qed
qed
lemma frechet_derivative_unique_within_open_interval:
fixes f::"'a::euclidean_space ⇒ 'b::real_normed_vector"
assumes "x ∈ box a b"
and "(f has_derivative f' ) (at x within box a b)"
and "(f has_derivative f'') (at x within box a b)"
shows "f' = f''"
proof -
from assms(1) have *: "at x within box a b = at x"
by (metis at_within_interior interior_open open_box)
from assms(2,3) [unfolded *] show "f' = f''"
by (rule frechet_derivative_unique_at)
qed
lemma frechet_derivative_at:
"(f has_derivative f') (at x) ⟹ f' = frechet_derivative f (at x)"
apply (rule frechet_derivative_unique_at[of f])
apply assumption
unfolding frechet_derivative_works[symmetric]
using differentiable_def
apply auto
done
lemma frechet_derivative_within_cbox:
fixes f :: "'a::euclidean_space ⇒ 'b::real_normed_vector"
assumes "∀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")
assume "h ≠ 0"
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 add: f'.zero)
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:
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
lemma rolle:
fixes f :: "real ⇒ real"
assumes "a < b"
and "f a = f b"
and "continuous_on {a .. b} f"
and "∀x∈{a <..< 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 * assms(3)] 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 * assms(3)] 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
def e ≡ "(a + b) /2"
case False
then have "f d = f c"
using d c assms(2) by auto
then have "⋀x. x ∈ {a..b} ⟹ f x = f d"
using c d
by force
then show ?thesis
apply (rule_tac x=e in bexI)
unfolding e_def
using assms(1)
apply auto
done
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 "continuous_on {a..b} f"
assumes "∀x∈{a<..<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 assms(1), of "λx. f x - (f b - f a) / (b - a) * x"] ballI)
fix x
assume x: "x ∈ {a <..< 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 assms(3)[rule_format,OF x])
qed (insert assms(1,2), 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_divide_cancel_right not_real_square_gt_zero
times_divide_eq_left)
qed
lemma mvt_simple:
fixes f :: "real ⇒ real"
assumes "a < b"
and "∀x∈{a..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 assms(2) unfolding differentiable_on_def differentiable_def by fast
then show "continuous_on {a..b} f"
by (rule differentiable_imp_continuous_on)
show "∀x∈{a<..<b}. (f has_derivative f' x) (at x)"
proof
fix x
assume x: "x ∈ {a <..< b}"
show "(f has_derivative f' x) (at x)"
unfolding at_within_open[OF x open_greaterThanLessThan,symmetric]
apply (rule has_derivative_within_subset)
apply (rule assms(2)[rule_format])
using x
apply auto
done
qed
qed (rule assms(1))
lemma mvt_very_simple:
fixes f :: "real ⇒ real"
assumes "a ≤ b"
and "∀x∈{a .. 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
apply (rule_tac x=a in bexI)
using assms(2)[THEN bspec[where x=a]]
unfolding has_derivative_def
unfolding True
using zero
apply auto
done
next
case False
then show ?thesis
using mvt_simple[OF _ assms(2)]
using assms(1)
by auto
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 "continuous_on {a .. b} f"
and "∀x∈{a<..<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)
apply (rule assms(1))
apply (intro continuous_intros assms(2))
using assms(3)
apply (fast 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 assms(1)
apply (rule_tac x="(a + b) /2" in bexI)
apply auto
done
qed
qed
subsection ‹More general bound theorems›
lemma 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"
def 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"
def 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)
def 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" .
{
assume "a ≠ y" with ‹a ≤ y› have "a < y" by simp
have "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
from elim have "φ' y * ¦x1 - y¦ ≤ φ x1 - φ y + e2 * ¦x1 - y¦"
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›])
def 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'}"
{
assume "x1 < y"
hence "?le x1"
using ‹x1 ∈ {a..<d'}› y_all_le by auto
} moreover {
assume "x1 ≥ y"
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 have "?le x1"
using ‹x1 ≥ y› by (auto simp: algebra_simps)
} ultimately show "?le x1" by arith
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
} moreover {
assume "a = y"
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›])
def 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
hence "y = b" using ‹d > 0› ‹y < b›
by (simp add: d'_def)
} ultimately have "y = b"
by auto
with le_y have "norm (f b - f a) ≤ φ b - φ a + e * (b - a + 1)"
by (simp add: algebra_simps)
} note * = this
{
fix e::real assume "e > 0"
hence "norm (f b - f a) ≤ φ b - φ a + e"
using *[of "e / (b - a + 1)"] ‹a < b› by simp
} thus ?thesis
by (rule field_le_epsilon)
qed
lemma differentiable_bound:
fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes "convex s"
and "∀x∈s. (f has_derivative f' x) (at x within s)"
and "∀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 *: "⋀u. u∈{0..1} ⟹ x + u *⇩R (y - x) ∈ s"
using assms(1)[unfolded convex_alt,rule_format,OF x y]
unfolding scaleR_left_diff_distrib scaleR_right_diff_distrib
by (auto simp add: algebra_simps)
have 0: "continuous_on (?p ` {0..1}) f"
using *
unfolding continuous_on_eq_continuous_within
apply -
apply rule
apply (rule differentiable_imp_continuous_within)
unfolding differentiable_def
apply (rule_tac x="f' xa" in exI)
apply (rule has_derivative_within_subset)
apply (rule assms(2)[rule_format])
apply auto
done
from * have 1: "continuous_on {0 .. 1} (f ∘ ?p)"
by (intro continuous_intros 0)+
{
fix u::real assume u: "u ∈{0 <..< 1}"
let ?u = "?p u"
interpret linear "(f' ?u)"
using u by (auto intro!: has_derivative_linear assms(2)[rule_format] *)
have "(f ∘ ?p has_derivative (f' ?u) ∘ (λu. 0 + u *⇩R (y - x))) (at u within box 0 1)"
apply (rule diff_chain_within)
apply (rule derivative_intros)+
apply (rule has_derivative_within_subset)
apply (rule assms(2)[rule_format])
using u *
apply auto
done
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 "continuous_on {0..1} ?φ"
by (rule continuous_intros)+
} note 3 = this
{
fix u::real assume u: "u ∈{0 <..< 1}"
have "(?φ has_vector_derivative B * norm (x - y)) (at u)"
by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
} note 4 = this
{
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 assms(2)[rule_format] *)
have "norm (f' ?u (y - x)) ≤ onorm (f' ?u) * norm (y - x)"
by (rule onorm) fact
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∈{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 = op + 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 (auto simp: ac_simps)
qed
lemma differentiable_bound_linearization:
fixes f::"'a::real_normed_vector ⇒ 'b::real_normed_vector"
assumes "⋀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∈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 -
def g ≡ "λx. f x - f' x0 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 B: "∀x∈{0..1}. onorm (λi. f' (a + x *⇩R (b - a)) i - f' x0 i) ≤ B"
using assms by (auto simp: fun_diff_def)
from differentiable_bound_segment[OF assms(1) g B] ‹x0 ∈ S›
show ?thesis
by (simp add: g_def field_simps linear_sub[OF has_derivative_linear[OF f']])
qed
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: "op * 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_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 "(f has_derivative f') (at (g y))"
and "bounded_linear g'"
and "g' ∘ f' = id"
and "continuous (at y) g"
and "open t"
and "y ∈ t"
and "∀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 (rule, rule)
fix e :: real
assume "e > 0"
with C(1) have *: "e / C > 0" by auto
obtain d0 where d0:
"0 < d0"
"∀ya. norm (ya - g y) < d0 ⟶ norm (f ya - f (g y) - f' (ya - g y)) ≤ e / C * norm (ya - g y)"
using assms(1)
unfolding has_derivative_at_alt
using * by blast
obtain d1 where d1:
"0 < d1"
"∀x. 0 < dist x y ∧ dist x y < d1 ⟶ dist (g x) (g y) < d0"
using assms(4)
unfolding continuous_at Lim_at
using d0(1) by blast
obtain d2 where d2:
"0 < d2"
"∀ya. dist ya y < d2 ⟶ ya ∈ t"
using assms(5)
unfolding open_dist
using assms(6) by blast
obtain d where d: "0 < d" "d < d1" "d < d2"
using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
then show "∃d>0. ∀z. norm (z - y) < d ⟶ norm (g z - g y - g' (z - y)) ≤ e * norm (g z - g y)"
apply (rule_tac x=d in exI)
apply rule
defer
apply rule
apply rule
proof -
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]
unfolding assms(7)[rule_format,OF ‹z∈t›]
apply (subst norm_minus_cancel[symmetric])
apply auto
done
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"
apply (rule mult_right_mono)
apply (rule d0(2)[rule_format,unfolded assms(7)[rule_format,OF ‹y∈t›]])
apply (cases "z = y")
defer
apply (rule d1(2)[unfolded dist_norm,rule_format])
using as d C d0
apply auto
done
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 auto
qed
have *: "(0::real) < 1 / 2"
by auto
obtain d where d:
"0 < 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
def 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)"
apply (rule add_left_mono)
using d and z
apply auto
done
also have "… ≤ norm (z - y) * C + 1 / 2 * norm (g z - g y)"
apply (rule add_right_mono)
using C
apply auto
done
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
apply rule
apply (rule assms)
apply rule
apply rule
proof -
fix e :: real
assume "e > 0"
then have *: "e / B > 0" by (metis ‹B > 0› divide_pos_pos)
obtain d' where d':
"0 < 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 real_lbound_gt_zero[OF d(1) d'(1)] by blast
show "∃d>0. ∀ya. norm (ya - y) < d ⟶ norm (g ya - g y - g' (ya - y)) ≤ e * norm (ya - y)"
apply (rule_tac x=k in exI)
apply auto
proof -
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]
using k as using ‹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(insert k, 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∈t. f (g y) = y"
shows "(g has_derivative g') (at (f x))"
apply (rule has_derivative_inverse_basic)
using assms
apply auto
done
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∈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 "f x ∈ interior (f ` s)"
and "continuous_on s f"
and "∀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 -
{
fix y
assume "y ∈ interior (f ` s)"
then obtain x where "x ∈ s" and *: "y = f x"
unfolding image_iff
using interior_subset
by auto
have "f (g y) = y"
unfolding * and assms(5)[rule_format,OF ‹x∈s›] ..
} note * = this
show ?thesis
apply (rule has_derivative_inverse_basic_x[OF assms(6-8)])
apply (rule continuous_on_interior[OF _ assms(3)])
apply (rule continuous_on_inv[OF assms(4,1)])
apply (rule assms(2,5) assms(5)[rule_format] open_interior assms(3))+
apply (metis *)
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∈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 (rule continuous_intros assms)+
using assms(4-6)
apply auto
done
qed
lemma brouwer_surjective_cball:
fixes f :: "'n::euclidean_space ⇒ 'n"
assumes "e > 0"
and "continuous_on (cball a e) f"
and "∀x∈s. ∀y∈cball a e. x + (y - f y) ∈ cball a e"
and "x ∈ s"
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 "continuous_on s f"
and "x ∈ s"
and "(f has_derivative f') (at x)"
and "bounded_linear g'" "f' ∘ g' = id"
and "t ⊆ s"
and "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 assms(4)
unfolding has_derivative_at_alt
using * by blast
obtain e1 where e1: "0 < e1" "cball x e1 ⊆ t"
using assms(8)
unfolding mem_interior_cball
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 real_lbound_gt_zero[OF *] by blast
have "∀z∈cball (f x) (e / 2). ∃y∈cball (f x) e. f (x + g' (y - f x)) = z"
apply rule
apply (rule brouwer_surjective_cball[where s="cball (f x) (e/2)"])
prefer 3
apply rule
apply rule
proof-
show "continuous_on (cball (f x) e) (λy. f (x + g' (y - f x)))"
unfolding g'.diff
apply (rule continuous_on_compose[of _ _ f, unfolded o_def])
apply (rule continuous_intros linear_continuous_on[OF assms(5)])+
apply (rule continuous_on_subset[OF assms(2)])
apply rule
apply (unfold image_iff)
apply (erule bexE)
proof-
fix y z
assume as: "y ∈cball (f x) e" "z = x + (g' y - g' (f x))"
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"
unfolding g'.diff[symmetric]
using B
by auto
also have "… ≤ e * B"
using as(1)[unfolded mem_cball dist_norm]
using B
by auto
also have "… ≤ e1"
using e
unfolding less_divide_eq
using B
by auto
finally have "z ∈ cball x e1"
unfolding mem_cball
by force
then show "z ∈ s"
using e1 assms(7) by auto
qed
next
fix y z
assume as: "y ∈ cball (f x) (e / 2)" "z ∈ cball (f x) e"
have "norm (g' (z - f x)) ≤ norm (z - f x) * B"
using B by auto
also have "… ≤ e * B"
apply (rule mult_right_mono)
using as(2)[unfolded mem_cball dist_norm] and B
unfolding norm_minus_commute
apply auto
done
also have "… < e0"
using e and B
unfolding less_divide_eq
by auto
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 *]
unfolding algebra_simps **
by auto
also have "… ≤ 1 / (B * 2) * norm (g' (z - f x)) + e/2"
using as(1)[unfolded mem_cball dist_norm]
by auto
also have "… ≤ 1 / (B * 2) * B * norm (z - f x) + e/2"
using * and 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"
apply (rule add_right_mono)
using as(2)[unfolded mem_cball dist_norm]
unfolding norm_minus_commute
apply auto
done
finally show "y + (z - f (x + g' (z - f x))) ∈ cball (f x) e"
unfolding mem_cball dist_norm
by auto
qed (insert e, auto) note lem = this
show ?thesis
unfolding mem_interior
apply (rule_tac x="e/2" in exI)
apply rule
apply (rule divide_pos_pos)
prefer 3
proof
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"
apply (rule mult_right_mono)
using z(1)
unfolding mem_cball dist_norm norm_minus_commute
using B
apply auto
done
also have "… ≤ e1"
using e B unfolding less_divide_eq by auto
finally have "x + g'(z - f x) ∈ t"
apply -
apply (rule e1(2)[unfolded subset_eq,rule_format])
unfolding mem_cball dist_norm
apply auto
done
then show "y ∈ f ` t"
using z by auto
qed (insert e, 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 right_inverse_linear:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes lf: "linear f"
and gf: "f ∘ g = id"
shows "linear g"
proof -
from gf have fi: "surj f"
by (auto simp add: surj_def o_def id_def) metis
from linear_surjective_isomorphism[OF lf fi]
obtain h:: "'a ⇒ 'a" where h: "linear h" "∀x. h (f x) = x" "∀x. f (h x) = x"
by blast
have "h = g"
apply (rule ext)
using gf h(2,3)
apply (simp add: o_def id_def fun_eq_iff)
apply metis
done
with h(1) show ?thesis by blast
qed
lemma has_derivative_inverse_strong:
fixes f :: "'n::euclidean_space ⇒ 'n"
assumes "open s"
and "x ∈ s"
and "continuous_on s f"
and "∀x∈s. g (f x) = x"
and "(f has_derivative f') (at x)"
and "f' ∘ g' = id"
shows "(g has_derivative g') (at (f x))"
proof -
have linf: "bounded_linear f'"
using assms(5) unfolding has_derivative_def by auto
then have ling: "bounded_linear g'"
unfolding linear_conv_bounded_linear[symmetric]
apply -
apply (rule right_inverse_linear)
using assms(6)
apply auto
done
moreover have "g' ∘ f' = id"
using assms(6) linf ling
unfolding linear_conv_bounded_linear[symmetric]
using linear_inverse_left
by auto
moreover have *:"∀t⊆s. x ∈ interior t ⟶ f x ∈ interior (f ` t)"
apply clarify
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"
apply (rule_tac x=d in exI)
apply rule
apply (rule d(1))
apply rule
apply rule
proof -
fix y
assume "0 < dist y (f x) ∧ dist y (f x) < d"
then have "g y ∈ g ` f ` (ball x e ∩ s)"
using d(2)[unfolded subset_eq,THEN bspec[where x=y]]
by (auto simp add: dist_commute)
then have "g y ∈ ball x e ∩ s"
using assms(4) by auto
then show "dist (g y) (g (f x)) < e"
using assms(4)[rule_format,OF ‹x ∈ s›]
by (auto simp add: dist_commute)
qed
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
proof -
from that have "y ∈ f ` s"
using interior_subset by auto
then obtain z where "z ∈ s" "y = f z" unfolding image_iff ..
then show ?thesis
using assms(4) by auto
qed
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∈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 "∀x∈s. (f has_derivative f'(x)) (at x)"
and "∀x∈s. g (f x) = x"
and "f' x ∘ g' x = id"
and "x ∈ s"
shows "(g has_derivative g'(x)) (at (f x))"
apply (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
apply (rule assms)+
unfolding continuous_on_eq_continuous_at[OF assms(1)]
apply rule
apply (rule differentiable_imp_continuous_within)
unfolding differentiable_def
using assms
apply auto
done
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 "bounded_linear g'"
and "g' ∘ f' a = id"
and "⋀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)"
defer
apply (subst euclidean_eq_iff)
using f'g'
apply auto
done
then have *: "0 < onorm g'"
unfolding onorm_pos_lt[OF assms(3)]
by fastforce
def 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" "ball a d2 ⊆ s"
using assms(2,1) ..
obtain d2 where d2: "0 < d2" "ball a d2 ⊆ s"
using assms(2)
unfolding open_contains_ball
using ‹a∈s› by blast
obtain d where d: "0 < d" "d < d1" "d < d2"
using real_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"
def ph ≡ "λw. w - g' (f w - f x)"
have ph':"ph = g' ∘ (λw. f' a w - (f w - f x))"
unfolding ph_def o_def
unfolding diff
using f'g'
by (auto simp: algebra_simps)
have "norm (ph x - ph y) ≤ (1 / 2) * norm (x - y)"
apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="λx v. v - g'(f' x v)"])
apply (rule_tac[!] ballI)
proof -
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
show "(ph has_derivative (λv. v - g' (f' u v))) (at u within ball a d)"
unfolding ph' *
apply (simp add: comp_def)
apply (rule bounded_linear.has_derivative[OF assms(3)])
apply (rule derivative_intros)
defer
apply (rule has_derivative_sub[where g'="λx.0",unfolded diff_0_right])
apply (rule has_derivative_at_within)
using assms(5) and ‹u ∈ s› ‹a ∈ s›
apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "λx. x"] has_derivative_bounded_linear)
done
have **: "bounded_linear (λx. f' u x - f' a x)" "bounded_linear (λx. f' a x - f' u x)"
apply (rule_tac[!] bounded_linear_sub)
apply (rule_tac[!] has_derivative_bounded_linear)
using assms(5) ‹u ∈ s› ‹a ∈ s›
apply auto
done
have "onorm (λv. v - g' (f' u v)) ≤ onorm g' * onorm (λw. f' a w - f' u w)"
unfolding *
apply (rule onorm_compose)
apply (rule assms(3) **)+
done
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"]
using d and u and onorm_pos_le[OF assms(3)]
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)"
apply (rule arg_cong[where f=norm])
unfolding ph_def
using diff
unfolding as
apply auto
done
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 "∀n. ∀x∈s. ((f n) has_derivative (f' n x)) (at x within s)"
and "∀n≥N. ∀x∈s. ∀h. 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 rule+
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)"
apply (rule differentiable_bound[where f'="λx h. f' m x h - f' n x h", OF assms(1) _ _ as(3-4)])
apply (rule_tac[!] ballI)
proof -
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 assms(2)[rule_format] ‹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"]
unfolding norm_minus_commute
by (auto simp add: algebra_simps)
also have "… ≤ e * norm h + e * norm h"
using assms(3)[rule_format,OF ‹N ≤ m› ‹x ∈ s›, of h]
using assms(3)[rule_format,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∈s. ((f n) has_derivative (f' n x)) (at x within s)"
and "∀e>0. ∃N. ∀n≥N. ∀x∈s. ∀h. norm (f' n x h - g' x h) ≤ e * norm h"
shows "∀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)"
proof (rule, rule)
fix e :: real
assume "e > 0"
then have *: "2 * (1/2* e) = e" "1/2 * e >0"
by auto
obtain N where "∀n≥N. ∀x∈s. ∀h. norm (f' n x h - g' x h) ≤ 1 / 2 * e * norm h"
using assms(3) *(2) by blast
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="1/2 *e", 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 "∀n. ∀x∈s. ((f n) has_derivative (f' n x)) (at x within s)"
and "∀e>0. ∃N. ∀n≥N. ∀x∈s. ∀h. norm (f' n x h - g' x h) ≤ e * norm h"
and "x0 ∈ s"
and "((λn. f n x0) ⤏ l) sequentially"
shows "∃g. ∀x∈s. ((λn. f n x) ⤏ g x) sequentially ∧ (g has_derivative g'(x)) (at x within s)"
proof -
have lem1: "∀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"
apply (rule bchoice)
unfolding convergent_eq_cauchy
proof
fix x
assume "x ∈ s"
show "Cauchy (λn. f n x)"
proof (cases "x = x0")
case True
then show ?thesis
using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
next
case False
show ?thesis
unfolding Cauchy_def
proof (rule, rule)
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 assms(5)]
unfolding Cauchy_def
using *(1) by blast
obtain N where N:
"∀m≥N. ∀n≥N.
∀xa∈s. ∀y∈s. norm (f m xa - f n xa - (f m y - f n y)) ≤
e / 2 / norm (x - x0) * norm (xa - y)"
using lem1 *(2) by blast
show "∃M. ∀m≥M. ∀n≥M. dist (f m x) (f n x) < e"
apply (rule_tac x="max M N" in exI)
proof rule+
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[rule_format,OF _ _ ‹x∈s› ‹x0∈s›, of m n] and as and False
by auto
also have "… < e / 2 + e / 2"
apply (rule add_strict_right_mono)
using as and M[rule_format]
unfolding dist_norm
apply auto
done
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: "∀e>0. ∃N. ∀n≥N. ∀x∈s. ∀y∈s. norm ((f n x - f n y) - (g x - g y)) ≤ e * norm (x - y)"
proof (rule, rule)
fix e :: real
assume *: "e > 0"
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 * 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)"
apply (rule_tac x=N in exI)
proof rule+
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
apply (rule_tac x=N in exI)
apply rule
apply rule
proof -
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[rule_format, of n m x y] and 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 (rule tendsto_ge_const[OF trivial_limit_sequentially])
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)
fix x
assume "x ∈ s"
then show "((λn. f n x) ⤏ g x) sequentially"
by (simp add: g)
have lem3: "∀u. ((λn. f' n x u) ⤏ g' x u) sequentially"
unfolding filterlim_def le_nhds_metric_le eventually_filtermap dist_norm
proof (intro allI impI)
fix u
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 assms(3)[folded eventually_sequentially] and ‹0 < e› and ‹x ∈ s›
by (fast elim: eventually_mono)
then show ?thesis
using ‹u = 0› and ‹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 assms(3)[folded eventually_sequentially] and ‹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])
apply (rule lem3[rule_format])
unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
apply (intro tendsto_intros)
apply (rule lem3[rule_format])
done
show "g' x (y + z) = g' x y + g' x z"
apply (rule tendsto_unique[OF trivial_limit_sequentially])
apply (rule lem3[rule_format])
unfolding lin[THEN bounded_linear.linear, THEN linear_add]
apply (rule tendsto_add)
apply (rule lem3[rule_format])+
done
obtain N where N: "∀h. norm (f' N x h - g' x h) ≤ 1 * norm h"
using assms(3) ‹x ∈ s› by (fast intro: zero_less_one)
have "bounded_linear (f' N x)"
using assms(2) ‹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 "∀e>0. eventually (λy. norm (g y - g x - g' x (y - x)) ≤ e * norm (y - x)) (at x within s)"
proof (rule, rule)
fix e :: real
assume "e > 0"
then have *: "e / 3 > 0"
by auto
obtain N1 where N1: "∀n≥N1. ∀x∈s. ∀h. norm (f' n x h - g' x h) ≤ e / 3 * norm h"
using assms(3) * by blast
obtain N2 where
N2: "∀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 assms(2)[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[rule_format, 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 "∀n. ∀x∈s. ((f n) has_derivative (f' n x)) (at x within s)"
and "∀e>0. ∃N. ∀n≥N. ∀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 assms(1) _ assms(3), of "λn x. f n x + (f 0 a - f n a)"])
apply (metis assms(2) has_derivative_add_const)
apply (rule ‹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>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 *[THEN choice] ..
obtain f' where
f: "∀x. ∀xa∈s. (f x has_derivative f' x xa) (at xa within s) ∧
(∀h. norm (f' x xa h - g' xa h) ≤ inverse (real (Suc x)) * norm h)"
using *[THEN choice] ..
show ?thesis
apply (rule has_antiderivative_sequence[OF assms(1), of f f'])
defer
apply rule
apply rule
proof -
fix e :: real
assume "e > 0"
obtain N where N: "inverse (real (Suc N)) < e"
using reals_Archimedean[OF ‹e>0›] ..
show "∃N. ∀n≥N. ∀x∈s. ∀h. norm (f' n x h - g' x h) ≤ e * norm h"
apply (rule_tac x=N in exI)
apply rule
apply rule
apply rule
apply rule
proof -
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"
using f[rule_format,THEN conjunct2, OF x, of n, THEN spec[where x=h]]
apply (rule order_trans)
using N *
apply (cases "h = 0")
apply auto
done
qed
qed (insert f, 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>0. ∃N. ∀n≥N. ∀x∈s. ∀h. norm (setsum (λ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_setsum)
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 "∀e>0. ∃N. ∀n≥N. ∀x∈s. ∀h. norm ((∑i<n. f' i x * h) - g' x * h) ≤ e * norm h"
proof (intro allI impI)
fix e :: real assume "e > 0"
with 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 setsum_left_distrib)
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 (insert assms, 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
def g' ≡ "λx. ∑i. f' i 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 op * (g' x)) (at x)"
by (simp add: has_field_derivative_def s)
have "((λx. ∑n. f n x) has_derivative op * (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)
show "∀i∈Basis. ∀e>0. ∃d. 0 < ¦d¦ ∧ ¦d¦ < e ∧ x + d *⇩R i ∈ s"
proof clarsimp
fix e :: real assume "0 < e"
with islimpt_approachable_real[of x s] not_bot
obtain x' where "x' ∈ s" "x' ≠ x" "¦x' - x¦ < e"
by (auto simp add: trivial_limit_within)
then show "∃d. d ≠ 0 ∧ ¦d¦ < e ∧ x + d ∈ s"
by (intro exI[of _ "x' - x"]) auto
qed
qed (insert f' f'', 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)
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 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_closed_interval:
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 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_within)
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 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(2)
unfolding has_vector_derivative_def
apply -
apply (drule diff_chain_at[OF assms(1)[unfolded has_vector_derivative_def]])
apply (simp only: o_def real_scaleR_def scaleR_scaleR)
done
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(2)
unfolding has_vector_derivative_def
apply -
apply (drule diff_chain_within[OF assms(1)[unfolded has_vector_derivative_def]])
apply (simp only: o_def real_scaleR_def scaleR_scaleR)
done
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_closed_interval 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:
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_at_general:
assumes "f differentiable at x" "(∃g'. (g has_field_derivative g') (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
by (auto simp: vector_derivative_works DERIV_deriv_iff_has_field_derivative)
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 cond_application_beta setsum.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›
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_inter_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 DERIV_within_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 (rule tendsto_ge_const)
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_inter_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 DERIV_within_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 (rule tendsto_le_const)
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'"
assumes "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:
assumes fx: "⋀x y. x ∈ X ⟹ y ∈ Y ⟹ ((λx. f x y) has_derivative blinfun_apply (fx x y)) (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 fx_cont: "continuous_on (X × Y) (λ(x, y). fx x y)"
assumes fy_cont: "continuous_on (X × Y) (λ(x, y). fy x y)"
assumes "x ∈ X" "y ∈ Y"
assumes "convex X" "convex Y"
shows "((λ(x, y). f x y) has_derivative (λ(tx, ty). fx x y tx + fy x y ty)) (at (x, y) within X × Y)"
proof (safe intro!: has_derivativeI tendstoI, goal_cases)
case (2 e')
def e≡"e' / 9"
have "e > 0" using ‹e' > 0› by (simp add: e_def)
have "(x, y) ∈ X × Y" using assms by auto
from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF this,
unfolded continuous_within, 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
def 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 ‹x ∈ X› ‹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 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∈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 y) (x' - x)) ≤ norm (x' - x) * e"
from fx[OF ‹x ∈ X› ‹y ∈ Y›, 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[unfolded continuous_on_eq_continuous_within, rule_format, OF SigmaI[OF ‹x ∈ X› ‹y ∈ Y›],
unfolded continuous_within, 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 y (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 y (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 y (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 - blinfun_apply (fx x y) (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 y (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)
qed (auto intro!: bounded_linear_intros simp: split_beta')
end